Abstract
Modal logic S5 is useful in various applications of artificial intelligence. In recent years, the advance in solving the satisfiability problem of S5 has allowed many large S5 formulas to be solved within a few minutes. In this context, a new challenge arises: how to generate a minimal S5 Kripke model efficiently? The minimal model generation can be useful for tasks such as model checking and debugging of logical specifications. This paper presents several efficient SAT-based methods and provides a symmetry-breaking technique for the minimal model generation problem of S5. Extensive experiments demonstrate that our methods are good at tackling many large instances and achieve state-of-the-art performances. We find that a minimal model of a large S5 formula is usually very small, and we analyze this phenomenon via a graph model. Due to this characteristic, our incremental method performs best in most cases, and we believe that it is more suitable for minimal S5 Kripke model generation.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
S5cheetah and benchmarks: http://www.square16.org/tools/s5cheetah/.
- 2.
- 3.
S52SAT 2.0. is not available at moment. So, we compare with S52SAT 1.0 as reference. http://www.cril.univ-artois.fr/%7emontmirail/s52SAT/v2/index.html.
- 4.
References
Abate, P., Goré, R., Widmann, F.: Cut-free single-pass tableaux for the logic of common knowledge. In: Workshop on Agents and Deduction at TABLEAUX. vol. 2007. Citeseer (2007)
Aguilera, J.P., Fernández-Duque, D.: Verification logic: an arithmetical interpretation for negative introspection. In: Advances in Modal Logic 11, proceedings of the 11th conference on Advances in Modal Logic, held in Budapest, Hungary, August 30 - September 2, 2016. pp. 1–20 (2016)
Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, 11–17 July 2009, pp. 399–404 (2009)
Balsiger, P., Heuerding, A., Schwendimann, S.: A benchmark method for the propositional modal logics k, kt, S4. J. Autom. Reason. 24(3), 297–317 (2000)
Bienvenu, M., Fargier, H., Marquis, P.: Knowledge compilation in the modal logic S5. In: Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2010, Atlanta, Georgia, USA, July 11–15, 2010 (2010)
Caridroit, T., Lagniez, J., Berre, D.L., de Lima, T., Montmirail, V.: A SAT-based approach for solving the modal logic S5-satisfiability problem. In: Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, 4–9 February 2017, San Francisco, California, USA. pp. 3864–3870 (2017)
Chu, Y., Luo, C., Cai, S., You, H.: Empirical investigation of stochastic local search for maximum satisfiability. Frontiers Comput. Sci. 13(1), 86–98 (2019). https://doi.org/10.1007/s11704-018-7107-z
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.: Reasoning about knowledge. MIT press, Cambridge (2004)
Fitting, M.: A simple propositional S5 tableau system. Ann. Pure Appl. Log. 96(1–3), 107–115 (1999)
Fitting, M.: Modality and databases. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS (LNAI), vol. 1847, pp. 19–39. Springer, Heidelberg (2000). https://doi.org/10.1007/10722086_2
Goranko, V., Otto, M.: Model theory of modal logic. In: Handbook of Modal Logic, pp. 249–329 (2007)
Grossi, D., Rey, S.: Credulous acceptability, poison games and modal logic. In: Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2019, Montreal, QC, Canada, 13–17 May 2019, pp. 1994–1996 (2019)
Hella, L., et al.: Weak models of distributed computing, with connections to modal logic. Distrib. Comput. 28(1), 31–53 (2013). https://doi.org/10.1007/s00446-013-0202-3
Huang, P., Liu, M., Wang, P., Zhang, W., Ma, F., Zhang, J.: Solving the satisfiability problem of modal logic S5 guided by graph coloring. In: Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, 10–16 August 2019. pp. 1093–1100 (2019)
Ignatiev, A., Morgado, A., Marques-Silva, J.: RC2: an efficient maxsat solver. J. Satisf. Boolean Model. Comput. 11(1), 53–64 (2019)
Ladner, R.E.: The computational complexity of provability in systems of modal propositional logic. SIAM J. Comput. 6(3), 467–480 (1977)
Lagniez, J.-M., Le Berre, D., de Lima, T., Montmirail, V.: An assumption-based approach for solving the minimal S5-satisfiability problem. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 1–18. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94205-6_1
Leuştean, I., Moangă, N., Şerbănuţă, T.F.: Operational semantics and program verification using many-sorted hybrid modal logic. In: Cerrito, S., Popescu, A. (eds.) TABLEAUX 2019. LNCS (LNAI), vol. 11714, pp. 446–476. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-29026-9_25
Massacci, F.: Design and results of the tableaux-99 non-classical (Modal) systems comparison. In: Murray, N.V. (ed.) TABLEAUX 1999. LNCS (LNAI), vol. 1617, pp. 14–18. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48754-9_2
Niveau, A., Zanuttini, B.: Efficient representations for the modal logic S5. In: Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, 9–15 July 2016. pp. 1223–1229 (2016)
Papacchini, F., Schmidt, R.A.: A tableau calculus for minimal modal model generation. Electron. Notes Theor. Comput. Sci. 278, 159–172 (2011)
Papacchini, F., Schmidt, R.A.: Terminating minimal model generation procedures for propositional modal logics. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 381–395. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08587-6_30
Patel-Schneider, P.F., Sebastiani, R.: A new general method to generate random modal formulae for testing decision procedures. J. Artif. Intell. Res. 18, 351–389 (2003)
Soto, M., Rossi, A., Sevaux, M.: Three new upper bounds on the chromatic number. Discret. Appl. Math. 159(18), 2281–2289 (2011)
Wan, H., Yang, R., Fang, L., Liu, Y., Xu, H.: A complete epistemic planner without the epistemic closed world assumption. In: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, 25–31 July 2015. pp. 3257–3263 (2015)
Acknowledgements
This work has been supported by the National Natural Science Foundation of China (NSFC) under grant No.61972384 and the Key Research Program of Frontier Sciences, Chinese Academy of Sciences under grant number QYZDJ-SSW-JSC036. Feifei Ma is also supported by the Youth Innovation Promotion Association CAS under grant No. Y202034. The authors would like to thank the anonymous reviewers for their comments and suggestions.
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Huang, P., Li, R., Liu, M., Ma, F., Zhang, J. (2021). Efficient SAT-Based Minimal Model Generation Methods for Modal Logic S5. In: Li, CM., Manyà, F. (eds) Theory and Applications of Satisfiability Testing – SAT 2021. SAT 2021. Lecture Notes in Computer Science(), vol 12831. Springer, Cham. https://doi.org/10.1007/978-3-030-80223-3_16
Download citation
DOI: https://doi.org/10.1007/978-3-030-80223-3_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-80222-6
Online ISBN: 978-3-030-80223-3
eBook Packages: Computer ScienceComputer Science (R0)