Traytel, Dmitriy
A Coalgebraic Decision Procedure for WS1S
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 |
|
Seminar: |
|
24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
|
|
Issue date: |
|
2015 |
|
Date of publication: |
|
2015 |
2015
