Higher-Order and Symbolic Computation, 18(1/2)
Relativizations for the Logic-Automata ConnectionNils Klarlund, AT&T Labs -- Research, Florham Park, New Jersey
|
Abstract: BDDs and their algorithms implement a decision
procedure for Quantified Propositional Logic. BDDs are a kind of
acyclic automata. But unrestricted automata (recognizing unbounded
strings of bit vectors) can be used to decide monadic second-order
logics, which are more expressive. Prime examples are WS1S, a
number-theoretic logic, or the string-based logical notation of
introductory texts. One problem is that it is not clear which one is
to be preferred in practice. For example, it is not known whether
these two logics are computationally equivalent to within a linear
factor, that is, whether a formula phi of one logic can be
transformed to a formula phi' of the other such that phi' is
true if and only if phi is and such that phi' is decided in time
linear in that of the time for phi. Another problem is that first-order variables in either version are given automata-theoretic semantics according to relativizations, which are syntactic means of restricting the domain of quantification of a variable. Such relativizations lead to technical arbitrations that may involve normalizing each subformula in an asymmetric manner or may introduce spurious state space explosions. In this paper, we investigate these problems through studies of congruences on strings. This algebraic framework is adapted to language-theoretic relativizations, where regular languages are intersected with restrictions. The restrictions are also regular languages. We introduce ternary and sexpartite characterizations of relativized regular languages. From properties of the resulting congruences, we are able to carry out detailed state space analyses that allow us to address the two problems. We report briefly on practical experiments that support our results. We conclude that WS1S with first-order variables can be robustly implemented in a way that efficiently subsumes string-based notations. |
This article is not yet available.