Under-approximating Cut Sets for Reachability in Large Scale Automata Networks

Loïc Paulevé (1) , Geoffroy Andrieux (2) , Heinz Koeppl (3)

1 IFA - Institut für Automatik - Automatic Control Laboratory
2 Dyliss - Dynamics, Logics and Inference for biological Systems and Sequences
3 BISON

In the scope of discrete finite-state models of interacting components, and calling the local state of a component a process, we present an algorithm for extracting sets of processes that are necessary for achieving the reachability of a given process. Those sets are referred to as cut sets and are computed from a particular abstract causality structure, so-called Graph of Local Causality, inspired from previous work and generalised here to Communicating Finite State Machines. We apply this new method to a very large model of biological interactions, providing sets of biological entities that, if de-activated, prevent molecules of interest to be active, up to the correctness of the model.

Domaines: Théorie et langage formel [cs.FL]

Loïc Paulevé, Geoffroy Andrieux, Heinz Koeppl. Under-approximating Cut Sets for Reachability in Large Scale Automata Networks. 2012. ⟨hal-00769447v1⟩