Evidence for Fixpoint Logic

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

3 Citaten (Scopus)

Samenvatting

For many modal logics, dedicated model checkers offer diagnostics (e.g., counterexamples) that help the user understand the result provided by the solver. Fixpoint logic offers a unifying framework in which such problems can be expressed and solved, but a drawback of this framework is that it lacks comprehensive diagnostics generation. We extend the framework with a notion of evidence, which can be specialized to obtain diagnostics for various model checking problems, behavioural equivalence and refinement checking problems. We demonstrate this by showing how our notion of evidence can be used to obtain diagnostics for the problem of deciding stuttering bisimilarity. Moreover, we show that our notion generalizes the existing notions of counterexample and witness for LTL and ACTL* model checking.
Originele taal-2Nederlands
Titel24th EACSL Annual Conference on Computer Science Logic (CSL 2015), September 7-10, 2015, Berlin, Germany
RedacteurenS. Kreutzer
UitgeverijSchloss Dagstuhl - Leibniz-Zentrum für Informatik
Pagina's78-93
ISBN van geprinte versie978-3-939897-90-3
DOI's
StatusGepubliceerd - 2015
Evenement24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany - Berlin, Duitsland
Duur: 7 sep 201510 sep 2015

Publicatie series

NaamLeibniz International Proceedings in Informatics (LIPIcs)
Volume41

Congres

Congres24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany
Verkorte titelCSL 2015
LandDuitsland
StadBerlin
Periode7/09/1510/09/15

Citeer dit

Cranen, S., Luttik, S. P., & Willemse, T. A. C. (2015). Evidence for Fixpoint Logic. In S. Kreutzer (editor), 24th EACSL Annual Conference on Computer Science Logic (CSL 2015), September 7-10, 2015, Berlin, Germany (blz. 78-93). (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 41). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CSL.2015.78