Logical Description and Analysis of Reactive Systems: Hiding, Composition, and Abstraction

Stephan Merz
We study aspects of three central issues in the formal design of reactive systems: hiding refers to the ability to control the visibility of specification detail, compositionality enables large systems to be assembled from separate components, and abstraction promises a higher degree of automation in the verification of large systems. The work is cast in the framework of temporal logic, and proof rules are provided to support all three concepts.
This is my habilitation thesis. It collects several results from earlier papers. The main novelties are a characterization of ω-regular languages that are invariant under finite stuttering by a class of ω-automata, and a completeness theorem for the quantified propositional version of TLA*, my extension of Lamport's TLA. These parts are extremely technical.
Available as: gzip'ed Postscript
  author = {Stephan Merz},
  title =  {Logical Description and Analysis of Reactive Systems},
  howpublished = {Habilitationsschrift, 
            Ludwig-Maximilians-Universit{\"a}t M{\"u}nchen},
  month = dec,
  year = 2001

Stephan Merz
Last modified: Mon Feb 17 11:50:31 MET 2003