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...

• Type: Conference
• Year: 1999
• Where: CAV
• Authors: Nils Klarlund
• Keywords: CAV 1999, Decision Procedure, Hardware, Monadic Second-order Logics, Rst-order Variables