| Autor: | Anuj Puri |
|---|---|
| Rok vydání: | 2000 |
| Předmět: |
Discrete mathematics
Correctness Dynamical systems theory Mathematics::Complex Variables Computer science Reachability problem Timed automaton Automaton Set (abstract data type) Control and Systems Engineering Reachability Modeling and Simulation Limit (mathematics) Electrical and Electronic Engineering Computer Science::Formal Languages and Automata Theory |
| Zdroj: | Discrete Event Dynamic Systems. 10:87-113 |
| ISSN: | 0924-6703 |
| DOI: | 10.1023/a:1008387132377 |
| Popis: | Timed automata are an important model for specifying and analyzing real-time systems. The main analysis performed on timed automata is the reachability analysis. In this paper we show that the standard approach for performing reachability analysis is not correct when the clocks drift even by a very small amount. Our formulation of the reachability problem for timed automata is as follows: we define the set R^*(T,Z_0)=\cap_{\eps>0}\reach(T_\eps,Z_0) where T_\eps is obtained from timed automaton T by allowing an \eps drift in the clocks. R^*(T,Z_0) is the set of states which can be reached in the timed automatonT from the initial states in Z_0 when the clocks drift by an infinitesimally small amount. We present an algorithm for computing R^*(T,Z_0) and provide a proof of its correctness. We show that R^*(T,Z_0) is robust with respect to various types of modeling errors. To prove the correctness of our algorithm, we need to understand the dynamics of timed automata—in particular, the structure of the limit cycles of timed automata. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink