Public announcement logic with distributed knowledge: expressivity, completeness and complexity. (English) Zbl 1310.03030
Summary: While dynamic epistemic logics with common knowledge have been extensively studied, dynamic epistemic logics with distributed knowledge have so far received far less attention. In this paper we study extensions of public announcement logic (PAL) with distributed knowledge, in particular their expressivity, axiomatisations and complexity. PAL extended only with distributed knowledge is not more expressive than standard epistemic logic with distributed knowledge. Our focus is therefore on PACD, the result of adding both common and distributed knowledge to PAL, which is more expressive than each of its component logics. We introduce an axiomatisation of PACD, which is not surprising: it is the combination of well-known axioms. The completeness proof, however, is not trivial, and requires novel combinations and extensions of techniques for dealing with S5 knowledge, distributed knowledge, common knowledge and public announcements at the same time. We furthermore show that PACD is decidable, more precisely that it is exptime-complete. This result also carries over to S5CD with common and distributed knowledge operators for all coalitions (and not only the grand coalition). Finally, we propose a notion of a trans-bisimulation to generalise certain results and give deeper insight into the proofs.
MSC:
| 03B42 | Logics of knowledge and belief (including belief change) |
Keywords:
public announcement logic; distributed knowledge; expressivity; completeness; decidability; computational complexity; unravelling; folding; trans-bisimulationReferences:
| [1] | Baltag, A., & Moss, L. (2004). Logics for epistemic programs. Synthese, 139, 165-224. · Zbl 1100.03010 · doi:10.1023/B:SYNT.0000024912.56773.5e |
| [2] | Baltag, A., Moss, L., & Solecki, S. (1998). The logic of public announcements, common knowledge, and private suspicions. In Procedings of TARK VII (pp. 43-56). · Zbl 1386.03019 |
| [3] | Blackburn, P., de Rijke, M., & Venema, Y. (2001). Modal logic. In Cambridge tracts in theoretical computer science (Vol. 53). · Zbl 0988.03006 |
| [4] | Fagin, R., Halpern, J., Moses, Y., & Vardi, M. (1995). Reasoning about Knowledge. MIT. · Zbl 0839.68095 |
| [5] | Fagin, R., Halpern, J., & Vardi, M. (1992). What can machines know? On the properties of knowledge in distributed systems. Journal of the ACM, 39(2), 328-376. · Zbl 0799.68179 · doi:10.1145/128749.150945 |
| [6] | Fischer, M. J., & Ladner, R. E. (1977). Propositional modal logic of programs. In Proceedings of STOC ’77 (pp. 286-294). New York: ACM. · Zbl 0373.02025 |
| [7] | Fischer, M. J., & Ladner, R. E. (1979). Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18(2), 194-211. · Zbl 0408.03014 · doi:10.1016/0022-0000(79)90046-1 |
| [8] | Gerbrandy, J. (1999) Bisimulations on planet kripke. Ph.D. thesis, ILLC. · Zbl 0759.68082 |
| [9] | Göller, S., Lohrey, M., & Lutz, C. (2007). PDL with intersection and converse is 2EXP-complete. In H. Seidl (Ed.), FOSSACS 2007, LNCS (Vol. 4423, pp. 198-212). Berlin: Springer. · Zbl 1180.03033 |
| [10] | Halpern, J., & Moses, Y. (1992). A guide to completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence, 54(3), 319-379. · Zbl 0762.68029 · doi:10.1016/0004-3702(92)90049-4 |
| [11] | Kooi, B., & van Benthem, J. (2004). Reduction axioms for epistemic actions. In Proceedings of AiML 2004 (pp. 197-211). · Zbl 0799.68179 |
| [12] | Ladner, R. E. (1977). The computational complexity of provability in systems of modal propositional logic. SIAM Journal on Computing, 6(3), 467-480. · Zbl 0373.02025 · doi:10.1137/0206033 |
| [13] | Lutz, C. (2005). PDL with intersection and converse is decidable. In L. Ong (Ed.), CSL 2005, LNCS (Vol. 3634, pp. 413-427). Berlin: Springer. · Zbl 1136.03316 |
| [14] | Lutz, C. (2006). Complexity and succinctness of public announcement logic. In Proceedings of AAMAS ’06 (pp. 137-143). New York: ACM. |
| [15] | Meyer, J. J., & van der Hoek, W. (1995). Epistemic logic for AI and computer science (Vol. 41). Cambridge: Cambridge University Press. · Zbl 0868.03001 · doi:10.1017/CBO9780511569852 |
| [16] | Plaza, J. (1989). Logics of public communications. In Proceedings of ISMIS ’89 (pp. 201-216). |
| [17] | Pratt, V. R. (1979). Models of program logics. In Proceedings of the 20th annual symposium on the foundations of computer science (FOCS’79) (pp. 115-122). |
| [18] | Roelofsen, F. (2007). Distributed knowledge. Journal of Applied Non-Classical Logics, 17(2), 255-273. · Zbl 1186.03032 · doi:10.3166/jancl.17.255-273 |
| [19] | van Benthem, J. (2006). Open problems in logical dynamics. In D. M. Gabbay, S. S. Goncharov, & M. Zakharyaschev (Eds.), Mathematical problems from applied logic I: Logics for the XXIst century (pp. 137-192). Berlin: Springer. · Zbl 1101.03018 |
| [20] | van Benthem, J. F. A. K. (1999). Update as relativization. ILLC (manuscript). |
| [21] | van Ditmarsch, H., van der Hoek, W., & Kooi, B. (2007). Dynamic epistemic logic. In Synthese library (Vol. 337). Springer. · Zbl 1156.03320 |
| [22] | van der Hoek, W., & Meyer, J. J. (1992). Making some issues of implicit knowledge explicit. International Journal of Foundations of Computer Science, 3(2), 193-224. · Zbl 0759.68082 · doi:10.1142/S0129054192000139 |
| [23] | van der Hoek, W., & Meyer, J. J. (1997). A complete epistemic logic for multiple agents: Combining distributed and common knowledge. In Epistemic logic and the theory of games and decisions (pp. 35-68). Dordrecht: Kluwer. · Zbl 0956.03022 |
| [24] | Wáng, Y. N., & Ågotnes, T. (2011). Public announcement logic with distributed knowledge. In Proceedings of LORI-III, LNCS (Vol. 6953, pp. 328-341). · Zbl 1298.03061 |
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.
