In this paper, we consider discrete-time continuous-space Piecewise Affine (PWA) systems with parameter uncertainties, and study temporal logic properties of their trajectories. Specifically, given a PWA system with polytopal parameter uncertainties, and a Linear Temporal Logic (LTL) formula over linear predicates in the states of the system, we attempt to find subsets of parameters guaranteeing the satisfaction of the formula by all trajectories of the system. We illustrate our method by applying it to a PWA model of a two-gene network.
展开▼
