Bounded model checking for knowledge and real time

DOI10.1016/j.artint.2007.05.005zbMath1168.68422OpenAlexW1971809028MaRDI QIDQ1028970

Alessio Lomuscio, Bożena Woźna, Wojciech Penczek

Publication date: 9 July 2009

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.artint.2007.05.005

zbMATH Keywords

model checkinginterpreted systemsreal time systemstemporal epistemic logics

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams ⋮ Checking EMTLK properties of timed interpreted systems via bounded model checking ⋮ Model checking and strategy synthesis for multi-agent systems for resource allocation ⋮ Combined model checking for temporal, probabilistic, and real-time logics ⋮ Bounded semantics ⋮ A Complete Quantified Epistemic Logic for Reasoning about Message Passing Systems ⋮ Parameterised verification for multi-agent systems

Uses Software

• VerICS
• MCK

Cites Work

• Model-checking in dense real-time
• A guide to completeness and complexity for modal logics of knowledge and belief
• Deontic interpreted systems
• Complete axiomatizations for reasoning about knowledge and branching time
• Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications
• Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams
• What can machines know?
• Applications of a logic of knowledge to motion planning under uncertainty
• Complete Axiomatizations for Reasoning about Knowledge and Time
• Computer Aided Verification
• Knowledge, timed precedence and clocks (preliminary report)
• Towards Bounded Model Checking for the Universal Fragment of TCTL
• Computational Logic in Multi-Agent Systems
• Analysis of timed systems using time-abstracting bisimulations
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Bounded model checking for knowledge and real time