CTL^+ is exponentially more succinct than CTL

DOI10.1007/3-540-46691-6_9MaRDI QIDQ4501666zbMATH OpenFDO

Authors Thomas Wilke

Publication date 7 November 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-46691-6_9

zbMATH Keywords

alternating tree automatoncomputation tree logicexpressivenesslengths of formulasmodal \(\mu\)-calculussuccinctness

Mathematics Subject Classification ID

Temporal logic (03B44) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A purely model-theoretic proof of the exponential succinctness gap between CTL\(^{+}\) and CTL
• scientific article; zbMATH DE number 2038753
• On the Hybrid Extension of CTL and CTL +
• CTL^* and ECTL^* as fragments of the modal -calculus
• An n! lower bound on formula size

Cited in

(28)

• Branching-time logics repeatedly referring to states
• CTL^* and ECTL^* as fragments of the modal -calculus
• From bidirectionality to alternation.
• On the expressivity and complexity of quantitative branching-time temporal logics
• On temporal logic versus Datalog
• Strategic reasoning with a bounded number of resources: the quest for tractability
• Model-checking graded computation-tree logic with finite path semantics
• To be fair, use bundles
• \(\text{BTL}_{2}\) and the expressive power of \(\text{ECTL}^{+}\)
• ATL* Satisfiability Is 2EXPTIME-Complete
• An automata-theoretic approach to infinite-state systems
• Branching-Time Temporal Logics with Minimal Model Quantifiers
• Branching-time logics with path relativisation
• Improved model checking of hierarchical systems
• \textit{Once} and \textit{for all}
• A decidable timeout-based extension of linear temporal logic
• Comparing the succinctness of monadic query languages over finite trees
• Refinement modal logic
• On the Way to Alternating Weak Automata
• Register games
• On the succinctness of atoms of dependency
• An n! lower bound on formula size
• The Complexity of CTL* + Linear Past
• A modal logic framework for reasoning about comparative distances and topology
• Modal logic is more succinct iff bi-implication is available in some form
• Boolean basis, formula size, and number of modal operators
• Arbitrary-arity tree automata for QCTL
• A purely model-theoretic proof of the exponential succinctness gap between CTL\(^{+}\) and CTL

This page was built for publication: CTL\(^+\) is exponentially more succinct than CTL

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