Tidsmæssig logik

Temporal logic ( temporal logic ; engelsk temporal logic ) - logik , i hvis udsagn det tidsmæssige aspekt tages i betragtning. Bruges til at beskrive sekvenser af begivenheder og deres forhold langs en tidsskala.

I oldtiden blev brugen af logik i det tidsmæssige aspekt studeret af filosofferne fra den megariske skole , især Diodorus Cronus og stoikerne . Moderne symbolsk tidslogik, først konceptualiseret og formuleret i 1950'erne af Arthur Pryor [1] på grundlag af modal logik , blev mest brugt og udviklet i datalogi takket være arbejdet fra Turing-prisvinderen Amir Pnueli .

Eksempel

Betydningen af udsagnet: "Jeg er sulten" ændrer sig ikke med tiden, men dens sandhed kan ændre sig: på et bestemt tidspunkt kan den være sand eller falsk, men ikke begge dele. I modsætning til ikke-temporelle logikker, hvor værdien af påstande ikke ændrer sig over tid, afhænger værdien i tidslogik af, hvornår den testes. Temporal logik giver dig mulighed for at udtrykke udsagn som "Jeg er altid sulten", "Jeg er nogle gange sulten" eller "Jeg er sulten , indtil jeg spiser."

Temporal Operators

Der er to slags operatører i tidslogik : logisk og modal. ( ) bruges almindeligvis som logiske operatorer . De modale operatorer, der bruges i lineær tidslogik og beregningstrælogik, er defineret som følger. $\neg ,\lor ,\land ,\rightarrow$

Tekstbetegnelse	Symbolbetegnelse	Definition	Beskrivelse
Binære operatorer
$\phi$ U $\psi$	$\phi ~\mathcal{U}~ \psi$	$\begin{matrix}(B\,\mathcal{U}\,C)(\phi)= \\ (\eksisterer i:C(\phi_i)\land(\forall j<i:B(\phi_j)) )\end{matrix}$	Indtil (stærk): skal udføres i en eller anden stat i fremtiden (eventuelt den nuværende), skal ejendommen udføres i alle stater op til (ikke inklusive) den udpegede. $\psi$ $\phi$
$\phi$ R $\psi$ $\phi$ V $\psi$	$\phi ~\mathcal{R}~ \psi$ $\phi ~\mathcal{V}~ \psi$	$\begin{matrix}(B\,\mathcal{R}\,C)(\phi)= \\ (\forall i:C(\phi_i)\lor(\eksisterer j<i:B(\phi_j)) )\end{matrix}$	R -udgivelse: Frigiver , hvis det er sandt, indtil det er sandt første gang (eller altid, hvis det ikke gør det). Ellers skal det blive sandt mindst én gang, før det bliver sandt første gang. $\phi$ $\psi$ $\psi$ $\phi$ $\phi$ $\psi$
Unære operatører
N $\phi$ x $\phi$	$\cirkel \phi$	$\mathcal{N}B(\phi_i)=B(\phi_{i+1})$	N e X t: skal være sand i tilstanden umiddelbart efter den givne. $\phi$
F $\phi$	$\Diamant \phi$	$\mathcal{F}B(\phi)=(sand\,\mathcal{U}\,B)(\phi)$	F uture: skal blive sandt i mindst én tilstand i fremtiden. $\phi$
G $\phi$	$\Boks \phi$	$\mathcal{G}B(\phi)=\neg\mathcal{F}\neg B(\phi)$	Globalt : skal være sandt i alle fremtidige stater. $\phi$
EN $\phi$	$\mathcal{A} \phi$	$\begin{matrix}(\mathcal{A}B)(\psi)= \\ (\forall \phi:\phi_0=\psi\to B(\phi))\end{matrix}$	A ll: Skal køre på alle grene, der starter med denne. $\phi$
E $\phi$	$\mathcal{E}\phi$	$\begin{matrix}(\mathcal{E}B)(\psi)= \\ (\eksisterer \phi:\phi_0=\psi\land B(\phi))\end{matrix}$	Eksisterer : Der er mindst én gren, der kører. $\phi$

Andre modale operatører

W - sætning, der betyder W eak indtil : svarende til $f Wg$ $fUg\lor Gf$

Dualitetsidentiteter

Ligesom de Morgans regler er der dualitetsegenskaber for tidsmæssige operatører:

$\phi ~\mathcal{U}~ \psi = \neg(\neg \phi ~\mathcal{V}~ \neg \psi)$
$\neg \Diamond \phi = \Boks \neg \phi$
$\neg \mathcal{A} \phi = \mathcal{E} \neg \phi$

Ansøgninger

Temporelle logikker bruges ofte til at udtrykke formelle verifikationskrav . For eksempel er egenskaber som "hvis en anmodning modtages, så vil der helt sikkert komme et svar på den" eller "funktionen kaldes ikke mere end én gang pr. beregning" er praktisk at formulere ved hjælp af tidsmæssige logikker. Forskellige automater bruges til at teste sådanne egenskaber, for eksempel Büchis automater til at teste egenskaber udtrykt i LTL lineær tidslogik .

Indstillinger

Den vigtigste universelle variant af tidslogik er den modale μ-calculus ( Scott - de Bakker , 1969); den inkluderer Henessy-Milner logik og CTL* som en delmængde , og de vigtigste varianter, der bruges i datalogi - lineær tidslogik ( LTL ) og beregningstrælogik ( CTL ) - er fragmenter af CTL * .

Derudover er der andre varianter af tidslogik, der ikke kan reduceres til modal μ-regning, for eksempel interval temporal logik og metrisk tidsmæssig logik

Nogle praktiske muligheder bruger kombinationer af tidslogik med andre logikker, især den tidsmæssige handlingslogik (skabt til TLA⁺- specifikationssproget ), der forbinder tidslogik og handlingslogik .

Noter

↑ Ricardo Caferra. Logik for datalogi og kunstig intelligens. - John Wiley & Sons, 2013. - 537 s. — ISBN 978-1-118-60426-7 .

Litteratur

Clark E. M., Gramberg O., Peled D. Verifikation af programmodeller. Modelkontrol. Moskva: MTsNMO. 2002. ISBN 5-94057-054-2

Ordbøger og encyklopædier	Stor russer Britannica (online)

Logikker

Filosofi • Semantik • Syntaks • Historie

Logiske grupper

klassisk logik	Aristotelisk logik propositionel logik Første ordens logik Anden ordens logik højere ordens logik
matematisk logik	mængdeteori Modelteori Beregnelighedsteori Bevisteori og konstruktiv matematik Lineær logik formelt system naturlig konklusion Sekvensberegning Algebra af logik Relevant logik Deontisk logik intuitionistisk logik Lambek regning
Ikke-klassisk logik	intuitionisme sløret logik Substrukturel logik logik Beskrivelseslogik Flerværdilogik Logisk syntese Bindende logik Tidsmæssig logik Modal logik ( Hybrid logik ) epistemisk logik
Filosofisk logik	Kritisk tænkning uformel logik deduktiv ræsonnement

Komponenter

Bortførelse (logik)
Sandsynlighed
udmelding
Fradrag / Induktion / Traduktion
Virkelighed
Induktiv begrundelse
slutning
boolsk konstant
Rigtigt
logisk følge
Logisk form
Nødvendige og tilstrækkelige betingelser
Beskrivelse
Definition
Substitution
Pakke
Kontrovers ( Antinomy )
Syntetisk dømmekraft / Analytisk dømmekraft
Link

Liste over booleske symboler