Knowledge forgetting in propositional \(\mu\)-calculus. (English) Zbl 07644141
Summary: The \(\mu\)-calculus is one of the most important logics describing specifications of transition systems. It has been extensively explored for formal verification in model checking due to its exceptional balance between expressiveness and algorithmic properties. From the perspective of systems/knowledge evolving, one may want to discard some atoms (elements) that become irrelevant or unnecessary in a specification; one may also need to know what makes something true, or the minimal condition under which something holds. This paper aims to address these scenarios for \(\mu\)-calculus in terms of knowledge forgetting. In particular, it proposes a notion of forgetting based on a generalized bisimulation and explores the semantic and logical properties of forgetting, including some reasoning complexity results. It also shows that forgetting can be employed to perform knowledge update.
MSC:
| 68Txx | Artificial intelligence |
References:
| [1] | Emerson, E.A.: Model checking and the μ-calculus. In: Immerman, N., Kolaitis, P.G. (eds.) Descriptive Complexity and Finite Models, Proceedings of a DIMACS Workshop 1996, Princeton, New Jersey, USA, January 14-17, 1996. DIMACS Series in Discrete Mathematics and Theoretical Computer Science. doi:10.1090/dimacs/031/06, vol. 31, pp 185-214 (1996) · Zbl 0877.03020 |
| [2] | Feng, R., Acar, E., Schlobach, S., Wang, Y., Liu, W.: On sufficient and necessary conditions in bounded CTL: a forgetting approach. In: Calvanese, D., Erdem, E., Thielscher, M. (eds.) Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020, Rhodes, Greece, September 12-18, 2020, pp. 361-370. doi:10.24963/kr.2020/37 (2020) |
| [3] | Dijkstra, EW, Guarded commands, nondeterminacy and formal derivation of programs, Commun. ACM, 18, 8, 453-457 (1975) · Zbl 0308.68017 · doi:10.1145/360933.360975 |
| [4] | Lin, F., Reiter, R.: Forget it!. In: Proceedings of the AAAI Fall Symposium on Relevance, New Orleans, US, pp 154-159 (1994) |
| [5] | Lin, F., On strongest necessary and weakest sufficient conditions, Artif. Intell., 128, 1-2, 143-159 (2001) · Zbl 0971.68127 · doi:10.1016/S0004-3702(01)00070-4 |
| [6] | Lang, J.; Liberatore, P.; Marquis, P., Propositional independence: Formula-variable independence and forgetting, J. Artif. Intell. Res., 18, 391-443 (2003) · Zbl 1056.68112 · doi:10.1613/jair.1113 |
| [7] | Su, K., Lv, G., Zhang, Y.: Reasoning about knowledge by variable forgetting. In: Dubois, D., Welty, C.A., Williams, M. (eds.) Principles of Knowledge Representation and Reasoning: Proceedings of the Ninth International Conference (KR2004), Whistler, Canada, June 2-5, 2004, pp. 576-586. http://www.aaai.org/Library/KR/2004/kr04-060.php (2004) |
| [8] | Baral, C.; Zhang, Y., Knowledge updates: Semantics and complexity issues, Artif. Intell., 164, 1-2, 209-243 (2005) · Zbl 1132.68720 · doi:10.1016/j.artint.2005.01.005 |
| [9] | Zhang, Y.; Zhou, Y., Knowledge forgetting: Properties and applications, Artif. Intell., 173, 16-17, 1525-1537 (2009) · Zbl 1187.03015 · doi:10.1016/j.artint.2009.07.005 |
| [10] | Fang, L.; Liu, Y.; Van Ditmarsch, H., Forgetting in multi-agent modal logics, Artif. Intell., 266, 51-80 (2019) · Zbl 1478.68351 · doi:10.1016/j.artint.2018.08.003 |
| [11] | Konev, B., Walther, D., Wolter, F.: Forgetting and uniform interpolation in large-scale description logic terminologies. In: IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, pp. 830-835 (2009) |
| [12] | Lutz, C., Wolter, F.: Foundations for uniform interpolation and forgetting in expressive description logics. In: Walsh, T. (ed.) IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, Barcelona, Catalonia, Spain, July 16-22, 2011, pp. 989-995. doi:10.5591/978-1-57735-516-8/IJCAI11-170(2011) |
| [13] | Zhao, Y., Schmidt, R.A., Wang, Y., Zhang, X., Feng, H.: A practical approach to forgetting in description logics with nominals. In: Proceedings of the AAAI Conference on Artificial Intelligence, pp. 3073-3079. https://aaai.org/ojs/index.php/AAAI/article/view/5702 (2020) |
| [14] | Eiter, T.; Wang, K., Semantic forgetting in answer set programming, Artif. Intell., 172, 14, 1644-1672 (2008) · Zbl 1184.68159 · doi:10.1016/j.artint.2008.05.002 |
| [15] | Wang, Y., Wang, K., Zhang, M.: Forgetting for answer set programs revisited. In: Rossi, F. (ed.) IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013, pp. 1162-1168. http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/6807 (2013) |
| [16] | Wang, Y.; Zhang, Y.; Zhou, Y.; Zhang, M., Knowledge forgetting in answer set programming, J. Artif. Intell. Res., 50, 31-70 (2014) · Zbl 1442.68228 · doi:10.1613/jair.4297 |
| [17] | Wang, Y., Wang, K., Wang, Z., Zhuang, Z.: Knowledge forgetting in circumscription: A preliminary report. In: Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, January 25-30, 2015, Austin, Texas, USA., pp. 1649-1655. http://www.aaai.org/ocs/index.php/AAAI/AAAI15/paper/view/9866(2015) |
| [18] | Delgrande, J.P., Wang, K.: A syntax-independent approach to forgetting in disjunctive logic programs. In: Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, January 25-30, 2015, Austin, Texas, USA., pp. 1482-1488. http://www.aaai.org/ocs/index.php/AAAI/AAAI15/paper/view/9555 (2015) |
| [19] | Gonçalves, R.; Knorr, M.; Leite, J.; Woltran, S., On the limits of forgetting in answer set programming, Artif. Intell., 286, 103307 (2020) · Zbl 1493.68350 · doi:10.1016/j.artint.2020.103307 |
| [20] | Maksimova, L., Temporal logics of “the next” do not have the beth property, Journal of Applied Non-Classical Logics, 1, 73-76 (1991) · Zbl 0914.03024 · doi:10.1080/11663081.1991.10510772 |
| [21] | Wolper, P., Temporal logic can be more expressive, Information and Control, 56, 1-2, 72-99 (1983) · Zbl 0534.03009 · doi:10.1016/S0019-9958(83)80051-5 |
| [22] | Katsuno, H., Mendelzon, A.O.: On the difference between updating a knowledge base and revising it. In: Allen, J.F., Fikes, R., Sandewall, E. (eds.) Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR’91). Cambridge, MA, USA, April 22-25, 1991, pp. 387-394 (1991) · Zbl 0765.68197 |
| [23] | Hoare, CAR, An axiomatic basis for computer programming, Commun. ACM, 12, 10, 576-580 (1969) · Zbl 0179.23105 · doi:10.1145/363235.363259 |
| [24] | Woodcock, J., Morgan, C.: Refinement of state-based concurrent systems. In: Bjørner, D., Hoare, C.A.R., Langmaack, H. (eds.) VDM ’90, VDM and Z - Formal Methods in Software Development, Third International Symposium of VDM Europe, Kiel, FRG, April 17-21, 1990, Proceedings. Lecture Notes in Computer Science, vol. 428, pp. 340-351. doi:10.1007/3-540-52513-0_18 (1990) |
| [25] | Legato, W.J.: A weakest precondition model for assembly language programs. April (2002) |
| [26] | Leino, KRM, Efficient weakest preconditions, Inf. Process. Lett., 93, 6, 281-288 (2005) · Zbl 1173.68563 · doi:10.1016/j.ipl.2004.10.015 |
| [27] | Dailler, S.; Hauzar, D.; Marché, C.; Moy, Y., Instrumenting a weakest precondition calculus for counterexample generation, J. Log. Algebraic Methods Program., 99, 97-113 (2018) · Zbl 1395.68097 · doi:10.1016/j.jlamp.2018.05.003 |
| [28] | Lin, F., Compiling causal theories to successor state axioms and STRIPS-like systems, J. Artif. Intell. Res., 19, 279-314 (2003) · Zbl 1026.68126 · doi:10.1613/jair.1135 |
| [29] | Doherty, P., Lukaszewicz, W., Szalas, A.: Computing strongest necessary and weakest sufficient conditions of first-order formulas. In: Nebel, B. (ed.) Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, IJCAI 2001, Seattle, Washington, USA, August 4-10, 2001, pp. 145-154 (2001) |
| [30] | Su, K.; Sattar, A.; Lv, G.; Zhang, Y., Variable forgetting in reasoning about knowledge, J. Artif. Intell. Res., 35, 677-716 (2009) · Zbl 1192.68677 · doi:10.1613/jair.2750 |
| [31] | Eiter, T., Kern-isberner, G.: A brief survey on forgetting from a knowledge representation and reasoning perspective, Künstliche Intell., 33, 1, 9-33 (2019) · doi:10.1007/s13218-018-0564-6 |
| [32] | Boole, G.: An Investigation of the Laws of Thought. (Reprinted by Dover Books, New York, 1954.) (1854) · Zbl 1528.68004 |
| [33] | Ackermann, W., Untersuchungen über das eliminationsproblem der mathematischen logik, Math. Ann., 110, 1, 390-413 (1935) · JFM 60.0022.01 · doi:10.1007/BF01448035 |
| [34] | Zhang, Y., Zhou, Y.: Forgetting revisited. In: Lin, F., Sattler, U., Truszczynski, M. (eds.) Principles of Knowledge Representation and Reasoning: Proceedings of the Twelfth International Conference, KR 2010, Toronto, Ontario, Canada, May 9-13, 2010. http://aaai.org/ocs/index.php/KR/KR2010/paper/view/1292 (2010) |
| [35] | Gabbay, D.M., Schmidt, R.A., Szalas, A.: Second-Order Quantifier Elimination - Foundations, Computational Aspects and Applications. Studies in logic : Mathematical logic and foundations, vol 12. http://collegepublications.co.uk/logic/mlf/?00009 (2008) · Zbl 1165.03011 |
| [36] | Visser, A.: Uniform interpolation and layered bisimulation. In: Gödel���96: Logical Foundations of Mathematics, Computer Science and Physics—Kurt GöDel’s Legacy, Brno, Czech Republic, August 1996, Proceedings, pp. 139-164 (1996) · Zbl 0854.03026 |
| [37] | Zhang, Y., Zhou, Y.: Properties of knowledge forgetting. In: Pagnucco, M., Thielscher, M (eds.) Proceedings of the Twelfth International Workshop on Non-Monotonic Reasoning, pp 68-75. Sydney, Australia (2008) |
| [38] | Wang, Z.; Wang, K.; Topor, RW; Pan, JZ, Forgetting for knowledge bases in dl-lite, Ann. Math. Artif. Intell., 58, 1-2, 117-151 (2010) · Zbl 1205.68410 · doi:10.1007/s10472-010-9187-9 |
| [39] | Konev, B.; Ludwig, M.; Walther, D.; Wolter, F., The logical difference for the lightweight description logic EL, J. Artif. Intell. Res., 44, 633-708 (2012) · Zbl 1253.68303 · doi:10.1613/jair.3552 |
| [40] | Zhao, Y., Schmidt, R.A.: Role forgetting for alcoqh(universal role)-ontologies using an ackermann-based approach. In: Sierra, C. (ed.) Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, pp. 1354-1361. doi:10.24963/ijcai.2017/188 (2017) |
| [41] | Zhang, Y.; Foo, NY, Solving logic program conflict through strong and weak forgettings, Artif. Intell., 170, 8-9, 739-778 (2006) · Zbl 1131.68037 · doi:10.1016/j.artint.2006.02.002 |
| [42] | Wong, K.-S.: Forgetting in Logic Programs. PhD thesis, The University of New South Wales (2009) |
| [43] | Delgrande, JP, A knowledge level account of forgetting, J. Artif. Intell. Res., 60, 1165-1213 (2017) · Zbl 1423.68488 · doi:10.1613/jair.5530 |
| [44] | Gonçalves, R., Knorr, M., Leite, J.: Forgetting in answer set programming - A survey. arXiv:abs/2107.07016 (2021) · Zbl 1403.68030 |
| [45] | D’Agostino, G., Hollenberg, M.: Uniform Interpolation, Automata and the Modal μ-Calculus. In: Kracht, M., De Rijke, M., Wansing, H., Zakharyaschev, M. (eds.) Advances in Modal Logic 1, Papers from the First Workshop on “Advances in Modal Logic,” Held in Berlin, Germany, 8-10 October 1996, pp 73-84 (1996) · Zbl 0906.03018 |
| [46] | Kozen, D., Results on the propositional mu-calculus, Theor. Comput. Sci., 27, 333-354 (1983) · Zbl 0553.03007 · doi:10.1016/0304-3975(82)90125-6 |
| [47] | D’Agostino, G.; Lenzi, G., On modal mu-calculus with explicit interpolants, J. Appl. Log., 4, 3, 256-278 (2006) · Zbl 1106.03024 · doi:10.1016/j.jal.2005.06.008 |
| [48] | Janin, D., Walukiewicz, I.: Automata for the modal μ-calculus and related results. In: Wiedermann, J., Hájek, P. (eds.) Mathematical Foundations of Computer Science 1995, 20th International Symposium, MFCS’95, Prague, Czech Republic, August 28 - September 1, 1995, Proceedings. Lecture Notes in Computer Science. doi:10.1007/3-540-60246-1_160, vol. 969, pp 552-562 (1995) · Zbl 1193.68163 |
| [49] | Bradfield, J.C., Walukiewicz, I.: The μ-calculus and model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. doi:10.1007/978-3-319-10575-8_26, pp 871-919 (2018) · Zbl 1392.68236 |
| [50] | D’Agostino, G.; Hollenberg, M., Logical questions concerning the μ-calculus: Interpolation, lyndon and los-tarski, J. Symb. Log., 65, 1, 310-332 (2000) · Zbl 0982.03011 · doi:10.2307/2586539 |
| [51] | Janin, D., Walukiewicz, I.: On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. In: International Conference on Concurrency Theory, pp. 263-277. Springer (1996) · Zbl 1514.68171 |
| [52] | Wang, Y.: On forgetting in tractable propositional fragments. arXiv:abs/1502.02799 (2015) |
| [53] | Hubert, C., Max, D., Remi, G., Florent, J., Denis, L., Christof, L., Sophie, T., Marc, T.: Tree Automata Techniques and Applications. https://jacquema.gitlabpages.inria.fr/files/tata.pdf (1997) |
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.
