A Relational Encoding for a Clash-Free Subset of ASMs

Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Wolfgang Reif

This paper defines a static check for clash-freedom of ASM rules, including sequential and parallel composition, nondeterministic choice, and recursion. The check computes a formula that, if provable, makes a relational encoding of ASM rules possible, which is an important prerequisite for efficient deduction. The check is general enough to cover all sequential rules as well as many typical uses of parallel composition.
published 2016 Proc. of 5th International Conference ABZ 2016

Publisher: Springer


The final publication is available at Springer via

For questions regarding the publication, please contact!