[{"oa_version":"None","month":"01","publication":"8th International Conference on Concurrency Theory","conference":{"name":"CONCUR: Concurrency Theory","start_date":"1997-07-01","end_date":"1997-07-04","location":"Warsaw, Poland"},"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["9783540691884"]},"publist_id":"124","date_published":"1997-01-01T00:00:00Z","type":"conference","status":"public","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication_status":"published","article_processing_charge":"No","date_created":"2018-12-11T12:09:36Z","alternative_title":["LNCS"],"title":"Modularity for timed and hybrid systems","intvolume":"      1243","_id":"4583","scopus_import":"1","author":[{"full_name":"Alur, Rajeev","last_name":"Alur","first_name":"Rajeev"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","page":"74 - 88","quality_controlled":"1","doi":"10.1007/3-540-63141-0_6","day":"01","abstract":[{"text":"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.","lang":"eng"}],"date_updated":"2022-08-17T08:47:55Z","year":"1997","citation":{"ista":"Alur R, Henzinger TA. 1997. Modularity for timed and hybrid systems. 8th International Conference on Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 1243, 74–88.","short":"R. Alur, T.A. Henzinger, in:, 8th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1997, pp. 74–88.","mla":"Alur, Rajeev, and Thomas A. Henzinger. “Modularity for Timed and Hybrid Systems.” <i>8th International Conference on Concurrency Theory</i>, vol. 1243, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1997, pp. 74–88, doi:<a href=\"https://doi.org/10.1007/3-540-63141-0_6\">10.1007/3-540-63141-0_6</a>.","ieee":"R. Alur and T. A. Henzinger, “Modularity for timed and hybrid systems,” in <i>8th International Conference on Concurrency Theory</i>, Warsaw, Poland, 1997, vol. 1243, pp. 74–88.","chicago":"Alur, Rajeev, and Thomas A Henzinger. “Modularity for Timed and Hybrid Systems.” In <i>8th International Conference on Concurrency Theory</i>, 1243:74–88. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1997. <a href=\"https://doi.org/10.1007/3-540-63141-0_6\">https://doi.org/10.1007/3-540-63141-0_6</a>.","ama":"Alur R, Henzinger TA. Modularity for timed and hybrid systems. In: <i>8th International Conference on Concurrency Theory</i>. Vol 1243. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 1997:74-88. doi:<a href=\"https://doi.org/10.1007/3-540-63141-0_6\">10.1007/3-540-63141-0_6</a>","apa":"Alur, R., &#38; Henzinger, T. A. (1997). Modularity for timed and hybrid systems. In <i>8th International Conference on Concurrency Theory</i> (Vol. 1243, pp. 74–88). Warsaw, Poland: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/3-540-63141-0_6\">https://doi.org/10.1007/3-540-63141-0_6</a>"},"volume":1243,"acknowledgement":"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.","extern":"1"}]