{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:18:49Z","timestamp":1778498329817,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642307928","type":"print"},{"value":"9783642307935","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-30793-5_2","type":"book-chapter","created":{"date-parts":[[2012,6,8]],"date-time":"2012-06-08T11:34:33Z","timestamp":1339155273000},"page":"18-34","source":"Crossref","is-referenced-by-count":21,"title":["A Small Model Theorem for Rectangular Hybrid Automata Networks"],"prefix":"10.1007","author":[{"given":"Taylor T.","family":"Johnson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sayan","family":"Mitra","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","unstructured":"Abbott, T.S., Jones, K.M., Consiglio, M.C., Williams, D.M., Adams, C.A.: Small aircraft transportation system, higher volume operations concept: Normal operations. Tech. Rep. NASA\/TM-2004-213022, NASA (August 2004)"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-540-73368-3_17","volume-title":"Computer Aided Verification","author":"P. Abdulla","year":"2007","unstructured":"Abdulla, P., Delzanno, G., Rezine, A.: Parameterized Verification of Infinite-State Processes with Global Conditions. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 145\u2013157. Springer, Heidelberg (2007)"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Deneux, J., Mahata, P.: Multi-clock timed networks. In: Proc. of 19th Annual IEEE Symposium Logic in Computer Science, pp. 345\u2013354 (July 2004)","DOI":"10.1109\/LICS.2004.1319629"},{"issue":"1","key":"2_CR4","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/S0304-3975(01)00330-9","volume":"290","author":"P.A. Abdulla","year":"2003","unstructured":"Abdulla, P.A., Jonsson, B.: Model checking of systems with many identical timed processes. Theoretical Computer Science\u00a0290(1), 241\u2013264 (2003)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"2_CR5","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science\u00a0138(1), 3\u201334 (1995)","journal-title":"Theoretical Computer Science"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-57318-6_30","volume-title":"Hybrid Systems","author":"R. Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol.\u00a0736, pp. 209\u2013229. Springer, Heidelberg (1993)"},{"issue":"6","key":"2_CR7","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"K.R. Apt","year":"1986","unstructured":"Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett.\u00a022(6), 307\u2013309 (1986)","journal-title":"Inf. Process. Lett."},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Computer Aided Verification","author":"T. Arons","year":"2001","unstructured":"Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.: Parameterized Verification with Automatically Computed Inductive Assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 221\u2013234. Springer, Heidelberg (2001)"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/11513988_39","volume-title":"Computer Aided Verification","author":"I. Balaban","year":"2005","unstructured":"Balaban, I., Fang, Y., Pnueli, A., Zuck, L.: IIV: An Invisible Invariant Verifier. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 408\u2013412. Springer, Heidelberg (2005)"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-642-14203-1_27","volume-title":"Automated Reasoning","author":"N. Bj\u00f8rner","year":"2010","unstructured":"Bj\u00f8rner, N.: Linear Quantifier Elimination as an Abstract Decision Procedure. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 316\u2013330. Springer, Heidelberg (2010)"},{"key":"2_CR11","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The Classical Decision Problem. Springer (2001)"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/11691372_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Brown","year":"2006","unstructured":"Brown, G., Pike, L.: Easy Parameterized Verification of Biphase Mark and 8N1 Protocols. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol.\u00a03920, pp. 58\u201372. Springer, Heidelberg (2006)"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-642-28891-3_28","volume-title":"NASA Formal Methods","author":"R. Bruttomesso","year":"2012","unstructured":"Bruttomesso, R., Carioni, A., Ghilardi, S., Ranise, S.: Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol.\u00a07226, pp. 279\u2013294. Springer, Heidelberg (2012)"},{"key":"2_CR14","unstructured":"Carioni, A., Ghilardi, S., Ranise, S.: MCMT in the land of parameterized timed automata. In: Proc. of VERIFY 2010 (July 2010)"},{"key":"2_CR15","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"2_CR17","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L. Moura De","year":"2011","unstructured":"De Moura, L., Bj\u00f8rner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM\u00a054, 69\u201377 (2011)","journal-title":"Commun. ACM"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/10722167_8","volume-title":"Computer Aided Verification","author":"G. Delzanno","year":"2000","unstructured":"Delzanno, G.: Automatic Verification of Parameterized Cache Coherence Protocols. In: Emerson, E., Sistla, A. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 53\u201368. Springer, Heidelberg (2000)"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-642-23702-7_26","volume-title":"Static Analysis","author":"A. Donaldson","year":"2011","unstructured":"Donaldson, A., Haller, L., Kroening, D., R\u00fcmmer, P.: Software Verification Using k-Induction. In: Yahav, E. (ed.) SAS 2011. LNCS, vol.\u00a06887, pp. 351\u2013368. Springer, Heidelberg (2011)"},{"key":"2_CR20","unstructured":"Dutertre, B., Sorea, M.: Timed systems in sal. Tech. Rep. SRI-SDL-04-03, SRI International (October 2004)"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-642-16265-7_12","volume-title":"Integrated Formal Methods","author":"J. Faber","year":"2010","unstructured":"Faber, J., Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: Automatic Verification of Parametric Specifications with Complex Topologies. In: M\u00e9ry, D., Merz, S. (eds.) IFM 2010. LNCS, vol.\u00a06396, pp. 152\u2013167. Springer, Heidelberg (2010)"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-31954-2_17","volume-title":"Hybrid Systems: Computation and Control","author":"G. Frehse","year":"2005","unstructured":"Frehse, G.: PHAVer: Algorithmic Verification of Hybrid Systems Past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol.\u00a03414, pp. 258\u2013273. Springer, Heidelberg (2005)"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"G. Frehse","year":"2011","unstructured":"Frehse, G., Le Guernic, C., Donz\u00e9, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: Scalable Verification of Hybrid Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 379\u2013395. Springer, Heidelberg (2011)"},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Y. Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.: Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 306\u2013320. Springer, Heidelberg (2009)"},{"key":"2_CR25","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1007\/s00165-008-0089-0","volume":"20","author":"O. Grinchtein","year":"2008","unstructured":"Grinchtein, O., Leucker, M.: Network invariants for real-time systems. Formal Aspects of Computing\u00a020, 619\u2013635 (2008)","journal-title":"Formal Aspects of Computing"},{"key":"2_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-642-16901-4_23","volume-title":"Formal Methods and Software Engineering","author":"Y. Hanna","year":"2010","unstructured":"Hanna, Y., Samuelson, D., Basu, S., Rajan, H.: Automating Cut-off for Multi-parameterized Systems. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol.\u00a06447, pp. 338\u2013354. Springer, Heidelberg (2010)"},{"key":"2_CR27","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1109\/LICS.1996.561342","volume-title":"IEEE Symposium on Logic in Computer Science (LICS)","author":"T.A. Henzinger","year":"1996","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: IEEE Symposium on Logic in Computer Science (LICS), p. 278. IEEE Computer Society, Washington, DC (1996)"},{"key":"2_CR28","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T.A. Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.H., Wong-Toi, H.: Hytech: a model checker for hybrid systems. Journal on Software Tools for Technology Transfer\u00a01, 110\u2013122 (1997)","journal-title":"Journal on Software Tools for Technology Transfer"},{"key":"2_CR29","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"T.A. Henzinger","year":"1998","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? Journal of Computer and System Sciences\u00a057, 94\u2013124 (1998)","journal-title":"Journal of Computer and System Sciences"},{"issue":"1-2","key":"2_CR30","first-page":"73","volume":"2","author":"T.T. Johnson","year":"2011","unstructured":"Johnson, T.T., Mitra, S.: Safe flocking in spite of actuator faults using directional failure detectors. Journal of Nonlinear Systems and Applications\u00a02(1-2), 73\u201395 (2011)","journal-title":"Journal of Nonlinear Systems and Applications"},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"Johnson, T.T., Mitra, S.: Parameterized verification of distributed cyber-physical systems: An aircraft landing protocol case study. In: ACM\/IEEE 3rd International Conference on Cyber-Physical Systems (April 2012)","DOI":"10.1109\/ICCPS.2012.24"},{"key":"2_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-642-21437-0_6","volume-title":"FM 2011: Formal Methods","author":"S.M. Loos","year":"2011","unstructured":"Loos, S.M., Platzer, A., Nistor, L.: Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol.\u00a06664, pp. 42\u201356. Springer, Heidelberg (2011)"},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"Manamcheri, K., Mitra, S., Bak, S., Caccamo, M.: A step towards verification and synthesis from simulink\/stateflow models. In: Proc. of the 14th Intl. Conf. on Hybrid Systems: Computation and Control, pp. 317\u2013318. ACM (2011)","DOI":"10.1145\/1967701.1967749"},{"key":"2_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/11916246_16","volume-title":"Rigorous Development of Complex Fault-Tolerant Systems","author":"C. Mu\u00f1oz","year":"2006","unstructured":"Mu\u00f1oz, C., Carre\u00f1o, V., Dowek, G.: Formal analysis of the operational concept for the small aircraft transportation system. In: Butler, M., Jones, C., Romanovsky, A., Troubitsyna, E. (eds.) Fault-Tolerant Systems, LNCS, vol. 4157, pp. 306\u2013325. Springer Berlin \/ Heidelberg (2006)"},{"key":"2_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/978-3-642-15205-4_36","volume-title":"Computer Science Logic","author":"A. Platzer","year":"2010","unstructured":"Platzer, A.: Quantified Differential Dynamic Logic for Distributed Hybrid Systems. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol.\u00a06247, pp. 469\u2013483. Springer, Heidelberg (2010)"},{"key":"2_CR36","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Quantified differential invariants. In: Proc. of the 14th ACM Intl. Conf. on Hybrid Systems: Computation and Control, pp. 63\u201372. ACM (2011)","DOI":"10.1145\/1967701.1967713"},{"key":"2_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"2001","unstructured":"Pnueli, A., Ruah, S., Zuck, L.: Automatic Deductive Verification with Invisible Invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 82\u201397. Springer, Heidelberg (2001)"},{"key":"2_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1007\/978-3-540-71493-4_43","volume-title":"Hybrid Systems: Computation and Control","author":"S. Umeno","year":"2007","unstructured":"Umeno, S., Lynch, N.: Safety Verification of an Aircraft Landing Protocol: A Refinement Approach. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol.\u00a04416, pp. 557\u2013572. Springer, Heidelberg (2007)"},{"key":"2_CR39","doi-asserted-by":"crossref","unstructured":"Viken, S., Brooks, F.: Demonstration of four operating capabilities to enable a small aircraft transportation system. In: The 24th Digital Avionics Systems Conference, DASC 2005, vol.\u00a02 (October 2005)","DOI":"10.1109\/DASC.2005.1563422"},{"key":"2_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/3-540-52148-8_6","volume-title":"Automatic Verification Methods for Finite State Systems","author":"P. Wolper","year":"1990","unstructured":"Wolper, P., Lovinfosse, V.: Verifying Properties of Large Sets of Processes with Network Invariants. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 68\u201380. Springer, Heidelberg (1990)"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-30793-5_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,30]],"date-time":"2025-03-30T06:29:30Z","timestamp":1743316170000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-30793-5_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642307928","9783642307935"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-30793-5_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}