Modal Extensions of the Logic of Abstract State Machines

Abstract

Based on the logic of non-deterministic Abstract State Machines (ASMs) we define a modal extension (\mathcal{M}\mathcal{L}{\text {ASM}})  by first introducing multi-step predicates and then adding quantification over the number of steps. We show that liveness conditions such as invariance, conditional and unconditional progress, and persistence on all or some runs of an ASM can be expressed in this logic. We show the existence of a complete fragment of (\mathcal{M}\mathcal{L}{\text {ASM}}), which still contains the interesting liveness conditions, and demonstrate the usefulness of this complete fragment by an example concerning mutual exclusion.

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{FerrarottiS24,
  author       = {Flavio Ferrarotti and
                  Klaus{-}Dieter Schewe},
  editor       = {Silvia Bonfanti and
                  Angelo Gargantini and
                  Michael Leuschel and
                  Elvinia Riccobene and
                  Patrizia Scandurra},
  title        = {Modal Extensions of the Logic of Abstract State Machines},
  booktitle    = {Rigorous State-Based Methods - 10th International Conference, {ABZ}
                  2024, Bergamo, Italy, June 25-28, 2024, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {14759},
  pages        = {123--140},
  publisher    = {Springer},
  year         = {2024},
  url          = {https://doi.org/10.1007/978-3-031-63790-2\_8},
  doi          = {10.1007/978-3-031-63790-2\_8},
  timestamp    = {Thu, 04 Jul 2024 22:05:23 +0200},
  biburl       = {https://dblp.org/rec/conf/zum/FerrarottiS24.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}