tailieunhanh - Model-Based Design for Embedded Systems- P art 15

Model-Based Design for Embedded Systems- P15:The unparalleled flexibility of computation has been a key driver and feature bonanza in the development of a wide range of products across a broad and diverse spectrum of applications such as in the automotive aerospace, health care, consumer electronics, etc. | 396 Model-Based Design for Embedded Systems FIGURE A Buchi-automaton monitor for checking an unbounded-response property. on the other hand the monitor moves to state 2 which is nonaccepting. If no execution is accepting the property is satisfied. TBA emptiness can be checked in theory on the region graph interpreted as a finite untimed Buchi automaton. In practice the time-abstract quotient graph or the zone graph can be used instead. The former can be easily shown to preserve liveness properties 106 . The fact that the zone graph can be used to check TBA emptiness is nontrivial and has been completely proven only recently 101 . Verification of Hybrid Automata Timed automata are a very special class of hybrid automata. The decidability results for timed automata were generalized to some slightly more complex classes such as multirate automata 6 80 and initialized rectangular automata 89 . In multirate automata the derivatives of the continuous variables can take constant values other than 1. In rectangular automata the derivatives are not constant and an allowed to take any value inside some interval. Decidability was also proved for some particular planar systems including 2-dimensional piecewise constant derivatives PCD 76 planar multipolynomial systems 26 and nondeterministic planar polygonal systems 14 . Despite these extensions however the reachability problem for general hybrid automata is undecidable. In fact this holds even for classes of systems with constant derivatives such as linear hybrid automata with three or more continuous variables 47 . Let us illustrate some of the issues that arise in hybrid automata reachability. We will focus only on the problem of computing the reachable sets of hybrid automata where continuous dynamics are defined by nontrivial differential equations. A major difficulty comes with the two-phase evolution of these systems which requires the ability to compute the successors or predecessors of sets of states not .