Approximating Event System Abstractions by Covering their States and Transitions

Jacques Julliand (1) , Olga Kouchnarenko (2) , Pierre-Alain Masson (3) , Guillaume Voiron (1)

1 FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174)
2 CASSIS - Combination of approaches to the security of infinite states systems
3 UTHealth - The University of Texas Health Science Center at Houston

In event systems, contrarily to sequential ones, the control flow is implicit. Consequently, their abstraction may give rise to disconnected and unreachable paths. This paper presents an algorithmic method for computing a reachable and connected under-approximation of the abstraction of a system specified as an event system. We compute the under-approximation with concrete instances of the abstract transitions, that cover all the states and transitions of the predicate-based abstraction. To be of interest, these concrete transitions have to be reachable and connected to each other. We propose an algorithmic method that instantiates each of the abstract transitions, with heuristics to favour their connectivity. The idea is to prolong whenever possible the already reached sequences of concrete transitions, and to parameterize the order in which the states and actions occur. The paper also reports on an implementation, which permits to provide experimental results confirming the interest of the approach with related heuristics.

Mots clés: Predicate abstraction; under-approximation; event systems

Domaines: Informatique et langage [cs.CL]

Jacques Julliand, Olga Kouchnarenko, Pierre-Alain Masson, Guillaume Voiron. Approximating Event System Abstractions by Covering their States and Transitions: Version 1. [Research Report] RR–FEMTO-ST–2496, FEMTO-ST. 2017. ⟨hal-01496470⟩