Document Open Access Logo

A Coalgebraic Decision Procedure for WS1S

Author Dmitriy Traytel

PDF
Thumbnail PDF

File

LIPIcs.CSL.2015.487.pdf
  • Filesize: 0.59 MB
  • 17 pages

Document Identifiers

Author Details

Dmitriy Traytel

Cite As Get BibTex

Dmitriy Traytel. A Coalgebraic Decision Procedure for WS1S. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 487-503, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CSL.2015.487

Abstract

Weak monadic second-order logic of one successor (WS1S) is a simple and natural formalism to specify regular properties. WS1S is decidable, although the decision procedure's complexity is non-elementary. Typically, decision procedures for WS1S exploit the logic-automaton connection, i.e. they escape the simple and natural formalism by translating formulas into equally expressive regular structures such as finite automata, regular expressions, or games. In this work, we devise a coalgebraic decision procedure for WS1S that stays within the logical world by directly operating on formulas. The key operation is the derivative of a formula, modeled after Brzozowski's derivatives of regular expressions. The presented decision procedure has been formalized and proved correct in the interactive proof assistant Isabelle.

Subject Classification

Keywords
  • WS1S
  • decision procedure
  • coalgebra
  • Brzozowski derivatives
  • Isabelle

Metrics

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

References

  1. Valentin Antimirov. Partial derivatives of regular expressions and finite automaton constructions. Theor. Comput. Sci., 155(2):291-319, March 1996. Google Scholar
  2. Abdelwaheb Ayari and David Basin. Bounded model construction for monadic second-order logics. In E. A. Emerson and A. P. Sistla, editors, CAV 2000, volume 1855 of LNCS, pages 99-112. Springer, 2000. Google Scholar
  3. D. Basin and N. Klarlund. Automata based symbolic reasoning in hardware verification. Formal Methods In System Design, 13:255-288, 1998. Extended version of: "Hardware verification using monadic second-order logic," CAV'95, LNCS 939. Google Scholar
  4. Kai Baukus, Saddek Bensalem, Yassine Lakhnech, and Karsten Stahl. Abstracting WS1S systems to verify parameterized networks. In Susanne Graf and Michael I. Schwartzbach, editors, TACAS 2000, volume 1785 of LNCS, pages 188-203. Springer, 2000. Google Scholar
  5. Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel. Truly modular (co)datatypes for Isabelle/HOL. In Gerwin Klein and Ruben Gamboa, editors, ITP 2014, volume 8558 of LNCS, pages 93-110. Springer, 2014. Google Scholar
  6. Filippo Bonchi and Damien Pous. Checking NFA equivalence with bisimulations up to congruence. In Roberto Giacobazzi and Radhia Cousot, editors, POPL 2013, pages 457-468. ACM, 2013. Google Scholar
  7. Janusz A. Brzozowski. Derivatives of regular expressions. J. ACM, 11(4):481-494, October 1964. Google Scholar
  8. J. Richard Büchi. Weak second-order arithmetic and finite automata. Z. Math. Logik und Grundl. Math., 6:66-92, 1960. Google Scholar
  9. Pascal Caron, Jean-Marc Champarnaud, and Ludovic Mignot. Partial derivatives of an extended regular expression. In A.-H. Dediu, S. Inenaga, and C. Martín-Vide, editors, LATA 2011, volume 6638 of LNCS, pages 179-191. Springer, 2011. Google Scholar
  10. Vincenzo Ciancia and Yde Venema. Stream automata are coalgebras. In Dirk Pattinson and Lutz Schröder, editors, CMCS 2012, volume 7399 of LNCS, pages 90-108. Springer, 2012. Google Scholar
  11. J.H. Conway. Regular Algebra and Finite Machines. Chapman and Hall mathematics series. Dover Publications, Incorporated, 2012. Google Scholar
  12. Nils Anders Danielsson. Total parser combinators. In P. Hudak and S. Weirich, editors, ICFP 2010, pages 285-296. ACM, 2010. Google Scholar
  13. Javier Esparza and Jan Kretínský. From LTL to deterministic automata: A Safraless compositional approach. In Armin Biere and Roderick Bloem, editors, CAV 2014, volume 8559 of LNCS, pages 192-208. Springer, 2014. Google Scholar
  14. Tomáš Fiedor, Lukáš Holík, Ondřej Lengál, and Tomáš Vojnar. Nested antichains for WS1S. In Christel Baier and Cesare Tinelli, editors, TACAS 2015, LNCS. Springer, 2015. to appear. Google Scholar
  15. Nate Foster, Dexter Kozen, Matthew Milano, Alexandra Silva, and Laure Thompson. A coalgebraic decision procedure for NetKAT. In David Walker, editor, POPL 2015, pages 343-355. ACM, 2015. Google Scholar
  16. Tobias Ganzow. Definability and Model Checking: The Role of Orders and Compositionality. PhD thesis, RWTH Aachen University, 2012. Google Scholar
  17. Tobias Ganzow and Lukasz Kaiser. New algorithm for weak monadic second-order logic on inductive structures. In Anuj Dawar and Helmut Veith, editors, CSL 2010, volume 6247 of LNCS, pages 366-380. Springer, 2010. Google Scholar
  18. Florian Haftmann and Tobias Nipkow. Code generation via higher-order rewrite systems. In M. Blume, N. Kobayashi, and G. Vidal, editors, FLOPS 2010, volume 6009 of LNCS, pages 103-117. Springer, 2010. Google Scholar
  19. Jad Hamza, Barbara Jobstmann, and Viktor Kuncak. Synthesis for regular specifications over unbounded domains. In Roderick Bloem and Natasha Sharygina, editors, FMCAD 2010, pages 101-109. IEEE, 2010. Google Scholar
  20. Jesper G. Henriksen, Jakob L. Jensen, Michael E. Jørgensen, Nils Klarlund, Robert Paige, Theis Rauhe, and Anders Sandholm. MONA: Monadic second-order logic in practice. In E. Brinksma, R. Cleaveland, K. Larsen, T. Margaria, and B. Steffen, editors, TACAS 1995, volume 1019 of LNCS, pages 89-110. Springer, 1995. Google Scholar
  21. Bart Jacobs. A bialgebraic review of deterministic automata, regular expressions and languages. In Kokichi Futatsugi, Jean-Pierre Jouannaud, and José Meseguer, editors, Algebra, Meaning, and Computation, volume 4060 of LNCS, pages 375-404. Springer, 2006. Google Scholar
  22. Jakob L. Jensen, Michael E. Jørgensen, Nils Klarlund, and Michael I. Schwartzbach. Automatic verification of pointer programs using monadic second-order logic. In Marina C. Chen, Ron K. Cytron, and A. Michael Berman, editors, PLDI 1997, pages 226-236. ACM, 1997. Google Scholar
  23. Nils Klarlund. Relativizations for the logic-automata connection. Higher-Order and Symbolic Computation, 18(1-2):79-120, 2005. Google Scholar
  24. Nils Klarlund and Anders Møller. MONA Version 1.4 User Manual. BRICS, Department of Computer Science, Aarhus University, January 2001. Notes Series NS-01-1. Available from http://www.brics.dk/mona/. Revision of BRICS NS-98-3. Google Scholar
  25. Nils Klarlund, Anders Møller, and Michael I. Schwartzbach. MONA implementation secrets. Int. J. Found. Comput. Sci., 13(4):571-586, 2002. Google Scholar
  26. Dexter Kozen. On the coalgebraic theory of Kleene algebra with tests. Technical Report http://hdl.handle.net/1813/10173, Computing and Information Science, Cornell University, March 2008.
  27. Albert R. Meyer. Weak monadic second order theory of succesor is not elementary-recursive. In Rohit Parikh, editor, Logic Colloquium, volume 453 of LNM, pages 132-154. Springer, 1975. Google Scholar
  28. Matthew Might, David Darais, and Daniel Spiewak. Parsing with derivatives: A functional pearl. In Manuel M. T. Chakravarty, Zhenjiang Hu, and Olivier Danvy, editors, ICFP 2011, pages 189-195. ACM, 2011. Google Scholar
  29. Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. Google Scholar
  30. Tobias Nipkow and Dmitriy Traytel. Unified decision procedures for regular expression equivalence. In G. Klein and R. Gamboa, editors, ITP 2014, volume 8558 of LNCS, pages 450-466. Springer, 2014. Google Scholar
  31. Damien Pous. Symbolic algorithms for language equivalence and Kleene algebra with test. In David Walker, editor, POPL 2015, pages 357-368. ACM, 2015. Google Scholar
  32. Jan J. M. M. Rutten. Automata and coinduction (an exercise in coalgebra). In D. Sangiorgi and R. de Simone, editors, CONCUR 1998, volume 1466 of LNCS, pages 194-218. Springer, 1998. Google Scholar
  33. Saharon Shelah. The monadic theory of order. Ann. Math., 102(3):379-419, 1975. Google Scholar
  34. Wolfgang Thomas. Languages, automata, and logic. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, pages 389-455. Springer, 1997. Google Scholar
  35. Dmitriy Traytel. [dWiNA Issue #1] Wrong results for simple formulas, 14 Jan 2015. Archived at URL: https://github.com/Raph-Stash/dWiNA/issues/1.
  36. Dmitriy Traytel. [Toss-devel] Toss deciding MSO, 14 Jan 2015. Archived at URL: http://sourceforge.net/p/toss/mailman/message/33232473/.
  37. Dmitriy Traytel. A codatatype of formal languages. In Gerwin Klein, Tobias Nipkow, and Lawrence Paulson, editors, Archive of Formal Proofs. http://afp.sf.net/entries/Coinductive_Languages.shtml, 2013.
  38. Dmitriy Traytel. Supplementary material. https://github.com/dtraytel/WS1S, 2015.
  39. Dmitriy Traytel and Tobias Nipkow. Verified decision procedures for MSO on words based on derivatives of regular expressions (extended version of [Dmitriy Traytel and Tobias Nipkow, 2013]). URL: http://www21.in.tum.de/~traytel/mso.pdf.
  40. Dmitriy Traytel and Tobias Nipkow. Verified decision procedures for MSO on words based on derivatives of regular expressions. In G. Morrisett and T. Uustalu, editors, ICFP 2013, pages 3-12. ACM, 2013. 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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact