Abstract
We discuss in this paper how connections, discovered almost forty years ago, between logics and automata can be used in practice. For such logics expressing regular sets, we have developed tools that allow efficient symbolic reasoning not attainable by theorem proving or symbolic model checking.
We explain how the logic-automaton connection is already exploited in a limited way for the case of Quantified Boolean Logic, where Binary Decision Diagrams act as automata. Next, we indicate how BDD data structures and algorithms can be extended to yield a practical decision procedure for a more general logic, namely WS1S, the Weak Second-order theory of One Successor. Finally, we mention applications of the automaton-logic connection to software engineering and program verification.
Preview
Unable to display preview. Download preview PDF.
References
A. Arnold. A syntactic congruence for rational ω-languages. Theoretical Computer Science, 39:333–335, 1985.
D. Basin and N. Klarlund. Beyond the finite in hardware verification. Submitted for publication. Extended version of: “Hardware verification using monadic second-order logic,” CAV '95, LNCS 939, 1996.
M. Biehl, N. Klarlund, and T. Rauhe. Algorithms for guided tree automata. In First International Workshop on Implementing Automata, WIA '96, Lecture Notes in Computer Science, 1260. Springer Verlag, 1996.
A. Boudet and H. Comon. Diophantine equations, presburger arithmetic and finite automata. In Trees and algebra in programming-CRAP, volume 1059 of LNCS, 1995.
R. E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing surveys, 24(3):293–318, September 1992.
J.R. Büchi. Weak second-order arithmetic and finite automata. Z. Math. Logik Grundl. Math., 6:66–92, 1960.
J. Doner. Tree acceptors and some of their applications. J. Comput. System Sci., 4:406–451, 1970.
C.C. Elgot. Decision problems of finite automata design and related arithmetics. Trans. Amer. Math. Soc., 98:21–52, 1961.
J. Glenn and W. Gasarch. Implementing WSIS via finite automata. In Automata Implementation, WIA '96, Proceedings, volume 1260 of LNCS, 1997.
Object Management Group. The Common Object Request Broker: architecture and specification, 1995 July. revision 2.0.
A. Gupta and A.L. Fisher. Parametric circuit representation using inductive boolean functions. In Computer Aided Verification, CAV '93, LNCS 697, pages 15–28, 1993.
A. Gupta and A.L. Fisher. Representation and symbolic manipulation of linearly inductive boolean functions. In Proceedings of the IEEE International Conference on Computer-Aided Design, pages 192–199. IEEE Computer Society Press, 1993.
J.G. Henriksen, J. Jensen, M. Jørgensen, N. Klarlund, B. Paige, T. Rauhe, and A. Sandholm. 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.
J.L. Jensen, M.E. Jørgensen, N. Klarlund, and M.I. Schwartzbach. Automatic verification of pointer programs using monadic second-order logic. In SIGPLAN '97 Conference on Programming Language Design and Implementation pages 226–234. SIGPLAN, 1997.
P. Kelb, T. Margaria, M. Mendler, and C. Gsottberger. Mosel: a flexible toolset for Monadic Second-order Logic. In Computer Aided Verification, CAV '97, Proceedings, LNCS 1217, 1997.
Y. Kesten, O. Maler, M. Marcus, and E. Shahar A. Pnueli. Symbolic model checking with rich assertional languages. In O. Grumberg, editor, Computer Aided Verification, CAV '97, volume 1254 of LNCS, 1997.
N. Klarlund. A homomorphism concept for ω-regularity. In Proc. of Computer Science Logic, 1994. To appear.
N. Klarlund. An n log n algorithm for online BDD refinement. In O. Grumberg, editor, Computer Aided Verification, CAV '97, volume 1254 of LNCS, 1997.
N. Klarlund, J. Koistinen, and M. Schwartzbach. Formal design constraints. In Proc. OOPSLA '96, 1996.
N Klarlund and T. Rauhe. Bdd algorithms and cache misses. Technical report, BRIGS Report Series RS-96-5, Department of Computer Science, University of Aarhus, 1996.
N. Klarlund and M. Schwartzbach. A domain-specific language for regular sets of strings and trees. In Proc. Conference on Domain Specific Languages. Usenix, ACM SIGPLAN, 1997.
H-T. Liaw and C-S. Lin. On the OBDD-representation of general Boolean functions. IEEE Trans. on Computers, C-41(6):661–664, 1992.
Ken McMillan. Symbolic Model Checking. Kluwer, 1993.
A.R. Meyer. Weak monadic second-order theory of successor is not elementary recursive. In R. Parikh, editor, Logic Colloquium, (Proc. Symposium on Logic, Boston, 1972), volume 453 of LNCS, pages 132–154, 1975.
F. Morawietz and T. Cornell. On the recognizability of relations over a tree definable in a monadic second order tree description language. Technical Report SFB 340, Seminar für Sprachwissenschaft Eberhard-Karls-Universität Tübingen, 1997.
L. Staiger O. Maler. On syntactic congruences for omega-languages. Theoretical Computer Science, 183:93–112, 1997.
A. Potthoff. Project to implement monadic-second order logic on finite trees. Unpublished., 1994.
M.O. Rabin. Decidability of second-order theories and automata on infinite trees. American Mathematical Society, 141:1–35, 1969.
B. Le Sac. Saturating right congruences. Informatique Théorique et Applications, 24:545–560, 1990.
L. Stockmeyer. The complexity of decision problems in automata theory and logic. PhD thesis, Dept. of Electrical Eng., M.I.T., Cambridge, MA, 1974. Report TR-133.
J.W. Thatcher and J.B. Wright. Generalized finite automata with an application to a decision problem of second-order logic. Math. Systems Theory, 2:57–82, 1968.
W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 133–191. MIT Press/Elsevier, 1990.
Jean E. Vuillemin. On circuits and numbers. IEEE Transactions on Computers, 43(8):868–879, 1994.
T. Wilke. An algebraic theory for regular languages of finite and infinite words. Int. T. of Algebra and Computation, 4:447–489, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Klarlund, N. (1998). Mona & Fido: The logic-automaton connection in practice. In: Nielsen, M., Thomas, W. (eds) Computer Science Logic. CSL 1997. Lecture Notes in Computer Science, vol 1414. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028022
Download citation
DOI: https://doi.org/10.1007/BFb0028022
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64570-2
Online ISBN: 978-3-540-69353-6
eBook Packages: Springer Book Archive