Abstract
BDDs and their algorithms implement a decision procedure for Quantified Propositional Logic. BDDs are a kind of acyclic automata. Unrestricted automata (recognizing unbounded strings of bit vectors) can be used to decide more expressive monadic second-order logics. Prime examples are WS1S, a number-theoretic logic, or a string-based notation such as those proposed in some introductory texts. It is not clear which one is to be preferred. Also, the inclusion of first-order variables in either version is problematic since their automata-theoretic semantics depends on restrictions. In this paper, we provide a mathematical framework to address these problems. We introduce three and six-valued characterizations of regular languages under restrictions. From properties of the resulting congruences, we are able to carry out detailed state space analyses that allows us to solve the two problems in WS1S in a way that require no extra normalization calculations compared to a naive decision procedure for string-oriented logic. We report briefly on the practical experiments that support our results. We conclude that WS1S with first-order variables is the superior choice among monadic second-order logics.