Combined model checking for temporal, probabilistic, and real-time logics

• DOI: 10.1016/j.tcs.2013.07.012
• Publication Date: 2013-07-25T16:33:48Z
• Authors: Savas Konur; Michael Fisher; Sven Schewe
• Keywords: Abstraction model checking

Model checking is a well-established technique for the formal verification of concurrent and distributed systems. In recent years, model has been extended adapted multi-agent systems, primarily to enable analysis belief–desire–intention While this successful, there need more complex logical frameworks in order verify realistic particular, probabilistic real-time aspects, as well knowledge, belief, goals, etc., are required. However, development new tools combinations logics both difficult time consuming. article, we show how checkers constituent temporal, probabilistic, can be re-used modular way when consider combined involving different dimensions. This avoids re-implementation procedures. We define approach, prove its correctness, establish complexity, it used describe existing approaches yet-unimplemented combinations. also demonstrate feasibility our approach on case study.