DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2015.78

Evidence for Fixpoint Logic

Authors: Sjoerd Cranen, Bas Luttik, and Tim A. C. Willemse

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

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.

Cite as

Sjoerd Cranen, Bas Luttik, and Tim A. C. Willemse. Evidence for Fixpoint Logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 78-93, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{cranen_et_al:LIPIcs.CSL.2015.78,
  author =	{Cranen, Sjoerd and Luttik, Bas and Willemse, Tim A. C.},
  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 =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.78},
  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*}
}

Search Results

Documents authored by Cranen, Sjoerd

Evidence for Fixpoint Logic

Abstract

Cite as

Thanks for your feedback!

Could not send message