Model checking discrete-time Piecewise Affine systems: Application to gene networks

In this paper, we focus on discrete-time continuous-space Piecewise Affine (PWA) systems, and study properties of their trajectories expressed as temporal and logical statements over polyhedral regions. Specifically, given a PWA system and a Linear Temporal Logic (LTL) formula over linear predicates in its state variables, we attempt to find the largest region of initial states from which all trajectories of the system satisfy the formula. Our method is based on a classical algorithm for the iterative computation of simulation quotients augmented with model checking. We show that the determinism inherent in the problem and the particular linear structure of the invariants and of the dynamics can be exploited in a computationally attractive algorithm. We illustrate the application of our method to the computation of basins of attraction for the two equilibria of a PWA model of a two-gene network.