Publications

2004

• A. Nowack. Slicing Abstract State Machines. In Abstract State Machines – Advances in Theory and Practice, vol. 3052 of LNCS. Springer, 2004.                                 
  Abstract   BibTeX

  In this work, we introduce slicing for Abstract State Machines (ASMs). The idea of this concept is analogous to the one of program slicing which is an established technique for extracting statements from a program that are relevant for its behaviour at a given point of interest. These statements form again a syntactically correct program called a slice. Previous work has focused on programming languages that differ substantially from ASMs. Although the concept of program slicing does not directly extend to ASMs, it is possible to find an analogous concept for ASMs. We present such an approach.

  In spite of the fact that a minimal slice is not computable in the general case, we identify an expressive class of ASMs for which a minimal (static) slice is computable (and prove the computability). This basic result can be extended in several ways. We present some extensions to larger classes of ASMs and other variants for the notion of slicing.

  @inproceedings{Nowack04a,
       author = {Antje Nowack},
       booktitle = {{Abstract State Machines -- Advances in Theory and Practice}},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Slicing Abstract State Machines}},
       url = {http://www.logic.rwth-aachen.de/pub/nowack/asm04.ps},
       volume = {3052},
       year = {2004},
  }
  

• A. Nowack. A Guarded Fragment for Abstract State Machines. In Proceedings of the ESSLLI 2004 Workshop on Guarded Fragments, 2004.                                 
  Abstract   BibTeX

  Abstract State Machines (ASMs) provide a formal method for transparent design and specification of complex dynamic systems. They combine advantages of informal and formal methods.

  Applications motivate a number of computability and decidability problems connected to ASMs. Such problems result for example from the area of verifying properties of ASMs. Their high expressive power leads rather directly to undecidability respectively uncomputability results for most interesting problems in the case of unrestricted ASMs. Consequently, it is rather natural to ask whether there exist expressive classes of ASMs for which we can prove positive decidability and computability results.

  In this work, we introduce such a class of ASMs. The idea of this class is the same as for the guarded fragment of first-order logic. We analyse the expressive power of this class and prove that it is stronger than Datalog LITE and the guarded fragment of first-order fixed point logic. Some decidability and computability results have been proven in earlier works.

  @inproceedings{Nowack04b,
       author = {Antje Nowack},
       booktitle = {{Proceedings of the ESSLLI 2004 Workshop on Guarded Fragments}},
       title = {{A Guarded Fragment for Abstract State Machines}},
       url = {http://www.logic.rwth-aachen.de/pub/nowack/GuardedASMs.ps},
       year = {2004},
  }
  

2003

• E. Grädel and A. Nowack. Quantum Computing and Abstract State Machines. In Abstract State Machines – Advances in Theory and Applications, vol. 2589 of LNCS, pp. 309 – 323. Springer, 2003.             
  BibTeX

  @inproceedings{GraedelNo03,
       author = {Erich Gr{\"a}del and Antje Nowack},
       booktitle = {{Abstract State Machines -- Advances in Theory and Applications}},
       pages = {309 -- 323},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Quantum Computing and Abstract State Machines}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrNo-asm03.ps},
       volume = {2589},
       year = {2003},
  }
  

• A. Nowack. Deciding the Verification Problem for Abstract State Machines. In Abstract State Machines – Advances in Theory and Applications, vol. 2589 of LNCS. Springer, 2003.                                 
  Abstract   BibTeX

  We study the decdability of general verification problems for ASMs. This corresponds to the question whether all computations of an ASM satisfy a property (usually expressed in some temporal logic). Because of undecidability in the general case, one has to identify classes of ASMs and classes of properties in order to receive positive decidability results. One idea for this could be to put simple restrictions on the ASMs as forbidding certain advanced constructs. But it turns out that this does not help much. Additionally, the restrictions in those cases are very strong. Consequently, one has to look for others. Such restrictions may result from techniques which are intended to be used in the proofs of decidability. One proof technique is the reduction to a decidable reasoning problem in logic. M. Spielmann has applied it to receive some positive decidability results.

  In this paper, we identify further classes of ASMs and classes of properties for which the general verification problem is decidable. Each proof is a reduction to the satisfiability problem of a fragment of linear temporal first-order logic which has respectively been proved to be decidable by I. Hodkinson, F. Wolter and M. Zakharyaschev.

  @inproceedings{Nowack03,
       author = {Antje Nowack},
       booktitle = {{Abstract State Machines -- Advances in Theory and Applications}},
       publisher = {{Springer}},
       series = {{LNCS}},
       title = {{Deciding the Verification Problem for Abstract State Machines}},
       url = {http://www.logic.rwth-aachen.de/pub/nowack/asm03.ps},
       volume = {2589},
       year = {2003},
  }
  

2000

• A. Nowack. Complexity Theory via Abstract State Machines. Diploma thesis, RWTH-Aachen, 2000.             
  BibTeX

  @misc{No00,
       author = {Antje Nowack},
       howpublished = {{Diploma thesis, RWTH-Aachen}},
       title = {{Complexity Theory via Abstract State Machines}},
       url = {http://www.logic.rwth-aachen.de/pub/nowack/DiplArbeit.ps.gz},
       year = {2000},
  }