CTL * - CTL*

CTL * je nadmnožinou logika výpočetního stromu (CTL) a lineární časová logika (LTL). Volně kombinuje kvantifikátory cest a časové operátory. Stejně jako CTL je CTL * logika větvícího času. Formální sémantika vzorců CTL * je definována s ohledem na daný Kripkeho struktura.

Dějiny

LTL bylo navrženo pro ověření počítačových programů nejprve do Amir Pnueli v roce 1977. O čtyři roky později v roce 1981 E. M. Clarke a E. A. Emerson vynalezl kontrolu CTL a CTL modelu. CTL * byl definován E. A. Emerson a Joseph Y. Halpern v roce 1983.[1]

CTL a LTL byly vyvinuty nezávisle před CTL *. Obě podlogiky se staly standardy v EU kontrola modelu komunita, zatímco CTL * má praktický význam, protože poskytuje expresivní testovací pole pro reprezentaci a porovnání těchto a dalších logik. To je překvapivé[Citace je zapotřebí ] protože výpočetní složitost kontroly modelu v CTL * není horší než v LTL: oba leží uvnitř PSPACE.

Syntax

The Jazyk z dobře vytvořené vzorce CTL * je generován následujícím jednoznačným (wrt bracketing) bezkontextová gramatika:

kde se pohybuje přes sadu atomové vzorce. Platné CTL * -formulae jsou vytvořeny pomocí neterminálu . Tyto vzorce se nazývají státní vzorce, zatímco ty vytvořené symbolem jsou nazývány vzorce cesty. (Výše uvedená gramatika obsahuje některá nadbytečnost; například stejně jako implikaci a ekvivalenci lze definovat jen pro Booleovy algebry (nebo výroková logika ) z negace a konjunkce a časové operátory X a U jsou dostatečné k definování dalších dvou.)

Operátoři jsou v zásadě stejní jako v CTL. V CTL však každý dočasný operátor () musí přímo předcházet kvantifikátor, zatímco v CTL * to není nutné. Kvantifikátor univerzální cesty může být definován v CTL * stejným způsobem jako pro klasický predikátový počet , i když to ve fragmentu CTL není možné.

Příklady vzorců

  • CTL * vzorec, který není ani v LTL, ani v CTL:
  • Vzorec LTL, který není v CTL:
  • CTL vzorec, který není v LTL:
  • CTL * vzorec, který je v CTL a LTL:

Poznámka: Když vezmeme LTL jako podmnožinu CTL *, je každému vzorci LTL implicitně předpona kvantifikátoru univerzální cesty .

Sémantika

Sémantika CTL * je definována s ohledem na některé Kripkeho struktura. Jak názvy napovídají, stavové vzorce jsou interpretovány s ohledem na stavy této struktury, zatímco vzorce cesty jsou interpretovány přes cesty v ní.

Státní vzorce

Pokud stát struktury Kripke splňuje stavový vzorec je označeno . Tento vztah je definován indukčně takto:

  8. pro všechny cesty začínající v
  9. pro nějakou cestu začínající v

Vzorce cesty

Vztah spokojenosti pro vzorce cesty a cesta je také definována indukčně. Za tímto účelem označte dílčí cestu :

Problémy s rozhodováním

Kontrola modelu CTL * je úplná na PSPACE[2] a problém uspokojivosti je 2EXPTIME-kompletní.[2][3]

Viz také

Reference

  1. ^ Emerson, E. Allen; Halpern, Joseph Y. (1983). ""Někdy se slova „a„ Ne Nikdy “vrátila„: 127–140. doi:10.1145/567067.567081. Citovat deník vyžaduje | deník = (Pomoc)
  2. ^ A b Baier, Christel; Katoen, Joost-Pieter (2008-01-01). Principy kontroly modelu (reprezentace a série mysli). MIT Press. ISBN  978-0262026499.
  3. ^ Orna Kupferman; Moshe Y. Vardi (červen 1999). „Církevní problém se vrátil“. Bulletin of Symbolic Logic. 5 (2): 245–263. doi:10.2307/421091. JSTOR  421091. S2CID  18833301.
  • Amir Pnueli: Časová logika programů. Proceedings of the 18. Annual Symposium on Foundations of Computer Science (FOCS), 1977, 46–57. DOI = 10,1109 / SFCS.1977,32
  • E. Allen Emerson, Joseph Y. Halpern: „Někdy“ a „ne nikdy“ znovu: na větvení versus lineární časová časová logika. J. ACM 33, 1 (leden 1986), 151–178. DOI = http://doi.acm.org/10.1145/4904.4999
  • Ph. Schnoebelen: Složitost kontroly časových logických modelů. Advances in Modal Logic 2002: 393–436

externí odkazy