[{"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","year":"1999","language":[{"iso":"eng"}],"doi":"10.1007/3-540-48320-9_8","type":"conference","_id":"4602","author":[{"full_name":"Alur, Rajeev","first_name":"Rajeev","last_name":"Alur"},{"full_name":"De Alfaro, Luca","first_name":"Luca","last_name":"De Alfaro"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Mang, Freddy","first_name":"Freddy","last_name":"Mang"}],"date_published":"1999-01-01T00:00:00Z","acknowledgement":"This research was supported in part by the NSF CAREER award CCR-9734115, by the NSF CAREER award CCR-9501708, by the DARPA (NASA Ames) grant NAG2-1214, by the DARPA (Wright-Patterson AFB) grant F33615-98-C-3614, by the ARO MURI grant DAAH- 04-96-1-0341, and by the Gigascale Silicon Research Center.","date_created":"2018-12-11T12:09:42Z","intvolume":"      1664","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","extern":"1","article_processing_charge":"No","conference":{"name":"CONCUR: Concurrency Theory","end_date":"1999-08-27","start_date":"1999-08-24","location":"Eindhoven, The Netherlands"},"quality_controlled":"1","publication_identifier":{"isbn":["9783540664253"]},"publist_id":"105","month":"01","volume":1664,"date_updated":"2022-09-01T14:15:35Z","status":"public","abstract":[{"text":"Modular techniques for automatic verification attempt to overcome the state-explosion problem by exploiting the modular structure naturally present in many system designs. Unlike other tasks in the verification of finite-state systems, current modular techniques rely heavily on user guidance. In particular, the user is typically required to construct module abstractions that are neither too detailed as to render insufficient benefits in state exploration, nor too coarse as to invalidate the desired systemproperties. In this paper, we construct abstractmodules automatically, using reachability and controllability information about the concrete modules. This allows us to leverage automatic verification techniques by applying them in layers: first we compute on the state spaces of system components, then we use the results for constructing abstractions, and finally we compute on the abstract state space of the system. Our experimental results indicate that if reachability and controllability information is used in the construction of abstractions, the resulting abstract modules are often significantly smaller than the concrete modules and can drastically reduce the space and time requirements for verification.","lang":"eng"}],"oa_version":"None","page":"82 - 97","publication_status":"published","day":"01","citation":{"apa":"Alur, R., De Alfaro, L., Henzinger, T. A., &#38; Mang, F. (1999). Automating modular verification. In <i>Proceedings of the 10th International Conference on Concurrency Theory</i> (Vol. 1664, pp. 82–97). Eindhoven, The Netherlands: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/3-540-48320-9_8\">https://doi.org/10.1007/3-540-48320-9_8</a>","short":"R. Alur, L. De Alfaro, T.A. Henzinger, F. Mang, in:, Proceedings of the 10th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1999, pp. 82–97.","mla":"Alur, Rajeev, et al. “Automating Modular Verification.” <i>Proceedings of the 10th International Conference on Concurrency Theory</i>, vol. 1664, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1999, pp. 82–97, doi:<a href=\"https://doi.org/10.1007/3-540-48320-9_8\">10.1007/3-540-48320-9_8</a>.","ista":"Alur R, De Alfaro L, Henzinger TA, Mang F. 1999. Automating modular verification. Proceedings of the 10th International Conference on Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 1664, 82–97.","ama":"Alur R, De Alfaro L, Henzinger TA, Mang F. Automating modular verification. In: <i>Proceedings of the 10th International Conference on Concurrency Theory</i>. Vol 1664. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 1999:82-97. doi:<a href=\"https://doi.org/10.1007/3-540-48320-9_8\">10.1007/3-540-48320-9_8</a>","chicago":"Alur, Rajeev, Luca De Alfaro, Thomas A Henzinger, and Freddy Mang. “Automating Modular Verification.” In <i>Proceedings of the 10th International Conference on Concurrency Theory</i>, 1664:82–97. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1999. <a href=\"https://doi.org/10.1007/3-540-48320-9_8\">https://doi.org/10.1007/3-540-48320-9_8</a>.","ieee":"R. Alur, L. De Alfaro, T. A. Henzinger, and F. Mang, “Automating modular verification,” in <i>Proceedings of the 10th International Conference on Concurrency Theory</i>, Eindhoven, The Netherlands, 1999, vol. 1664, pp. 82–97."},"alternative_title":["LNCS"],"scopus_import":"1","title":"Automating modular verification","publication":"Proceedings of the 10th International Conference on Concurrency Theory"},{"abstract":[{"text":"In order to study control problems for hybrid systems, we generalize hybrid automata to hybrid games —say, controller vs. plant. If we specify the continuous dynamics by constant lower and upper bounds, we obtain rectangular games. We show that for rectangular games with objectives expressed in Ltl (linear temporal logic), the winning states for each player can be computed, and winning strategies can be synthesized. Our result is sharp, as already reachability is undecidable for generalizations of rectangular systems, and optimal —singly exponential in the size of the game structure and doubly exponential in the size of the Ltl objective. Our proof systematically generalizes the theory of hybrid systems from automata (single-player structures) [9] to games (multi-player structures): we show that the successively more general infinite-state classes of timed, 2D rectangular, and rectangular games induce successively weaker, but still finite, quotient structures called game bisimilarity, game similarity, and game trace equivalence. These quotients can be used, in particular, to solve the Ltl control problem.","lang":"eng"}],"day":"01","page":"320 - 335","publication_status":"published","oa_version":"None","date_updated":"2022-09-02T10:54:12Z","status":"public","title":"Rectangular hybrid games","publication":"Proceedings of the 10th International Conference on Concurrency Theory","citation":{"ista":"Henzinger TA, Horowitz B, Majumdar R. 1999. Rectangular hybrid games. Proceedings of the 10th International Conference on Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 1664, 320–335.","short":"T.A. Henzinger, B. Horowitz, R. Majumdar, in:, Proceedings of the 10th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1999, pp. 320–335.","mla":"Henzinger, Thomas A., et al. “Rectangular Hybrid Games.” <i>Proceedings of the 10th International Conference on Concurrency Theory</i>, vol. 1664, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1999, pp. 320–35, doi:<a href=\"https://doi.org/10.1007/3-540-48320-9_23\">10.1007/3-540-48320-9_23</a>.","apa":"Henzinger, T. A., Horowitz, B., &#38; Majumdar, R. (1999). Rectangular hybrid games. In <i>Proceedings of the 10th International Conference on Concurrency Theory</i> (Vol. 1664, pp. 320–335). Eindhoven, The Netherlands: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/3-540-48320-9_23\">https://doi.org/10.1007/3-540-48320-9_23</a>","ama":"Henzinger TA, Horowitz B, Majumdar R. Rectangular hybrid games. In: <i>Proceedings of the 10th International Conference on Concurrency Theory</i>. Vol 1664. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 1999:320-335. doi:<a href=\"https://doi.org/10.1007/3-540-48320-9_23\">10.1007/3-540-48320-9_23</a>","chicago":"Henzinger, Thomas A, Benjamin Horowitz, and Ritankar Majumdar. “Rectangular Hybrid Games.” In <i>Proceedings of the 10th International Conference on Concurrency Theory</i>, 1664:320–35. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1999. <a href=\"https://doi.org/10.1007/3-540-48320-9_23\">https://doi.org/10.1007/3-540-48320-9_23</a>.","ieee":"T. A. Henzinger, B. Horowitz, and R. Majumdar, “Rectangular hybrid games,” in <i>Proceedings of the 10th International Conference on Concurrency Theory</i>, Eindhoven, The Netherlands, 1999, vol. 1664, pp. 320–335."},"alternative_title":["LNCS"],"_id":"4485","author":[{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Benjamin","full_name":"Horowitz, Benjamin","last_name":"Horowitz"},{"first_name":"Ritankar","full_name":"Majumdar, Ritankar","last_name":"Majumdar"}],"date_published":"1999-01-01T00:00:00Z","year":"1999","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","doi":"10.1007/3-540-48320-9_23","language":[{"iso":"eng"}],"type":"conference","publication_identifier":{"isbn":["9783540664253"]},"publist_id":"245","quality_controlled":"1","month":"01","volume":1664,"acknowledgement":"This research was supported in part by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the DARPA (NASA Ames) grant NAG2-1214, by the DARPA (Wright-Patterson AFB) grant F33615-98-C-3614, and by the ARO MURI grant DAAH-04-96-1-0341.","date_created":"2018-12-11T12:09:05Z","intvolume":"      1664","conference":{"name":"CONCUR: Concurrency Theory","location":"Eindhoven, The Netherlands"},"extern":"1","article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17"}]