Advertisement
Published in:
2011 | OriginalPaper | Chapter
The BMC Method for the Existential Part of RTCTLK and Interleaved Interpreted Systems
Authors : Bożena Woźna-Szcześniak, Agnieszka Zbrzezny, Andrzej Zbrzezny
Published in: Progress in Artificial Intelligence
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
In the paper, we focus on the formal verification of multi-agent systems – modelled by interleaved interpreted systems – by means of the bounded model checking (BMC) method, where specifications are expressed in the existential fragment of the Real-Time Computation Tree Logic augmented to include standard epistemic operators (
Rtectlk
). In particular, we define an improved SAT-based BMC for
Rtectlk
, and present performance evaluation of our newly developed BMC method by means of the well known train controller and generic pipeline systems.