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.487
URN: urn:nbn:de:0030-drops-54335
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5433/
Go to the corresponding LIPIcs Volume Portal

Traytel, Dmitriy

A Coalgebraic Decision Procedure for WS1S

pdf-format:
30.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{traytel:LIPIcs:2015:5433,
  author =	{Dmitriy Traytel},
  title =	{{A Coalgebraic Decision Procedure for WS1S}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{487--503},
  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/5433},
  URN =		{urn:nbn:de:0030-drops-54335},
  doi =		{10.4230/LIPIcs.CSL.2015.487},
  annote =	{Keywords: WS1S, decision procedure, coalgebra, Brzozowski derivatives, Isabelle}
}

Keywords: WS1S, decision procedure, coalgebra, Brzozowski derivatives, Isabelle
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