@inproceedings{4583,
  abstract     = {In a trace-based world, the modular specification, verification, 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 define 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 prepositional timed modules. By giving a fixpoint characterization of the game, we present a symbolic procedure for checking the receptiveness of linear hybrid modules. Finally, we present an assume-guarantee principle for reasoning about timed and hybrid modules, and a method for synthesizing receptive controllers of timed and hybrid modules.},
  author       = {Alur, Rajeev and Henzinger, Thomas A},
  booktitle    = {8th International Conference on Concurrency Theory},
  isbn         = {9783540691884},
  location     = {Warsaw, Poland},
  pages        = {74 -- 88},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Modularity for timed and hybrid systems}},
  doi          = {10.1007/3-540-63141-0_6},
  volume       = {1243},
  year         = {1997},
}