In many Discrete-Event Systems (DES) both state and event information are of importance to the systems designer. To obtain compositionally consistent hierarchical models of systems, the behavior of Discrete-Event Systems with unobservable transitions and state output maps is considered. Observers for deterministic DES are generalized to nondeterministic DES and characterized using the join semilattice of compatible partitions of a transition system. This characterization points to efficient algorithms for computing both strong and weak state-event observers as solutions to the Relational Coarsest Partition problem (RCP). The strong and weak observation equivalences of Milner are shown to be special cases of our observers under the trivial (constant) state output map. The state-event equivalence based upon the observers is shown to be a congruence for a parallel composition operator, allowing the replacement of modules by their quotient systems.
Logics such as Ostroff's RTTL allow for the specification and verification
of a system's state-event behavior. To make realistic problems amenable
to analysis, a designer must typically decompose the system into
subsystems (modules) and use algebraic abstraction (quotient systems) to
obtain hierarchical system models that preserve the properties to be
verified. In this thesis we use state-event observational equivalence to
perform compositionally consistent model reduction for a subclass of
formulas of state-event linear temporal logics, with particular attention
to a discrete time temporal logic that is a simplification of RTTL. The
reduction technique allows limited use of immediate operators. In the
process, we develop a method of specifying modules' input/output behavior
by defining observable satisfaction for RTTL-style temporal logics. The
results are applied to the shut-down system of a nuclear reactor.
PDF file, 1 MB: lawford-phd.pdf
GZIP compressed PostScript, 420 KB: lawford-phd.ps.gz (Use gunzip to uncompress)
If you have trouble downloading, look here for more information.
