This work aims to investigate conditions under which program analysis can be viewed as algebraically solving equations involving terms of subclasses of Kleene algebras and variables. In this paper, we show how to solve a kind of linear equations in which variables appear only on one side of the equality sign, over a*-continuous action lattice. Furthermore, based on the method developed for solving equations, we present how model checking of a restricted version of the linear μ-calculus over finite traces can be done by algebraic manipulations. Finally, we give some ideas on how to extend the resolution method to other classes of equations and algebraic structures. © 2008 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Ktari, B., Lajeunesse-Robert, F., & Bolduc, C. (2008). Solving linear equations in*-continuous action lattices. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4988 LNCS, pp. 289–303). Springer Verlag. https://doi.org/10.1007/978-3-540-78913-0_22
Mendeley helps you to discover research relevant for your work.