Sciweavers

CONCUR
1997
Springer

Modularity for Timed and Hybrid Systems

13 years 7 months ago
Modularity for Timed and Hybrid Systems
Abstract. In a trace-based world, the modular speci cation, veri cation, and control of live systems require each module to be receptive that is, each module must be able to meet its liveness assumptions no matter how the other modules behave. In a real-time world, liveness is automatically present in the form of diverging time. The receptiveness condition, then, translates to the requirement that a module must be able to let time diverge no matter how the environment behaves. We study the receptiveness condition for real-time systems by extending the model of reactive modules to timed and hybrid modules. We de ne the receptiveness of such a module as the existence of a winning strategy in a game of the module against its environment. By solving the game on region graphs, we present an (optimal) Exptime algorithm for checking the receptiveness of propositional timed modules. By giving a xpoint characterization of the game, we present a symbolic procedure for checking the receptiveness ...
Rajeev Alur, Thomas A. Henzinger
Added 07 Aug 2010
Updated 07 Aug 2010
Type Conference
Year 1997
Where CONCUR
Authors Rajeev Alur, Thomas A. Henzinger
Comments (0)