Branching-time logics with path relativisation

DOI10.1016/j.jcss.2013.05.005zbMath1297.68170OpenAlexW2148033627MaRDI QIDQ386037

Martin Lange, Markus Latte

Publication date: 13 December 2013

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jcss.2013.05.005

zbMATH Keywords

computational complexitymodel checkingtemporal logicsatisfiabilityexpressivity\(\omega\)-languagesbranching-time logicrelativized quantifiers

Mathematics Subject Classification ID

Logic in computer science (03B70) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Complexity of computation (including implicit computational complexity) (03D15) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Related Items

Temporal logics with language parameters

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Model-checking in dense real-time
• Propositional dynamic logic of nonregular programs
• 25 years of model checking. History, achievements, perspectives
• A purely model-theoretic proof of the exponential succinctness gap between CTL\(^{+}\) and CTL
• Propositional dynamic logic of regular programs
• Reasoning about infinite computations
• Games for synthesis of controllers with partial observation.
• Pushdown processes: Games and model-checking
• Decision procedures and expressiveness in the temporal logic of branching time
• Propositional dynamic logic with recursive programs
• Counterexample-guided abstraction refinement for symbolic model checking
• Computation Tree Regular Logic for Genetic Regulatory Networks
• Visibly pushdown languages
• Propositional dynamic logic of looping and converse is elementarily decidable
• “Sometimes” and “not never” revisited
• The complexity of propositional linear temporal logics
• The Complexity of Tree Automata and Logics of Programs
• A CTL-Based Logic for Program Abstractions
• Extended Computation Tree Logic
• Model Checking Software
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• A Decision Procedure for CTL* Based on Tableaux and Automata
• Foundations of Software Science and Computation Structures
• Reachability analysis of pushdown automata: Application to model-checking