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

Stephan Merz

Abstract

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.

Note

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

Reference

@Misc{merz:habil,
  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
}