Cycle detection in computation tree logic

2Citations
Citations of this article
7Readers
Mendeley users who have this article in their library.

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

Cite

CITATION STYLE

APA

Fontaine, G., Mogavero, F., Murano, A., Perelli, G., & Sorrentino, L. (2016). Cycle detection in computation tree logic. In Electronic Proceedings in Theoretical Computer Science, EPTCS (Vol. 226, pp. 164–177). Open Publishing Association. https://doi.org/10.4204/EPTCS.226.12

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free