Model checking propositional dynamic logic with all extras

Kozen, 1990, Logics of programs, 789 Harel, 2000 Harel, 1984, Dynamic logic, 497 Fischer, 1979, Propositional dynamic logic of regular programs, J. Comput. System Sci., 18, 194, 10.1016/0022-0000(79)90046-1 Vardi, 1986, Automata-theoretic techniques for modal logic of programs, J. Comput. System Sci., 32, 183, 10.1016/0022-0000(86)90026-7 J.-J.C. Meyer, Dynamic logic reasoning about actions and agents, in: Proc. Workshop on Logic-Based Artificial Intelligence, Washington, DC, USA, 1999 Spalazzi, 2000, A dynamic logic for acting, sensing, and planning, J. Logic Comput., 10, 787, 10.1093/logcom/10.6.787 van Harmelen, 1992, (ML)2: A formal language for KADS models of expertise, Knowledge Acquisition, 4, 127, 10.1016/1042-8143(92)90017-U Fensel, 1995 van Ditmarsch, 2003, Concurrent dynamic epistemic logic for MAS, 201 Giacomo, 1994, Boosting the correspondence between description logics and propositional dynamic logics, 205 Streett, 1981, Propositional dynamic logic of looping and converse, 375 Harel, 1985, Recurring dominoes: Making the highly undecidable highly understandable, Ann. Discrete Math., 24, 51 Harel, 1983, Propositional dynamic logic of nonregular programs, J. Comput. System Sci., 26, 222, 10.1016/0022-0000(83)90014-4 Pratt, 1979, Models of program logics, 115 Streett, 1982, Propositional dynamic logic of looping and converse is elementarily decidable, Inform. Control, 54, 121, 10.1016/S0019-9958(82)91258-X Vardi, 1985, The taming of converse: Reasoning about two-way computations, vol. 193, 413 Danecki, 1984, Nondeterministic propositional dynamic logic with intersection is decidable, vol. 208, 34 Lange, 2005, A lower complexity bound for propositional dynamic logic with intersection, vol. 5 K. Striegnitz, Model checking for contextual reasoning in NLG, in: P. Blackburn, M. Kohlhase (Eds.), Proc. of Inference in Computational Semantics, ICoS-3, 2001, pp. 101–115 Bertini, 2003, Model checking for detection of sport highlights, 215 van der Hoek, 2002, Model checking knowledge and time, vol. 2318, 95 Penczek, 2003, Verifying epistemic properties of multi-agent systems via bounded model checking, Fundamenta Informatica, 55, 167 1996 Strassen, 1969, Gaussian elimination is not optimal, Numer. Math., 13, 354, 10.1007/BF02165411 Warshall, 1962, A theorem on boolean matrices, J. ACM, 9, 11, 10.1145/321105.321107 Tarski, 1955, A lattice-theoretical fixpoint theorem and its application, Pacific J. Math., 5, 285, 10.2140/pjm.1955.5.285 Chandra, 1981, Alternation, J. ACM, 28, 114, 10.1145/322234.322243 Greibach, 1965, A new normal form theorem for context-free phrase structure grammars, J. ACM, 12, 42, 10.1145/321250.321254 Ibarra, 1992, A characterization of exponential-time languages by alternating context-free grammars, TCS, 99, 301, 10.1016/0304-3975(92)90355-J Okhotin, 2001, Conjunctive grammars, J. Automata Lang. Combin., 6, 519 Mayer, 1996, The complexity of PDL with interleaving, TCS, 161, 109, 10.1016/0304-3975(95)00095-X