Timed I/O Automata: A Mathematical Framework for Modeling and Analyzing Real-Time Systems

We describe the Timed Input/Output Automata (TIOA) framework, a general mathematical framework for modeling and analyzing real-time systems. It is based on timed I/O automata, which engage in both discrete transitions and continuous trajectories. The framework includes a notion of external behavior, and notions of composition and abstraction. We define safety and liveness properties for timed I/O automata, and a notion of receptiveness, and prove basic results about all of these notions. The TIOA framework is defined as a special case of the new Hybrid I/O Automata (HIOA) modeling framework for hybrid systems. Specifically, a TIOA is an HIOA with no external variables; thus, TIOAs communicate via shared discrete actions only, and do not interact continuously. This restriction is consistent with previous real-time system models, and gives rise to some simplifications in the theory (compared to HIOA). The resulting model is expressive enough to describe complex timing behavior, and ...

• Type: Conference
• Year: 2003
• Where: RTSS
• Authors: Dilsun Kirli Kaynar, Nancy A. Lynch, Roberto Segala, Frits W. Vaandrager
• Keywords: Applied Computing, Hybrid I/O Automata, RTSS 2003, Timed I/O Automata, Timed Input/Output Automata