Extended computation tree logic

DOI10.1007/978-3-642-16242-8_6zbMATH Open1306.68098arXiv1006.3709OpenAlexW3123850752MaRDI QIDQ4933296FDOQ4933296

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)

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.

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

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

Mathematics Subject Classification ID

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

Cited In (27)

• Semantics of infinite tree logic programming
• 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
• Title not available (Why is that?)
• Extended full computation-tree logics for paraconsistent model checking
• Quantified computation tree logic
• Computation tree logic for synchronization properties
• Model checking of RegCTL
• Title not available (Why is that?)
• 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
• Min-max Computation Tree Logic
• Cycle detection in computation tree logic
• Title not available (Why is that?)
• Reachability logic: an efficient fragment of transitive closure logic
• Local distributed model checking of RegCTL
• Branching-time logics with path relativisation
• Title not available (Why is that?)
• Title not available (Why is that?)

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)