Bounded model checking for knowledge and real time

DOI10.1016/J.ARTINT.2007.05.005MaRDI QIDQ1028970zbMATH OpenOpenAlexFDO

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

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

interpreted systemsmodel checkingreal time systemstemporal epistemic logics

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1973987
• Completeness of bounded model checking temporal logic of knowledge
• Bounded model checking for timed automata
• On Expressiveness and Complexity in Real-Time Model Checking
• Model-checking in dense real-time
• scientific article; zbMATH DE number 2087624
• Bounded model checking for temporal epistemic logic in synchronous multi-agent systems
• Bounded Model Checking for Parametric Timed Automata

Cites work

• A guide to completeness and complexity for modal logics of knowledge and belief
• Analysis of timed systems using time-abstracting bisimulations
• Applications of a logic of knowledge to motion planning under uncertainty
• Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams
• Bounded model checking for deontic interpreted systems
• Complete axiomatizations for reasoning about knowledge and branching time
• Complete Axiomatizations for Reasoning about Knowledge and Time
• Computational Logic in Multi-Agent Systems
• Computer Aided Verification
• Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications
• Deontic interpreted systems
• scientific article; zbMATH DE number 1799521 (Why is no real title available?)
• scientific article; zbMATH DE number 177824 (Why is no real title available?)
• scientific article; zbMATH DE number 1973987 (Why is no real title available?)
• scientific article; zbMATH DE number 2064229 (Why is no real title available?)
• scientific article; zbMATH DE number 1500666 (Why is no real title available?)
• scientific article; zbMATH DE number 2140441 (Why is no real title available?)
• scientific article; zbMATH DE number 2087624 (Why is no real title available?)
• scientific article; zbMATH DE number 2104641 (Why is no real title available?)
• scientific article; zbMATH DE number 795590 (Why is no real title available?)
• Knowledge, timed precedence and clocks (preliminary report)
• Modal logic
• Model-checking in dense real-time
• Towards Bounded Model Checking for the Universal Fragment of TCTL
• What can machines know?

Cited in

(13)

• Model checking and strategy synthesis for multi-agent systems for resource allocation
• Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams
• Parameterised verification for multi-agent systems
• SAT-based bounded model checking for weighted deontic interpreted systems
• Checking EMTLK properties of timed interpreted systems via bounded model checking
• A Complete Quantified Epistemic Logic for Reasoning about Message Passing Systems
• Combined model checking for temporal, probabilistic, and real-time logics
• Verifying real-time properties of multi-agent systems via SMT-based bounded model checking
• Bounded semantics
• Bounded Model Checking Real-Time Multi-agent Systems with Clock Differences: Theory and Implementation
• scientific article; zbMATH DE number 5051662 (Why is no real title available?)
• VERICS 2007 -- a model checker for knowledgee and real-time
• Computational Logic in Multi-Agent Systems

Describes a project that uses

Uses Software

• VerICS
• MCK

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

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