TY - GEN
T1 - Equational abstractions
AU - Meseguer, José
AU - Palomino, Miguel
AU - Martí-Oliet, Narciso
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2003.
PY - 2003
Y1 - 2003
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=7044268976&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=7044268976&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-45085-6_2
DO - 10.1007/978-3-540-45085-6_2
M3 - Conference contribution
AN - SCOPUS:7044268976
SN - 3540405593
SN - 9783540405597
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 2
EP - 16
BT - Automated Deduction - CADE-19 - 19th International Conference on Automated Deduction, Proceedings
A2 - Baader, Franz
PB - Springer
T2 - 19th International Conference on Automated Deduction, CADE 2003
Y2 - 28 July 2003 through 2 August 2003
ER -