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

DOI10.1016/J.IPL.2008.06.003MaRDI QIDQ975478zbMATH OpenOpenAlexFDO

Authors 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

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)

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

Cites work

• scientific article; zbMATH DE number 2038753 (Why is no real title available?)
• scientific article; zbMATH DE number 1500644 (Why is no real title available?)
• An \(n!\) lower bound on formula size
• Decision procedures and expressiveness in the temporal logic of branching time

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)