Beräkningsträdlogik

Beräkningsträdlogik ( CTL ) är en förgreningstidslogik , vilket betyder att dess modell av tid är en trädliknande struktur där framtiden inte bestäms; det finns olika vägar i framtiden, varav vilken som helst kan vara en verklig väg som realiseras. Den används i formell verifiering av mjukvaru- eller hårdvaruartefakter, vanligtvis av mjukvaruapplikationer som kallas modellcheckers , som avgör om en given artefakt har säkerhets- eller livlighetsegenskaper . Till exempel kan CTL specificera att när något initialt villkor är uppfyllt (t.ex. alla programvariabler är positiva eller inga bilar på en motorväg går över två körfält), så undviker alla möjliga exekveringar av ett program något oönskat villkor (t.ex. dividera ett tal med noll eller två bilar som kolliderar på en motorväg). I det här exemplet kan säkerhetsegenskapen verifieras av en modellkontroll som utforskar alla möjliga övergångar från programtillstånd som uppfyller initialvillkoret och säkerställer att alla sådana exekveringar uppfyller egenskapen. Beräkningsträdlogik tillhör en klass av tidslogik som inkluderar linjär temporal logik (LTL). Även om det finns egenskaper som endast kan uttryckas i CTL och egenskaper som endast kan uttryckas i LTL, kan alla egenskaper som kan uttryckas i endera logiken också uttryckas i CTL* .

CTL föreslogs först av Edmund M. Clarke och E. Allen Emerson 1981, som använde den för att syntetisera så kallade synkroniseringsskelett , dvs abstraktioner av samtidiga program .

Syntax för CTL

Språket för välformade formler för CTL genereras av följande grammatik :

${\begin{aligned}\phi &::=\bot \mid \top \mid p\mid (\neg \ phi )\mid (\phi \land \phi )\mid (\phi \lor \phi )\mid (\phi \Rightarrow \phi )\mid (\phi \Leftrightarrow \phi )\\&\mid \quad { \mbox{AX }}\phi \mid {\mbox{EX }}\phi \mid {\mbox{AF }}\phi \mid {\mbox{EF }}\phi \mid {\mbox{AG }} \phi \mid {\mbox{EG }}\phi \mid {\mbox{A }}[\phi {\mbox{ U }}\phi ]\mid {\mbox{E }}[\phi {\mbox { U }}\phi ]\end{aligned}}$

där $p$ sträcker sig över en uppsättning atomformler . Det är inte nödvändigt att använda alla anslutningar – till exempel $\{\neg ,\land ,{\mbox{AX}},{\mbox{AU}}, {\mbox{EU}}\}$ består av en komplett uppsättning anslutningar, och de andra kan definieras med hjälp av dem.

• ${\mbox{A}}$ betyder "längs alla vägar" (oundvikligen)
• ${\mbox{E}}$ betyder 'längs åtminstone (det finns) en väg' (eventuellt)

Till exempel är följande en välformad CTL-formel:

${\mbox{EF }}({\mbox{EG }}p\Högerpil {\mbox{AF }}r)$

Följande är inte en välformad CTL-formel:

${\mbox{EF }}{\big (}r{\mbox{ U }}q{\big )}$

Problemet med den här strängen är att $U$ endast kan uppstå när den paras ihop med en $A$ eller en $E$ .

CTL använder atomära propositioner som sina byggstenar för att göra uttalanden om tillstånden i ett system. Dessa propositioner kombineras sedan till formler med logiska operatorer och temporala operatorer .

Operatörer

Logiska operatorer

De logiska operatorerna är de vanliga: ¬, ∨, ∧, ⇒ och ⇔. Tillsammans med dessa operatorer kan CTL-formler också använda de booleska konstanterna sant och falskt .

Temporala operatörer

De temporala operatorerna är följande:

• Kvantifierare över vägar
  • A Φ – A ll: Φ måste hålla på alla banor från det aktuella tillståndet.
  • E Φ – Finns : det finns minst en väg från det aktuella tillståndet där Φ gäller.
• Sökvägsspecifika kvantifierare
  • X φ – Ne x t: φ måste hålla i nästa tillstånd (denna operator anges ibland N istället för X ).
  • G φ – Globalt : φ måste hålla på hela den efterföljande banan.
  • F φ – F inally: φ måste så småningom hålla (någonstans på den efterföljande banan).
  • φ U ψ – U ntil: φ måste hålla åtminstone tills vid någon position ψ håller. Detta innebär att ψ kommer att verifieras i framtiden.
  • φ W ψ – W eak tills: φ måste hålla tills ψ håller. Skillnaden med U är att det inte finns någon garanti för att ψ någonsin kommer att verifieras. W - operatören kallas ibland "om inte".

I CTL* kan de temporala operatorerna blandas fritt. I CTL måste operatören alltid grupperas i två: en vägoperatör följt av en statlig operatör. Se exemplen nedan. CTL* är strikt mer uttrycksfull än CTL.

Minimal uppsättning operatörer

I CTL finns minimala uppsättningar av operatörer. Alla CTL-formler kan transformeras till att endast använda dessa operatorer. Detta är användbart vid modellkontroll . En minimal uppsättning operatorer är: {true, ∨, ¬, EG , EU , EX }.

Några av de transformationer som används för temporala operatorer är:

• EF φ == E [true U ( φ )] ( eftersom F φ == [true U ( φ )] )
• AX φ == ¬ EX (¬ φ )
• AG φ == ¬ EF (¬ φ ) == ¬ E [true U (¬ φ )]
• AF φ == A [true U φ ] == ¬ EG (¬ φ )
• A [ φ U ψ ] == ¬( E [(¬ ψ ) U ¬( φ ∨ ψ )] ∨ EG (¬ ψ ) )

Semantik för CTL

Definition

CTL-formler tolkas över övergångssystem . Ett övergångssystem är en trippel ${\displaystyle {\mathcal {M}}=(S,{\rightarrow },L)} ,$ där $S$ är en uppsättning tillstånd , ${\rightarrow }\subseteq S\times S$ är en övergångsrelation, som antas vara seriell, dvs varje tillstånd har minst en efterföljare, och $L$ är en märkningsfunktion , tilldela propositionsbokstäver till stater. Låt ${\mathcal {M}}=(S,\rightarrow ,L)$ vara en sådan övergångsmodell

med $s\in S,\phi \in F$ där F är mängden wffs över språket för M $\displaystyle {\mathcal {M}}}$ .

definieras relationen för semantisk entailment ${\displaystyle ({\mathcal {M}},s\models \phi )} rekursivt på$$\phi$ :

1. ${\Big (}({\mathcal {M}},s)\modeller \top {\Big )}\land { \Big (}({\mathcal {M}},s)\inte \models \bot {\Big )}$
2. ${\Big (}({\mathcal {M}},s)\modeller p{\Big )}\Leftrightarrow {\Big (}p\in L(s){\Big )}$
3. ${\Big (}({\mathcal {M}},s)\modeller \neg \phi {\Big )} \Leftrightarrow {\Big (}({\mathcal {M}},s)\inte \models \phi {\Big )}$
4. ${\Big (}({\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 )}$
5. ${\Big (}({\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 )}$
6. ${\Big (}({\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 ) }$
7. ${\bigg (}({\mathcal {M}},s)\models \phi _{1}\Leftrightarrow \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}{\ stor )}{\Big )}{\bigg )}$
8. ${\Big (}({\mathcal {M}},s) \models AX\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s\rightarrow s_{1}\rangle {\big (}({\mathcal {M}},s_{1})\ modeller \phi {\big )}{\Big )}$
9. ${\Big (}({\mathcal {M}},s) \models EX\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s\rightarrow s_{1}\rangle {\big (}({\mathcal {M}},s_{1})\ modeller \phi {\big )}{\Big )}$
10. ${\Big (} ({\mathcal {M}},s)\models AG\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s =s_{1})\forall i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}$
11. ${\Big (} ({\mathcal {M}},s)\models EG\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s =s_{1})\forall i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}$
12. ${\Big (} ({\mathcal {M}},s)\models AF\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s =s_{1})\exists i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}$
13. ${\Big (} ({\mathcal {M}},s)\models EF\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s =s_{1})\exists i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}$
14. ${\bigg (}({\mathcal {M}},s)\modeller A[\phi _{1}U\phi _{2}]{\bigg )}\Leftrightarrow {\bigg (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\ Stor (}{\big (}({\mathcal {M}},s_{i})\models \phi _{2}{\big )}\land {\big (}\forall (j<i)( {\mathcal {M}},s_{j})\models \phi _{1}{\big )}{\Big )}{\bigg )}$
15. ${\bigg (}({\mathcal {M}},s)\models E[\phi _{1}U\phi _{2}]{\bigg )}\Leftrightarrow {\bigg (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\ Stor (}{\big (}({\mathcal {M}},s_{i})\models \phi _{2}{\big )}\land {\big (}\forall (j<i)( {\mathcal {M}},s_{j})\models \phi _{1}{\big )}{\Big )}{\bigg )}$

Karakterisering av CTL

Reglerna 10–15 ovan hänvisar till beräkningsvägar i modeller och är det som i slutändan kännetecknar "Beräkningsträdet"; de är påståenden om naturen hos det oändligt djupa beräkningsträdet som är rotat i det givna tillståndet $s$ .

Semantiska ekvivalenser

Formlerna $\phi$ och $\psi$ sägs vara semantiskt ekvivalenta om något tillstånd i någon modell som uppfyller den ena också uppfyller den andra. Detta betecknas $\phi \equiv \psi$

Det kan ses att A och E är dualer, som är universella respektive existentiella beräkningsvägkvantifierare: $\neg A\Phi \equiv E\neg \Phi$ .

Dessutom är det G och F också.

Därför kan en instans av De Morgans lagar formuleras i CTL:

$\neg AF\phi \equiv EG\neg \phi$

$\neg EF\phi \equiv AG\neg \phi$

$\neg AX\phi \equiv EX\neg \phi$

Det kan visas med hjälp av sådana identiteter att en delmängd av de tidsmässiga CTL-kopplingarna är adekvata om den innehåller ${\displaystyle EU} ,$ minst en av $\{AX,EX\}$ och minst en av $\{EG,AF,AU\}$ och de booleska kopplingarna.

De viktiga ekvivalenserna nedan kallas expansionslagarna ; de gör det möjligt att utveckla verifieringen av en CTL-anslutning mot dess efterföljare i tid.

$AG\phi \equiv \phi \land AXAG\phi$

$EG\phi \equiv \phi \land EXEG\phi$

$AF\phi \equiv \phi \lor AXAF\phi$

$EF\phi \equiv \phi \lor EXEF\phi$

$A[\phi U\psi ]\equiv \psi \lor (\phi \ land AXA[\phi U\psi ])$

$E[\phi U\psi ]\equiv \psi \lor ( \phi \land EXE[\phi U\psi ])$

Exempel

Låt "P" betyda "Jag gillar choklad" och Q betyder "Det är varmt ute."

• AG .P

"Jag kommer att gilla choklad från och med nu, oavsett vad som händer."

• EF .P

"Det är möjligt att jag kanske gillar choklad någon dag, åtminstone för en dag."

• AF . EG .P

"Det är alltid möjligt (AF) att jag plötsligt börjar gilla choklad för resten av tiden." (Obs: inte bara resten av mitt liv, eftersom mitt liv är ändligt, medan G är oändligt).

• EG . AF .P

"Beroende på vad som händer i framtiden (E) är det möjligt att jag under resten av tiden (G) kommer att vara garanterad minst en (AF) chokladliknande dag framför mig. Men om något går någonsin fel, då är alla spel avstängda och det finns ingen garanti för om jag någonsin kommer att gilla choklad."

De två följande exemplen visar skillnaden mellan CTL och CTL*, eftersom de tillåter att till-operatören inte är kvalificerad med någon sökvägsoperatör ( A eller E ):

• AG (P U Q)

"Från och med nu tills det är varmt ute kommer jag att gilla choklad varje dag. När det väl är varmt ute är alla vad som gäller om jag kommer att gilla choklad längre. Åh, och det kommer garanterat att vara varmt ute så småningom, om än bara för en enda dag."

• EF (( EX .P) U ( AG .Q))

"Det är möjligt att: det kommer så småningom en tid då det kommer att vara varmt för alltid (AG.Q) och att det före den tiden alltid kommer att finnas något sätt att få mig att gilla choklad nästa dag (EX.P)."

Relationer med andra logiker

Beräkningsträdlogik (CTL) är en delmängd av CTL* såväl som av den modala μ-kalkylen . CTL är också ett fragment av Alur, Henzinger och Kupfermans alternating-time temporal logic ( ATL).

Beräkningsträdlogik (CTL) och linjär temporal logik (LTL) är båda en delmängd av CTL*. CTL och LTL är inte likvärdiga och de har en gemensam delmängd, vilket är en riktig delmängd av både CTL och LTL.

• FG .P finns i LTL men inte i CTL.
• AG (P⇒(( EX .Q)∧( EX ¬Q))) och AG.EF .P finns i CTL men inte i LTL.

Tillägg

CTL har utökats med andra ordningens kvantifiering $\exists p$ och $\forall p$ till kvantifierad beräkningsträdlogik (QCTL). Det finns två semantiker:

• trädets semantik. Vi märker noder i beräkningsträdet. QCTL* = QCTL = MSO över träd. Modellkontroll och tillfredsställelse är tornet kompletta.
• strukturens semantik. Vi märker stater. QCTL* = QCTL = MSO över grafer . Modellkontroll är PSPACE-komplett men tillfredsställelse är obestämbar .

En minskning från modellkontrollproblemet för QCTL med struktursemantik till TQBF (true quantified Boolean Formler) har föreslagits, för att dra fördel av QBF-lösare.

Se även

• Probabilistisk CTL
• Rättvis logik för beräkningsträd
• Linjär tidslogik

• EM Clarke; EA Emerson (1981). "Design och syntes av synkroniseringsskelett med hjälp av tidslogik för förgreningstid" ( PDF) . Programlogik, Workshops förfarande, föreläsningsanteckningar i datavetenskap . Springer, Berlin. 131 : 52–71.
•   Michael Huth; Mark Ryan (2004). Logik i datavetenskap (andra upplagan) . Cambridge University Press. sid. 207. ISBN 978-0-521-54310-1 .
• Emerson, EA; Halpern, JY (1985). "Beslutsprocedurer och uttrycksfullhet i den tidsmässiga logiken av förgrening av tid". Tidskrift för data- och systemvetenskap . 30 (1): 1–24. doi : 10.1016/0022-0000(85)90001-7 .
• Clarke, EM; Emerson, EA & Sistla, AP (1986). "Automatisk verifiering av samtidiga system i finita tillstånd med hjälp av tidslogikspecifikationer". ACM-transaktioner på programmeringsspråk och system . 8 (2): 244–263. doi : 10.1145/5397.5399 .
•   Emerson, EA (1990). "Tidsmässig och modal logik". I Jan van Leeuwen (red.). Handbook of Theoretical Computer Science, vol. B . MIT Press. s. 955–1072. ISBN 978-0-262-22039-2 .

externa länkar

• Undervisningsbilder av CTL