A purely model-theoretic proof of the exponential succinctness gap between CTL\(^{+}\) and CTL

DOI10.1016/J.IPL.2008.06.003zbMath1191.68412OpenAlexW2001959058MaRDI QIDQ975478

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)

Related Items (3)

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

Cites Work

• Unnamed Item
• Unnamed Item
• Decision procedures and expressiveness in the temporal logic of branching time
• An n  ! lower bound on formula size

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