Temporaalinen logiikka

Temporal logic ( temporal logic ; englanniksi temporal logic ) - logiikka , jonka lauseissa ajallinen aspekti otetaan huomioon. Käytetään kuvaamaan tapahtumasarjoja ja niiden suhdetta aika-asteikolla.

Muinaisina aikoina logiikan käyttöä ajallisesti tutkivat megarialaisen koulukunnan filosofit , erityisesti Diodorus Cronus , ja stoalaiset . Moderni symbolinen temporaalinen logiikka, jonka Arthur Pryor [1] käsitteli ja muotoili ensimmäisen kerran 1950-luvulla modaalilogiikan perusteella , sitä käytettiin ja kehitettiin tietotekniikassa laajimmin Turing-palkinnon voittajan Amir Pnuelin työn ansiosta .

Esimerkki

Lausunnon: "Minulla on nälkä" merkitys ei muutu ajan myötä, mutta sen totuus voi muuttua: tietyllä ajanhetkellä se voi olla totta tai tarua, mutta ei molempia. Toisin kuin ei-ajallisessa logiikassa, jossa väitteiden arvo ei muutu ajan myötä, aikalogiikassa arvo riippuu siitä, milloin se testataan. Ajallinen logiikka antaa sinun ilmaista väitteitä, kuten "olen aina nälkäinen", "olen joskus nälkäinen" tai "olen nälkäinen , kunnes syön".

Temporal Operators

Temporaalisessa logiikassa on kahdenlaisia operaattoreita : looginen ja modaalinen. ( ) käytetään yleisesti loogisina operaattoreina . Lineaarisessa aikalogiikassa ja laskentapuulogiikassa käytettävät modaalioperaattorit määritellään seuraavasti. $\neg ,\lor ,\land ,\rightarrow$

Tekstin nimitys	Symbolimerkintä	Määritelmä	Kuvaus
Binäärioperaattorit
$\phi$ U $\psi$	$\phi ~\mathcal{U}~ \psi$	$\begin{matrix}(B\,\mathcal{U}\,C)(\phi)= \\ (\olemassa i:C(\phi_i)\land(\forall j<i:B(\phi_j)) )\end{matriisi}$	U ntil (vahva): tulee suorittaa jossain tilassa tulevaisuudessa (mahdollisesti nykyisessä), ominaisuus on suoritettava kaikissa tiloissa määritettyyn tilaan saakka (ei mukaan lukien). $\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{matriisi}$	R - julkaisu: Vapautuu , jos tosi , kunnes se on totta ensimmäistä kertaa (tai aina, jos se ei ole). Muussa tapauksessa siitä tulee totta ainakin kerran ennen kuin se tulee todeksi ensimmäistä kertaa. $\phi$ $\psi$ $\psi$ $\phi$ $\phi$ $\psi$
Unaariset operaattorit
N $\phi$ X $\phi$	$\circ \phi$	$\mathcal{N}B(\phi_i)=B(\phi_{i+1})$	N e X t: täytyy olla tosi heti annettua seuraavassa tilassa. $\phi$
F $\phi$	$\Timantti \phi$	$\mathcal{F}B(\phi)=(true\,\mathcal{U}\,B)(\phi)$	T uilaisuus : tulee toteutua ainakin yhdessä tilassa tulevaisuudessa. $\phi$
G $\phi$	$\Box \phi$	$\mathcal{G}B(\phi)=\neg\mathcal{F}\neg B(\phi)$	G lobaalisesti: täytyy olla totta kaikissa tulevissa valtioissa. $\phi$
A $\phi$	$\mathcal{A} \phi$	$\begin{matrix}(\mathcal{A}B)(\psi)= \\ (\forall \phi:\phi_0=\psi\to B(\phi))\end{matrix}$	A ll: On suoritettava kaikilla haaroilla, jotka alkavat tästä. $\phi$
E $\phi$	$\mathcal{E}\phi$	$\begin{matrix}(\mathcal{E}B)(\psi)= \\ (\exists \phi:\phi_0=\psi\land B(\phi))\end{matrix}$	E olemassa: Ainakin yksi haara on käynnissä. $\phi$

Muut modaalioperaattorit

W - lause, joka tarkoittaa W eak till : vastaa $f Wg$ $fUg\lor Gf$

Kaksinaisuus-identiteetit

Kuten de Morganin säännöissä, temporaalisille operaattoreille on kaksinaisuusominaisuuksia:

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

Sovellukset

Temporaalista logiikkaa käytetään usein ilmaisemaan muodollisia varmennusvaatimuksia . Esimerkiksi ominaisuudet, kuten "jos pyyntö vastaanotetaan, siihen tulee varmasti vastaus" tai "funktiota kutsutaan enintään kerran laskutoimituksessa" on kätevä muotoilla ajallisen logiikan avulla. Tällaisten ominaisuuksien testaamiseen käytetään erilaisia automaatteja, esimerkiksi Büchin automaatteja LTL-lineaarisella aikalogiikalla ilmaistujen ominaisuuksien testaamiseen .

Vaihtoehdot

Temporaalisen logiikan pääasiallinen universaali muunnelma on modaalinen μ-laskenta ( Scott - de Bakker , 1969); se sisältää Henessy-Milner-logiikan ja CTL* osajoukona , ja tietojenkäsittelytieteen tärkeimmät muunnelmat - lineaarinen aikalogiikka ( LTL ) ja laskentapuulogiikka ( CTL ) - ovat CTL:n * fragmentteja .

Lisäksi on olemassa muitakin ajallisen logiikan muunnelmia, jotka eivät ole pelkistettävissä modaaliseen μ-laskentaan, esimerkiksi intervalliaikalogiikka ja metrinen temporaalinen logiikka

Joissakin käytännön vaihtoehdoissa käytetään temporaalisen logiikan yhdistelmiä muiden logiikojen kanssa, erityisesti sellainen on temporaalinen toimintalogiikka ( luotu TLA⁺ -määrittelykielelle ), joka yhdistää temporaalisen logiikan ja toimintalogiikan .

Muistiinpanot

↑ Ricardo Caferra. Tietojenkäsittelytieteen ja tekoälyn logiikka. - John Wiley & Sons, 2013. - 537 s. — ISBN 978-1-118-60426-7 .

Kirjallisuus

Clark E. M., Gramberg O., Peled D. Ohjelmamallien verifiointi. Mallin tarkistus. Moskova: MTsNMO. 2002. ISBN 5-94057-054-2

Sanakirjat ja tietosanakirjat	Iso venäläinen Britannica (verkossa)

Logiikka

Filosofia • Semantiikka • Syntaksi • Historia

Logiikkaryhmät

klassista logiikkaa	Aristoteelinen logiikka propositionaalinen logiikka Ensimmäisen asteen logiikka Toisen asteen logiikka korkeamman asteen logiikkaa
matemaattinen logiikka	joukko teoria Mallin teoria Lasketettavuuden teoria Todistusteoria ja konstruktiivinen matematiikka Lineaarinen logiikka muodollinen järjestelmä luonnollinen johtopäätös Sekvenssilaskenta Logiikan algebra Asiaankuuluva logiikka Deonttinen logiikka intuitionistinen logiikka Lambek-laskenta
Ei-klassinen logiikka	intuitionismi sumea logiikka Alirakennelogiikka logiikka Kuvauslogiikka Moniarvoinen logiikka Logiikka synteesi Sidontalogiikka Temporaalinen logiikka Modaalinen logiikka ( Hybridilogiikka ) episteeminen logiikka
Filosofinen logiikka	Kriittinen ajattelu epävirallista logiikkaa deduktiivinen päättely

Komponentit

Sieppaus (logiikka)
Todennäköisyys
lausunto
Vähennys / Induktio / Traduction
Todellisuus
induktiivinen päättely
päättely
boolen vakio
Totta
loogista seuraamista
Looginen muoto
Tarpeelliset ja riittävät olosuhteet
Kuvaus
Määritelmä
Korvaus
Paketti
Kiista ( Antinomia )
Synteettinen arviointi / Analyyttinen arviointi
Linkki

Luettelo loogisista symboleista