Document Open Access Logo

Evidence for Fixpoint Logic

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

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2015.78.pdf
  • Filesize: 0.53 MB
  • 16 pages

Document Identifiers

Subject Classification

Keywords
  • fixpoint logic
  • diagnostics
  • counterexample
  • model checking
  • stuttering bisimilarity
  • ACTL*

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.CSL.2015.78

Author Details

Sjoerd Cranen
Bas Luttik
Tim A. C. Willemse

References

  1. J. Brotherston and A. Simpson. Sequent calculi for induction and infinite descent. J. Log. Comput., 21(6):1177-1216, 2011. Google Scholar
  2. M. Chechik and A. Gurfinkel. A framework for counterexample generation and exploration. STTT, 9(5-6):429-445, 2007. Google Scholar
  3. T. Chen, B. Ploeger, J.C. van de Pol, and T.A.C. Willemse. Equivalence checking for infinite systems using parameterized boolean equation systems. In CONCUR 2007, volume 4703 of LNCS, pages 120-135. Springer, 2007. Google Scholar
  4. E.M. Clarke, S. Jha, Y. Lu, and H. Veith. Tree-like counterexamples in model checking. In LICS 2002, pages 19-29. IEEE Computer Society, 2002. Google Scholar
  5. R. Cleaveland. On automatically explaining bisimulation inequivalence. In CAV 1990, volume 531 of LNCS, pages 364-372. Springer, 1991. Google Scholar
  6. S. Cranen. Getting the point - Obtaining and understanding fixpoints in model checking. PhD thesis, Technische Universiteit Eindhoven, 2015. Available at URL: http://repository.tue.nl/791780.
  7. S. Cranen, J.F. Groote, J.J.A. Keiren, F.P.M. Stappers, E.P. de Vink, J.W. Wesselink, and T.A.C. Willemse. An overview of the mCRL2 toolset and its recent advances. In TACAS 2013, volume 7795 of LNCS, pages 199-213. Springer, 2013. Google Scholar
  8. S. Cranen, J.F. Groote, and M.A. Reniers. A linear translation from CTL* to the first-order modal μ-calculus. Theoretical Computer Science, 412(28):3129-3139, 2011. Google Scholar
  9. S. Cranen, B. Luttik, and T.A.C. Willemse. Proof graphs for parameterised boolean equation systems. In CONCUR 2013, volume 8052 of LNCS, pages 470-484. Springer, 2013. Google Scholar
  10. Z. Ésik and P. Rondogiannis. A fixed point theorem for non-monotonic functions. Theoretical Computer Science, 574:18-38, 2015. Google Scholar
  11. O. Friedmann and M. Lange. The modal μ-calculus caught off guard. In TABLEAUX 2011, volume 6793 of LNCS, pages 149-163. Springer, 2011. Google Scholar
  12. C. Grabmayer. Relating Proof Systems for Recursive Types. PhD thesis, Vrije Univesiteit Amsterdam, 2005. Google Scholar
  13. E. Grädel. Model checking games. Electr. Notes Theor. Comput. Sci., 67:15-34, 2002. Google Scholar
  14. J.F. Groote and R. Mateescu. Verification of temporal properties of processes in a setting with data. In AMAST 1998, volume 1548 of LNCS, pages 74-90. Springer, 1999. Google Scholar
  15. J.F. Groote and T.A.C. Willemse. Model-checking processes with data. Science of Computer Programming, 56(3):251-273, 2005. Google Scholar
  16. J.F. Groote and T.A.C. Willemse. Parameterised boolean equation systems. Theoretical Computer Science, 343(3):332-369, 2005. Google Scholar
  17. D. Janin. Automata, tableaus and a reduction theorem for fixpoint calculi in arbitrary complete lattices. In LICS 1997, pages 172-182. IEEE Computer Society, 1997. Google Scholar
  18. H. Korver. Computing distinguishing formulas for branching bisimulation. In CAV 1991, volume 575 of LNCS, pages 13-23. Springer, 1992. Google Scholar
  19. L. Libkin. Elements of Finite Model Theory. Springer, 2004. Google Scholar
  20. Y. Moschovakis. Elementary induction on abstract structures. North Holland, 1974. Google Scholar
  21. K.S. Namjoshi. A simple characterization of stuttering bisimulation. In FSTTCS 1997, volume 1346 of LNCS, pages 284-296. Springer, 1997. Google Scholar
  22. S. Shoham and O. Grumberg. A game-based framework for CTL counterexamples and 3-valued abstraction-refinement. ACM Trans. Comput. Log., 9(1), 2007. Google Scholar
  23. L. Tan. Evidence-Based Verification. PhD thesis, Department of Computer Science, State University of New York, 2002. Google Scholar
  24. A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific journal of Mathematics, 5(2):285-309, 1955. Google Scholar
  25. W. Thomas. Computation tree logic and regular omega-languages. In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School/Workshop 1988, volume 354 of LNCS, pages 690-713. Springer, 1989. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact