KIT | KIT-Bibliothek | Impressum | Datenschutz

Generation of counterexamples for the my--calculus

Kick, Alexander


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 to fair CTL formulae. Model checkers constructed just recently
can check arbitrary $\mu$-calculus formulae. How to construct
counterexamples for arbitrary \muf has not been investigated yet. This
paper shows how counterexamples and witnesses for the whole
$\mu$-calculus can be constructed.

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