DocumentCode
1310234
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
Volume
55
Issue
12
fYear
2010
Firstpage
2834
Lastpage
2840
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;
fLanguage
English
Journal_Title
Automatic Control, IEEE Transactions on
Publisher
ieee
ISSN
0018-9286
Type
jour
DOI
10.1109/TAC.2010.2072530
Filename
5560749
Link To Document