Computation Tree Logic

Sintaxa CTL

Sintaxă CTL are două etape în cazul în care, în formulele CTL sunt clasificate în formule de stare şi formule de traiectorie. Prima afirmaţie este cu privire la propozitii atomice de stare şi a structurii lor ramificat, în timp ce formule de drum exprimă proprietăţi temporale a căii.

Definiţie 1

Formule de stare CTL peste setul de propoziţii atomice AP (AP – mulţime de propoziţii atomice = observaţii care apar în formule/ proprietăţi/ specificaţii) sunt formate în funcţie de gramatică următoarele:

în cazul în care a AP şi φ este o formulă drum.

Formule de drum CTL sunt formate în funcţie de gramatică următoarele:

în cazul în care Φ, Φ1 şi Φ2 sunt formulele de stare.

Literele greceşti mari va indica formule CTL de stare şi literele greceşti mici va indica formule CTL de traiectorie.

Operatori temporali (modalităţi de adevăr pe o traiectorie):

• X (next): în următoarea stare ○

• F (future): există cel putin o stre viitoare ◊

• G (globally): toate stările viitoare □

• U (until): prop1 obligatorie până când apare prop2

Uneori se mai defineşte şi următorul operator:

• R (release): apariţia prop1 elimină obligativitatea prop2

Conectorii temporali folosesc două litere:

- A şi E pentru cuantificarea în lăţime:

- A se iau toate alternativele din punctul de ramificare (All)

- E există cel puţin o alternativă în punctul de ramificare (Exists)

- G şi F cuantifică de-a lungul drumurilor

CTL face distincţia între formulele de stare şi formulele de traiectorie. Intuitiv, formule de stare exprimă o proprietate a unei stări, în timp ce formule de traiectorie exprimă o proprietate a unui drum, de exemplu, o secvenţă infinită de stări. Operatorii temporali şi sunt operatorii de traiectorie. Formula este valabilă pentru o traiectorie, dacă Φ apare în starea următoare în drum, şi este valabilă pentru o traiectorie, dacă există o anumită stare de-a lungul drumului pentru care Ψ şi Φ este valabilă în toate statele înainte de această stare. Formulele de traiectorie pot fi transformate în formulele de stat prin prefixarea lor fie cu cuantificator calea (pronunţat „pentru unele căi”) sau cuantificatorul calea (pronunţat „pentru toate căile”). Reţineţi că operatorii liniari temporală sau sunt necesari pentru a fi imediat precedate de pentru a obţine o formulă legală de stare. Formula este valabilă într-o stare în cazul în care există unele căi care îndeplineşte φ care începe în această stare. La fel, este valabilă într-o stare în cazul în care toate căile care încep în această stare satisface φ.

Exemplu: Formule legale CTL

Fie AP = un set de propoziţii atomice. Exemple corecte de formule sintactice CTL sunt

şi .

Câteva exemple de formule, care sunt incorecte sunt sintactic

Primul nu este o formulă CTL pentru că nu este o formulă de traiectorie şi, astfel, nu trebuie să fie precedată de . A doua formulă, nu este o formulă CTL, deoarece trueU (x = 1) este o formulă de traiectorie mai degrabă decât o formulă de stare, şi, astfel, nu poate fi precedată de O. Reţineţi că,

sunt, cu toate acestea, sintactic formule corecte CTL.

Operatorii booleeni true, false, , → şi sunt definite în mod obişnuit. Modalităţile temporale „în cele din urmă”, „întotdeauna” şi „slab până când” pot fi derivate, în mod similar, ca şi pentru LTL-după cum urmează:

în cele din urmă:

întotdeauna:

este pronunţat „Φ deţine potenţial” şi este pronunţat „Φ este inevitabilă”. □ este pronunţat „potenţial întotdeauna Φ”, este pronunţat „invariant Φ” şi este pronunţat „pentru toate traiectorile următoare Φ”.

Reţineţi că „întotdeauna” Φ nu pot fi obţinute din „ecuaţia” □Φ = (ca în LTL), deoarece operatorii de logică propoziţională nu pot fi aplicate ca formule traiectorie. În special, nu este o formulă CTL.