Időbeli logika

Temporal logic ( temporal logic ; angol temporal logic ) - logika , melynek kijelentéseiben az időbeli szempontot veszik figyelembe. Az események sorozatának és azok kapcsolatának leírására szolgál egy időskála mentén.

Az ókorban a logika időbeli használatát tanulmányozták a megariai iskola filozófusai , különösen Diodorus Cronus és a sztoikusok . A modern szimbolikus időbeli logikát, amelyet először az 1950-es években Arthur Pryor [1] fogalmazott meg a modális logika alapján , a Turing-díjas Amir Pnueli munkásságának köszönhetően a számítástechnikában használták és fejlesztették ki a legszélesebb körben .

Példa

Az „éhes vagyok” állítás jelentése az idő múlásával nem változik, de az igazsága változhat: egy adott pillanatban lehet igaz vagy hamis, de nem mindkettő. Ellentétben a nem időbeli logikákkal, ahol az állítások értéke nem változik az idő múlásával, az időbeli logikában az érték attól függ, hogy mikor tesztelik. Az időbeli logika lehetővé teszi olyan kijelentések kifejezését, mint „ mindig éhes vagyok”, „ néha éhes vagyok” vagy „éhes vagyok, amíg meg nem eszem”.

Időbeli operátorok

Az időbeli logikában kétféle operátor létezik : logikai és modális. ( ) általában logikai operátorként használatosak . A lineáris időlogikában és a számítási fa logikában használt modális operátorok az alábbiak szerint vannak definiálva. $\neg ,\lor ,\land ,\rightarrow$

Szöveges megjelölés	Szimbólum megjelölés	Meghatározás	Leírás
Bináris operátorok
$\phi$ U $\psi$	$\phi ~\mathcal{U}~ \psi$	$\begin{mátrix}(B\,\mathcal{U}\,C)(\phi)= \\ (\exists i:C(\phi_i)\land(\forall j<i:B(\phi_j)) )\end{mátrix}$	U ntil (erős): a jövőben valamilyen állapotban (esetleg a jelenlegiben) végre kell hajtani, a tulajdonságot a kijelölt állapotig (ide nem értve) minden állapotban végre kell hajtani. $\psi$ $\phi$
$\phi$ R $\psi$ $\phi$ V $\psi$	$\phi ~\mathcal{R}~ \psi$ $\phi ~\mathcal{V}~ \psi$	$\begin{mátrix}(B\,\mathcal{R}\,C)(\phi)= \\ (\forall i:C(\phi_i)\lor(\exists j<i:B(\phi_j)) )\end{mátrix}$	R kiadás: Kiadja , ha igaz , egészen az első alkalommal, amikor igaz (vagy mindig, ha nem). Ellenkező esetben legalább egyszer igazzá kell válnia, mielőtt az első alkalommal igazzá válik. $\phi$ $\psi$ $\psi$ $\phi$ $\phi$ $\psi$
Unáris operátorok
N $\phi$ x $\phi$	$\circ \phi$	$\mathcal{N}B(\phi_i)=B(\phi_{i+1})$	N e X t: igaznak kell lennie az adott állapotot közvetlenül követő állapotban. $\phi$
F $\phi$	$\Gyémánt \phi$	$\mathcal{F}B(\phi)=(igaz\,\mathcal{U}\,B)(\phi)$	Jövő : a jövőben legalább egy állapotban igazzá kell válnia. $\phi$
G $\phi$	$\Box \phi$	$\mathcal{G}B(\phi)=\neg\mathcal{F}\neg B(\phi)$	G lobálisan: minden jövőbeli állapotban igaznak kell lennie. $\phi$
A $\phi$	$\mathcal{A} \phi$	$\begin{matrix}(\mathcal{A}B)(\psi)= \\ (\forall \phi:\phi_0=\psi\to B(\phi))\end{mátrix}$	A ll: Minden ágon futnia kell, ezzel kezdve. $\phi$
E $\phi$	$\mathcal{E}\phi$	$\begin{matrix}(\mathcal{E}B)(\psi)= \\ (\exists \phi:\phi_0=\psi\land B(\phi))\end{mátrix}$	Létezik : Legalább egy ág fut. $\phi$

Egyéb modális operátorok

W állítás jelentése W eak till : ekvivalens $f Wg$ $fUg\lor Gf$

Kettős identitások

De Morgan szabályaihoz hasonlóan vannak dualitási tulajdonságok az időbeli operátorok számára:

$\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$

Alkalmazások

Az időbeli logikákat gyakran használják a formális ellenőrzési követelmények kifejezésére . Például az olyan tulajdonságokat, mint „ha egy kérés érkezik, akkor biztosan érkezik rá válasz” vagy „a függvényt számításonként legfeljebb egyszer hívják meg”, kényelmes az időbeli logikákkal megfogalmazni. Különféle automatákat használnak az ilyen tulajdonságok tesztelésére, például Büchi automatákat az LTL lineáris időlogikában kifejezett tulajdonságok tesztelésére .

Opciók

Az időbeli logika fő univerzális változata a modális μ-kalkulus ( Scott - de Bakker , 1969); részhalmazként tartalmazza a Henessy-Milner logikát és a CTL* -t , és a számítástechnikában használt fő változatok - lineáris időlogika ( LTL ) és számítási fa logika ( CTL ) - a CTL * töredékei .

Ezen kívül vannak az időlogikának más változatai is, amelyek nem redukálhatók modális μ-kalkulusra, például intervallum-időlogika és metrikus időlogika

Egyes gyakorlati lehetőségek az időbeli logikát más logikákkal kombinálják, különösen ilyen az időbeli cselekvési logika (a TLA⁺ specifikációs nyelvhez készült ), amely összeköti az időbeli logikát és a cselekvési logikát .

Jegyzetek

↑ Ricardo Caferra. Logika a számítástechnikához és a mesterséges intelligenciához. - John Wiley & Sons, 2013. - 537 p. — ISBN 978-1-118-60426-7 .

Irodalom

Clark E. M., Gramberg O., Peled D. Programmodellek ellenőrzése. Modellellenőrzés. Moszkva: MTsNMO. 2002. ISBN 5-94057-054-2

Szótárak és enciklopédiák	Nagy orosz Britannica (online)

Logikák

Filozófia • Szemantika • Szintaxis • Történelem

Logikai csoportok

klasszikus logika	Arisztotelészi logika propozíciós logika Elsőrendű logika Másodrendű logika magasabb rendű logika
matematikai logika	halmazelmélet Modellelmélet Kiszámíthatóság elmélet Bizonyításelmélet és konstruktív matematika Lineáris logika formális rendszer természetes következtetés Sorozatszámítás Logikai algebra Releváns logika Deontikus logika intuicionista logika Lambek kalkulus
Nem klasszikus logika	intuicionizmus zavaros logika Szubstrukturális logika logika Leírás logika Többértékű logika Logikai szintézis Kötési logika Időbeli logika Modális logika ( Hibrid logika ) episztemikus logika
Filozófiai logika	Kritikus gondolkodás informális logika deduktív érvelés

Alkatrészek

Logikai szimbólumok listája