Name
Abstract | ||
|---|---|---|
The propositional modal mu-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. |
Year | DOI | Venue |
|---|---|---|
2020 | 10.1134/S0361768820080137 | PROGRAMMING AND COMPUTER SOFTWARE |
DocType | Volume | Issue |
Journal | 46 | 8 |
ISSN | Citations | PageRank |
0361-7688 | 0 | 0.34 |
References | Authors | |
0 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yensen Limón | 1 | 0 | 0.34 |
| Everardo Bárcenas | 2 | 23 | 9.15 |
| Edgard Benítez-Guerrero | 3 | 9 | 10.06 |
| Guillermo Molero-Castillo | 4 | 0 | 0.34 |
| Alejandro Velázquez-Mena | 5 | 0 | 0.34 |