Выполнимость мю-исчисления с арифметическими ограничениями
Йенсен ЛИМОН-ПРИЕГО,
Исмаэль Эверардо БАРСЕНАС-ПАТИНЬО,
Эдгард Иван БЕНЕТЕС-ГЕРРЕРО,
Гильермо Хильберто МОЛЕРО-КАСТИЛЬО,
Алехандро ВЕЛАСКЕС-МЕНА https://doi.org/10.15514/ISPRAS-2021-33(2)-12
Аннотация
Пропозициональное модальное µ-исчисление является хорошо известным языком спецификаций систем помеченных переходов. В этой работе мы изучаем расширение этой логики с помощью обратных модальностей и арифметических ограничений Пресбургера, интерпретируемых на древовидных моделях. Мы описываем алгоритм выполнимости, основанный на построении по уровням моделей Фишера-Ларднера. Также сообщается о совместном выполнении нескольких экспериментов. Кроме того, мы описываем применение алгоритма для решения задач статического анализа полуструктурированных данных.
Об авторах
Йенсен ЛИМОН-ПРИЕГО
Университет Веракрузана
Мексика
Мексика
Кандидат наук
Исмаэль Эверардо БАРСЕНАС-ПАТИНЬО
Университет Веракрузана
Мексика
Мексика
Кандидат наук, доцент
Эдгард Иван БЕНЕТЕС-ГЕРРЕРО
Университет Веракрузана
Россия
Россия
Кандидат наук, профессор
Гильермо Хильберто МОЛЕРО-КАСТИЛЬО
Национальный автономный университет Мексики
Мексика
Мексика
Кандидат наук, доцент
Алехандро ВЕЛАСКЕС-МЕНА
Университет Веракрузана
Мексика
Мексика
Магистр, доцент
Список литературы
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.
Рецензия
Для цитирования:
ЛИМОН-ПРИЕГО Й., БАРСЕНАС-ПАТИНЬО И., БЕНЕТЕС-ГЕРРЕРО Э., МОЛЕРО-КАСТИЛЬО Г., ВЕЛАСКЕС-МЕНА А. Выполнимость мю-исчисления с арифметическими ограничениями. Труды Института системного программирования РАН. 2021;33(2):191-200. https://doi.org/10.15514/ISPRAS-2021-33(2)-12
For citation:
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
Послать статью по эл. почте 