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 ...

• Type: Conference
• Year: 1997
• Where: CONCUR
• Authors: Rajeev Alur, Thomas A. Henzinger
• Keywords: CONCUR 1997, Distributed And Parallel Computing, Hybrid Modules, Modular Speci Cation, Receptiveness Condition