KIT | KIT-Bibliothek | Impressum | Datenschutz

Formula dependent model reduction through elimination of invisible transitions for checking fragments of CTL

Kick, Alexander


We present a reduction algorithm which reduces Kripke structures by
eliminating transitions from the model which do not affect the visible
components of the model. These are exactly the variables contained in
the specification formula. The reduction algorithm preserves the truth
of special CTL formulae. In contrast to formula-dependent reduction
algorithms presented so far, which are mostly computationally
expensive, our algorithm needs only one pass through the reachable
states of the model. Nevertheless, preliminary results show that models
are reduced considerably, which is plausible because, in general, the
number of visible components of a reactive system is small compared to
the number of internal components.

Open Access Logo

Volltext §
DOI: 10.5445/IR/35295
Cover der Publikation
Zugehörige Institution(en) am KIT Informatik für Ingenieure und Naturwissenschaftler (Inf. für Ing. u. Naturwiss.)
Publikationstyp Buch
Publikationsjahr 1995
Sprache Englisch
Identifikator urn:nbn:de:swb:90-AAA352953
KITopen-ID: 35295
Erscheinungsvermerk Karlsruhe 1995. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1995,27.)
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page