Cycle Detection in Computation Tree Logic

TL;DR

This paper introduces Cycle-CTL*, a new temporal logic extension that explicitly talks about cycles, enhancing expressiveness for system verification, with model checking complexity similar to CTL* and satisfiability decidability for certain fragments.

Contribution

It presents Cycle-CTL*, an expressive extension of CTL* with cycle quantification, and analyzes its model checking and satisfiability complexities using automata-theoretic methods.

Findings

Cycle-CTL* strictly extends CTL* and is orthogonal to mu-calculus.

Model checking for Cycle-CTL* is PSPACE-Complete.

Satisfiability for the existential-cycle fragment is decidable in 2ExpTime.

Abstract

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 mu-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.