Abstract
We propose a bounded model checking (BMC) method for the verification of multi-agent systems' (MASs). The MASs are modelled by deontic interleaved interpreted systems, and specifications are expressed in the logic . The verification approach is based on the state of the art solutions to BMC, one of the mainstream approaches in verification of reactive systems. We test our results on a typical communication scenario: train controller problem with faults. © 2012 Springer-Verlag.
Cite
CITATION STYLE
Woźna-Szcześniak, B., & Zbrzezny, A. (2012). SAT-based bounded model checking for deontic interleaved interpreted systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7327 LNAI, pp. 494–503). https://doi.org/10.1007/978-3-642-30947-2_54
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
