{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:23:11Z","timestamp":1759638191811,"version":"3.37.3"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2017,7,1]],"date-time":"2017-07-01T00:00:00Z","timestamp":1498867200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2017,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>The dynamic behavior of a car can be modeled as a hybrid system involving continuous state changes and discrete state transitions. We show that the control of safe (collision free) lane change maneuvers in multi-lane traffic on highways can be described by finite state machines extended with continuous variables coming from the environment. We use standard theory for controller synthesis to derive the dynamic behavior of a lane-change controller. Thereby, we contrast the setting of interleaving semantics and synchronous concurrent semantics. We also consider the possibility of exchanging knowledge between neighboring cars in order to come up with the right decisions. Finally, we address compositional verification using an assumption-guarantee paradigm.<\/jats:p>","DOI":"10.1007\/s00165-017-0424-4","type":"journal-article","created":{"date-parts":[[2017,3,13]],"date-time":"2017-03-13T09:18:21Z","timestamp":1489396701000},"page":"583-600","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Synthesizing and verifying controllers for multi-lane traffic maneuvers"],"prefix":"10.1145","volume":"29","author":[{"given":"Gregor V.","family":"Bochmann","sequence":"first","affiliation":[{"name":"School of Electrical Engineering and Computer Science, University of Ottawa, Ottawa, ON, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Hilscher","sequence":"additional","affiliation":[{"name":"Department of Computing Science, University of Oldenburg, Oldenburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2913-7943","authenticated-orcid":false,"given":"Sven","family":"Linker","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Liverpool, Liverpool, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3600-2046","authenticated-orcid":false,"given":"Ernst-R\u00fcdiger","family":"Olderog","sequence":"additional","affiliation":[{"name":"Department of Computing Science, University of Oldenburg, Oldenburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Abramson N (1970) The ALOHA system: another alternative for computer communications. In: Proceedings of fall joint computer conference AFIPS \u201970 pp 281\u2013285. ACM","DOI":"10.1145\/1478462.1478502"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/151646.151649"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Benveniste A Caillaud B Ferrari A Mangeruca L Passerone R Sofronis C (2008) Multiple viewpoint contract-based specification and design. In: de Boer FS Bonsangue MM Graf S de Roever WP (eds) Formal methods for components and objects (FMCO 2007) vol 5382 of LNCS. Springer Berlin pp 200\u2013225","DOI":"10.1007\/978-3-540-92188-2_9"},{"key":"e_1_2_1_2_4_2","unstructured":"Benveniste A Caillaud B Nickovic D Passerone R Raclet J-B Reinkemeier P Sangiovanni-Vincentelli A Damm W Henzinger T Larsen K (2012) Contracts for systems design. Technical report 8147 INRIA Research Center Rennes\u2014Bretagne Atlantique November 2012. 64\u00a0pp"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2015.06.006"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-011-0216-x"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2009.2039237"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Damm W Dierks H Oehlerking J Pnueli A (2010) Towards component based design of hybrid systems: safety and stability. In: Manna Z Peled DA (eds) Time for verification essays in memory of Amir Pnueli vol 6200 of LNCS. Springer Berlin pp 96\u2013143","DOI":"10.1007\/978-3-642-13754-9_6"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Damm W Finkbeiner B (2011) Does it pay to extend the perimeter of a world model? In: Butler MJ Schulte W (eds) Formal methods (FM 2011) vol 6664 of LNCS. Springer Berlin pp 12\u201326","DOI":"10.1007\/978-3-642-21437-0_4"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1080\/00207170600587531"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Dijkstra EW (1968) Cooperating sequential processes. In: Genuys F (ed) Programming languages: NATO Advanced Study Institute. Academic Press London pp 43\u2013112","DOI":"10.1007\/978-1-4757-3472-0_2"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Damm W M\u00f6hlmann E Rakow A (2014) Component based design of hybrid systems: a case study on concurrency and coupling. In: Hybrid systems: computation and control (HSCC). ACM New York pp 145\u2013150","DOI":"10.1145\/2562059.2562120"},{"key":"e_1_2_1_2_13_2","unstructured":"de Roever WP de Boer FS Hannemann U Hooman J Lakhnech Y Poel M Zwiers J (2001) Concurrency verification\u2014introduction to compositional and noncompositional methods. Cambridge University Press Cambridge"},{"key":"#cr-split#-e_1_2_1_2_14_2.1","doi-asserted-by":"crossref","unstructured":"Frese C Beyerer J (2011) A comparison of motion planning algorithms for cooperative collision avoidance of multiple cognitive automobiles. In: IEEE intelligent vehicles symposium","DOI":"10.1109\/IVS.2011.5940489"},{"key":"#cr-split#-e_1_2_1_2_14_2.2","unstructured":"(IV) 2011 Baden-Baden Germany June 5-9 2011 pp 1156-1162"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/128733.128734"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Hilscher M Linker S Olderog E-R Ravn AP (2011) An abstract model for proving safety of multi-lane traffic manoeuvres. In: Proceedings of ICFEM. Springer Berlin pp 404\u2013419","DOI":"10.1007\/978-3-642-24559-6_28"},{"key":"e_1_2_1_2_17_2","unstructured":"Jones CB (1983) Specification and design of (parallel) programs. In: Mason REA (ed) Information processing vol 83 of IFIP. Elsevier North-Holland pp 321\u2013332"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/9.664155"},{"key":"e_1_2_1_2_19_2","unstructured":"Linker S (2015) Proofs for traffic safety\u2014combining diagrams and logic. Ph.D. thesis Carl von Ossietzky Universit\u00e4t Oldenburg"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Loos SM Platzer A Nistor L (2011) Adaptive cruise control: hybrid distributed and now formally verified. In: Michael B Schulte W (eds) Formal methods (FM 2011) vol 6664 of LNCS. Springer Berlin pp 42\u201356","DOI":"10.1007\/978-3-642-21437-0_6"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00067-1"},{"key":"e_1_2_1_2_22_2","unstructured":"Lynch NA Segala R Vaandrager FW Weinberg HB (1999) Hybrid I\/O automata. Technical report CSI-R9907 Computing Science Institute University of Nijmegen April 1999"},{"issue":"3","key":"e_1_2_1_2_23_2","first-page":"219","article-title":"An introduction to input\/output automata.","volume":"2","author":"Lynch NA","year":"1989","journal-title":"CWI Q"},{"key":"e_1_2_1_2_24_2","unstructured":"Meyer B (1997) Object-oriented software construction 2nd edn. Prentice Hall Englewood Cliffs"},{"key":"e_1_2_1_2_25_2","unstructured":"Milner R (1989) Communication and concurrency. Prentice-Hall Englewood Cliffs"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Mauw S Reniers MA (1997) High-level message sequence charts. In: Cavalli A Sarma A (eds) SDL 1997: time for testing\u2014SDL MSC and Trends. Elsevier Science B.V. London pp 291\u2013306","DOI":"10.1016\/B978-044482816-3\/50020-4"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/357195.357196"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Olderog E-R Ravn AP Wisniewski R (2015) Linking spatial and dynamic models for traffic maneuvers. In: 54th IEEE conference on decision and control (CDC) Osaka Japan. IEEE pp 6809\u20136816","DOI":"10.1109\/CDC.2015.7403292"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Platzer A (2007) A temporal dynamic logic for verifying hybrid system invariants. In: Artemov SN Nerode A (eds) Logical foundations of computer science: international symposium (LFCS 2007) vol 4514 of LNCS. Springer Berlin pp 457\u2013471","DOI":"10.1007\/978-3-540-72734-7_32"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Platzer A (2010) Logical analysis of hybrid systems: proving theorems for complex dynamics. Springer Berlin","DOI":"10.1007\/978-3-642-14509-4"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Pnueli A (1985) In transition from global to modular reasoning about programs. In: Apt KR (ed) Logics and models of concurrent systems vol 13 of NATO ASI series F. Springer Berlin pp 123\u2013144","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1137\/0325013"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.sysconle.2004.10.002"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10626-011-0127-6"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Bochmann GV Hilscher M Linker S Olderog E-R (2015) Synthesizing controllers for multi-lane traffic maneuvers. In: Li X Liu Z Yi W (eds) 1st symposium on dependable software engineering: theories tools and applications (SETTA) vol 9409 of LNCS. Springer Berlin pp 1\u201316","DOI":"10.1007\/978-3-319-25942-0_5"},{"key":"e_1_2_1_2_36_2","unstructured":"Wirtz B Strazny T Rakow J Rakow A (2011) A lane change assistance system: cooperation and hybrid control. Technical report 78 SFB\/TR 14 AVACS July 2011. ISSN: 1860-9821 http:\/\/www.avacs.org"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/1067915.1067920"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-017-0424-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0424-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0424-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-017-0424-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:14:54Z","timestamp":1641485694000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-017-0424-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7]]},"references-count":38,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2017,7]]}},"alternative-id":["10.1007\/s00165-017-0424-4"],"URL":"https:\/\/doi.org\/10.1007\/s00165-017-0424-4","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2017,7]]}}}