Abstraction reduces the problem of whether an infinite state system satisfies a temporal logic property to model checking that property on a finite state abstract version. The most common abstractions are quotients of the original system. We present a simple method of defining quotient abstractions by means of equations collapsing the set of states. Our method yields the minimal quotient system together with a set of proof obligations that guarantee its executability and can be discharged with tools such as those in the Maude formal environment.
CITATION STYLE
Meseguer, J., Palomino, M., & Martí-Oliet, N. (2003). Equational abstractions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2741, pp. 2–16). Springer Verlag. https://doi.org/10.1007/978-3-540-45085-6_2
Mendeley helps you to discover research relevant for your work.