A purely model-theoretic proof of the exponential succinctness gap between CTL^+ and CTL

DOI10.1016/J.IPL.2008.06.003zbMATH Open1191.68412OpenAlexW2001959058MaRDI QIDQ975478FDOQ975478

Martin Lange

Publication date: 9 June 2010

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ipl.2008.06.003

Recommendations

• A finite-model-theoretic view on propositional proof complexity
• The complexity of satisfiability for fragments of CTL and \(\text{CTL}^*\)
• An asymptotically tight bound on countermodels for Łukasiewicz logic
• Some exponential lower bounds on formula-size in modal logic
• Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models
• On the gap between \(\mathit{ess}(f)\) and \(\mathit{cnf}_{-}\mathit{size}(f)\)
• A model theoretic proof of a subexponential time witnessing theorem
• On the absence of finite approximation relative to model completeness in propositional provability logic
• On the computability-theoretic complexity of trivial, strongly minimal models
• On absence of finite approximation relative to model completeness in the propositional provability logic

zbMATH Keywords

specification languagestemporal logicssmall model property

Mathematics Subject Classification ID

Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Decision procedures and expressiveness in the temporal logic of branching time
• An n  ! lower bound on formula size
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (3)

• On regular temporal logics with past
• On the Hybrid Extension of CTL and CTL +
• Branching-time logics with path relativisation

This page was built for publication: A purely model-theoretic proof of the exponential succinctness gap between CTL\(^{+}\) and CTL

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