Model checking for hybrid logic

DOI10.1007/s10849-009-9088-7zbMath1193.03053MaRDI QIDQ1047796

Martin Lange

Publication date: 6 January 2010

Published in: Journal of Logic, Language and Information (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10849-009-9088-7

zbMATH Keywords

Büchi games; local model checking

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

03B62: Combined logics

Related Items

Model checking for hybrid branching-time logics, The expressibility of fragments of hybrid graph logic on finite digraphs, Hybrid Specification of Reactive Systems: An Institutional Approach

Uses Software

• CESAR

Cites Work

• An essay in combinatory dynamic logic
• Using branching time temporal logic to synthesize synchronization skeletons
• Tableau-based model checking in the propositional mu-calculus
• Local model checking in the modal mu-calculus
• Symbolic model checking: \(10^{20}\) states and beyond
• Hybridizing concept languages
• Model checking and boolean graphs
• A linear-time model-checking algorithm for the alternation-free modal mu- calculus
• Hierarchies of modal and temporal logics with reference pointers
• Model checking hybrid logics (with an application to semistructured data)
• A lattice-theoretical fixpoint theorem and its applications
• Interpolation for extended modal languages
• A first step towardsmodeling semistructured data in hybrid multimodal logic
• The computational complexity of hybrid temporal logics
• An approach to tense logic¹
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item