Cycle detection in computation tree logic

DOI10.1016/J.IC.2018.09.007MaRDI QIDQ1784962zbMATH OpenOpenAlexFDO

Authors Gaëlle Fontaine, Fabio Mogavero, Aniello Murano, Giuseppe Perelli, Loredana Sorrentino

Publication date 27 September 2018

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1609.04095

zbMATH Keywords

verificationmodel checkingsatisfiabilitytemporal logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

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.

Recommendations

• scientific article; zbMATH DE number 7439738
• Extended computation tree logic
• Quantified computation tree logic
• Quantified CTL: expressiveness and complexity
• Counting CTL

Cites work

• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 1223729 (Why is no real title available?)
• scientific article; zbMATH DE number 1980931 (Why is no real title available?)
• scientific article; zbMATH DE number 7439738 (Why is no real title available?)
• scientific article; zbMATH DE number 3212004 (Why is no real title available?)
• Alternating-time temporal logic
• An automata-theoretic approach to branching-time model checking
• Automata, logics, and infinite games. A guide to current research
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Decision procedures and expressiveness in the temporal logic of branching time
• Deterministic generators and games for LTL fragments
• Enriched MU-Calculi Module Checking
• Finitary winning in \({\omega}\)-regular games
• From liveness to promptness
• Infinite games on finitely coloured graphs with applications to automata on infinite trees
• Module checking
• On promptness in parity games
• Pushdown module checking
• Reasoning about strategies: on the model-checking problem
• Reasoning about strategies: on the satisfiability problem
• TYPENESS FOR ω-REGULAR AUTOMATA
• Temporal logic can be more expressive
• The Complexity of Enriched Mu-Calculi
• \textit{Once} and \textit{for all}
• “Sometimes” and “not never” revisited

Cited in

(4)

• Computation tree logic for synchronization properties
• Computation tree logic with deadlock detection
• scientific article; zbMATH DE number 7439738 (Why is no real title available?)
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Cycle detection in computation tree logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1784962)