Model Reduction of Discrete Real-Time Systems

by Mark Lawford

Abstract: 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.

Download (1700k, postscript) OR phd.pdf (1200k, PDF)

NOTE: PDF version how contains bookmarks and hyperlinks to all internal references.

BibTeX Entry

        author={Mark Lawford},
        title={Model Reduction of Discrete Real-Time Systems},
        school="Dept.\ of Elec.\ \& Comp.\ Eng., Univ.\ of Toronto, Canada",

[ CAS | ML | Papers ]