Logical Description and Analysis of Reactive Systems:
Hiding, Composition, and Abstraction
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.