Property-Dependent Reductions for the Modal Mu-Calculus

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 (Lmu). First, we determine, for any Lmu formula, the maximal set of actions that can be hidden in the LTS without changing the interpretation of the formula. Then, we define dsbrLmu, a fragment of Lmu 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 dsbrLmu 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.Lorsqu'on analyse le comportement des systèmes concurrents à espace d'états fini par model checking, une manière de lutter contre l'explosion d'états est de réduire le modèle le plus possible tout en préservant les propriétés à vérifier. Nous considérons le cadre des systèmes basés sur actions, dont les comportements peuvent être représentés par des systèmes de transitions étiquetées (STEs), et dont les propriétés temporelles d'intérêt peuvent être formulées en mu-calcul modal (Lmu). D'abord, nous déterminons, pour toute formule de Lmu, l'ensemble maximal des actions qui peuvent être masquées dans le STE sans changer l'interprétation de la formule. Ensuite, nous définissons dsbrLmu, un fragment de Lmu qui est compatible avec la bisimulation de branchement sensible à la divergence. Ceci permet d'appliquer le masquage maximal et de réduire le STE à la volée en utilisant la tau-confluence sensible à la divergence pendant la vérification de la formule dsbrLmu. Les expériences que nous avons effectuées sur différents exemples de protocoles de communication et de systèmes distribués montrent que cette approche de réduction peut améliorer de manière significative les performances de la vérification à la volée