Rules for Abstraction

Stephan Merz

Abstract

Abstraction techniques for the verification of reactive systems promise to provide a theoretical basis for the integration of automatic and interactive proof techniques. In this paper, we give an account of homomorphic abstraction by studying a series of proof rules in Lamport's Temporal Logic of Actions. We believe that the main advantage of a logical formalization of abstraction is that it points towards more refined abstraction techniques. Specifically, we demonstrate two novel techniques that appear helpful in the verification of liveness properties over abstract models.

Note

This paper reflects my first attempts to make abstraction useful in order to prove liveness properties of reactive systems (conventional wisdom held that abstraction could be used only for safety properties). It explains the basic idea at the hand of the "dining mathematician" example borrowed from Dams et al. It is superseded by the subsequent development of predicate diagrams, which provide for a more elegant presentation and simplify the decomposition between theorem proving and model checking.

© Springer-Verlag

Available as:  gzip'ed Postscript 

Reference

@InProceedings{merz:abstraction,
  author =    {Stephan Merz},
  title =     {Rules for Abstraction},
  booktitle = {Advances in Computing Science---ASIAN'97},
  editor =    {R. K. Shyamasundar and K. Ueda},
  volume =    1345,
  series =    {Lecture Notes in Computer Science},
  year =      1997,
  publisher = {Springer-Verlag},
  address =   {Kathmandu, Nepal},
  month =     dec,
  pages =     {32--45}
}