Counting CTL

DOI10.1007/978-3-642-12032-9_15MaRDI QIDQ3557853zbMATH OpenOpenAlexFDO

Authors François Laroussinie, Antoine Meyer, Eudes Petonnet

Publication date 27 April 2010

Published in Foundations of Software Science and Computational Structures (Search for Journal in Brave)

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

Mathematics Subject Classification ID

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

Abstract: This paper presents a range of quantitative extensions for the temporal logic CTL. We enhance temporal modalities with the ability to constrain the number of states satisfying certain sub-formulas along paths. By selecting the combinations of Boolean and arithmetic operations allowed in constraints, one obtains several distinct logics generalizing CTL. We provide a thorough analysis of their expressiveness and succinctness, and of the complexity of their model-checking and satisfiability problems (ranging from P-complete to undecidable). Finally, we present two alternative logics with similar features and provide a comparative study of the properties of both variants.

Recommendations

• Counting CTL
• Quantified computation tree logic
• Quantified CTL: expressiveness and complexity
• scientific article; zbMATH DE number 1512710
• On the expressivity and complexity of quantitative branching-time temporal logics

Cited in

(17)

• On the expressivity and complexity of quantitative branching-time temporal logics
• Quantified computation tree logic
• Model checking for fragments of the interval temporal logic HS at the low levels of the polynomial time hierarchy
• Cycle detection in computation tree logic
• Efficient data validation for geographical interlocking systems
• Interactive verification of architectural design patterns in FACTum
• A survey on temporal logics for specifying and verifying real-time systems
• Quantitative -calculus and CTL based on constraint semirings
• Extending temporal logics with data variable quantifications
• A counting logic for structure transition systems
• Counting CTL
• Making Metric Temporal Logic Rational
• Model-Checking Counting Temporal Logics on Flat Structures
• Two-variable logics with some betweenness relations: expressiveness, satisfiability and membership
• Pebble weighted automata and weighted logics
• Trace-length independent runtime monitoring of quantitative policies in LTL
• Introducing robust reachability

This page was built for publication: Counting CTL

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