Temporal logik

Temporal logic ( temporal logic ; engelsk temporal logic ) - logik , i vars uttalanden den tidsmässiga aspekten beaktas. Används för att beskriva händelseförlopp och deras förhållande längs en tidsskala.

I forntida tider studerades användningen av logik i den tidsmässiga aspekten av filosoferna från den megariska skolan , i synnerhet Diodorus Cronus och stoikerna . Modern symbolisk tidslogik, som först konceptualiserades och formulerades på 1950-talet av Arthur Pryor [1] på basis av modal logik , användes mest och utvecklades inom datavetenskap tack vare arbetet av Turingpristagaren Amir Pnueli .

Exempel

Innebörden av uttalandet: "Jag är hungrig" förändras inte med tiden, men dess sanning kan förändras: vid ett visst ögonblick kan det vara sant eller falskt, men inte både och. I motsats till icke-temporala logiker, där värdet av påståenden inte förändras över tiden, i temporal logik, beror värdet på när det testas. Temporal logik låter dig uttrycka uttalanden som "Jag är alltid hungrig", "Jag är ibland hungrig" eller "Jag är hungrig tills jag äter."

Temporal Operators

Det finns två typer av operatorer i temporal logik : logisk och modal. ( ) används ofta som logiska operatorer . Modaloperatorerna som används i linjär tidslogik och beräkningsträdlogik definieras enligt följande. $\neg ,\lor ,\land ,\rightarrow$

Textbeteckning	Symbolbeteckning	Definition	Beskrivning
Binära operatorer
$\phi$ U $\psi$	$\phi ~\mathcal{U}~ \psi$	$\begin{matrix}(B\,\mathcal{U}\,C)(\phi)= \\ (\exists i:C(\phi_i)\land(\forall j<i:B(\phi_j)) )\end{matris}$	Till (stark): måste exekveras i någon stat i framtiden (möjligen den nuvarande), egenskapen måste exekveras i alla stater upp till (inte inklusive) den utsedda. $\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(\exists j<i:B(\phi_j)) )\end{matris}$	R release: Släpps om sant tills första gången det är sant (eller alltid om det inte gör det). Annars måste det bli sant minst en gång innan det blir sant första gången. $\phi$ $\psi$ $\psi$ $\phi$ $\phi$ $\psi$
Unära operatörer
N $\phi$ X $\phi$	$\cirkel \phi$	$\mathcal{N}B(\phi_i)=B(\phi_{i+1})$	N e X t: måste vara sant i tillståndet omedelbart efter det givna. $\phi$
F $\phi$	$\Diamant \phi$	$\mathcal{F}B(\phi)=(true\,\mathcal{U}\,B)(\phi)$	F uture: måste bli sann i minst ett tillstånd i framtiden. $\phi$
G $\phi$	$\Box \phi$	$\mathcal{G}B(\phi)=\neg\mathcal{F}\neg B(\phi)$	Globalt : måste vara sant i alla framtida stater. $\phi$
A $\phi$	$\mathcal{A} \phi$	$\begin{matrix}(\mathcal{A}B)(\psi)= \\ (\forall \phi:\phi_0=\psi\to B(\phi))\end{matrix}$	A ll: Måste köras på alla grenar som börjar med den här. $\phi$
E $\phi$	$\mathcal{E}\phi$	$\begin{matrix}(\mathcal{E}B)(\psi)= \\ (\exists \phi:\phi_0=\psi\land B(\phi))\end{matrix}$	Finns : Det finns minst en gren som är igång. $\phi$

Andra modala operatorer

W - sats som betyder W eak tills : motsvarar $f Wg$ $fUg\lor Gf$

Dualitetsidentiteter

Liksom de Morgans regler finns det dualitetsegenskaper för temporära operatörer:

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

Applikationer

Temporal logik används ofta för att uttrycka formella verifieringskrav . Till exempel, egenskaper som "om en förfrågan tas emot kommer ett svar definitivt att komma till den" eller "funktionen anropas inte mer än en gång per beräkning" är bekvämt att formulera med hjälp av tidslogik. Olika automater används för att testa sådana egenskaper, till exempel Büchis automater för att testa egenskaper uttryckta i LTL linjär tidslogik .

Alternativ

Den huvudsakliga universella varianten av temporal logik är den modala μ-kalkylen ( Scott - de Bakker , 1969); den inkluderar Henessy-Milner logik och CTL* som en delmängd , och de huvudsakliga varianterna som används inom datavetenskap - linjär tidslogik ( LTL ) och beräkningsträdlogik ( CTL ) - är fragment av CTL * .

Dessutom finns det andra varianter av temporal logik som inte kan reduceras till modal μ-kalkyl, till exempel intervall temporal logik och metrisk temporal logik

Vissa praktiska alternativ använder kombinationer av temporal logik med andra logiker, i synnerhet, sådan är den temporala handlingslogiken (skapad för TLA⁺- specifikationsspråket ), som kopplar samman temporal logik och handlingslogik .

Anteckningar

↑ Ricardo Caferra. Logik för datavetenskap och artificiell intelligens. - John Wiley & Sons, 2013. - 537 sid. — ISBN 978-1-118-60426-7 .

Litteratur

Clark E. M., Gramberg O., Peled D. Verifiering av programmodeller. Modellkontroll. Moskva: MTsNMO. 2002. ISBN 5-94057-054-2

Ordböcker och uppslagsverk	Stor ryss Britannica (online)

Logik

Filosofi • Semantik • Syntax • Historia

Logiska grupper

klassisk logik	Aristotelisk logik propositionell logik Första beställningslogik Andra ordningens logik högre ordningslogik
matematisk logik	mängdteori Modellteori Beräkningsbarhetsteori Bevisteori och konstruktiv matematik Linjär logik formellt system naturlig slutsats Sekvenskalkyl Algebra av logik Relevant logik Deontisk logik intuitionistisk logik Lambek kalkyl
Icke-klassisk logik	intuitionism rolig logik Substrukturell logik logik Beskrivningslogik Flervärdig logik Logisk syntes Bindande logik Temporal logik Modal logik ( Hybrid logik ) epistemisk logik
Filosofisk logik	Kritiskt tänkande informell logik deduktiva resonemang

Komponenter

Bortförande (logik)
Sannolikhet
påstående
Avdrag / Induktion / Traduktion
Verklighet
induktivt resonemang
slutledning
boolesk konstant
Sann
logiskt följa
Logisk form
Nödvändiga och tillräckliga förutsättningar
Beskrivning
Definition
Utbyte
Paket
Kontrovers ( Antinomy )
Syntetisk bedömning / Analytisk bedömning
Länk

Lista över booleska symboler