Sciweavers

CAV
1999
Springer

A Theory of Restrictions for Logics and Automata

13 years 8 months ago
A Theory of Restrictions for Logics and Automata
BDDs and their algorithms implement a decision procedure for Quanti ed Propositional Logic. BDDs are a kind of acyclic automata. Unrestricted automata (recognizing unbounded strings ofbit 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 rst-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 f...
Nils Klarlund
Added 03 Aug 2010
Updated 03 Aug 2010
Type Conference
Year 1999
Where CAV
Authors Nils Klarlund
Comments (0)