Anzeige
Erschienen in:
2017 | OriginalPaper | Buchkapitel
Simple Bounded MTLK Model Checking for Timed Interpreted Systems
verfasst von : Agnieszka M. Zbrzezny, Andrzej Zbrzezny
Erschienen in: Agent and Multi-Agent Systems: Technology and Applications
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Abstract
We present a new translation of Metric Temporal Logic with knowledge operators (MTLK) to the Linear Temporal Logic with knowledge operators and with a new set of the atomic propositions (\({\mathrm{{\mathrm{{LTL}}}}_\mathrm{q}\mathrm {K}}\)). We investigate a SAT-based bounded model checking (BMC) method for MTLK. The semantics of MTLK is defined over timed interpreted systems (TIS). We show how to implement the bounded model checking technique for \({\mathrm{{\mathrm{{LTL}}}}_\mathrm{q}\mathrm {K}}\) and timed interpreted systems, and as a case study, we apply the technique in the analysis of the Timed Generic Pipeline Paradigm modelled by TIS. We also present the differences between the old translation of MTLK and the new one. The theoretical description is supported by the experimental results that demonstrate the efficiency of the method.