Model Reduction of Modules for State-Event Temporal Logics

by M. Lawford, J.S. Ostroff and W.M. Wonham

Abstract: In many Discrete-Event Systems (DES) both state and event information are of importance to the systems designer. 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 paper we use state-event observational equivalence to perform model reduction for a subclass of formulas of state-event linear temporal logics, with particular attention being paid to a discrete time temporal logic that is a simplification of RTTL. The reduction technique allows limited use of immediate operators.

NOTE: This is an updated version of the paper that corrects a typograpical error in Definition 11 on p. 274!

Download

FORTE96.ps (280k, postscript) OR FORTE96.pdf (228k, PDF)

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

BibTeX Entry

@incollection{LaOsWo:96,
        author={M. Lawford and J.S. Ostroff and W.M. Wonham},
        title={Model reduction of modules for
        state-event temporal logics},
        editor={R. Gotzhein and J. Bredereke}, 
        booktitle={Formal Description Techniques IX: Theory,
                  application 
                  and tools, Proceedings of FORTE/PSTV'96}, 
        pages={263--278},
        publisher={Chapman \& Hall}, 
        year={1996}
        }