{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:22:53Z","timestamp":1725664973973},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540631415"},{"type":"electronic","value":"9783540691884"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63141-0_18","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:09:15Z","timestamp":1330297755000},"page":"258-272","source":"Crossref","is-referenced-by-count":13,"title":["On the complexity of verifying concurrent transition systems"],"prefix":"10.1007","author":[{"given":"David","family":"Harel","sequence":"first","affiliation":[]},{"given":"Orna","family":"Kupferman","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"issue":"2","key":"18_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253\u2013284, 1991.","journal-title":"Theoretical Computer Science"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"A. Aziz, V. Singhal, F. Balarin, R. Brayton, and A.L. Sangiovanni-Vincentelli. Equivalences for fair kripke structures. In Proc. 21st ICALP, Jerusalem, 1994.","DOI":"10.1007\/3-540-58201-0_82"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"S. Bensalem, A. Bouajjani, C. Loiseaux, and J. Sifakis. Property preserving simulations. In Proc. 4th CAV, LNCS 663, Montreal, 1992.","DOI":"10.1007\/3-540-56496-9_21"},{"issue":"6","key":"18_CR4","doi-asserted-by":"crossref","first-page":"638","DOI":"10.1007\/BF03180566","volume":"4","author":"J. Balcazar","year":"1992","unstructured":"J. Balcazar, J. Gabarro, and M. Santha. Deciding bisimilarity is P-complete. Formal Aspects of Computing, 4(6):638\u2013648, 1992.","journal-title":"Formal Aspects of Computing"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"O. Bemholtz, M.Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. In Proc. 6th CAV, LNCS 818, pages 142\u2013155, Stanford, 1994.","DOI":"10.1007\/3-540-58179-0_50"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"E.M. Clarke and O. Grumberg and D. Long. Verification tools for finite-state concurrent systems. In Decade of Concurrency-Reflections and Perspectives,LNCS 803, pages 124\u2013175, 1993.","DOI":"10.1007\/3-540-58043-3_19"},{"issue":"1","key":"18_CR7","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"A.K. Chandra","year":"1981","unstructured":"A.K. Chandra, D.C. Kozen, and L.J. Stockmeyer. Alternation. Journal of the Association for Computing Machinery, 28(1):114\u2013133, January 1981.","journal-title":"Journal of the Association for Computing Machinery"},{"issue":"3","key":"18_CR8","doi-asserted-by":"crossref","first-page":"517","DOI":"10.1145\/176584.176587","volume":"41","author":"D. Drusinsky","year":"1994","unstructured":"D. Drusinsky and D. Harel. On the power of bounded concurrency I: Finite automata. Journal of the ACM, 41(3):517\u2013539, 1994.","journal-title":"Journal of the ACM"},{"issue":"3","key":"18_CR9","doi-asserted-by":"crossref","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"O. Grumberg and D.E. Long. Model checking and modular verification. ACM Trans. on Programming Languages and Systems, 16(3):843\u2013871, 1994.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"18_CR10","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"D. Harel. Statecharts: A visual formalism for complex systems. Sci. Comp. Prog., 8:231\u2013274, 1987.","journal-title":"Sci. Comp. Prog."},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"D. Harel. A thesis for bounded concurrency. In Proc. 14th MFOCS, LNCS 379, pages 35\u201348, New York, 1989.","DOI":"10.1007\/3-540-51486-4_55"},{"key":"18_CR12","volume-title":"Algebraic theory of Processes","author":"M. Hennessy","year":"1985","unstructured":"M. Hennessy. Algebraic theory of Processes. MIT Press, Cambridge, 1985."},{"issue":"3","key":"18_CR13","doi-asserted-by":"crossref","first-page":"540","DOI":"10.1145\/176584.176588","volume":"41","author":"T. Hirst","year":"1994","unstructured":"T. Hirst and D. Harel. On the power of bounded concurrency II: Pushdown automata. Journal of the ACM, 41(3):540\u2013554, 1994.","journal-title":"Journal of the ACM"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"D. Harel, R. Rosner, and M.Y. Vardi. On the power of bounded concurrency iii: Reasoning about programs. In Proc. 5th LICS, Philadelphia, 1990.","DOI":"10.1109\/LICS.1990.113770"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"D. Kozen. Lower bounds for natural proof systems. In Proc. 18th FOCS, pages 254\u2013266, 1977.","DOI":"10.1109\/SFCS.1977.16"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan. Computer Aided Verification of Coordinating Processes. Princeton Univ. Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"O. Kupferman and M.Y. Vardi. Verification of fair transition systems. In Proc. 8th CAV, LNCS 1102, pages 372\u2013382. Rutgers, 1996.","DOI":"10.1007\/3-540-61474-5_84"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proc. 12th POPL, pages 97\u2013107, New Orleans, 1985.","DOI":"10.1145\/318593.318622"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"D. Lehman, A. Pnueli, and J. Stavi. Impartiality, justice, and fairness \u2014the ethics of concurrent termination. In Proc. 8th ICALP, LNCS 115, pages 264\u2013277. 1981.","DOI":"10.1007\/3-540-10843-2_22"},{"key":"18_CR20","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1109\/TSE.1984.5010246","volume":"10","author":"S.S. Lam","year":"1984","unstructured":"S.S. Lam and A.U. Shankar. Protocol verification via projection. IEEE Trans. on Software Engineering, 10:325\u2013342, 1984.","journal-title":"IEEE Trans. on Software Engineering"},{"key":"18_CR21","unstructured":"R. Milner. An algebraic definition of simulation between programs. In Proc. 2nd IJCAl, pages 481\u2013489, 1971."},{"key":"18_CR22","volume-title":"LNCS 92","author":"R. Milner","year":"1980","unstructured":"R. Milner. A Calculus of Communicating Systems, LNCS 92, Springer Verlag, Berlin, 1980."},{"key":"18_CR23","volume-title":"Communication and Concurrecny","author":"R. Milner","year":"1989","unstructured":"R. Milner. Communication and Concurrecny. Prentice-Hall, Englewood Clifs, 1989."},{"key":"18_CR24","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, Berlin, January 1992."},{"key":"18_CR25","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A.P. Sistla","year":"1987","unstructured":"A.P. Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for B\u00fcchi automata with applications to temporal logic. Theoretical Computer Science, 49:217\u2013237, 1987.","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"18_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1\u201337, November 1994.","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","CONCUR '97: Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63141-0_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T11:35:35Z","timestamp":1640950535000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63141-0_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631415","9783540691884"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-63141-0_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}