Open AccessMu-Calculus Satisfiability with Arithmetic Constraints
Author(s) -
Йенсен Лимон-Приего,
Исмаэль Эверардо Барсенас-Патиньо,
Эдгард Иван Бенетес-Герреро,
Гильермо Хильберто Молеро-Кастильо,
Алехандро Веласкес-Мена
Publication year - 2021
Publication title -
trudy instituta sistemnogo programmirovaniâ ran/trudy instituta sistemnogo programmirovaniâ
Language(s) - English
Resource type - Journals
eISSN - 2220-6426
pISSN - 2079-8156
DOI - 10.15514/ispras-2021-33(2)-12
Subject(s) - satisfiability , converse , presburger arithmetic , modal logic , computer science , propositional calculus , extension (predicate logic) , calculus (dental) , algorithm , modal , programming language , mathematics , theoretical computer science , decidability , medicine , chemistry , geometry , dentistry , polymer chemistry
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.