---
res:
  bibo_abstract:
  - Rectangular hybrid automata model digital control programs of analog plant environments.
    We study rectangular hybrid automata where the plant state evolves continuously
    in real-numbered time, and the controller samples the plant state and changes
    the control state discretely, only at the integer points in time. We prove that
    rectangular hybrid automata have finite bisimilarity quotients when all control
    transitions happen at integer times, even if the constraints on the derivatives
    of the variables vary between control states. This is sharply in contrast with
    the conventional model where control transitions may happen at any real time,
    and already the reachability problem is undecidable. Based on the finite bisimilarity
    quotients, we give an exponential algorithm for the symbolic sampling-controller
    synthesis of rectangular automata. We show our algorithm to be optimal by proving
    the problem to be EXPTIME-hard. We also show that rectangular automata form a
    maximal class of systems for which the sampling-controller synthesis problem can
    be solved algorithmically.@eng
  bibo_authorlist:
  - 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
  - foaf_Person:
      foaf_givenName: Peter
      foaf_name: Kopke, Peter
      foaf_surname: Kopke
  bibo_doi: 10.1007/3-540-63165-8_213
  bibo_volume: 1256
  dct_date: 1997^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/9783540631651
  dct_language: eng
  dct_publisher: Springer@
  dct_title: Discrete-time control for rectangular hybrid automata@
...