Cycle detection in computation tree logic

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.

Authors

• Gaëlle Fontaine
• Fabio Mogavero
• Aniello Murano University of Naples Federico II
• Giuseppe Perelli
• Loredana Sorrentino

Keywords

• Temporal logic
• Model checking
• Satisfiability
• Verification