KIT | KIT-Bibliothek | Impressum | Datenschutz

From tableaux to 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. This paper shows how counterexamples and witnesses for the
whole µ-Calculus can be constructed. The witness construction is
derived in a formal way from the local model checking method. The
witness construction presented in this paper is polynomial in the
model
and the formula.

Open Access Logo


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