Publications

2000

• M. Spielmann. Model Checking Abstract State Machines and Beyond. In International Workshop on Abstract State Machines ASM 2000, LNCS, pp. 323–340. Springer, 2000.                                 
  Abstract   BibTeX

  We propose a systematic investigation of the (semi-) automatic verifiability of ASMs. As a first step, we put forward two verification problems concerning the correctness of ASMs and investigate the decidability and complexity of both problems.

  @inproceedings{Sp00a,
       author = {Marc Spielmann},
       booktitle = {{International Workshop on Abstract State Machines ASM 2000}},
       pages = {323--340},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Model Checking Abstract State Machines and Beyond}},
       url = {http://www.logic.rwth-aachen.de/pub/spielmann/asm00.ps},
       year = {2000},
  }
  

• M. Spielmann. Verification of Relational Transducers for Electronic Commerce. In 19th ACM Symposium on Principles of Database Systems PODS 2000, Dallas, pp. 92–93. ACM Press, 2000.                                 
  Abstract   BibTeX

  Motivated by recent work of Abiteboul, Vianu, Fordham, and Yesha [PODS`98] we investigate the verifiability of transaction protocols specifying the interaction of multiple parties via a network, where each party is equipped with an (active) database that participates in the interaction. Such transaction protocols typically occur in the context of electronic commerce applications and can be formalized as relational transducers. We introduce a class of powerful relational transducers based on Gurevich's abstract state machines and show that several verification problems related to electronic commerce applications can be solved for these transducers. Our approach is, in some sense, complementary to the approach in [PODS`98].

  @inproceedings{Sp00b,
       author = {Marc Spielmann},
       booktitle = {{19th ACM Symposium on Principles of Database Systems PODS 2000, Dallas}},
       pages = {92--93},
       publisher = {ACM Press},
       title = {{Verification of Relational Transducers for Electronic Commerce}},
       url = {http://www.logic.rwth-aachen.de/pub/spielmann/pods00.ps},
       year = {2000},
  }
  

1999

• E. Grädel and M. Spielmann. Logspace Reducibility via Abstract State Machines. In World Congress on Formal Methods (FM `99) (J. Wing, J. Woodcock, and J. Davies, Eds.), vol. 1709 of LNCS, pp. 1738–1757. Springer, 1999.                                 
  Abstract   BibTeX

  Logspace computable functions play an important role in many areas of computer science, most notably in complexity theory, where logspace computable functions constitute the standard notion of reducibility. However, logspace reductions are defined by means of Turing machines which work on bit-strings, whereas many problems arising in computer science are naturally viewed as problems on structures (e.g., graphs). Unfortunately, there is a problem with encoding structures as bit-strings. Often we do not want to distinguish between isomorphic structures. More precisely, we want to identify an instance of a problem with an isomorphism class of structures rather than with a single structure. But there is no known efficiently computable string-encoding of isomorphism classes of structures. The situation calls for a computation model that works directly on structures and does not distinguish between isomorphic structures. \par Here we present a notion of logspace reducibility among structures which is based on abstract state machines (ASM)–a computation model on structures that has the desired isomorphism-invariance property. Our reductions are logspace computable (due to the syntactic restrictions we impose on ASM-programs) and are equally expressive as the logic (FO+DTC) enriched with the ability to handle small sets. On ordered structures they precisely capture Logspace. Our work continues that of Blass, Gurevich and Shelah on the choiceless fragment of Ptime. Indeed, our reductions can be seen as the choiceless fragment of Logspace.

  @inproceedings{GrSp99,
       author = {Erich Gr{\"a}del and Marc Spielmann},
       booktitle = {{World Congress on Formal Methods (FM `99)}},
       editor = {J. Wing and J. Woodcock and J. Davies},
       pages = {1738--1757},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Logspace Reducibility via Abstract State Machines}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrSp-fm99.ps},
       volume = {1709},
       year = {1999},
  }
  

• M. Spielmann. Automatic Verification of Abstract State Machines. In Proceedings of 11th International Conference on Computer-Aided Verification (CAV `99), vol. 1633 of LNCS, pp. 431–442. Springer, 1999.                                 
  Abstract   BibTeX

  Abstract state machines (ASMs) provide the basis of a successful methodology for specification and verification of software and hardware systems. Nevertheless, computer aided verification of ASM-programs has not yet been well-developed. In this paper we try to shed some light on the limits of automatic verifiability of ASM-programs. We introduce a class of restricted ASM-programs, which are called nullary programs, and provide an algorithm that decides whether a given nullary program satisfies a given correctness property (expressible in a CTL$^*$-like temporal logic) on all inputs. Our decision algorithm runs in PSPACE and we show that this is optimal. We also show that straightforward generalizations of nullary programs cannot be verified algorithmically, as some basic verification problems become undecidable.

  @inproceedings{Sp99,
       author = {Marc Spielmann},
       booktitle = {{Proceedings of 11th International Conference on Computer-Aided Verification (CAV `99)}},
       pages = {431--442},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Automatic Verification of Abstract State Machines}},
       url = {http://www.logic.rwth-aachen.de/pub/spielmann/cav99.ps},
       volume = {1633},
       year = {1999},
  }
  

1997

• Y. Gurevich and M. Spielmann. Recursive Abstract State Machines. JUCS, vol. 3(4), pp. 233–246, 1997.                                 
  Abstract   BibTeX

  According to the ASM thesis, any algorithm is essentially a Gurevich abstract state machine. The only objection to this thesis, at least in its sequential version, has been that ASMs do not capture recursion properly. To this end, we suggest recursive ASMs.

  @article{GuSp97,
       author = {Yuri Gurevich and Marc Spielmann},
       journal = {JUCS},
       number = {4},
       pages = {233--246},
       title = {{Recursive Abstract State Machines}},
       url = {http://www.logic.rwth-aachen.de/pub/spielmann/jucs97.ps},
       volume = {3},
       year = {1997},
  }