License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2015.78
URN: urn:nbn:de:0030-drops-54080
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5408/
Go to the corresponding LIPIcs Volume Portal

Cranen, Sjoerd ; Luttik, Bas ; Willemse, Tim A. C.

Evidence for Fixpoint Logic

pdf-format:
5.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{cranen_et_al:LIPIcs:2015:5408,
  author =	{Sjoerd Cranen and Bas Luttik and Tim A. C. Willemse},
  title =	{{Evidence for Fixpoint Logic}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{78--93},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Stephan Kreutzer},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5408},
  URN =		{urn:nbn:de:0030-drops-54080},
  doi =		{10.4230/LIPIcs.CSL.2015.78},
  annote =	{Keywords: fixpoint logic, diagnostics, counterexample, model checking, stuttering bisimilarity, ACTL*}
}

Keywords: fixpoint logic, diagnostics, counterexample, model checking, stuttering bisimilarity, ACTL*
Collection: 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
Issue Date: 2015
Date of publication: 07.09.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI