{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T04:03:18Z","timestamp":1781064198253,"version":"3.54.1"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319952451","type":"print"},{"value":"9783319952468","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-95246-8_11","type":"book-chapter","created":{"date-parts":[[2018,7,19]],"date-time":"2018-07-19T06:50:32Z","timestamp":1531983032000},"page":"182-205","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":34,"title":["A Formal Semantics for Traffic Sequence Charts"],"prefix":"10.1007","author":[{"given":"Werner","family":"Damm","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Eike","family":"M\u00f6hlmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Peikenkamp","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Astrid","family":"Rakow","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,7,20]]},"reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-642-21437-0_4","volume-title":"FM 2011: Formal Methods","author":"W Damm","year":"2011","unstructured":"Damm, W., Finkbeiner, B.: Does it pay to extend the perimeter of a world model? In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 12\u201326. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-21437-0_4"},{"issue":"1","key":"11_CR2","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1023\/A:1011227529550","volume":"19","author":"W Damm","year":"2001","unstructured":"Damm, W., Harel, D.: LSCs: breathing life into message sequence charts. Formal Methods Syst. Des. 19(1), 45\u201380 (2001). \nhttps:\/\/doi.org\/10.1023\/A:1011227529550","journal-title":"Formal Methods Syst. Des."},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/978-3-319-24246-0_12","volume-title":"Frontiers of Combining Systems","author":"W Damm","year":"2015","unstructured":"Damm, W., Horbach, M., Sofronie-Stokkermans, V.: Decidability of verification of safety properties of spatial families of linear hybrid automata. In: Lutz, C., Ranise, S. (eds.) FroCoS 2015. LNCS (LNAI), vol. 9322, pp. 186\u2013202. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-24246-0_12"},{"key":"11_CR4","unstructured":"Damm, W., Kemper, S., M\u00f6hlmann, E., Peikenkamp, T., Rakow, A.: Traffic sequence charts - from visualization to semantics. Reports of SFB\/TR 14 AVACS 117, SFB\/TR 14 AVACS, October 2017"},{"key":"11_CR5","unstructured":"Damm, W., Kemper, S., M\u00f6hlmann, E., Peikenkamp, T., Rakow, A.: Traffic sequence charts - a visual language for capturing traffic scenarios. In: Embedded Real Time Software and Systems - ERTS2018, February 2018"},{"issue":"4","key":"11_CR6","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. Math. Struct. Comput. Sci. 23(4), 676\u2013725 (2013). \nhttps:\/\/doi.org\/10.1017\/S0960129512000230","journal-title":"Math. Struct. Comput. Sci."},{"issue":"1\u20133","key":"11_CR7","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/j.scico.2004.05.013","volume":"55","author":"W Damm","year":"2005","unstructured":"Damm, W., Westphal, B.: Live and let die: LSC based verification of UML models. Sci. Comput. Program. 55(1\u20133), 117\u2013159 (2005). \nhttps:\/\/doi.org\/10.1016\/j.scico.2004.05.013","journal-title":"Sci. Comput. Program."},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/3-540-45500-0_17","volume-title":"Theoretical Aspects of Computer Software","author":"M Fr\u00e4nzle","year":"2001","unstructured":"Fr\u00e4nzle, M.: What will be eventually true of polynomial hybrid automata? In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 340\u2013359. Springer, Heidelberg (2001). \nhttps:\/\/doi.org\/10.1007\/3-540-45500-0_17"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-319-23506-6_11","volume-title":"Correct System Design","author":"M Fr\u00e4nzle","year":"2015","unstructured":"Fr\u00e4nzle, M., Hansen, M.R., Ody, H.: No need knowing numerous neighbours. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design. LNCS, vol. 9360, pp. 152\u2013171. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-23506-6_11"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/3-540-48168-0_10","volume-title":"Computer Science Logic","author":"M Fr\u00e4nzle","year":"1999","unstructured":"Fr\u00e4nzle, M.: Analysis of hybrid systems: an ounce of realism can save an infinity of states. In: Flum, J., Rodriguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 126\u2013139. Springer, Heidelberg (1999). \nhttps:\/\/doi.org\/10.1007\/3-540-48168-0_10"},{"key":"11_CR11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19029-2","volume-title":"Come, Let\u2019s Play: Scenario-Based Programming Using LSC\u2019s and the Play-Engine","author":"D Harel","year":"2003","unstructured":"Harel, D., Marelly, R.: Come, Let\u2019s Play: Scenario-Based Programming Using LSC\u2019s and the Play-Engine. Springer, New York (2003). \nhttps:\/\/doi.org\/10.1007\/978-3-642-19029-2"},{"issue":"1","key":"11_CR12","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"TA Henzinger","year":"1998","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94\u2013124 (1998)","journal-title":"J. Comput. Syst. Sci."},{"key":"11_CR13","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. 6991, pp. 404\u2013419. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-24559-6_28"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-319-46750-4_16","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2016","author":"M Hilscher","year":"2016","unstructured":"Hilscher, M., Schwammberger, M.: An abstract model for proving safety of autonomous urban traffic. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 274\u2013292. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-46750-4_16"},{"key":"11_CR15","unstructured":"ITU-T: ITU-T recommendation Z.120: Message Sequence Chart (MSC) (2011). \nhttps:\/\/www.itu.int\/rec\/T-REC-Z.120-201102-I"},{"key":"11_CR16","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-319-02812-5_17","volume-title":"Complex Systems Design and Management","author":"S Kemper","year":"2014","unstructured":"Kemper, S., Etzien, C.: A visual logic for the description of highway traffic scenarios. In: Aiguier, M., Boulanger, F., Krob, D., Marchal, C. (eds.) Complex Systems Design and Management, pp. 233\u2013245. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-02812-5_17"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Linker, S., Hilscher, M.: Proof theory of a multi-lane spatial logic. Log. Methods Comput. Sci. 11(3) (2015). \nhttp:\/\/lmcs.episciences.org\/1580","DOI":"10.2168\/LMCS-11(3:4)2015"},{"issue":"1","key":"11_CR18","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/S0890-5401(03)00067-1","volume":"185","author":"Nancy Lynch","year":"2003","unstructured":"Lynch, N., Segala, R., Vaandrager, F.: Hybrid I\/O automata. Inf. Comput. 185(1), 105\u2013157 (2003). \nhttp:\/\/www.sciencedirect.com\/science\/article\/pii\/S0890540103000671","journal-title":"Information and Computation"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-319-25150-9_24","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2015","author":"H Ody","year":"2015","unstructured":"Ody, H.: Undecidability results for multi-lane spatial logic. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) ICTAC 2015. LNCS, vol. 9399, pp. 404\u2013421. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-25150-9_24"},{"key":"11_CR20","unstructured":"VIRES Simulationstechnologie GmbH: OpenDRIVE (2015). \nhttp:\/\/www.opendrive.org\n\n. Accessed 07 Sept 2017"},{"key":"11_CR21","unstructured":"VIRES Simulationstechnologie GmbH: OpenCRG (2016). \nhttp:\/\/www.opencrg.org\n\n. Accessed 07 Sept 2017"},{"key":"11_CR22","unstructured":"VIRES Simulationstechnologie GmbH: OpenSCENARIO (2017). \nhttp:\/\/www.openscenario.org\n\n. Accessed 07 Sept 2017"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"Zhang, P., Grunske, L., Tang, A., Li, B.: A formal syntax for probabilistic timed property sequence charts. In: 2009 IEEE\/ACM International Conference on Automated Software Engineering, pp. 500\u2013504, November 2009","DOI":"10.1109\/ASE.2009.56"},{"issue":"7","key":"11_CR24","doi-asserted-by":"publisher","first-page":"841","DOI":"10.1002\/spe.1038","volume":"41","author":"P Zhang","year":"2011","unstructured":"Zhang, P., Li, W., Wan, D., Grunske, L.: Monitoring of probabilistic timed property sequence charts. Softw.: Pract. Exp. 41(7), 841\u2013866 (2011). \nhttps:\/\/doi.org\/10.1002\/spe.1038","journal-title":"Softw.: Pract. Exp."}],"container-title":["Lecture Notes in Computer Science","Principles of Modeling"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-95246-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,7,19]],"date-time":"2018-07-19T06:55:31Z","timestamp":1531983331000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-95246-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319952451","9783319952468"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-95246-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}