×

Equational abstractions in rewriting logic and Maude. (English) Zbl 1335.68143

Braga, Christiano (ed.) et al., Formal methods: foundations and applications. 17th Brazilian symposium, SBMF 2014, Maceió, AL, Brazil, September 29 – October 1, 2014. Proceedings. Berlin: Springer (ISBN 978-3-319-15074-1/pbk). Lecture Notes in Computer Science 8941, 17-31 (2015).
Summary: Maude is a high-level language and high-performance system supporting both equational and rewriting computation for a wide range of applications. Maude also provides a model checker for linear temporal logic. The model-checking procedure can be used to prove properties when the set of states reachable from an initial state in a system is finite; when this is not the case, it may be possible to use an equational abstraction technique for reducing the size of the state space. 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 of the original infinite system. The most common abstractions are quotients of the original system. We present a simple method for defining quotient abstractions by means of equations identifying states. Our method yields the minimal quotient system together with a set of proof obligations that guarantee its executability, which can be discharged with tools such as those available in the Maude formal environment. The proposed method will be illustrated by means of detailed examples.
For the entire collection see [Zbl 1330.68018].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
68N15 Theory of programming languages
68Q42 Grammars and rewriting systems
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007) · Zbl 1115.68046
[2] Durán, F.; Meseguer, J., On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories, Journal of Logic and Algebraic Programming, 81, 7-8, 816-850 (2012) · Zbl 1272.03139 · doi:10.1016/j.jlap.2011.12.004
[3] Durán, F.; Rocha, C.; Álvarez, JM; Agha, G.; Danvy, O.; Meseguer, J., Towards a Maude Formal Environment, Formal Modeling: Actors, Open Systems, Biological Systems, 329-351 (2011), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-24933-4_17
[4] Giesl, J.; Demri, S.; Kapur, D.; Weidenbach, C., Proving termination of programs automatically with \({\sf AProVE}\), Automated Reasoning, 184-191 (2014), Heidelberg: Springer, Heidelberg · Zbl 1409.68256 · doi:10.1007/978-3-319-08587-6_13
[5] Meseguer, J.; Palomino, M.; Martí-Oliet, N., Equational abstractions, Theoretical Computer Science, 403, 2-3, 239-264 (2008) · Zbl 1155.68050 · doi:10.1016/j.tcs.2008.04.040
[6] Meseguer, J.; Palomino, M.; Martí-Oliet, N., Algebraic simulations, Journal of Logic and Algebraic Programming, 79, 2, 103-143 (2010) · Zbl 1184.68300 · doi:10.1016/j.jlap.2009.07.003
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.