Theory of hybrid systems and discrete event systems
Anuj Puri · 1996
A continuous system has a continuous state space and an evolution law given by a differential or a difference equation. A discrete event system is modeled by an automaton which changes state in response to events. A hybrid system contains both continuous and discrete event sub-systems. In this thesis we study some theoretical problems in the design and analysis of hybrid systems and discrete event systems. We first consider the reachability question for a hybrid system--is a target state reachable from an initial state? We show that for hybrid automata with rectangular inclusions, the reachability question can be answered in a finite number of steps. Hybrid systems with more general dynamics can be reduced to hybrid systems with rectangular inclusions using abstractions. We next consider an Automated Vehicle Highway System (AVHS) design. We consider the safety question: can there be a collision between two vehicles on the AVHS? We show that the AVHS is safe provided the controllers in the vehicles satisfy a set of constraints. The constraints require the reach set $Reach\sb{f}(X\sb0,t$)--the set of states reached after time t starting from an initial set $X\sb0$ for a differential inclusion $\dot x \in f(x$)--to satisfy a simple criterion. We show that this problem is equivalent to solving an optimal control problem. We then consider some computational questions for differential inclusions. For a Lipschitz differential inclusion $\dot x \in f(x$), we give a method to compute an arbitrary close approximation of $Reach\sb{f}(X\sb0,t$). For a differential inclusion $\dot x \in f(x$), and any $\epsilon>$ 0, we define a finite sample graph $A\sp{\epsilon}$. Using graph $A\sp{\epsilon}$, we can compute the $\epsilon$-invariant sets of the differential inclusion--the sets that remain invariant under $\epsilon$-perturbations in f. We also consider some dynamical games played on graphs. The synthesis and the control problem for $\omega$-automata can be formulated as a game between two players. We discuss games on $\omega$-automata and the payoff games. We show that $\omega$-automata games do not necessarily have a value when restricted to positional strategies. We exhibit a bound on the amount of memory required to play these games. We then consider the discounted and mean payoff games. We present the successive approximation and the policy iteration algorithm for solving payoff games. We then show that an $\omega$-automata game with the chain acceptance condition can be solved as a mean payoff game. Solving a chain game is equivalent to solving the model checking problem for propositional $\mu$-calculus. Hence, the policy iteration method can be used to model check $\mu$-calculus formula. This is at present the most efficient algorithm for model checking propositional $\mu$-calculus.