Formal analysis of Piecewise Affine systems under parameter uncertainty with application to gene networks

In this paper, we consider discrete-time continuous-space piecewise affine (PWA) systems with uncertain parameters, and study temporal logic properties of their trajectories. Specifically, given a PWA system with polyhedral parameter uncertainties 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 the iterative computation and model checking of finite transition systems simulating the original PWA system. We illustrate our method by computing the basins of attraction for the two equilibria of a PWA model of a two-gene network.