CTL*

CTL* jest nadzbiorem obliczeniowej logiki drzewa (CTL) i liniowej logiki czasowej (LTL). Swobodnie łączy kwantyfikatory ścieżki i operatory czasowe. Podobnie jak CTL, CTL* jest logiką czasu rozgałęzienia. Formalna semantyka formuł CTL* jest zdefiniowana w odniesieniu do danej struktury Kripkego .

Historia

LTL został zaproponowany do weryfikacji programów komputerowych, po raz pierwszy przez Amira Pnueli w 1977 roku. Cztery lata później, w 1981 roku, EM Clarke i EA Emerson wynaleźli CTL i sprawdzanie modeli CTL . CTL* został zdefiniowany przez EA Emersona i Josepha Y. Halperna w 1983 roku.

CTL i LTL zostały opracowane niezależnie przed CTL*. Obie logiki podrzędne stały się standardami w zajmującej się sprawdzaniem modeli , podczas gdy CTL* ma znaczenie praktyczne, ponieważ zapewnia ekspresyjne stanowisko testowe do reprezentowania i porównywania tych i innych logik. Jest to zaskakujące ^{[ potrzebne źródło ]} , ponieważ złożoność obliczeniowa sprawdzania modelu w CTL* nie jest gorsza niż w przypadku LTL: oba leżą w PSPACE .

Składnia

Język dobrze sformułowanych formuł CTL* jest generowany przez następującą jednoznaczną (w odniesieniu do nawiasów) gramatykę bezkontekstową :

{\ dis styl gry \Fi

{\ Displaystyle \ phi :: = \ Phi \ mid (\ neg \ phi) \ mid (\ phi \ ziemia \phi )\mid (\phi \lor \phi )\mid (\phi \Rightarrow \phi )\mid (\phi \Leftrightarrow \phi )\mid X\phi \mid F\phi \mid G\phi \mid [\phi U\phi ]\mid [\phi R\phi ]}

gdzie mieści $wzorów$ w zbiorze atomowych . Prawidłowe formuły CTL * są budowane przy użyciu nieterminalnych ${\ displaystyle \ Phi}$ . Formuły $ścieżki$ nazywane są formułami stanu , podczas gdy formuły utworzone przez symbol nazywane są formułami . (Powyższa gramatyka zawiera pewne nadmiarowości; na przykład, jak również implikacja i równoważność można zdefiniować tak, jak tylko dla $logiki$ lub zdań ) z negacji i koniunkcji oraz czasowego operatory X i U są wystarczające do zdefiniowania dwóch pozostałych .)

Operatorzy są zasadniczo tacy sami jak w CTL . Jednak w CTL każdy operator czasowy ( $)$ kwantyfikatorem, podczas gdy w CTL * nie Kwantyfikator ścieżki uniwersalnej można zdefiniować w CTL * w taki sam sposób, jak w przypadku klasycznego rachunku predykatów ${\ Displaystyle A \ phi = \ neg E \ neg \ phi}$ , chociaż nie jest to możliwe w CTL fragment.

Przykłady formuł

Formuła CTL *, która nie jest ani w LTL, ani w CTL: $land AFG (p)}$
Formuła LTL, której nie ma w CTL: ${\ Displaystyle \ AFG (p)}$
Formuła CTL, której nie ma w LTL: ${\ Displaystyle \ EX (p)}$
Formuła CTL *, która jest w CTL i LTL: ${\ Displaystyle \ AG (p)}$

Uwaga: przyjmując LTL jako podzbiór CTL *, każda formuła LTL jest domyślnie poprzedzona uniwersalnym kwantyfikatorem ścieżki ${\ displaystyle A}$ .

Semantyka

Semantyka CTL* jest zdefiniowana w odniesieniu do pewnej struktury Kripkego . Jak sugerują nazwy, formuły stanów są interpretowane w odniesieniu do stanów tej struktury, podczas gdy formuły ścieżek są interpretowane na podstawie ścieżek w niej.

Formuły stanowe

Jeśli stan struktury $Kripkego$ spełnia formułę stanu, jest oznaczony $s \ modele \ Phi$ $Displaystyle$ . Relacja ta jest zdefiniowana indukcyjnie w następujący sposób:

${\ Displaystyle {\ duży (} ({\ mathcal {M}}, s) \ modele \ top {\ duży)} \ ziemia { \Big (}({\mathcal {M}},s)\not \models \bot {\Big )}}$
${\ Displaystyle {\ duży (} ({\ mathcal {M}}, s) \ modele p {\ duży)} \ strzałka w lewo {\ duży (}p\w L(s){\Duży )}}$
${\ Displaystyle {\ duży (} ({\ mathcal {M}}, s) \ modele \ neg \ Phi {\ duży)} \Leftrightarrow {\Big (}({\mathcal {M}},s)\not \models \Phi {\Big )}}$
${\ Displaystyle {\ Duży (} ({\ mathcal { M}},s)\models \Phi _{1}\land \Phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s) \models \Phi _{1}{\big )}\land {\big (}({\mathcal {M}},s)\models \Phi _{2}{\big )}{\Big )}}$
${\ Displaystyle {\ Duży (} ({\ mathcal { M}},s)\models \Phi _{1}\lor \Phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s) \models \Phi _{1}{\big )}\lor {\big (}({\mathcal {M}},s)\models \Phi _{2}{\big )}{\Big )}}$
${\ Displaystyle {\ Duży (} ({\ mathcal { M}},s)\models \Phi _{1}\Rightarrow \Phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s) \not \models \Phi _{1}{\big )}\lor {\big (}({\mathcal {M}},s)\models \Phi _{2}{\big )}{\Big ) }}$
${\ Displaystyle {\ bigg (} ({\ mathcal {M}}, s) \ modele \ Phi _ {1} \ Strzałka w prawo \ Phi _ {2} {\bigg )}\Leftrightarrow {\bigg (}{\Big (}{\big (}({\mathcal {M}},s)\models \Phi _{1}{\big)}\land {\ big (}({\mathcal {M}},s)\models \Phi _{2}{\big )}{\Big )}\lor {\Big (}\neg {\big (}({\mathcal {M}},s)\models \Phi _{1}{\big )}\land \neg {\big (}({\mathcal {M}},s)\models \Phi _{2}{\ duży )}{\duży )}{\bigg )}}$
${\ Displaystyle {\ duży (} ({\ mathcal {M}}, s) \ modele A \ phi {\ duży)} \ Leftrightarrow {\ duży ( } \ pi \ modele \ phi}$ dla wszystkich ścieżek ${\ Displaystyle \ \ pi}$ począwszy od ${\ Displaystyle s {\ duży}}}$
${\ Displaystyle {\ duży (} ({\ mathcal {M}}, s) \ modele E \ phi {\ duży)} \ Leftrightarrow {\ duży ( } \ pi \ modele \ phi}$ dla pewnej ścieżki ${\ Displaystyle \ \ pi}$ począwszy od ${\ Displaystyle s {\ duży)}}$

Formuły ścieżki

${\ Displaystyle \ pi = s_ {0} \ do s_{1}\to \cdots }$ satysfakcji ${\ Displaystyle \ pi \ modele \ phi}$ $dla$ formuł ścieżki i ścieżki jest również definiowane indukcyjnie. W tym celu niech $\ do$ ścieżkę podrzędną ${n + 1} \ do \ kropki }$ :

${\ Displaystyle {\ Duży (} \ pi \ modele \ Phi {\ Duży)} \ Strzałka w lewo {\ Duży (} ({\ mathcal {M}}, s_{0})\modele \Phi {\Duży )}}$
${\ Displaystyle {\ Duży (} \ pi \ modele \ neg \ phi {\ Duży)} \ Leftrightarrow {\ Duży (} \ pi \ nie \ modele \ phi {\ Duży )}}$
${\ Displaystyle {\ Duży (} \ pi \ modele \ phi _ {1} \ ziemia \ phi _ {2 }{\Big )}\Leftrightarrow {\Big (}{\big (}\pi \models \phi _{1}{\big )}\land {\big (}\pi \models \phi _{2} {\duży duży )}}$
${\ Displaystyle {\ Duży (} \ pi \ modele \ phi _ {1} \ lor \ phi _ {2 }{\Big )}\Leftrightarrow {\Big (}{\big (}\pi \models \phi _{1}{\big )}\lor {\big (}\pi \models \phi _{2} {\duży duży )}}$
${\ Displaystyle {\ Duży (} \ pi \ modele \ phi _ {1} \ Strzałka w prawo \ phi _ {2 }{\Big )}\Leftrightarrow {\Big (}{\big (}\pi \not \models \phi _{1}{\big )}\lor {\big (}\pi \models \phi _{ 2}{\duży )}{\duży )}}$
${\ Displaystyle {\ bigg (}\pi \models \phi _{1}\Leftrightarrow \phi _{2}{\bigg )}\Leftrightarrow {\bigg (}{\Big (}{\big (}\pi \models \phi _ {1}{\big )}\land {\big (}\pi \models \phi _{2}{\big)}{\Big )}\lor {\Big (}\neg {\big (}\ pi \models \phi _{1}{\big )}\land \neg {\big (}\pi \models \phi _{2}{\big )}{\Big )}{\bigg )}}$
${\ Displaystyle {\ Duży (} \ pi \ modele X \ phi {\ Duży)} \ Strzałka w lewo {\ Duży (} \ pi [1] \ modele \ phi {\Duży}}}$
${\ Displaystyle {\ duży (} \ pi \ modele F \ phi {\ duży)} \ Leftrightarrow {\ duży (} \ istnieje n \ geqslant 0:\pi [n]\modele \phi {\Duży)}}$
${\ Displaystyle {\ duży (} \ pi \ modele G \ phi {\ duży)} \ Leftrightarrow {\ duży (} \ forall n \ geqslant 0:\pi [n]\modele \phi {\Duży)}}$
${\ Displaystyle {\ Duży (} \ pi \models [\phi _{1}U\phi _{2}]{\Big )}\Leftrightarrow {\Big (}\exists n\geqslant 0:{\big (}\pi [n]\models \ phi _{2}\land \forall 0\leqslant k<n:~\pi [k]\models \phi _{1}{\big )}{\Big )}}$

Problemy decyzyjne

Sprawdzanie modelu CTL* jest PSPACE-zupełne, a problem spełnialności jest 2EXPTIME- zupełne.

Zobacz też

Amir Pnueli : Czasowa logika programów. Materiały z 18. dorocznego sympozjum na temat podstaw informatyki (FOCS), 1977, 46–57. DOI=10.1109/SFCS.1977.32
E. Allen Emerson , Joseph Y. Halpern : „Czasami” i „nie nigdy” ponownie: o rozgałęzieniach i liniowej logice czasowej. J. ACM 33, 1 (styczeń 1986), 151–178. DOI= http://doi.acm.org/10.1145/4904.4999
Ph. Schnoebelen: Złożoność sprawdzania modelu logiki czasowej. Postępy w logice modalnej 2002: 393–436

Linki zewnętrzne

CTL Slajdy dydaktyczne profesora Alessandro Artale na Wolnym Uniwersytecie Bozen-Bolzano