{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T06:10:08Z","timestamp":1736662208844,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540499947"},{"type":"electronic","value":"9783540499954"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11944836_24","type":"book-chapter","created":{"date-parts":[[2006,11,28]],"date-time":"2006-11-28T04:48:02Z","timestamp":1164689282000},"page":"248-259","source":"Crossref","is-referenced-by-count":3,"title":["On Decidability of LTL Model Checking for Process Rewrite Systems"],"prefix":"10.1007","author":[{"given":"Laura","family":"Bozzelli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mojm\u00edr","family":"K\u0159et\u00ednsk\u00fd","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vojt\u011bch","family":"\u0158eh\u00e1k","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Strej\u010dek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"24_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"CONCUR\u201997: Concurrency Theory","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243, pp. 135\u2013150. Springer, Heidelberg (1997)"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1007\/3-540-61604-7_71","volume-title":"CONCUR \u201996: Concurrency Theory","author":"A. Bouajjani","year":"1996","unstructured":"Bouajjani, A., Habermehl, P.: Constrained properties, semilinear systems, and petri nets. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol.\u00a01119, pp. 481\u2013497. Springer, Heidelberg (1996)"},{"key":"#cr-split#-24_CR3.1","doi-asserted-by":"crossref","unstructured":"Bozzelli, L., K\u0159et\u00ednsk\u00fd, M., \u0158eh\u00e1k, V., Strej\u010dek, J.: On Decidability of LTL Model Checking for Weakly Extended Process Rewrite Systems. Technical Report FIMU-RS-2006-05, Faculty of Informatics, Masaryk University, Brno (2006);","DOI":"10.1007\/11944836_24"},{"key":"#cr-split#-24_CR3.2","unstructured":"A full version of the paper presented at FSTTCS 2006"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-540-30579-8_19","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L. Bozzelli","year":"2005","unstructured":"Bozzelli, L.: Model checking for process rewrite systems and a class of action-based regular properties. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 282\u2013297. Springer, Heidelberg (2005)"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/BFb0017477","volume-title":"Trees in Algebra and Programming - CAAP \u201994","author":"J. Esparza","year":"1994","unstructured":"Esparza, J.: On the decidability of model checking for several mu-calculi and petri nets. In: Tison, S. (ed.) CAAP 1994. LNCS, vol.\u00a0787, pp. 115\u2013129. Springer, Heidelberg (1994)"},{"key":"24_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1007\/3-540-63139-9_32","volume-title":"Application and Theory of Petri Nets 1997","author":"P. Habermehl","year":"1997","unstructured":"Habermehl, P.: On the complexity of the linear-time \u03bc-calculus for Petri nets. In: Az\u00e9ma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol.\u00a01248, pp. 102\u2013116. Springer, Heidelberg (1997)"},{"key":"24_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-28644-8_23","volume-title":"CONCUR 2004 - Concurrency Theory","author":"M. K\u0159et\u00ednsk\u00fd","year":"2004","unstructured":"K\u0159et\u00ednsk\u00fd, M., \u0158eh\u00e1k, V., Strej\u010dek, J.: Extended process rewrite systems: Expressiveness and reachability. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 355\u2013370. Springer, Heidelberg (2004)"},{"key":"24_CR8","series-title":"ENTCS","first-page":"75","volume-title":"Proceedings of INFINITY 2003","author":"M. K\u0159et\u00ednsk\u00fd","year":"2004","unstructured":"K\u0159et\u00ednsk\u00fd, M., \u0158eh\u00e1k, V., Strej\u010dek, J.: On extensions of process rewrite systems: Rewrite systems with weak finite-state unit. In: Proceedings of INFINITY 2003. ENTCS, vol.\u00a098, pp. 75\u201388. Elsevier, Amsterdam (2004)"},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/11590156_17","volume-title":"FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science","author":"M. K\u0159et\u00ednsk\u00fd","year":"2005","unstructured":"K\u0159et\u00ednsk\u00fd, M., \u0158eh\u00e1k, V., Strej\u010dek, J.: Reachability of hennessy-milner properties for weakly extended PRS. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol.\u00a03821, pp. 213\u2013224. Springer, Heidelberg (2005)"},{"key":"24_CR10","unstructured":"Lipton, R.: The reachability problem is exponential-space hard. Technical Report\u00a062, Department of Computer Science, Yale University (1976)"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"Maidl, M.: The common fragment of CTL and LTL. In: Proc. 41st Annual Symposium on Foundations of Computer Science, pp. 643\u2013652 (2000)","DOI":"10.1109\/SFCS.2000.892332"},{"issue":"3","key":"24_CR12","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1137\/0213029","volume":"13","author":"E.W. Mayr","year":"1984","unstructured":"Mayr, E.W.: An algorithm for the general Petri net reachability problem. SIAM Journal on Computing\u00a013(3), 441\u2013460 (1984)","journal-title":"SIAM Journal on Computing"},{"key":"24_CR13","unstructured":"Mayr, R.: Decidability and Complexity of Model Checking Problems for Infinite-State Systems. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (1998)"},{"issue":"1","key":"24_CR14","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1006\/inco.1999.2826","volume":"156","author":"R. Mayr","year":"2000","unstructured":"Mayr, R.: Process rewrite systems. Information and Computation\u00a0156(1), 264\u2013286 (2000)","journal-title":"Information and Computation"},{"key":"24_CR15","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)"},{"key":"24_CR16","volume-title":"Computation: Finite and Infinite Machines","author":"M.L. Minsky","year":"1967","unstructured":"Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall, Englewood Cliffs (1967)"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc.\u00a018th IEEE Symposium on the Foundations of Computer Science, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"24_CR18","unstructured":"Strej\u010dek, J.: Linear Temporal Logic: Expressiveness and Model Checking. PhD thesis, Faculty of Informatics, Masaryk University in Brno (2004)"}],"container-title":["Lecture Notes in Computer Science","FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11944836_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T05:02:38Z","timestamp":1736658158000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11944836_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540499947","9783540499954"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/11944836_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}