Abstract
We consider multi-agent systems' (MASs) modelled by deontic interleaved interpreted systems and we provide a new SAT-based bounded model checking (BMC) method for these systems. The properties of MASs are expressed by means of the metric temporal logic with discrete semantics and extended to include epistemic and deontic operators. The proposed BMC approach is based on the state of the art solutions to BMC. We test our results on a typical MASs scenario: train controller problem with faults. © Springer-Verlag Berlin Heidelberg 2013.
Cite
CITATION STYLE
Woźna-Szcześniak, B., & Zbrzezny, A. (2013). SAT-based BMC for deontic metric temporal logic and deontic interleaved interpreted systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7784 LNAI, pp. 170–189). https://doi.org/10.1007/978-3-642-37890-4_10
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
