{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:15Z","timestamp":1760202615837},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540222361"},{"type":"electronic","value":"9783540277934"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27793-4_17","type":"book-chapter","created":{"date-parts":[[2010,9,5]],"date-time":"2010-09-05T22:49:31Z","timestamp":1283726971000},"page":"298-311","source":"Crossref","is-referenced-by-count":7,"title":["LTL Model Checking for Modular Petri Nets"],"prefix":"10.1007","author":[{"given":"Timo","family":"Latvala","sequence":"first","affiliation":[]},{"given":"Marko","family":"M\u00e4kel\u00e4","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"17_CR1","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1093\/comjnl\/43.3.224","volume":"43","author":"S. Christensen","year":"2000","unstructured":"Christensen, S., Petrucci, L.: Modular analysis of Petri Nets. The Computer Journal\u00a043(3), 224\u2013242 (2000)","journal-title":"The Computer Journal"},{"key":"17_CR2","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"17_CR3","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1109\/LICS.1989.39190","volume-title":"Proc. 4th IEEE Symposium on Logic in Computer Science","author":"E.M. Clarke","year":"1989","unstructured":"Clarke, E.M., Long, D.E., McMillan, K.L.: Compositional model checking. In: Parikh, R. (ed.) Proc. 4th IEEE Symposium on Logic in Computer Science, pp. 353\u2013362. IEEE Computer Society Press, Los Alamitos (1989)"},{"key":"17_CR4","first-page":"1637","volume-title":"Handbook of Automated Reasoning","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Schlingloff, B.-H.: Model checking. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1637\u20131790. Elsevier, Amsterdam (2001)"},{"key":"17_CR5","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design\u00a01, 275\u2013288 (1992)","journal-title":"Formal Methods in System Design"},{"issue":"3","key":"17_CR6","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1016\/0196-6774(82)90023-2","volume":"3","author":"D. Dolev","year":"1982","unstructured":"Dolev, D., Klawe, M., Rodeh, M.: An O(n log n) unidirectional distributed algorithm for extrema finding in a circle. Journal of Algorithms\u00a03(3), 245\u2013260 (1982)","journal-title":"Journal of Algorithms"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45740-2_1","volume-title":"Applications and Theory of Petri Nets 2001","author":"S. Donatelli","year":"2001","unstructured":"Donatelli, S.: Kronecker algebra and (stochastic) Petri nets: Is it worth the effort. In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol.\u00a02075, pp. 1\u201318. Springer, Heidelberg (2001)"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/3-540-45139-0_4","volume-title":"Model Checking Software","author":"J. Esparza","year":"2001","unstructured":"Esparza, J., Heljanko, K.: Implementing LTL model checking with net unfoldings. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 37\u201356. Springer, Heidelberg (2001)"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Esparza, J., Heljanko, K.: A new unfolding approach to LTL model checking. Technical Report HUT-TCS-A60, Helsinki University of Technology (April 2000), Available from http:\/\/www.tcs.hut.fi\/Publications","DOI":"10.1007\/3-540-45022-X_40"},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P. Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 53\u201365. Springer, Heidelberg (2001)"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/3-540-36135-9_20","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2002","author":"D. Giannakopoulou","year":"2002","unstructured":"Giannakopoulou, D., Lerda, F.: From states to transitions: Improving translation of ltl formulae to b\u00fcchi automata. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol.\u00a02529, pp. 308\u2013326. Springer, Heidelberg (2002)"},{"key":"17_CR12","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Formal Methods for Industrial Critical Systems","author":"H. Hansen","year":"2002","unstructured":"Hansen, H., Penczek, W., Valmari, A.: Stuttering-insensitive automata for on-the-fly detection livelock properties. In: Formal Methods for Industrial Critical Systems. Electronic Notes in Theoretical Computer Science, vol.\u00a066(2). Elsevier, Amsterdam (2002)"},{"key":"17_CR13","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-60794-3","volume-title":"Coloured Petri Nets","author":"K. Jensen","year":"1997","unstructured":"Jensen, K.: Coloured Petri Nets, vol.\u00a01. Springer, Berlin (1997)"},{"key":"17_CR14","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994)"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/3-540-44829-2_5","volume-title":"Model Checking Software","author":"T. Latvala","year":"2003","unstructured":"Latvala, T.: Efficient model checking of safety properties. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 74\u201388. Springer, Heidelberg (2003)"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/3-540-45740-2_15","volume-title":"Applications and Theory of Petri Nets 2001","author":"T. Latvala","year":"2001","unstructured":"Latvala, T.: Model checking LTL properties of high-level Petri nets with fairness constraints. In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol.\u00a02075, pp. 242\u2013262. Springer, Heidelberg (2001)"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/3-540-44919-1_15","volume-title":"Applications and Theory of Petri Nets 2003","author":"M. M\u00e4kel\u00e4","year":"2003","unstructured":"M\u00e4kel\u00e4, M.: Model checking safety properties in modular high-level nets. In: van der Aalst, W.M.P., Best, E. (eds.) ICATPN 2003. LNCS, vol.\u00a02679, pp. 201\u2013220. Springer, Heidelberg (2003)"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"434","DOI":"10.1007\/3-540-48068-4_25","volume-title":"Application and Theory of Petri Nets 2002","author":"M. M\u00e4kel\u00e4","year":"2002","unstructured":"M\u00e4kel\u00e4, M.: Maria: modular reachability analyser for algebraic system nets. In: Esparza, J., Lakos, C.A. (eds.) ICATPN 2002. LNCS, vol.\u00a02360, pp. 434\u2013444. Springer, Heidelberg (2002)"},{"key":"17_CR19","unstructured":"Petrucci, L.: Design and validation of a controller. In: Proceedings of the 4th World Multiconference on Systemics, Cybernetics and Informatics, Orlando, FL, USA, July 2000, vol.\u00a0VIII, pp. 684\u2013688. International Institute of Informatics and Systemics (2000)"},{"key":"17_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"Computer Aided Verification","author":"F. Somenzio","year":"2000","unstructured":"Somenzio, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 248\u2013263. Springer, Heidelberg (2000)"},{"key":"17_CR21","first-page":"133","volume-title":"Handbook of Theoretical Computer Science","author":"W. Thomas","year":"1990","unstructured":"Thomas, W.: Automata on infinite objects. In: Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B, pp. 133\u2013191. Elsevier, Amsterdam (1990)"},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1007\/3-540-65306-6_21","volume-title":"Lectures on Petri Nets I: Basic Models","author":"A. Valmari","year":"1998","unstructured":"Valmari, A.: The state explosion problem. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol.\u00a01491, pp. 429\u2013528. Springer, Heidelberg (1998)"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/3-540-45510-8_3","volume-title":"Modeling and Verification of Parallel Processes","author":"A. Valmari","year":"2001","unstructured":"Valmari, A.: Composition and abstraction. In: Cassez, F., Jard, C., Rozoy, B., Dermot, M. (eds.) MOVEP 2000. LNCS, vol.\u00a02067, pp. 58\u201399. Springer, Heidelberg (2001)"},{"key":"17_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/3-540-56922-7_33","volume-title":"Computer Aided Verification","author":"A. Valmari","year":"1993","unstructured":"Valmari, A.: On-the-fly verification with stubborn sets. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 397\u2013408. Springer, Heidelberg (1993)"},{"key":"17_CR25","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"M.Y. Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logic of programs. Journal of Computer and System Sciences\u00a032, 183\u2013221 (1986)","journal-title":"Journal of Computer and System Sciences"},{"key":"17_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency","author":"M.Y. Vardi","year":"1996","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol.\u00a01043, pp. 238\u2013266. Springer, Heidelberg (1996)"},{"key":"17_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"472","DOI":"10.1007\/3-540-63166-6_51","volume-title":"Computer Aided Verification","author":"K. Varpaaniemi","year":"1997","unstructured":"Varpaaniemi, K., Heljanko, K., Lilius, J.: PROD 3.2 \u2013 an advanced tool for efficient reachability analysis. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 472\u2013475. Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","Applications and Theory of Petri Nets 2004"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27793-4_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:20:31Z","timestamp":1605759631000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27793-4_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540222361","9783540277934"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27793-4_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}