PREG axiomatizer – a ground bisimilarity checker for GSOS with predicates. (English) Zbl 1344.68199
Corradini, Andrea (ed.) et al., Algebra and coalgebra in computer science. 4th international conference, CALCO 2011, Winchester, UK, August 30 – September 2, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22943-5/pbk). Lecture Notes in Computer Science 6859, 378-385 (2011).
Summary: PREG Axiomatizer is a tool used for proving strong bisimilarity between ground terms consisting of operations in the GSOS format extended with predicates. It automatically derives sound and ground-complete axiomatizations using a technique proposed by the authors of this paper. These axiomatizations are provided as input to the Maude system, which, in turn, is used as a reduction engine for provided ground terms. These terms are bisimilar if and only if their normal forms obtained in this fashion are equal. The motivation of this tool is the optimized handling of equivalence checking between complex ground terms within automated provers and checkers.
For the entire collection see [Zbl 1221.68011].
For the entire collection see [Zbl 1221.68011].
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 68Q55 | Semantics in the theory of computing |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
