Modularity for timed and hybrid systems Conference Paper

Author(s): Alur, Rajeev; Henzinger, Thomas A
Title: Modularity for timed and hybrid systems
Title Series: LNCS
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.
Conference Title: CONCUR: Concurrency Theory
Volume: 1243
Conference Dates: July 1–4, 1997
Conference Location: Warsaw, Poland
ISBN: 978-3-95977-017-0
Publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik  
Date Published: 1997-01-01
Start Page: 74
End Page: 88
DOI: 10.1007/3-540-63141-0_6
Notes: This research was supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA grant NAG2-892, and by the SRC contract 95-DC-324.036.
Open access: no
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
Related IST Austria Work