Title :
Formal Analysis of Discrete-Time Piecewise Affine Systems
Author :
Yordanov, Boyan ; Belta, Calin
Author_Institution :
Dept. of Biomed. Eng., Boston Univ., Boston, MA, USA
Abstract :
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.
Keywords :
discrete time systems; formal verification; iterative methods; temporal logic; PWA system; discrete-time piecewise affine systems; finite quotients; formal analysis; iterative computation; linear temporal logic formula; model checking; synthetic gene networks; Analytical models; Computational modeling; Construction industry; Genetic programming; Integrated circuit modeling; Trajectory; Abstraction; formal analysis; genetic networks; model checking; piecewise affine (PWA) systems; uncertain systems;
Journal_Title :
Automatic Control, IEEE Transactions on
DOI :
10.1109/TAC.2010.2072530
