CTL *

In informatica teorica , in particolare nella verifica formale , CTL * (pronunciato CTL stella in inglese) è una logica temporale . Questa è una generalizzazione dell'albero logico del tempo (in) (CTL: logica dell'albero di calcolo ) e della logica temporale lineare (LTL: logica temporale lineare ). Combina liberamente quantificatori su percorsi e operatori temporali. CTL * è quindi logica ad albero. La semantica delle formule CTL * si basa su una struttura Kripke .

Storico

La logica lineare temporale (LTL) è stata proposta per la prima volta da Amir Pnueli nel 1977, allo scopo di verificare i programmi per computer. Quattro anni dopo, nel 1981, Edmund M. Clarke e Allen Emerson inventarono il CTL e il controllo dei modelli . CTL * è stato definito da Emerson e Joseph Y. Halpern nel 1986.

È interessante notare che CTL e LTL sono stati sviluppati indipendentemente, prima di CTL *. Queste due logiche sono diventate molto importanti all'interno della comunità di controllo dei modelli, mentre CTL * rimane poco utilizzato . Questo è sorprendente , Perché la complessità algoritmica del controllo del modello CTL * non è peggiore di quella del controllo del modello LTL: questi due problemi sono in PSPACE .

Sintassi

Il linguaggio delle formule CTL * è generato dalla seguente grammatica libera dal contesto :

{\ displaystyle \ Phi :: = \ top \ mid p \ mid \ neg \ Phi \ mid (\ Phi \ land \ Phi) \ mid A \ phi \ mid E \ phi}

dov'è una proposizione atomica ;

p

{\ Displaystyle \ phi :: = \ Phi \ mid \ neg \ phi \ mid (\ phi \ land \ phi) \ mid X \ phi \ mid (\ phi U \ phi)}

Le formule CTL * valide vengono costruite utilizzando il simbolo . Queste formule sono chiamate formule di stato , mentre quelle create utilizzando il simbolo sono chiamate formule di percorso . $\ Phi$ $\ phi$

Semantica

La semantica di CTL * è interpretata in una struttura Kripke . Gli stati sono decorati con proposizioni atomiche . $p$

CTL * permette di ragionare sia sugli stadi di calcolo (attraverso le formule di stato interpretate in relazione agli stati) sia sui calcoli nel loro complesso (con le formule di cammino interpretate sui cammini).

Possiamo fornire la seguente semantica intuitiva:

${\ displaystyle A \ phi}$ indica che sarà verificato in tutti i calcoli possibili; $\ phi$
${\ displaystyle E \ phi}$ indica che si può trovare un calcolo tale che sia verificato; $\ phi$
$X \ phi$ indica che sarà verificato dalla fase successiva del calcolo; $\ phi$
${\ displaystyle \ phi _ {1} U \ phi _ {2}}$ indica che sarà verificato nel resto del calcolo, finché non sarà vero. $\ phi _ {1}$ $\ phi _ {2}$

Formule di stato

Notiamo quando uno stato di una struttura Kripke soddisfa una formula di stato . Questa relazione è definita induttivamente dalle seguenti regole: $s \ modelli \ Phi$ $S$ $\ Phi$

${\ displaystyle ({\ mathcal {M}}, s) \ models \ top}$ sempre ;
${\ displaystyle ({\ mathcal {M}}, s) \ models p}$ se e solo se decora ; $p$ $S$
${\ displaystyle ({\ mathcal {M}}, s) \ models \ neg \ Phi}$ se e solo se ; ${\ displaystyle ({\ mathcal {M}}, s) \ non \ models \ Phi}$
${\ displaystyle ({\ mathcal {M}}, s) \ models \ Phi _ {1} \ land \ Phi _ {2}}$ se e solo se e ; ${\ displaystyle ({\ mathcal {M}}, s) \ models \ Phi _ {1}}$ ${\ displaystyle ({\ mathcal {M}}, s) \ models \ Phi _ {2}}$
${\ displaystyle ({\ mathcal {M}}, s) \ models A \ phi}$ se e solo se per qualsiasi percorso che inizia in ; $\ pi \ models \ phi$ $\ \ pi$ $S$
${\ displaystyle ({\ mathcal {M}}, s) \ models E \ phi}$ se e solo se per almeno un percorso che inizia in . $\ pi \ models \ phi$ $\ \ pi$ $S$

Formule di percorso

Notiamo quando un percorso di una struttura Kripke soddisfa una formula di percorso . Nota anche il sottopercorso . Questa relazione di soddisfazione è definita induttivamente dalle seguenti regole: $\ pi \ models \ phi$ $\ pi = s_ {0} \ to s_ {1} \ to \ cdots$ $\ phi$ $\ \ pi [n]$ $s_ {n} \ to s _ {{n + 1}} \ to \ cdots$

${\ displaystyle ({\ mathcal {M}}, \ pi) \ models \ Phi}$ se e solo se ; ${\ displaystyle ({\ mathcal {M}}, s_ {0}) \ models \ Phi}$
${\ displaystyle ({\ mathcal {M}}, \ pi) \ models \ neg \ phi}$ se e solo se ; ${\ displaystyle ({\ mathcal {M}}, \ pi) \ non \ models \ phi}$
${\ displaystyle ({\ mathcal {M}}, \ pi) \ models \ phi _ {1} \ land \ phi _ {2}}$ se e solo se e ; ${\ displaystyle ({\ mathcal {M}}, \ pi) \ models \ phi _ {1}}$ ${\ displaystyle ({\ mathcal {M}}, \ pi) \ models \ phi _ {2}}$
${\ displaystyle ({\ mathcal {M}}, \ pi) \ models X \ phi}$ se e solo se ; ${\ displaystyle ({\ mathcal {M}}, \ pi [1]) \ models \ phi}$
${\ displaystyle ({\ mathcal {M}}, \ pi) \ models (\ phi _ {1} U \ phi _ {2})}$ se e solo se tale e abbiamo . ${\ displaystyle \ esiste n \ geqslant 0}$ ${\ displaystyle ({\ mathcal {M}}, \ pi [n]) \ models \ phi _ {2}}$ ${\ displaystyle \ forall 0 \ leqslant k <n}$ ${\ displaystyle ({\ mathcal {M}}, \ pi [k]) \ models \ phi _ {1}}$

Termini aggiuntivi

Possiamo definire le modalità ("accadrà almeno una volta in futuro") e ("accadrà sempre in futuro") come segue: $F$ $G$

${\ displaystyle F \ phi \ equiv \ top U \ phi}$ ;
${\ Displaystyle G \ phi \ equiv \ neg F \ neg \ phi}$ .

Notare che si applicano alle formule del percorso.

Esempi di formule

Formula CTL * che non è né in LTL né in CTL: ${\ Displaystyle EX (p) \ land AFG (p)}$
Formula LTL che non è in CTL: ${\ displaystyle AFG (p)}$
Formula CTL che non è in LTL: ${\ displaystyle EX (p)}$
Formula CTL * che è in CTL e LTL: ${\ displaystyle AG (p)}$

Nota: quando si considera LTL come un sottoinsieme di CTL *, qualsiasi formula di LTL è implicitamente preceduta dal quantificatore del percorso universale $A.$

Problemi decisionali

Il controllo del modello di CTL * è PSPACE-completo e il problema di soddisfacibilità è 2EXPTIME-completo.

Note e riferimenti

Christel Baier e Joost-Pieter Katoen , Principi del Modello Controllo (Rappresentanza e Mente serie) , The MIT Press,1 ° gennaio 2008, 975 p. ( ISBN 978-0-262-02649-9 e 0-262-02649-X , leggi online )
(in) Orna Kupferman e Moshe Y. Vardi , " Church's problem revisited " , Bulletin of Symbolic Logic , vol. 5, n o 2Giugno 1999, p. 245-263 ( DOI 10.2307 / 421091 , leggi in linea )

Bibliografia

(en) Amir Pnueli , " La logica temporale dei programmi ", Atti del 18 ° simposio annuale sui fondamenti dell'informatica (FOCS), 1977, 46–57. DOI = 10.1109 / SFCS.1977.32 ( leggi online [PDF] )
(en) E. Allen Emerson e Joseph Y. Halpern, " " Talvolta "e" Non mai "rivisitato: sulla ramificazione contro la logica temporale lineare " , Journal of the ACM , vol. 33, n o 1,Gennaio 1986, p. 151-178 ( DOI http://doi.acm.org/10.1145/4904.4999 , leggi online [PDF] )
(it) Philippe Schnoebelen, " La complessità del controllo del modello logico temporale ". Advances in Modal Logic 2002 : 393–436 ( collegamento in linea [PDF] )

Vedi anche

link esterno

(it) Diapositive didattiche sul CTL del professor Alessandro Artale presso la Libera Università di Bolzano