Extended computation tree logic

DOI10.1007/978-3-642-16242-8_6MaRDI QIDQ4933296zbMATH OpenOpenAlexFDO

Authors Roland Axelsson, Matthew Hague, Stephan Kreutzer, Martin Lange, Markus Latte

Publication date 12 October 2010

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

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

Mathematics Subject Classification ID

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

Abstract: We introduce a generic extension of the popular branching-time logic CTL which refines the temporal until and release operators with formal languages. For instance, a language may determine the moments along a path that an until property may be fulfilled. We consider several classes of languages leading to logics with different expressive power and complexity, whose importance is motivated by their use in model checking, synthesis, abstract interpretation, etc. We show that even with context-free languages on the until operator the logic still allows for polynomial time model-checking despite the significant increase in expressive power. This makes the logic a promising candidate for applications in verification. In addition, we analyse the complexity of satisfiability and compare the expressive power of these logics to CTL* and extensions of PDL.

Recommendations

• Quantified computation tree logic
• Axiomatising extended computation tree logic
• Axiomatising extended computation tree logic
• Branching-time logics with path relativisation
• Model checking of RegCTL

Cited in

(27)

• Semantics of infinite tree logic programming
• scientific article; zbMATH DE number 1863182 (Why is no real title available?)
• Branching-time logics and fairness, revisited
• Model-checking graded computation-tree logic with finite path semantics
• ACTLW -- an action-based computation tree logic with unless operator
• scientific article; zbMATH DE number 4119650 (Why is no real title available?)
• Extended full computation-tree logics for paraconsistent model checking
• Quantified computation tree logic
• Computation tree logic for synchronization properties
• Model checking of RegCTL
• scientific article; zbMATH DE number 1536557 (Why is no real title available?)
• A CTL-based logic for program abstractions
• Graded Computation Tree Logic with Binary Coding
• Computation tree logic with deadlock detection
• Temporal logics with language parameters
• Axiomatising extended computation tree logic
• Axiomatising extended computation tree logic
• Temporal Logic with Recursion.
• On the Model Checking Problem for Some Extension of CTL*
• Action and State Based Computation Tree Measurement Language and Algorithms
• Cycle detection in computation tree logic
• Min-max Computation Tree Logic
• scientific article; zbMATH DE number 2084327 (Why is no real title available?)
• Reachability logic: an efficient fragment of transitive closure logic
• Local distributed model checking of RegCTL
• Branching-time logics with path relativisation
• scientific article; zbMATH DE number 1948485 (Why is no real title available?)

This page was built for publication: Extended computation tree logic

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