×

Relativizations for the logic-automata connection. (English) Zbl 1084.68064

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

MSC:

68Q45 Formal languages and automata
03B25 Decidability of theories and sets of sentences
03D05 Automata and formal grammars in connection with logical questions

Software:

MONA; Mosel
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Ayari, A. and Basin, D. Bounded model construction for monadic second-order logics. In Computer Aided Verification, 2000 pp. 99–112. · Zbl 0974.68115
[2] Basin, D. and Klarlund, N. 1998, Automata based symbolic reasoning in hardware verification. Formal Methods in System Design, Extended version of ”Hardware verification using monadic second-order logic,” Computer aided verification: 7th International Conference, CAV ’95, LNCS 939, 1995, pp. 255–288.
[3] Bell, J. and Machover, M. A Course in Mathematical Logic. North-Holland, 1977. · Zbl 0359.02001
[4] Bryant, R. E. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3) (1992) 293–318. · doi:10.1145/136035.136043
[5] Büchi, J. Weak second-order arithmetic and finite automata. Z. Math. Logik Grundl. Math., 6 (1960) 66–92. · Zbl 0103.24705 · doi:10.1002/malq.19600060105
[6] Elgot, C. Decision problems of finite automata design and related arithmetics. Trans. Amer. Math. Soc., 98 (1961) 21–52. · Zbl 0111.01102 · doi:10.1090/S0002-9947-1961-0139530-9
[7] Henriksen, J., Jensen, J., Jørgensen, M., Klarlund, N., Paige, B., Rauhe, T., and Sandholm, A. Mona: Monadic Second-order logic in practice. In Tools and Algorithms for the Construction and Analysis of Systems, First International Workshop, TACAS ’95, LNCS 1019, 1996.
[8] Elgaard, J., Klarlund, N., A.M. Mona 1.x: New techniques for WS1S and WS2S. In Computer Aided Verification, CAV ’98, Proceedings, Vol. 1427 of LNCS. Springer Verlag, 1998.
[9] Kelb, P., Margaria, T., Mendler, M., and Gsottberger, C. Mosel: A flexible toolset for Monadic Second-order Logic. In Computer Aided Verification, CAV ’97, Proceedings, 1997,
[10] Klarlund, N. Mona & Fido: The logic-automaton connection in practice. In CSL ’97 Proceedings. LNCS 1414, Springer-Verlag, 1998. · Zbl 0916.68099
[11] Klarlund, N. and Møller, A. MONA Version 1.3 User Manual, BRICS. URL: http://www.brics.dk/mona, 1998,
[12] Klarlund, N., Møller, A., and Schwartzbach, M. MONA implementation Secrets. International Journal of Foundations of Computer Science, 13(4) (2002) 571–586. · Zbl 1066.68079 · doi:10.1142/S012905410200128X
[13] Møller, A. and Schwartzbach, M. The pointer assertion logic engine. In Proceedings of ACM SIGPLAN Conference of Programming Language Design and Implementation, 2001.
[14] Smith, M. and Klarlund, N. Verification of a sliding window protocol using IOA and MONA. In FORTE/PSTV 2000: IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XIII), and Protocol Specification, Testing, and Verification (PSTV XX). Kluwer Academic Publishers, 2000 pp. 19–34.
[15] Straubing, H. Finite Automata, Formal Logic, and Circuit Complexity. Birkhäuser, 1994. · Zbl 0816.68086
[16] Thomas, W. Languages, automata, and logic. In Handbook of Formal Languages. G. Rozenberg and A. Salomaa (Eds.). Springer Verlag, Chapt. Languages, automata, and logic, 1997.
[17] Trakhtenbrot, B. Finite automata and the logic of one-place predicates. Sib. Math. J, 3 (1962) 103–131. In Russian. English translation: AMS Transl., 59 (1966), 23–55. · Zbl 0115.00701
[18] Vaillette, N. Logical specification of finite-state transductions for NLP. Natural Language Engineering, 9(1) (2003).
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.