05940627

a

05940627 Mateescu, Radu Wijs, Anton Property-dependent reductions for the modal mu-calculus. Groce, Alex (ed.) et al., Model checking software. 18th international SPIN workshop, Snowbird, UT, USA, July 14--15, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22305-1/pbk). Lecture Notes in Computer Science 6823, 2-19 (2011). 2011 Berlin: Springer EN

doi:10.1007/978-3-642-22306-8_2

Summary: When analyzing the behavior of finite-state concurrent systems by model checking, one way of fighting state explosion is to reduce the model as much as possible whilst preserving the properties under verification. We consider the framework of action-based systems, whose behaviors can be represented by labeled transition systems (Ltss), and whose temporal properties of interest can be formulated in modal $\mu $-calculus ($L _{\mu })$. First, we determine, for any $L _{\mu }$ formula, the maximal set of actions that can be hidden in the Lts without changing the interpretation of the formula. Then, we define $L _{\mu } ^{\text{dsbr}}$, a fragment of $L _{\mu }$ which is compatible with divergence-sensitive branching bisimulation. This enables us to apply the maximal hiding and to reduce the Lts on-the-fly using divergence-sensitive $\tau $-confluence during the verification of any $L _{\mu } ^{\text{dsbr} }$ formula. The experiments that we performed on various examples of communication protocols and distributed systems show that this reduction approach can significantly improve the performance of on-the-fly verification.