{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T17:41:27Z","timestamp":1743097287310,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540253334"},{"type":"electronic","value":"9783540319801"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-31980-1_29","type":"book-chapter","created":{"date-parts":[[2010,7,11]],"date-time":"2010-07-11T22:44:59Z","timestamp":1278888299000},"page":"445-460","source":"Crossref","is-referenced-by-count":52,"title":["Temporal Logic for Scenario-Based Specifications"],"prefix":"10.1007","author":[{"given":"Hillel","family":"Kugler","sequence":"first","affiliation":[]},{"given":"David","family":"Harel","sequence":"additional","affiliation":[]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[]},{"given":"Yuan","family":"Lu","sequence":"additional","affiliation":[]},{"given":"Yves","family":"Bontemps","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"29_CR1","first-page":"70","volume":"17","author":"R. Alur","year":"1996","unstructured":"Alur, R., Holzmann, G.J., Peled, D.: An analyzer for message sequence charts. Software Concepts and Tools\u00a017(2), 70\u201377 (1996)","journal-title":"Software Concepts and Tools"},{"key":"29_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/3-540-48320-9_10","volume-title":"CONCUR\u201999. Concurrency Theory","author":"R. Alur","year":"1999","unstructured":"Alur, R., Yannakakis, M.: Model checking of message sequence charts. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, pp. 114\u2013129. Springer, Heidelberg (1999)"},{"key":"29_CR3","unstructured":"Bontemps, Y.: Automated verification of state-based specifications against scenarios (a step toward relating inter-object to intra-object specifications). Master\u2019s thesis. University of Namur, Belgium (June 2001)"},{"key":"29_CR4","unstructured":"Bunker, A., Gopalakrishnan, G.: Verifying a VCI Bus Interface Model Using an LSC-based Specification. In: Proceedings of the Sixth Biennial World Conference on Integrated Design and Process Technology, pp. 1\u201312 (2002)"},{"key":"29_CR5","unstructured":"Bunker, A., Slind, K.: Property Generation for Live Sequence Charts. Technical report. University of Utah (2003)"},{"key":"29_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/BFb0013029","volume-title":"Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency","author":"E.M. Clarke","year":"1988","unstructured":"Clarke, E.M., Draghicescu, I.A.: Expressibility results for linear-time and branching-time logics. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. LNCS, vol.\u00a0354, pp. 428\u2013437. Springer, Heidelberg (1988)"},{"issue":"1","key":"29_CR7","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 in System Design\u00a019(1), 45\u201380 (2001)","journal-title":"Formal Methods in System Design"},{"issue":"2","key":"29_CR8","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1023\/A:1011279932612","volume":"19","author":"W. Damm","year":"2001","unstructured":"Damm, W., Klose, J.: Verification of a radio-based signalling system using the statemate verification environment. Formal Methods in System Design\u00a019(2), 121\u2013141 (2001)","journal-title":"Formal Methods in System Design"},{"key":"29_CR9","first-page":"995","volume-title":"Handbook of theoretical computer science","author":"E.A. Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logics. In: van Leeuwen, J. (ed.) Handbook of theoretical computer science, vol.\u00a0B, pp. 995\u20131072. Elsevier, Amsterdam (1990)"},{"key":"29_CR10","series-title":"Lecture Notes in Computer Science","first-page":"407","volume-title":"Temporal Logic in Specification","author":"D. Gabbay","year":"1987","unstructured":"Gabbay, D.: The declarative past and imperative future. In: Temporal Logic in Specification. LNCS, vol.\u00a0398, pp. 407\u2013448. Springer, Heidelberg (1987)"},{"key":"29_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/3-540-45319-9_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E.L. Gunter","year":"2001","unstructured":"Gunter, E.L., Muscholl, A., Peled, D.: Compositional message sequence charts. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 496\u2013511. Springer, Heidelberg (2001)"},{"key":"29_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/3-540-44674-5_1","volume-title":"Implementation and Application of Automata","author":"D. Harel","year":"2001","unstructured":"Harel, D., Kugler, H.: Synthesizing state-based object systems from LSC specifications. Int. J. of Foundations of Computer Science (IJFCS), 13(1), 5\u201351, (Febuary 2002) Also In: Yu, S., P\u0103un, A. (eds.) CIAA 2000. LNCS, vol.\u00a02088, pp. 5\u201351. Springer, Heidelberg (2001)"},{"key":"29_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/3-540-36126-X_23","volume-title":"Formal Methods in Computer-Aided Design","author":"D. Harel","year":"2002","unstructured":"Harel, D., Kugler, H., Marelly, R., Pnueli, A.: Smart play-out of behavioral requirements. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 378\u2013398. Springer, Heidelberg (2002)"},{"key":"29_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-19029-2","volume-title":"Come, Let\u2019s Play: Scenario-Based Programming Using LSCs and the Play-Engine","author":"D. Harel","year":"2003","unstructured":"Harel, D., Marelly, R.: Come, Let\u2019s Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003)"},{"issue":"2","key":"29_CR15","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/s10270-002-0015-5","volume":"2","author":"D. Harel","year":"2003","unstructured":"Harel, D., Marelly, R.: Specifying and Executing Behavioral Requirements: The Play In\/Play-Out Approach. Software and System Modeling (SoSyM)\u00a02(2), 82\u2013107 (2003)","journal-title":"Software and System Modeling (SoSyM)"},{"key":"29_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1007\/3-540-45022-X_57","volume-title":"Automata, Languages and Programming","author":"J.G. Henriksen","year":"2000","unstructured":"Henriksen, J.G., Mukund, M., Kumar, K.N., Thiagarajan, P.S.: On message sequence graphs and finitely generated regular MSC languages. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol.\u00a01853, pp. 675\u2013686. Springer, Heidelberg (2000)"},{"key":"29_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1007\/3-540-44612-5_36","volume-title":"Mathematical Foundations of Computer Science 2000","author":"J.G. Henriksen","year":"2000","unstructured":"Henriksen, J.G., Mukund, M., Kumar, K.N., Thiagarajan, P.S.: Regular collections of Message Sequence Charts. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol.\u00a01893, pp. 675\u2013686. Springer, Heidelberg (2000)"},{"key":"29_CR18","unstructured":"Rhapsody. I-Logix, Inc., products web page, http:\/\/www.ilogix.com\/products\/"},{"key":"29_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/3-540-45319-9_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Klose","year":"2001","unstructured":"Klose, J., Wittke, H.: An automata based interpretation of live sequence charts. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, p. 512. Springer, Heidelberg (2001)"},{"key":"29_CR20","doi-asserted-by":"crossref","unstructured":"Lettrari, M., Klose, J.: Scenario-based monitoring and testing of real-time UML models. In: 4th Int. Conf. on the Unified Modeling Language, Toronto (October 2001)","DOI":"10.1007\/3-540-45441-1_24"},{"key":"29_CR21","doi-asserted-by":"crossref","unstructured":"Maidl, M.: The common fragment of CTL and LTL. In: Proc. 41st IEEE Symp. Found. of Comp. Sci., pp. 643\u2013652 (2000)","DOI":"10.1109\/SFCS.2000.892332"},{"key":"29_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/BFb0053553","volume-title":"Foundations of Software Science and Computation Structures","author":"A. Muscholl","year":"1998","unstructured":"Muscholl, A., Peled, D., Su, Z.: Deciding properties for message sequence charts. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol.\u00a01378, pp. 226\u2013242. Springer, Heidelberg (1998)"},{"key":"29_CR23","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symp. Found. of Comp. Sci., pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"29_CR24","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1145\/587051.587077","volume-title":"Proceedings of the tenth ACM SIGSOFT symposium on Foundations of software engineering","author":"B. Sengupta","year":"2002","unstructured":"Sengupta, B., Cleaveland, R.: Triggered message sequence charts. In: Proceedings of the tenth ACM SIGSOFT symposium on Foundations of software engineering, pp. 167\u2013176. ACM Press, New York (2002)"},{"key":"29_CR25","unstructured":"UML. Documentation of the unified modeling language (UML). Available from the Object Management Group (OMG), http:\/\/www.omg.org"},{"key":"29_CR26","unstructured":"Z.120 ITU-TS Recommendation Z.120: Message Sequence Chart (MSC). ITU-TS, Geneva (1996)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-31980-1_29.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T20:31:25Z","timestamp":1740256285000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31980-1_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540253334","9783540319801"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31980-1_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}