Lazy Automata Techniques for WS1S

Tomáš Fiedor, Lukáš Holík, Petr Janků +2

We present a new decision procedure for the logic WS1S. It originates from the classical approach, which first builds an automaton accepting all models of a formula and then tests…