KIT | KIT-Bibliothek | Impressum | Datenschutz

Reduced witnesses for the my--calculus

Kick, Alexander

Abstract:

Symbolic temporal logic model checking is an automatic verification
method. One of its main features is that a counterexample can be
constructed when a temporal formula does not hold for the model.
Most model checkers so far have restricted the type of formulae that
can be checked and for which counterexamples can be constructed to
fair CTL formulae. In a previous paper, we have presented an algorithm

which constructs counterexamples and witnesses for the whole
µ-Calculus. The witnesses constructed by this algorithm can be
huge, however. In this paper, we show how to construct reduced
witnesses.

Open Access Logo


Volltext §
DOI: 10.5445/IR/60795
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-AAA607955
KITopen-ID: 60795
Erscheinungsvermerk Karlsruhe 1995. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1995,47.)
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page