{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:10:27Z","timestamp":1725495027763},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540422525"},{"type":"electronic","value":"9783540457404"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45740-2_15","type":"book-chapter","created":{"date-parts":[[2007,11,15]],"date-time":"2007-11-15T15:30:51Z","timestamp":1195140651000},"page":"242-262","source":"Crossref","is-referenced-by-count":9,"title":["Model Checking LTL Properties of High-Level Petri Nets with Fairness Constraints"],"prefix":"10.1007","author":[{"given":"Timo","family":"Latvala","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,6,28]]},"reference":[{"key":"15_CR1","unstructured":"CCITT. Specification and description language (SDL). Technical Report Z.100, ITU-T, 1996."},{"key":"15_CR2","series-title":"Lect Notes Comput Sci","first-page":"52","volume-title":"Proceedings of the IBM Workshop on Logics of Programs","author":"E.M. Clarke","year":"1981","unstructured":"E.M. Clarke and E.A. Emerson. Design and synthesis of syncronization of skeletons using branching time temporal logic. In Proceedings of the IBM Workshop on Logics of Programs, pages 52\u201371. Springer-Verlag, 1981. LNCS 131."},{"key":"15_CR3","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"C. Courcoubetis, M.Y. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1:275\u2013288, 1992.","journal-title":"Formal Methods in System Design"},{"key":"15_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/3-540-48119-2_16","volume-title":"Proceeding of the World Congress on Formal Methods in the Development of Computing Systems (FM\u201999)","author":"J.-M. Couvreur","year":"1999","unstructured":"J-M. Couvreur. On-the-fly verification of linear temporal logic. In Proceeding of the World Congress on Formal Methods in the Development of Computing Systems (FM\u201999), volume 1, pages 253\u2013271, Berlin, 1999. Springer-Verlag. LNCS 1708."},{"key":"15_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/3-540-48683-6_23","volume-title":"Proceedings of the International Conference on Computer Aided Verification (CAV\u201999)","author":"M. Daniele","year":"1999","unstructured":"M. Daniele, F. Giunchiglia, and M.Y Vardi. Improved automata generation for linear temporal logic. In Proceedings of the International Conference on Computer Aided Verification (CAV\u201999), pages 249\u2013260, Berlin, 1999. Springer-Verlag. LNCS 1633."},{"issue":"3","key":"15_CR6","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E.A. Emerson","year":"1987","unstructured":"E.A. Emerson and C-L. Lei. Modalities for model checking: Branching time logic strikes back. Science of Computer Programming, 8(3):275\u2013306, 1987.","journal-title":"Science of Computer Programming"},{"key":"15_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4886-6","volume-title":"Fairness","author":"N. Francez","year":"1986","unstructured":"N. Francez. Fairness. Springer-Verlag, New York, 1986."},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"R. Gerth, D. Peled, M.Y. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Proceedings of the 15th Workshop Protocol Specification, Testing, and Verification, Warsaw, June 1995. North-Holland.","DOI":"10.1007\/978-0-387-34892-6_1"},{"issue":"13","key":"15_CR9","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1023\/A:1008771008310","volume":"14","author":"P. Godefroid","year":"1999","unstructured":"P. Godefroid and D.E Long. Symbolic protocol verification with Queue BDDs. Formal Methods in System Design, 14(13):257\u2013271, May 1999.","journal-title":"Formal Methods in System Design"},{"key":"15_CR10","volume-title":"Memorandum UCB\/ERL M94\/12","author":"R. Hojati","year":"1994","unstructured":"R. Hojati, V. Singhal, and R.K. Brayton. Edge-Streett \/ edge-Rabin automata environment for formal verification using language containment. Memorandum UCB\/ERL M94\/12,Electronics Research Laboratory, University of California, Cory Hall, Berkley, 1994."},{"issue":"5","key":"15_CR11","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"G.J. Holzmann. The model checker Spin. IEEE Transactions on Software Engineering, 23(5):279\u2013295, May 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"15_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-60794-3","volume-title":"Coloured Petri Nets","author":"K. Jensen","year":"1997","unstructured":"K. Jensen. Coloured Petri Nets, volume 1. Springer-Verlag, Berlin, 1997."},{"key":"15_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1007\/3-540-63166-6_8","volume-title":"Proceedings of the 9th International Conference on Computer Aided Verification (CAV\u201997)","author":"R. Kaivola","year":"1997","unstructured":"R. Kaivola. Using compositional preorders in the verification of sliding window protocol. In Proceedings of the 9th International Conference on Computer Aided Verification (CAV\u201997), pages 48\u201359. Springer-Verlag, 1997. LNCS 1254."},{"key":"15_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0055036","volume-title":"Proceedings of the 25th International Colloquium on Automata, Languages and Programming (ICALP 1998)","author":"Y. Kesten","year":"1998","unstructured":"Y. Kesten, A. Pnueli, and L. Raviv. Algorithmic verification of linear temporal properties. In Proceedings of the 25th International Colloquium on Automata, Languages and Programming (ICALP 1998), pages 1\u201316. Springer-Verlag, 1998. LNCS 1443."},{"key":"15_CR15","first-page":"16","volume":"51","author":"E. Kindler","year":"1996","unstructured":"E. Kindler and W. Reisig. Algebraic system nets for modeling distributed algorithms. Petri Net Newsletter, 51:16\u201331, 1996.","journal-title":"Petri Net Newsletter"},{"key":"15_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/3-540-69108-1_19","volume-title":"Proceedings of the International Conference on Application and Theory of Petri Nets 1998 (ICAPTN\u201998)","author":"E. Kindler","year":"1998","unstructured":"E. Kindler and H. V\u00f6lzer. Flexibility in algebraic nets. In Proceedings of the International Conference on Application and Theory of Petri Nets 1998 (ICAPTN\u201998), pages 345\u2013364. Springer-Verlag, 1998. LNCS 1420."},{"key":"15_CR17","volume-title":"Computer-Aided Verfication of Coordinating Processes: The Automata-Theoretic Approach","author":"R.P. Kurshan","year":"1994","unstructured":"R.P. Kurshan. Computer-Aided Verfication of Coordinating Processes: The Automata-Theoretic Approach. Princeon University Press, Princeton, New Jersey, 1994."},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"T. Latvala. Model checking linear temporal logic properties of Petri nets with fairness constraints. Research Report A67, Helsinki University of Technology, Jan 2001.","DOI":"10.1007\/3-540-45740-2_15"},{"issue":"1-4","key":"15_CR19","doi-asserted-by":"crossref","first-page":"175","DOI":"10.3233\/FI-2000-43123409","volume":"43","author":"T. Latvala","year":"2000","unstructured":"T. Latvala and K. Heljanko. Coping with strong fairness. Fundamenta Informaticae, 43(1-4):175\u2013193, 2000.","journal-title":"Fundamenta Informaticae"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite state programs satisfy their linear specification. In Proceedings of the 12th ACM Symposium on Principles of Programming Languages, pages 97\u2013107, 1985.","DOI":"10.1145\/318593.318622"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"M. M\u00e4kel\u00e4. Maria: Modular reachability analyzer for algebraic system nets. On-line documentation, 1999. http:\/\/www.tcs.hut.fi\/maria .","DOI":"10.1007\/978-1-4615-4493-7_53"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The temporal logic of programs. In Proceedings of 18th IEEE Symposium on Foundation of Computer Science, pages 46\u201357, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"J.P. Quielle and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proceedings of the 5th International Symposium on Programming, pages 337\u2013350, 1981.","DOI":"10.1007\/3-540-11494-7_22"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"M. Rauch Henzinger and J.A. Telle. Faster algorithms for the nonemptiness of Streett automata and for communication protocol pruning. In Proceedings of the 5th Scandinavian Workshop on Algorithm Theory(SWAT\u201996), 1997.","DOI":"10.1007\/3-540-61422-2_117"},{"key":"15_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(91)90203-E","volume":"80","author":"W. Reisig","year":"1991","unstructured":"W. Reisig. Petri nets and algebraic specifications. Theoretical Computer Science, 80:1\u201334, March 1991.","journal-title":"Theoretical Computer Science"},{"key":"15_CR26","unstructured":"M. R\u00f6nkk\u00f6. A distributed object oriented implementation of an algorithm converting a LTL formula to a generalised B\u00fcchi automaton. On-line documentation, 1998. http:\/\/www.abo.fi\/%7Emronkko\/PROJECT\/LTL2BUCHI\/abstract.html ."},{"issue":"8","key":"15_CR27","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1109\/26.3772","volume":"36","author":"K. Sabnani","year":"1988","unstructured":"K. Sabnani. An algorithmic technique for protocol verification. IEEE Transactions on Communications, 36(8):235\u2013248, 1988.","journal-title":"IEEE Transactions on Communications"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"S. Safra. On the complexity of omega-automata. In 29th Annual Symposium on Foundations of Computer Science, pages 319\u2013327. IEEE, 1988.","DOI":"10.1109\/SFCS.1988.21948"},{"key":"15_CR29","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/3-540-44988-4_27","volume-title":"Proceedings of the 21st International Conference on Application and Theory of Petri Nets (ICATPN 2000)","author":"K. Schmidt","year":"2000","unstructured":"K. Schmidt. LoLA: A low level analyser. In Proceedings of the 21st International Conference on Application and Theory of Petri Nets (ICATPN 2000), pages 465\u2013474. Springer-Verlag, 2000. LNCS 1825."},{"issue":"3","key":"15_CR30","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"A.P. Sistla and E.M. Clarke. The complexity of propositional linear temporal logic. Journal of the Association for Computing Machinery, 32(3):733\u2013749, July 1985.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"M.A. Smith and N. Klarlund. Verification of a sliding window protocol using IOA and MONA. In Proceeding of the 20th Joint International Conference on Formal Methods for Distributed Systems and Communication Protocols (FORTE\/PSTV 2000), pages 19\u201334. Kluwer Academic Publishers, 2000.","DOI":"10.1007\/978-0-387-35533-7_2"},{"key":"15_CR32","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"Proceedings of the International Conference on Computer Aided Verification (CAV2000)","author":"F. Somenzio","year":"2000","unstructured":"F. Somenzio and R. Bloem. Efficient b\u00f6chi automata from LTL formulae. In Proceedings of the International Conference on Computer Aided Verification (CAV2000), pages 248\u2013263. Springer-Verlag, 2000. LNCS 1855."},{"key":"15_CR33","first-page":"99","volume":"11","author":"N.V. Stenning","year":"1976","unstructured":"N.V Stenning. A data transfer protocol. In Computer Networks, volume 11, pages 99\u2013110, 1976.","journal-title":"Computer Networks"},{"key":"15_CR34","first-page":"133","volume":"B","author":"W. Thomas","year":"1990","unstructured":"W. Thomas. Automata on infinite objects. In Handbook of Theoretical Computer Science, volume B, pages 133\u2013191. Elsevier, 1990.","journal-title":"Handbook of Theoretical Computer Science"},{"key":"15_CR35","first-page":"385","volume-title":"Handbook of Formal Languages","author":"W. Thomas","year":"1997","unstructured":"W. Thomas. Languages, automata and logic. In G Rozenberg and A Salomaa, editors, Handbook of Formal Languages, volume 3, pages 385\u2013455. Springer-Verlag, New York, 1997."},{"key":"15_CR36","series-title":"Lect Notes Comput Sci","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":"A. Valmari. The state explosion problem. In Lectures on Petri Nets I: Basic Models, pages 429\u2013528. Springer-Verlag, 1998. LNCS 1491."},{"key":"15_CR37","unstructured":"K. Varpaaniemi, J. Halme, K. Hiekkanen, and T. Pyssysalo. PROD reference manual. Technical Report 13, Helsinki University of Technology, 1995."},{"key":"15_CR38","doi-asserted-by":"crossref","unstructured":"P. Wolper. Expressing interesting properties of programs in propositional temporal logic. In Proceedings of the 13th ACM Symposium on Principles of Programming Languages, pages 184\u2013194, 1986.","DOI":"10.1145\/512644.512661"}],"container-title":["Lecture Notes in Computer Science","Applications and Theory of Petri Nets 2001"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45740-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,27]],"date-time":"2021-08-27T20:59:40Z","timestamp":1630097980000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45740-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540422525","9783540457404"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/3-540-45740-2_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}