Simple SMT-Based Bounded Model Checking for Timed Interpreted Systems

摘要

The paper deals with symbolic approach to bounded model checking (BMC) for metric temporal logic with epistemic operators (MTLK) that is interpreted over timed interpreted systems (TIS). We present an SMT-based BMC method based on the translation of MTLK formulae to LTL_qK formulae. We show how to implement the bounded model checking technique for LTL_qK logic and timed interpreted systems, and we present full translation to SMT problem for LTL_qK. 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.