Cycle detection in computation tree logic

Temporal logic is a very powerful formalism deeply investigated and used in formal system design and verification. Its application usually reduces to solving specific decision problems such as model checking and satisfiability. In these kind of problems, the solution often requires detecting some specific properties over cycles. For instance, this happens when using classic techniques based on automata, game-theory, SCC decomposition, and the like. Surprisingly, no temporal logics have been considered so far with the explicit ability of talking about cycles. In this paper we introduce Cycle-CTL∗, an extension of the classical branching-time temporal logic CTL∗ along with cycle quantifications in order to predicate over cycles. This 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 investigate the model checking problem for Cycle-CTL∗ and show that it is PSPACE-COMPLETE as for CTL∗. We also study the satisfiability problem for the existential-cycle fragment of the logic and show that it is solvable in 2EXPTIME. This result makes use of an automata-theoretic approach along with novel ad hoc definitions of bisimulation and tree-like unwinding.