{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T01:40:03Z","timestamp":1743990003290,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642327582"},{"type":"electronic","value":"9783642327599"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32759-9_8","type":"book-chapter","created":{"date-parts":[[2012,8,21]],"date-time":"2012-08-21T10:12:30Z","timestamp":1345543950000},"page":"52-67","source":"Crossref","is-referenced-by-count":11,"title":["A Formal Approach to Autonomous Vehicle Coordination"],"prefix":"10.1007","author":[{"given":"Mikael","family":"Asplund","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Atif","family":"Manzoor","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M\u00e9lanie","family":"Bouroche","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Siobh\u00e0n","family":"Clarke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vinny","family":"Cahill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Althoff, M., Althoff, D., Wollherr, D., Buss, M.: Safety verification of autonomous vehicles for coordinated evasive maneuvers. In: IEEE Intelligent Vehicles Symposium, IV (2010), doi:10.1109\/IVS.2010.5548121","DOI":"10.1109\/IVS.2010.5548121"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R.: Formal verification of hybrid systems. In: Proceedings of the Ninth ACM International Conference on Embedded Software, EMSOFT. ACM (2011), doi:10.1145\/2038642.2038685","DOI":"10.1145\/2038642.2038685"},{"key":"8_CR3","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2010), http:\/\/www.SMT-LIB.org"},{"key":"8_CR4","unstructured":"Bhandal, C., Bouroche, M., Hughes, A.: A process algebraic description of a temporal wireless network protocol. In: Proceedings of the Fourth International Workshop on Formal Methods for Interactive Systems (2011)"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Bouroche, M.: Real-Time Coordination of Mobile Autonomous Entities. PhD thesis, Dept. of Computer Science, Trinity College Dublin (2007)","DOI":"10.1109\/ITSC.2006.1707391"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Chandra, T.D., Hadzilacos, V., Toueg, S., Charron-Bost, B.: On the impossibility of group membership. In: Fifteenth Annual ACM Symposium on Principles of Distributed Computing (PODC). ACM Press (1996), doi:10.1145\/248052.248120","DOI":"10.1145\/248052.248120"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Damm, W., Hungar, H., Olderog, E.-R.: Verification of cooperating traffic agents. International Journal of Control\u00a079(5) (2006), doi:10.1080\/00207170600587531","DOI":"10.1080\/00207170600587531"},{"key":"8_CR8","unstructured":"De Moura, L., Bj\u00f8rner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM\u00a054 (2011), doi: http:\/\/doi.acm.org\/10.1145\/1995376.1995394"},{"key":"8_CR9","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)"},{"issue":"1","key":"8_CR10","first-page":"591","volume":"31","author":"K. Dresner","year":"2008","unstructured":"Dresner, K., Stone, P.: A multiagent approach to autonomous intersection management. J. Artif. Int. Res.\u00a031(1), 591\u2013656 (2008)","journal-title":"J. Artif. Int. Res."},{"key":"8_CR11","unstructured":"European Commission. Eu energy and transport in figures (2010), http:\/\/ec.europa.eu\/energy\/publications\/statistics\/statistics_en.htm (accessed January 2012)"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Henzinger, T.: The theory of hybrid automata. In: Proceedings. Eleventh Annual IEEE Symposium on Logics in Computer Science, LICS 1966 (1996), doi:10.1109\/LICS.1996.561342","DOI":"10.1109\/LICS.1996.561342"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Herde, C., Eggers, A., Franzle, M., Teige, T.: Analysis of hybrid systems using hysat. In: Third International Conference on Systems, ICONS (2008), doi:10.1109\/ICONS.2008.17","DOI":"10.1109\/ICONS.2008.17"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Huang, J., Blech, J., Raabe, A., Buckl, C., Knoll, A.: Static scheduling of a time-triggered network-on-chip based on SMT solving. In: Design, Automation Test in Europe Conference Exhibition (DATE), pp. 509\u2013514 (2012)","DOI":"10.1109\/DATE.2012.6176522"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Livadas, C., Lygeros, J., Lynch, N.: High-level modeling and analysis of the traffic alert and collision avoidance system (tcas). Proceedings of the IEEE\u00a088(7) (2000), doi:10.1109\/5.871302","DOI":"10.1109\/5.871302"},{"key":"8_CR16","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. Loos","year":"2011","unstructured":"Loos, S., 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":"8_CR17","doi-asserted-by":"crossref","unstructured":"Loos, S.M., Platzer, A.: Safe intersections: At the crossing of hybrid systems and verification. In: 14th International IEEE Conference on Intelligent Transportation Systems, ITSC (2011), doi:10.1109\/ITSC.2011.6083138","DOI":"10.1109\/ITSC.2011.6083138"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Naumann, R., Rasche, R., Tacken, J., Tahedi, C.: Validation and simulation of a decentralized intersection collision avoidance algorithm. In: IEEE Conference on Intelligent Transportation System, ITSC (1997), doi:10.1109\/ITSC.1997.660579","DOI":"10.1109\/ITSC.1997.660579"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reas.\u00a041(2) (2008), doi:10.1007\/s10817-008-9103-8","DOI":"10.1007\/s10817-008-9103-8"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-642-05089-3_35","volume-title":"FM 2009: Formal Methods","author":"A. Platzer","year":"2009","unstructured":"Platzer, A., Clarke, E.M.: Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 547\u2013562. Springer, Heidelberg (2009)"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking Safety Properties Using Induction and a SAT-Solver. In: Hunt Jr., W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 108\u2013125. Springer, Heidelberg (2000)"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Sin, M.L., Bouroche, M., Cahill, V.: Scheduling of dynamic participants in real-time distributed systems. In: 30th IEEE Symposium on Reliable Distributed Systems, SRDS (2011), doi:10.1109\/SRDS.2011.37","DOI":"10.1109\/SRDS.2011.37"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Slot, M., Cahill, V.: A reliable membership service for vehicular safety applications. In: IEEE Intelligent Vehicles Symposium, IV (2011), doi:10.1109\/IVS.2011.5940487","DOI":"10.1109\/IVS.2011.5940487"},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-642-15898-8_10","volume-title":"Formal Methods for Industrial Critical Systems","author":"W. Steiner","year":"2010","unstructured":"Steiner, W., Dutertre, B.: SMT-Based Formal Verification of a TTEthernet Synchronization Function. In: Kowalewski, S., Roveri, M. (eds.) FMICS 2010. LNCS, vol.\u00a06371, pp. 148\u2013163. Springer, Heidelberg (2010)"},{"key":"8_CR25","unstructured":"The World Bank. Road safety (2011), http:\/\/www.worldbank.org\/transport\/roads\/safety.htm (accessed December 2011)"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Tomlin, C., Pappas, G., Sastry, S.: Conflict resolution for air traffic management: a study in multiagent hybrid systems. IEEE Transactions on Automatic Control\u00a043(4) (1998), doi:10.1109\/9.664154","DOI":"10.1109\/9.664154"},{"key":"8_CR27","unstructured":"Traffic Accident Causation in Europe (TRACE) FP6-2004-IST-4. Deliverable 1.3 road users and accident causation (2009)"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Verma, R., Vecchio, D.: Semiautonomous multivehicle safety. IEEE Robotics Automation Magazine\u00a018(3) (2011), doi:10.1109\/MRA.2011.942114","DOI":"10.1109\/MRA.2011.942114"},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"Zimmermann, A., Hommel, G.: A train control system case study in model-based real time system design. In: Proceedings. International Parallel and Distributed Processing Symposium, 2003 (2003), doi:10.1109\/IPDPS.2003.1213234","DOI":"10.1109\/IPDPS.2003.1213234"}],"container-title":["Lecture Notes in Computer Science","FM 2012: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32759-9_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T01:01:10Z","timestamp":1743987670000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32759-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642327582","9783642327599"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32759-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}