scientific article; zbMATH DE number 1500644

MaRDI QIDQ4501666zbMATH OpenFDO

Authors Thomas Wilke

Publication date 7 November 2000

zbMATH Keywords

computation tree logicexpressivenesssuccinctnessmodal \(\mu\)-calculusalternating tree automatonlengths of formulas

Mathematics Subject Classification ID

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

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

(24)

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

This page was built for publication:

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