Branching-time logics with path relativisation

DOI10.1016/J.JCSS.2013.05.005MaRDI QIDQ386037zbMATH OpenOpenAlexFDO

Authors Markus Latte, Martin Lange

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 checkingsatisfiabilitytemporal logicexpressivity\(\omega\)-languagesbranching-time logicrelativized quantifiers

Mathematics Subject Classification ID

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

Recommendations

• Extended computation tree logic
• An infinite hierarchy of temporal logics over branching time
• scientific article; zbMATH DE number 4119600
• scientific article; zbMATH DE number 1759449
• Decision procedures and expressiveness in the temporal logic of branching time

Cites work

• scientific article; zbMATH DE number 1705163 (Why is no real title available?)
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 3983144 (Why is no real title available?)
• scientific article; zbMATH DE number 3664335 (Why is no real title available?)
• scientific article; zbMATH DE number 1048047 (Why is no real title available?)
• scientific article; zbMATH DE number 2038753 (Why is no real title available?)
• scientific article; zbMATH DE number 1500644 (Why is no real title available?)
• scientific article; zbMATH DE number 941396 (Why is no real title available?)
• scientific article; zbMATH DE number 3237829 (Why is no real title available?)
• 25 years of model checking. History, achievements, perspectives
• A CTL-based logic for program abstractions
• A decision procedure for \(\mathrm{CTL}^{*}\) based on tableaux and automata
• A purely model-theoretic proof of the exponential succinctness gap between CTL\(^{+}\) and CTL
• Computation Tree Regular Logic for Genetic Regulatory Networks
• Counterexample-guided abstraction refinement for symbolic model checking
• Decision procedures and expressiveness in the temporal logic of branching time
• Extended computation tree logic
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Foundations of Software Science and Computation Structures
• Games for synthesis of controllers with partial observation.
• Model Checking Software
• Model checking of RegCTL
• Model-checking in dense real-time
• Propositional dynamic logic of looping and converse is elementarily decidable
• Propositional dynamic logic of nonregular programs
• Propositional dynamic logic of regular programs
• Propositional dynamic logic with recursive programs
• Pushdown processes: Games and model-checking
• Reachability analysis of pushdown automata: Application to model-checking
• Reasoning about infinite computations
• The Complexity of Tree Automata and Logics of Programs
• The complexity of propositional linear temporal logics
• Visibly pushdown languages
• “Sometimes” and “not never” revisited

Cited in

(9)

• Branching-time logics repeatedly referring to states
• A branching time logic with past operators
• \(R\)-generability, and definability in branching time logics
• scientific article; zbMATH DE number 4119600 (Why is no real title available?)
• Finite and Circular Path Models for Branching Time Logics
• A Branching Time Variant of CaRet
• Temporal logics with language parameters
• Extended computation tree logic
• Sublogics of a branching time logic of robustness

This page was built for publication: Branching-time logics with path relativisation

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