Practical Abstractions for Model Checking Continuous-Time Multi-Agent Systems

Much work has been done to contain the state-space explosion by smart representation and/or reduction of input models. Symbolic Model checking of temporal logics in a well established technique model checking based on SATor BDD-based representations to verify and validate properties of multi-agent systems (MAS). of the state/transition space [36, 42, 44, 45, 47, 48, 50] fall into the However, practical model checking requires input models of manageable former group. Model reduction methods include partial-order reduction size. In this paper, we extend the model reduction method [28, 41, 49], equivalence-based reductions [2, 6, 25], and by variable-based abstraction, proposed recently by Jamroga and state abstraction [21], see below for a detailed discussion.