화학공학소재연구정보센터
IEEE Transactions on Automatic Control, Vol.55, No.12, 2834-2840, 2010
Formal Analysis of Discrete-Time Piecewise Affine Systems
In this technical note, we study temporal logic properties of trajectories of discrete-time piecewise affine (PWA) systems. Specifically, given a PWA system and a linear temporal logic formula over regions in its state space, 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 quotients. We illustrate our method by analyzing PWA models of two synthetic gene networks.