Evidence for Fixpoint Logic

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

5 Citations (Scopus)

Abstract

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.
Original languageDutch
Title of host publication24th EACSL Annual Conference on Computer Science Logic (CSL 2015), September 7-10, 2015, Berlin, Germany
EditorsS. Kreutzer
PublisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik
Pages78-93
ISBN (Print)978-3-939897-90-3
DOIs
Publication statusPublished - 2015
Event24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany - Berlin, Germany
Duration: 7 Sep 201510 Sep 2015

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
Volume41

Conference

Conference24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany
Abbreviated titleCSL 2015
Country/TerritoryGermany
CityBerlin
Period7/09/1510/09/15

Cite this