{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:10:07Z","timestamp":1775873407441,"version":"3.50.1"},"reference-count":47,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":1837,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2009,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We study satisfiability and infinite-state model checking in ICPDL, which extends Propositional Dynamic Logic (PDL) with intersection and converse operators on programs. The two main results of this paper are that (i) satisfiability is in 2\u0395\u03a7\u03a1\u03a4\u0399\u039c\u0395, thus 2\u0395\u03a7\u03a1\u03a4\u0399\u039c\u0395-complete by an existing lower bound, and (ii) infinite-state model checking of basic process algebras and pushdown systems is also 2\u0395\u03a7\u03a1\u03a4\u0399\u039c\u0395-complete. Both upper bounds are obtained by polynomial time computable reductions to \u03c9-regular tree satisfiability in ICPDL, a reasoning problem that we introduce specifically for this purpose. This problem is then reduced to the emptiness problem for alternating two-way automata on infinite trees. Our approach to (i) also provides a shorter and more elegant proof of Danecki's difficult result that satisfiability in IPDL is in 2\u0395\u03a7\u03a1\u03a4\u0399\u039c\u0395. We prove the lower bound(s) for infinite-state model checking using an encoding of alternating Turing machines.<\/jats:p>","DOI":"10.2178\/jsl\/1231082313","type":"journal-article","created":{"date-parts":[[2009,1,4]],"date-time":"2009-01-04T15:18:44Z","timestamp":1231082324000},"page":"279-314","source":"Crossref","is-referenced-by-count":17,"title":["PDL with intersection and converse: satisfiability and infinite-state model checking"],"prefix":"10.1017","volume":"74","author":[{"family":"Stefan G\u00f6ller","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Markus","family":"Lohrey","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carsten","family":"Lutz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200003832_ref047","unstructured":"W\u00f6hrle Stefan , Decision problems over infinite graphs: Higher-order pushdown systems and synchronized products, Dissertation, RWTH, Aachen, 2005."},{"key":"S0022481200003832_ref046","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2894"},{"key":"S0022481200003832_ref045","first-page":"127","volume-title":"Proceedings of the 20th conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2000), New Delhi, India","author":"Walukiewicz","year":"2000"},{"key":"S0022481200003832_ref043","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15648-8_31"},{"key":"S0022481200003832_ref042","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(86)90026-7"},{"key":"S0022481200003832_ref041","doi-asserted-by":"publisher","DOI":"10.1145\/860575.860608"},{"key":"S0022481200003832_ref039","doi-asserted-by":"publisher","DOI":"10.1007\/11562948_3"},{"key":"S0022481200003832_ref037","volume-title":"Proceedings of the 26th ACM symposium on Principles of Database Systems (PODS 2007)","author":"Cate"},{"key":"S0022481200003832_ref035","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(80)90061-6"},{"key":"S0022481200003832_ref034","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90133-2"},{"key":"S0022481200003832_ref033","first-page":"281","volume-title":"Dynamic logic for reasoning about actions and agents","author":"Meyer","year":"2000"},{"key":"S0022481200003832_ref032","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00101-8"},{"key":"S0022481200003832_ref028","first-page":"1072","volume":"70","author":"Lange","year":"2005","journal-title":"2-Exp Time lower bounds for propositional dynamic logics with intersection"},{"key":"S0022481200003832_ref026","first-page":"36","volume-title":"Proceedings of the 12th international conference on Computer Aided Verification (CAV 2000), Chicago, USA","author":"Kupferman","year":"2000"},{"key":"S0022481200003832_ref024","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0012782"},{"key":"S0022481200003832_ref021","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00151-7"},{"key":"S0022481200003832_ref020","first-page":"198","volume-title":"Proceedings of the 10th international conference on Foundations of Software Science and Computational Structures (FoSSaCS 2007)","author":"G\u00f6ller","year":"2007"},{"key":"S0022481200003832_ref029","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00306-6"},{"key":"S0022481200003832_ref031","doi-asserted-by":"publisher","DOI":"10.3166\/jancl.15.189-213"},{"key":"S0022481200003832_ref013","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5803.001.0001","volume-title":"Reasoning about knowledge","author":"Fagin","year":"1995"},{"key":"S0022481200003832_ref040","volume-title":"A complete epistemic logic for multiple agents\u2014combining distributed and common knowledge","author":"van der Hoek","year":"1997"},{"key":"S0022481200003832_ref023","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic logic","author":"Harel","year":"2000"},{"key":"S0022481200003832_ref005","article-title":"Uniform solution of parity games on prefix-recognizable graphs","volume":"68","author":"Cachat","year":"2002","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"S0022481200003832_ref019","first-page":"349","volume-title":"Proceedings of the 20th international conference on Computer Science Logic (CSL 2006, Szeged, Hungary","author":"G\u00f6ller","year":"2006"},{"key":"S0022481200003832_ref008","volume-title":"Model checking","author":"Clarke","year":"2000"},{"key":"S0022481200003832_ref025","first-page":"371","volume-title":"Proceedings of the 14th international conference on Computer Aided Verification CAV 2002, Copenhagen, Denmark","volume":"2404","author":"Kupferman","year":"2002"},{"key":"S0022481200003832_ref016","first-page":"67","volume-title":"Models, algebras, and proofs: selected papers of the X Latin American symposium on mathematical logic held in Bogota","volume":"203","author":"Flum","year":"1999"},{"key":"S0022481200003832_ref015","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90046-1"},{"key":"S0022481200003832_ref006","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00089-5"},{"key":"S0022481200003832_ref036","volume-title":"Theory of recursive functions and effective computability","author":"Rogers","year":"1968"},{"key":"S0022481200003832_ref027","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2005.08.002"},{"key":"S0022481200003832_ref038","doi-asserted-by":"publisher","DOI":"10.1145\/1142351.1142398"},{"key":"S0022481200003832_ref014","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90046-5"},{"key":"S0022481200003832_ref022","first-page":"51","article-title":"Recurring dominoes: making the highly undecidable highly understandable","volume":"24","author":"Harel","year":"1985","journal-title":"Annals of Discrete Mathematics"},{"key":"S0022481200003832_ref012","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00139-1"},{"key":"S0022481200003832_ref030","first-page":"413","volume-title":"Proceedings of the 19th international workshop on Computer Science Logic (CSL 2005), Oxford, UK","author":"Lutz","year":"2005"},{"key":"S0022481200003832_ref044","first-page":"628","volume-title":"Proceedings of the 25th International Colloquium on Automata, Languages and Programming (1CALP '98), Aalborg, Denmar","author":"Vardi","year":"1998"},{"key":"S0022481200003832_ref004","volume-title":"The description logic handbook: Theory, implementation and applications","author":"Baader","year":"2003"},{"key":"S0022481200003832_ref003","doi-asserted-by":"publisher","DOI":"10.1145\/1075382.1075387"},{"key":"S0022481200003832_ref002","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/13.6.939"},{"key":"S0022481200003832_ref001","doi-asserted-by":"publisher","DOI":"10.3166\/jancl.15.115-135"},{"key":"S0022481200003832_ref007","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322243"},{"key":"S0022481200003832_ref009","first-page":"34","volume-title":"Proceedings of the 5th Symposium on Computation Theory (Zaborow, Poland)","author":"Danecki","year":"1984"},{"key":"S0022481200003832_ref010","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030342"},{"key":"S0022481200003832_ref011","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0017477"},{"key":"S0022481200003832_ref017","first-page":"205","volume-title":"Proceedings of the 12th national conference on Artifical Intelligence (AAAI '94)","author":"de giacomo","year":"1994"},{"key":"S0022481200003832_ref018","doi-asserted-by":"publisher","DOI":"10.1007\/11874683_23"}],"container-title":["The Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200003832","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,6]],"date-time":"2025-02-06T18:31:47Z","timestamp":1738866707000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200003832\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,3]]},"references-count":47,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2009,3]]}},"alternative-id":["S0022481200003832"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1231082313","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,3]]}}}