A theory of restrictions for logics and automata

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 congruen- ces, 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.