{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:17:20Z","timestamp":1778498240767,"version":"3.51.4"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319242453","type":"print"},{"value":"9783319242460","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24246-0_12","type":"book-chapter","created":{"date-parts":[[2015,9,19]],"date-time":"2015-09-19T04:20:53Z","timestamp":1442636453000},"page":"186-202","source":"Crossref","is-referenced-by-count":4,"title":["Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata"],"prefix":"10.1007","author":[{"given":"Werner","family":"Damm","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthias","family":"Horbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viorica","family":"Sofronie-Stokkermans","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,12]]},"reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/978-3-642-35873-9_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P.A. Abdulla","year":"2013","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L.: All for the price of few. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol.\u00a07737, pp. 476\u2013495. Springer, Heidelberg (2013)"},{"issue":"3","key":"12_CR2","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1109\/32.489079","volume":"22","author":"R. Alur","year":"1996","unstructured":"Alur, R., Henzinger, T.A., Ho, P.: Automatic symbolic verification of embedded systems. IEEE Trans. Software Eng.\u00a022(3), 181\u2013201 (1996)","journal-title":"IEEE Trans. Software Eng."},{"key":"12_CR3","unstructured":"Damm, W., Horbach, M., Sofronie-Stokkermans, V.: Decidability of verification of safety properties of spatial families of linear hybrid automata. Tech. Rep. 111, SFB\/TR 14 AVACS (2014). \n                      \n                        http:\/\/www.avacs.org"},{"issue":"4","key":"12_CR4","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/s11786-011-0098-x","volume":"5","author":"W. Damm","year":"2011","unstructured":"Damm, W., Ihlemann, C., Sofronie-Stokkermans, V.: PTIME parametric verification of safety properties for reasonable linear hybrid automata. Mathematics in Computer Science\u00a05(4), 469\u2013497 (2011)","journal-title":"Mathematics in Computer Science"},{"issue":"4","key":"12_CR5","doi-asserted-by":"publisher","first-page":"676","DOI":"10.1017\/S0960129512000230","volume":"23","author":"W. Damm","year":"2013","unstructured":"Damm, W., Peter, H., Rakow, J., Westphal, B.: Can we build it: formal synthesis of control strategies for cooperative driver assistance systems. Mathematical Structures in Computer Science\u00a023(4), 676\u2013725 (2013)","journal-title":"Mathematical Structures in Computer Science"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Srinivasan, J.: A decidable temporal logic to reason about many processes. In: Proc. PODS 1990, pp. 233\u2013246. ACM (1990)","DOI":"10.1145\/93385.93425"},{"key":"12_CR7","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":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-540-78929-1_14","volume-title":"Hybrid Systems: Computation and Control","author":"G. Frehse","year":"2008","unstructured":"Frehse, G., Jha, S.K., Krogh, B.H.: A counterexample-guided approach to parameter synthesis for linear hybrid automata. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol.\u00a04981, pp. 187\u2013200. Springer, Heidelberg (2008)"},{"key":"12_CR9","unstructured":"Frese, C.: A comparison of algorithms for planning cooperative motions of cognitive automobiles. In: Proc. 2010 Joint Workshop of Fraunhofer IOSB and Institute for Anthropomatics, Vision and Fusion Laboratory. No. IES-2010-06 in Karlsruher Schriften zur Anthropomatik, vol.\u00a07, pp. 75\u201390. KIT Scientific Publishing (2010)"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-642-16111-7_10","volume-title":"KI 2010: Advances in Artificial Intelligence","author":"C. Frese","year":"2010","unstructured":"Frese, C., Beyerer, J.: Planning cooperative motions of cognitive automobiles using tree search algorithms. In: Dillmann, R., Beyerer, J., Hanebeck, U.D., Schultz, T. (eds.) KI 2010. LNCS, vol.\u00a06359, pp. 91\u201398. Springer, Heidelberg (2010)"},{"issue":"2","key":"12_CR11","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1142\/S0129054113400091","volume":"24","author":"L. Fribourg","year":"2013","unstructured":"Fribourg, L., K\u00fchne, U.: Parametric verification and test coverage for hybrid automata using the inverse method. Int. J. Found. Comput. Sci.\u00a024(2), 233\u2013250 (2013)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-642-24559-6_28","volume-title":"Formal Methods and Software Engineering","author":"M. Hilscher","year":"2011","unstructured":"Hilscher, M., Linker, S., Olderog, E.-R., Ravn, A.P.: An abstract model for proving safety of multi-lane traffic manoeuvres. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol.\u00a06991, pp. 404\u2013419. Springer, Heidelberg (2011)"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-60385-9_1","volume-title":"Correct Hardware Design and Verification Methods","author":"H. Hungar","year":"1995","unstructured":"Hungar, H., Grumberg, O., Damm, W.: What if model checking must be truly symbolic. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol.\u00a0987, pp. 1\u201320. Springer, Heidelberg (1995)"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-540-78800-3_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Ihlemann","year":"2008","unstructured":"Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 265\u2013281. Springer, Heidelberg (2008)"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-02959-2_9","volume-title":"Automated Deduction \u2013 CADE-22","author":"C. Ihlemann","year":"2009","unstructured":"Ihlemann, C., Sofronie-Stokkermans, V.: System description: H-PILoT. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 131\u2013139. Springer, Heidelberg (2009)"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-642-14203-1_4","volume-title":"Automated Reasoning","author":"C. Ihlemann","year":"2010","unstructured":"Ihlemann, C., Sofronie-Stokkermans, V.: On hierarchical reasoning in combinations of theories. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 30\u201345. Springer, Heidelberg (2010)"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Jacobs, S., Bloem, R.: Parameterized synthesis. Logical Methods in CS\u00a010(1) (2014)","DOI":"10.2168\/LMCS-10(1:12)2014"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-642-18275-4_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Jacobs","year":"2011","unstructured":"Jacobs, S., Kuncak, V.: Towards complete reasoning about axiomatic specifications. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 278\u2013293. Springer, Heidelberg (2011)"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Johnson, T.T., Mitra, S.: Parametrized verification of distributed cyber-physical systems: An aircraft landing protocol case study. In: Proc. CPS 2012, pp. 161\u2013170. IEEE (2012)","DOI":"10.1109\/ICCPS.2012.24"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Johnson, T.T., Mitra, S.: A small model theorem for rectangular hybrid automata networks. In: Giese, H., Rosu, G. (eds.) FORTE\/FMOODS 2012. LNCS, vol.\u00a07273, pp. 18\u201334. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-30793-5_2"},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1007\/978-3-642-14295-6_55","volume-title":"Computer Aided Verification","author":"A. Kaiser","year":"2010","unstructured":"Kaiser, A., Kroening, D., Wahl, T.: Dynamic cutoff detection in parameterized concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 645\u2013659. Springer, Heidelberg (2010)"},{"key":"12_CR22","first-page":"191","volume":"20","author":"L. Khachian","year":"1979","unstructured":"Khachian, L.: A polynomial time algorithm for linear programming. Soviet Math. Dokl.\u00a020, 191\u2013194 (1979)","journal-title":"Soviet Math. Dokl."},{"issue":"1\u20132","key":"12_CR23","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/S0304-3975(00)00177-8","volume":"266","author":"M. Koubarakis","year":"2001","unstructured":"Koubarakis, M.: Tractable disjunctions of linear constraints: basic results and applications to temporal reasoning. Theo. Comp. Sci.\u00a0266(1\u20132), 311\u2013339 (2001)","journal-title":"Theo. Comp. Sci."},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/11513988_47","volume-title":"Computer Aided Verification","author":"S. McPeak","year":"2005","unstructured":"McPeak, S., Necula, G.C.: Data structure specifications via local equality axioms. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 476\u2013490. Springer, Heidelberg (2005)"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"Mickelin, O., Ozay, N., Murray, R.M.: Synthesis of correct-by-construction control protocols for hybrid systems using partial state information. In: Proc. ACC 2014, pp. 2305\u20132311. IEEE (2014)","DOI":"10.1109\/ACC.2014.6859229"},{"key":"12_CR26","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.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"1","key":"12_CR27","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1145\/200836.200848","volume":"42","author":"B. Nebel","year":"1995","unstructured":"Nebel, B., B\u00fcrckert, H.J.: Reasoning about temporal relations: A maximal tractable subclass of Allen\u2019s interval algebra. J. of the ACM\u00a042(1), 43\u201366 (1995)","journal-title":"J. of the ACM"},{"issue":"2","key":"12_CR28","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10817-008-9103-8","volume":"41","author":"A. Platzer","year":"2008","unstructured":"Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reasoning\u00a041(2), 143\u2013189 (2008)","journal-title":"J. Autom. Reasoning"},{"key":"12_CR29","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":"12_CR30","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/11532231_16","volume-title":"Automated Deduction \u2013 CADE-20","author":"V. Sofronie-Stokkermans","year":"2005","unstructured":"Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 219\u2013234. Springer, Heidelberg (2005)"},{"key":"12_CR31","series-title":"LNCS (LNAI)","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-14203-1_15","volume-title":"Automated Reasoning","author":"V. Sofronie-Stokkermans","year":"2010","unstructured":"Sofronie-Stokkermans, V.: Hierarchical reasoning for the verification of parametric systems. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol.\u00a06173, pp. 171\u2013187. Springer, Heidelberg (2010)"},{"key":"12_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/978-3-642-38574-2_25","volume-title":"Automated Deduction \u2013 CADE-24","author":"V. Sofronie-Stokkermans","year":"2013","unstructured":"Sofronie-Stokkermans, V.: Hierarchical reasoning and model generation for the verification of parametric hybrid systems. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol.\u00a07898, pp. 360\u2013376. Springer, Heidelberg (2013)"},{"issue":"3","key":"12_CR33","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0020-0190(85)90076-6","volume":"20","author":"E. Sontag","year":"1985","unstructured":"Sontag, E.: Real addition and the polynomial hierarchy. Inf. Proc. Letters\u00a020(3), 115\u2013120 (1985)","journal-title":"Inf. Proc. Letters"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24246-0_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T00:41:56Z","timestamp":1559263316000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24246-0_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319242453","9783319242460"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24246-0_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}