A Relational Encoding for a Clash-Free Subset of ASMs

Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Wolfgang Reif
Digital Printed Abstract View Cite
Type
Short Paper
Publication
5th International Conference on ASM, Alloy, B, TLA, VDM, and Z (ABZ'16)

Abstract

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.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{SchellhornEPR16,
  author       = {Gerhard Schellhorn and
                  Gidon Ernst and
                  J{\"{o}}rg Pf{\"{a}}hler and
                  Wolfgang Reif},
  editor       = {Michael J. Butler and
                  Klaus{-}Dieter Schewe and
                  Atif Mashkoor and
                  Mikl{\'{o}}s Bir{\'{o}}},
  title        = {A Relational Encoding for a Clash-Free Subset of ASMs},
  booktitle    = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 5th International
                  Conference, {ABZ} 2016, Linz, Austria, May 23-27, 2016, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {9675},
  pages        = {237--243},
  publisher    = {Springer},
  year         = {2016},
  url          = {https://doi.org/10.1007/978-3-319-33600-8\_15},
  doi          = {10.1007/978-3-319-33600-8\_15},
  timestamp    = {Tue, 07 May 2024 20:13:31 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/SchellhornEPR16.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'16

Related