×

PDL with intersection and converse: Satisfiability and infinite-state model checking. (English) Zbl 1181.03034

M. J. Fischer and R. E. Ladner [“Propositional dynamic logic of regular programs”, J. Comput. Syst. Sci. 18, 194–211 (1979; Zbl 0408.03014)] introduced Propositional Dynamic Logic (PDL) as a formalism to reason about programs. PDL consists of two types of objects: properties (interpreted as sets of states) and programs (interpreted as binary relations on states). A PDL formula is interpreted at some state of a transition system (i.e. a vertex of a graph). Programs appear in formulas inside the modal operators \(\langle\;\rangle\) and \([\;]\), a formula \(\langle p\rangle\varphi\) being satisfied at state \(q\) if there is a \(q'\) satisfying \(\varphi\) such that \(p(q,q')\) (i.e. an execution of \(p\) from state \(q\) to \(q'\)). Similarly \([p]\) is satisfied at state \(q\) if all \(q'\) such that \(p(q,q')\) satisfy \(\varphi\). Programs are built up using union, composition, iteration (Kleene star) and test (interpreted as the set of \((q,q)\) such that \(q\) satisfies some PDL formula).
This paper considers PDL extended with two additional program operators: converse (C) and intersection (I), denoted as ICPDL. The authors consider satisfiability, which is the question of the existence of a transition system satisfying some formula, and infinite-state model checking, which is whether some (possibly infinite) transition system satisfies some formula.
They first show that satisfiability in ICPDL is in 2EXPTIME, and so, by a result of M. Lange and C. Lutz [“2-ExpTime lower bounds for propositional dynamic logics with intersection”, J. Symb. Log. 70, No. 4, 1072–1086 (2005; Zbl 1100.03017)], it is 2EXPTIME-complete. The proof consists of three parts. In the first one, it is shown that a satisfiable ICPDL formula is satisfied by a transition system of tree width (a graph-theoretic notion, which measures how “far” a graph is from being a tree) at most two. In the second part, satisfiability of ICPDL is reduced to satisfiability by a tree accepted by a two-way alternating parity automaton (TWAPTA, see [M. Y. Vardi, Lect. Notes Comput. Sci. 1443, 628–641 (1998; Zbl 0909.03019)]). Finally, the last step is to reduce this last problem to non-emptiness for TWAPTAs.
Their second main result shows that model-checking pushdown systems (PDS) and basic process algebras (BPA) (PDSs with a single state) is 2EXPTIME-complete. The upper bound is shown using the previous results on satisfiability by a tree accepted by a two-way alternating parity automaton. The lower bound is proved by extending a technique from [I. Walukiewicz, Lect. Notes Comput. Sci. 1974, 127–138 (2000; Zbl 1044.68111)].
Furthermore, the authors also consider satisfiability for PDL extended with a loop-construct (a construct to express that a program starts and ends in the same state), which they show below to EXPTIME. Finally, satisfiability in ICPDL (in fact already in IPDL) extended with program negation (set complementation of the program) is undecidable (in fact \(\Sigma_1^1\)-complete).

MSC:

03B70 Logic in computer science
03D05 Automata and formal grammars in connection with logical questions
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
68Q25 Analysis of algorithms and problem complexity
68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] DOI: 10.1016/0022-0000(86)90026-7 · Zbl 0622.03017 · doi:10.1016/0022-0000(86)90026-7
[2] Proceedings of the 19th international Colloquium on Trees in Algebra and Programming (CAAP ’94), Edinburgh, U.K. pp 115– (1994)
[3] Proceedings of the 2nd international joint conference on Autonomous Agents and Multiagent Systems (AAMAS 2002) pp 201– (2003)
[4] A complete epistemic logic for multiple agents–combining distributed and common knowledge (1997)
[5] Proceedings of the 5th Symposium on Computation Theory (Zaborow, Poland) pp 34– (1984)
[6] Model checking (2000)
[7] Proceedings of the 3rd international symposium on Automated Technology for Verification and Analysis (ATVA 2005), Taipei, Taiwan pp 3– (2005)
[8] DOI: 10.1145/322234.322243 · Zbl 0473.68043 · doi:10.1145/322234.322243
[9] Proceedings of the twenty-fifth ACM SIGACT-S1GMOD-SIGART symposium on Principles of Database Systems [PODS 2006) pp 328– (2006)
[10] Theoretical Computer Science 290 pp 79– (2002)
[11] Proceedings of the 26th ACM symposium on Principles of Database Systems (PODS 2007)
[12] Electronic Notes in Theoretical Computer Science 68 (2002)
[13] Theory of recursive functions and effective computability (1968)
[14] The description logic handbook: Theory, implementation and applications (2003) · Zbl 1058.68107
[15] DOI: 10.1145/1075382.1075387 · Zbl 05459217 · doi:10.1145/1075382.1075387
[16] DOI: 10.1016/0022-0000(80)90061-6 · Zbl 0424.03010 · doi:10.1016/0022-0000(80)90061-6
[17] DOI: 10.1093/logcom/13.6.939 · Zbl 1093.68032 · doi:10.1093/logcom/13.6.939
[18] DOI: 10.1016/0304-3975(87)90133-2 · Zbl 0636.68108 · doi:10.1016/0304-3975(87)90133-2
[19] DOI: 10.3166/jancl.15.115-135 · Zbl 1185.03056 · doi:10.3166/jancl.15.115-135
[20] Dynamic logic for reasoning about actions and agents pp 281– (2000)
[21] DOI: 10.1016/S0304-3975(00)00101-8 · Zbl 0973.68169 · doi:10.1016/S0304-3975(00)00101-8
[22] DOI: 10.3166/jancl.15.189-213 · Zbl 1185.03058 · doi:10.3166/jancl.15.189-213
[23] Proceedings of the 19th international workshop on Computer Science Logic (CSL 2005), Oxford, UK pp 413– (2005)
[24] DOI: 10.1016/S0304-3975(00)00306-6 · Zbl 0992.68150 · doi:10.1016/S0304-3975(00)00306-6
[25] 2-Exp Time lower bounds for propositional dynamic logics with intersection 70 pp 1072– (2005)
[26] Journal of Applied Logic 4 pp 39– (2005)
[27] Proceedings of the 12th international conference on Computer Aided Verification (CAV 2000), Chicago, USA pp 36– (2000)
[28] Proceedings of the 14th international conference on Computer Aided Verification CAV 2002, Copenhagen, Denmark 2404 pp 371– (2002) · Zbl 0993.00049
[29] DOI: 10.1007/BFb0012782 · doi:10.1007/BFb0012782
[30] Dynamic logic (2000) · Zbl 0976.68108
[31] Annals of Discrete Mathematics 24 pp 51– (1985)
[32] DOI: 10.1016/S0304-3975(01)00151-7 · Zbl 1061.03022 · doi:10.1016/S0304-3975(01)00151-7
[33] Proceedings of the 10th international conference on Foundations of Software Science and Computational Structures (FoSSaCS 2007) pp 198– (2007)
[34] Proceedings of the 20th international conference on Computer Science Logic (CSL 2006, Szeged, Hungary pp 349– (2006)
[35] Infinite state model-checking of propositional dynamic logics (2006) · Zbl 1225.68116
[36] Proceedings of the 12th national conference on Artifical Intelligence (AAAI ’94) pp 205– (1994)
[37] Models, algebras, and proofs: selected papers of the X Latin American symposium on mathematical logic held in Bogota 203 pp 67– (1999)
[38] DOI: 10.1016/0022-0000(79)90046-1 · Zbl 0408.03014 · doi:10.1016/0022-0000(79)90046-1
[39] DOI: 10.1006/inco.2000.2894 · Zbl 1003.68072 · doi:10.1006/inco.2000.2894
[40] DOI: 10.1016/0304-3975(85)90046-5 · Zbl 0565.68032 · doi:10.1016/0304-3975(85)90046-5
[41] Proceedings of the 20th conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2000), New Delhi, India pp 127– (2000)
[42] Reasoning about knowledge (1995) · Zbl 0839.68095
[43] Proceedings of the 25th International Colloquium on Automata, Languages and Programming (1CALP ’98), Aalborg, Denmar pp 628– (1998)
[44] DOI: 10.1016/S0890-5401(03)00139-1 · Zbl 1078.68081 · doi:10.1016/S0890-5401(03)00139-1
[45] Proceedings of logics of programs pp 413– (1985)
[46] Proceedings of Mathematical Foundations of Computer Science 1984 (MFCS 1984) pp 573– (1984)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.