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

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

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

(29)

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

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)