---
res:
  bibo_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.@eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Rajeev
      foaf_name: Alur, Rajeev
      foaf_surname: Alur
  - foaf_Person:
      foaf_givenName: Thomas A
      foaf_name: Henzinger, Thomas A
      foaf_surname: Henzinger
      foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
    orcid: 0000−0002−2985−7724
  bibo_doi: 10.1007/3-540-63141-0_6
  bibo_volume: 1243
  dct_date: 1997^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/9783540691884
  dct_language: eng
  dct_publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik@
  dct_title: Modularity for timed and hybrid systems@
...