Mu-Calculus Satisfiability with Arithmetic Constraints
Yensen LIMÓN-PRIEGO,
Ismael Everardo BÁRCENAS-PATIÑO,
Edgard Iván BENÍTEZ-GUERRERO,
Guillermo Gilberto MOLERO-CASTILLO,
Alejandro VELAZQUEZ-MENA https://doi.org/10.15514/ISPRAS-2021-33(2)-12
Abstract
The propositional modal μ-calculus is a well-known specification language for labeled transition systems. In this work, we study an extension of this logic with converse modalities and Presburger arithmetic constraints, interpreted over tree models. We describe a satisfiability algorithm based on breadth-first construction of Fischer-Lardner models. An implementation together several experiments are also reported. Furthermore, we also describe an application of the algorithm to solve static analysis problems over semi-structured data.
About the Authors
Yensen LIMÓN-PRIEGO
Universidad Veracruzana
Mexico
Mexico
Ph. D.
Ismael Everardo BÁRCENAS-PATIÑO
National Autonomous University of Mexico
Mexico
Mexico
Ph. D. in Computer Science, Assistant Professor
Edgard Iván BENÍTEZ-GUERRERO
Universidad Veracruzana
Russian Federation
Russian Federation
Ph. D. in Computer Science, Full-time Professor
Guillermo Gilberto MOLERO-CASTILLO
National Autonomous University of Mexico
Mexico
Mexico
Ph.D. in Information Technologies, Associate Professor
Alejandro VELAZQUEZ-MENA
National Autonomous University of Mexico
Mexico
Mexico
Master of Science, Associate Professor
References
1. P. A. Bonatti, C. Lutz, A. Murano, and M. Y. Vardi. The complexity of enriched mu-calculi. Logical Methods in Computer Science, vol. 4, no. 3, 2008, pp. 1-27.
2. E. Bárcenas and J. Lavalle. Global numerical constraints on trees. Logical Methods in Computer Science, vol. 10, no. 2, 2014, pp. 1-28.
3. E. Bárcenas, E. Benı́tez-Guerrero, J. Lavalle, and G. Molero-Castillo. Presburger constraints on tree. Computación y Sistemas, vol. 24, no. 1, 2020, pp. 281-303.
4. Y. Limón, E. Bárcenas, E. Benı́tez-Guerrero, G. Molero-Castillo, and A. Velázquez-Mena. A satisfiability algorithm for the mu-calculus for trees with presburger constraint. In Proc. of the 7th International Conference in Software Engineering Research and Innovation (CONISOFT), 2019, pp. 72-79.
5. S. Demri and D. Lugiez. Complexity of modal logics with Presburger constraints. Journal of Applied Logic, vol. 8, no. 3, 2010, pp. 233–252.
6. H. Seidl, T. Schwentick, and A. Muscholl. Counting in trees. In Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas, vol. 2. Amsterdam University Press, 2008, pp. 575-612.
7. H. Seidl, T. Schwentick, and A. Muscholl. Numerical document queries. In Proc. of the 22nd ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 2003, pp. 155-166.
8. L. de Moura and N. Bjørner. Z3: An efficient SMT solver. Lecture Notes in Computer Science, vol. 4963, 2008, pp. 337-340.
9. K. Hoder, N. Bjørner, and L. de Moura. µz – an efficient engine for fixed points with constraints. Lecture Notes in Computer Science, vol. 6806, 2011, pp. 457-462.
10. W. Conradie, Y. Fomatati, A. Palmigiano, and S. Sourabh. Algorithmic correspondence for intuitionistic modal mu-calculus. Theoretical Computer Science, vol. 564, 2015, pp. 30-62.
11. M. Biehl, N. Klarlund, and T. Rauhe. Mona: Decidable arithmetic in practice. Lecture Notes in Computer Science, vol. 1135, 1996, pp. 459-462.
12. P. Genevès, N. Layaı̈da, and A. Schmitt. Efficient static analysis of XML paths and types. In Proc. of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2007, pp. 342-351.
13. Y. Limón, E. Bárcenas, E. Benı́tez-Guerrero, and M. A. M. Nieto. Depth-first reasoning on trees. Computación y Sistemas, vol. 22, no. 1, 2018, pp. 189-201.
14. M. Junedi, P. Genevès, and N. Layaı̈da. XML query-update independence analysis revisited. In Proc. of the ACM Symposium on Document Engineering, 2012, pp. 95-98.
15. M. J. Fischer and R. E. Ladner. Propositional modal logic of programs. In Proc. of the ACM Symposium on Theory of Computing, 1977, pp. 286-294.
16. The World Wide Web Consortium (W3C), XPath 2.0 W3C Recommendation, 2010.
17. К.Ю. Лисовский. Разработка XML-приложений на языке Scheme. Программирование, том 28, no. 4, 2002 г., стр. 20-32 / K.Yu. Lisovsky. XML applications development in Scheme. Programming and Computer Software, vol. 28, no. 4, 2002, pp. 197–206.
18. Y. Limón, E. Bárcenas, E. Benı́tez-Guerrero, and G. Molero. On the consistency of context-aware systems. Journal of Intelligent and Fuzzy Systems, vol. 34, no. 5, 2018, pp. 3373–3383.
19. И.В. Машечкин, М.И. Петровский, Д.В. Царев, М.Н. Чикунов. Методы машинного обучения для задачи обнаружения и мониторинга экстремистской информации в сети Интернет. Программирование, том 45, no. 3, 2019 г., стр. 18-37 / I.V. Mashechkin, M.I. Petrovskiy, D.V. Tsarev, and M.N. Chikunov. Machine learning methods for detecting and monitoring extremist information on the Internet. Programming and Computer Software, vol. 45, no. 3, 2019, pp. 99–115.
Review
For citations:
LIMÓN-PRIEGO Ye., BÁRCENAS-PATIÑO I., BENÍTEZ-GUERRERO E., MOLERO-CASTILLO G., VELAZQUEZ-MENA A. Mu-Calculus Satisfiability with Arithmetic Constraints. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2021;33(2):191-200. (In Russ.) https://doi.org/10.15514/ISPRAS-2021-33(2)-12
Email this article 