We introduce Cycle-CTL⋆, an extension of CTL⋆ with cycle quantifications that are able to predicate over cycles. The introduced logic turns out to be very expressive. Indeed, we prove that it strictly extends CTL⋆ and is orthogonal to μCALCULUS. We also give an evidence of its usefulness by providing few examples involving non-regular properties. We extensively investigate both the model-checking and satisfiability problems for Cycle-CTL⋆ and some of its variants/fragments.
Cycle detection in computation tree logic / Fontaine, G.; Mogavero, F.; Murano, A.; Perelli, G.; Sorrentino, L.. - In: INFORMATION AND COMPUTATION. - ISSN 0890-5401. - 262:(2018), pp. 265-279. [10.1016/j.ic.2018.09.007]
Cycle detection in computation tree logic
Perelli G.
;
2018
Abstract
We introduce Cycle-CTL⋆, an extension of CTL⋆ with cycle quantifications that are able to predicate over cycles. The introduced logic turns out to be very expressive. Indeed, we prove that it strictly extends CTL⋆ and is orthogonal to μCALCULUS. We also give an evidence of its usefulness by providing few examples involving non-regular properties. We extensively investigate both the model-checking and satisfiability problems for Cycle-CTL⋆ and some of its variants/fragments.| File | Dimensione | Formato | |
|---|---|---|---|
|
Fontaine_Cycle_2018.pdf
solo gestori archivio
Tipologia:
Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza:
Tutti i diritti riservati (All rights reserved)
Dimensione
522.35 kB
Formato
Adobe PDF
|
522.35 kB | Adobe PDF | Contatta l'autore |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
