Logic programming approach to automata-based decision procedures. (English) Zbl 1353.68039
Summary: We propose a novel technique that reduces the decision problem of WSnS (weak monadic second-order logic with \(n\) successors) to the problem of evaluation of Complex-value Datalog queries. We then show how the use of advanced implementation techniques for Logic Programs, in particular the use of tabling in the XSB system, yields a considerable improvement in performance over more traditional approaches. We also explore various optimizations of the proposed technique based on variants of tabling and goal reordering. Although our primary focus is on WS1S, the logic of single successor, we show that it is straightforward to adapt our approach for other logics with existing automata-theoretic decision procedures, for example WS2S.
MSC:
| 68N17 | Logic programming |
| 03B25 | Decidability of theories and sets of sentences |
| 03D05 | Automata and formal grammars in connection with logical questions |
| 68Q45 | Formal languages and automata |
Keywords:
WS1S; WS2S; automata; complex-value Datalog \((\text{Datalog}^{\text{cv}})\); magic sets; SLG-resolutionReferences:
| [1] | Büchi, J. R., Weak second-order arithmetic and finite automata, Z. Math. Log. Grundl. Math., 6, 66-92 (1960) · Zbl 0103.24705 |
| [2] | Rabin, M. O., Decidability of second-order theories and automata on infinite trees, Trans. Am. Math. Soc., 141, 1-35 (1969) · Zbl 0221.02031 |
| [3] | Klarlund, N., MONA & FIDO: the logic-automaton connection in practice, (Computer Science Logic. Computer Science Logic, LNCS, vol. 1414 (1997), Springer-Verlag: Springer-Verlag London, UK), 311-326 · Zbl 0916.68099 |
| [4] | Henriksen, J. G.; Jensen, J. L.; Jörgensen, M. E.; Klarlund, N.; Paige, R.; Rauhe, T.; Sandholm, A., MONA: monadic second-order logic in practice, (TACAS. TACAS, LNCS, vol. 1019 (1995)), 89-110 |
| [5] | Bryant, R. E., Symbolic boolean manipulation with Ordered Binary Decision Diagrams, ACM Comput. Surv., 24, 3, 293-318 (1992) |
| [6] | Beeri, C.; Naqvi, S.; Shmueli, O.; Tsur, S., Set constructors in a logic database language, J. Log. Program., 10, 3&4, 181-232 (1991) · Zbl 0724.68016 |
| [7] | Chen, W.; Swift, T.; Warren, D. S., Efficient implementation of general logical queries (1993), SUNY at Stony Brook, Tech. rep. |
| [8] | Chen, W.; Warren, D., Query evaluation under the well-founded semantics, PODS, 168-179 (1993) |
| [9] | Abiteboul, S.; Beeri, C., The power of languages for the manipulation of complex values, VLDB J., 4, 4, 727-794 (1995) |
| [10] | Sagonas, K. F.; Swift, T.; Warren, D. S., XSB as an efficient deductive database engine, (SIGMOD Conference (1994)), 442-453 |
| [11] | Unel, G.; Toman, D., Deciding weak monadic second-order logics using complex-value datalog, (Proc. LPAR (2005)), (Short Paper) |
| [12] | Unel, G.; Toman, D., Logic programming approach to automata-based decision procedures, (Dahl, V.; Niemel, I., Logic Programming. Logic Programming, Lecture Notes in Computer Science, vol. 4670 (2007), Springer: Springer Berlin, Heidelberg), 165-179 · Zbl 1213.03018 |
| [13] | Elgot, C. C., Decision problems of finite automata design and related arithmetics, Trans. Am. Math. Soc., 98, 21-52 (1961) · Zbl 0111.01102 |
| [14] | Grädel, E.; Thomas, W.; Wilke, T., Automata, Logics and Infinite Games: A Guide to Current Research (2002), Springer, [outcome of a Dagstuhl seminar, February 2001] · Zbl 1011.00037 |
| [15] | Thomas, W., Languages, automata, and logic, (Handbook of Formal Languages, vol. 3 (1997), Springer-Verlag New York, Inc.: Springer-Verlag New York, Inc. New York, NY, USA) |
| [16] | Meyer, A. R., Weak monadic second order theory of successor is not elementary-recursive (1973), MIT: MIT Cambridge, MA, USA, Tech. rep. |
| [17] | Stockmeyer, L., The complexity of decision problems in automata theory and logic (1974), MIT Lab for Computer Science, Ph.D. thesis |
| [18] | Ramakrishnan, R.; Srivastava, D.; Sudarshan, S.; Seshadri, P., The CORAL deductive system, VLDB J., 3, 2, 161-210 (1994) |
| [19] | Grumbach, S.; Vianu, V., Tractable query languages for complex object databases, (Proceedings of the 10th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (1991)), 315-327 |
| [20] | Abiteboul, S.; Hull, R.; Vianu, V., Foundations of Databases (1995), Addison-Wesley · Zbl 0848.68031 |
| [21] | Beeri, C.; Ramakrishnan, R., On the power of magic, J. Log. Program., 10, 1/2/3&4, 255-299 (1991) · Zbl 0722.68018 |
| [22] | Mumick, I. S., Query optimization in deductive and relational databases (1991), Department of Computer Science, Stanford University, Ph.D. thesis |
| [23] | Freire, J.; Swift, T.; Warren, D. S., Beyond depth-first strategies: improving tabled logic programs through alternative scheduling, J. Funct. Logic Program., 3 (1998) · Zbl 0924.68054 |
| [24] | Klarlund, N.; Møller, A., MONA Version 1.4 User Manual, BRICS (January 2001), Department of Computer Science, Aarhus University, Revision of BRICS NS-98-3 |
| [25] | Klarlund, N.; Møller, A.; Schwartzbach, M. I., MONA implementation secrets, Int. J. Found. Comput. Sci., 13, 4, 571-586 (2002) · Zbl 1066.68079 |
| [26] | Ramakrishnan, I. V.; Rao, P.; Sagonas, K. F.; Swift, T.; Warren, D. S., Efficient tabling mechanisms for logic programs, (International Conference on Logic Programming (1995)), 697-711 |
| [27] | Dawson, S.; Ramakrishnan, C. R.; Skiena, S.; Swift, T., Principles and practice of unification factoring, TOPLAS, 18, 5, 528-563 (1996) |
| [28] | Chaudhuri, S., An overview of query optimization in relational systems, (PODS (1998)), 34-43 |
| [29] | Ullman, J. D., Principles of Database and Knowledge-Base Systems, vol. 1&2 (1989), Computer Science Press |
| [30] | Thatcher, J. W.; Wright, J. B., Generalized finite automata theory with an application to a decision problem of second-order logic, Math. Syst. Theory, 2, 57-81 (1968) · Zbl 0157.02201 |
| [31] | Büchi, J. R., On a decision method in restricted second-order arithmetic, (Proc. 1960 Int. Congr. for Logic, Methodology and Philosophy of Science (1962)), 1-11 · Zbl 0147.25103 |
| [32] | McNaughton, R., Testing and generating infinite sequences by a finite automaton, Inf. Control, 9, 521-530 (1966) · Zbl 0212.33902 |
| [33] | Emerson, E. A., Automata, tableaux and temporal logics (extended abstract), (Proceedings Conference on Logics of Programs. Proceedings Conference on Logics of Programs, LNCS, vol. 193 (1985), Springer-Verlag: Springer-Verlag Brooklyn), 79-87 · Zbl 0603.03005 |
| [34] | Emerson, E. A.; Jutla, C. S., The complexity of tree automata and logics of programs, (Proceedings of the 29th IEEE Symposium on Foundations of Computer Science. Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, FOCS’88, White Plains (1988), IEEE Computer Society Press: IEEE Computer Society Press Los Alamitos, CA), 328-337 |
| [35] | Emerson, E. A.; Sistla, A. P., Deciding full branching time logics, Inf. Control, 61, 3, 175-201 (1984) · Zbl 0593.03007 |
| [36] | Kaivola, R., Using automata to characterise fixed point temporal logics (1997), University of Edinburgh, Ph.D. thesis |
| [37] | Mukund, M., Linear-time temporal logic and Büchi automata, (Tutorial Talk, Winter School on Logic and Computer Science (1997), ISI: ISI Calcutta) |
| [38] | Muller, D. E.; Saoudi, A.; Schupp, P. E., Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time, (Symposium on Logic in Computer Science. Symposium on Logic in Computer Science, LICS ’88 (1988), IEEE Computer Society Press: IEEE Computer Society Press Washington, D.C., USA), 422-427 |
| [39] | Vardi, M. Y., An automata-theoretic approach to linear temporal logic, (Banff Higher Order Workshop (1995)), 238-266 · Zbl 1543.68236 |
| [40] | Vardi, M. Y., Alternating automata: unifying truth and validity for temporal logics, (CADE (1997)), 191-206 · Zbl 1430.68156 |
| [41] | Vardi, M. Y.; Wolper, P., Automata-theoretic techniques for modal logics of programs (extended abstract), (Proceedings 16th Annual ACM Symp. on the Theory of Computing. Proceedings 16th Annual ACM Symp. on the Theory of Computing, STOC’84 (1984), ACM Press: ACM Press New York), 446-456 |
| [42] | Vardi, M. Y.; Wolper, P., Reasoning about infinite computations, Inf. Comput., 115, 1, 1-37 (1994) · Zbl 0827.03009 |
| [43] | Kupferman, O.; Vardi, M. Y.; Wolper, P., An automata-theoretic approach to branching-time model checking, J. ACM, 47, 2, 312-360 (2000) · Zbl 1133.68376 |
| [44] | Clarke, E.; Grumberg, D.; Long, D., Model checking and abstraction, ACM Trans. Program. Lang. Syst., 16, 5, 1512-1542 (1994) |
| [45] | Emerson, E. A.; Jutla, C. S.; Sistla, A. P., On model checking for the \(μ\)-calculus and its fragments, Theor. Comput. Sci., 258, 1-2, 491-522 (2001) · Zbl 0973.68120 |
| [46] | Vardi, M. Y.; Wolper, P., An automata-theoretic approach to automatic program verification, (Proc. of the First Symposium on Logic in Computer Science (1986)), 322-331 |
| [47] | Courcoubetis, C.; Vardi, M. Y.; Wolper, P.; Yannakis, M., Memory efficient algorithms for the verification of temporal properties, Form. Methods Syst. Des., 1, 275-288 (1992) |
| [48] | Daniele, M.; Giunchiglia, F.; Vardi, M. Y., Improved automata generation for linear temporal logic, (Computer-Aided Verification. Computer-Aided Verification, Proc. 11th Int. Conference, vol. 1633 (1999)), 249-260 · Zbl 1046.68588 |
| [49] | Gastin, P.; Oddoux, D., Fast LTL to Büchi automata translation, (Computer Aided Verification, Proc. 13th Int. Conference. Computer Aided Verification, Proc. 13th Int. Conference, LNCS, vol. 2102 (2001), Springer), 53-65 · Zbl 0991.68044 |
| [50] | Gerth, R.; Peled, D.; Vardi, M. Y.; Wolper, P., Simple on-the-fly automatic verification of linear temporal logic, (Proceedings of the 29th IEEE Symposium on Foundations of Computer Science. Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, Warsaw (1988)) |
| [51] | Jard, J.; Jeron, T., On-line model-checking for finite temporal logic specifications, (Automatic Verification Methods for Finite State Systems, Proc. Int. Workshop. Automatic Verification Methods for Finite State Systems, Proc. Int. Workshop, Grenoble. Automatic Verification Methods for Finite State Systems, Proc. Int. Workshop. Automatic Verification Methods for Finite State Systems, Proc. Int. Workshop, Grenoble, Lecture Notes in Computer Science, vol. 407 (1989), Springer-Verlag: Springer-Verlag Grenoble), 189-196 |
| [52] | Somenzi, F.; Bloem, R., Efficient Büchi automata from LTL formulae, (Computer-Aided Verification. Computer-Aided Verification, Proc. 12th Int. Conference, vol. 1633 (2000)), 247-263 · Zbl 0974.68086 |
| [53] | Friedmann, O.; Latte, M.; Lange, M., A decision procedure for \(CTL^*\) based on tableaux and automata, (Automated Reasoning, Proceedings of 5th International Joint Conference. Automated Reasoning, Proceedings of 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19 (2010)), 331-345 · Zbl 1257.03035 |
| [54] | Wolper, P., Constructing automata from temporal logic formulas: a tutorial, (European Educational Forum: School on Formal Methods and Performance Analysis (2000)), 261-277 · Zbl 0990.68088 |
| [55] | Emerson, E. A.; Jutla, C. S., Tree automata, Mu-calculus and determinacy (extended abstract), (Proceedings of the 32nd IEEE Symposium on Foundations of Computer Science (1991)), 368-377 |
| [56] | Janin, D.; Walukiewicz, I., Automata for the modal \(μ\)-calculus and related results, (MFCS. MFCS, LNCS, vol. 969 (1995), Springer-Verlag: Springer-Verlag London, UK), 552-562 · Zbl 1193.68163 |
| [57] | Niwinski, D., Fixed points vs. infinite generation, (Symposium on Logic in Computer Science. Symposium on Logic in Computer Science, LICS ’88 (1988), IEEE Computer Society Press: IEEE Computer Society Press Washington, D.C., USA), 402-409 |
| [58] | Streett, R. S.; Emerson, E. A., An automata theoretic decision procedure for the propositional mu-calculus, Inf. Comput., 81, 3, 249-264 (1989) · Zbl 0671.03023 |
| [59] | Vardi, M. Y., Reasoning about the past with two-way automata, (ICALP. ICALP, LNCS, vol. 1443 (1998)), 628-641 · Zbl 0909.03019 |
| [60] | Baader, F.; Calvanese, D.; McGuinness, D. L.; Nardi, D.; Patel-Schneider, P. F., The Description Logic Handbook: Theory, Implementation and Applications (2010), Cambridge University Press: Cambridge University Press New York, NY, USA · Zbl 1191.68652 |
| [61] | Tobies, S., Complexity results and practical algorithms for logics in knowledge representation, CoRR cs.LO/0106031 |
| [62] | Iosif, R.; Rogalewicz, A.; Vojnar, T., Deciding entailments in inductive separation logic with tree automata, (ATVA’14 (2014)), 201-218 · Zbl 1448.68266 |
| [63] | Traytel, D.; Nipkow, T., Decision procedures for MSO on words based on derivatives of regular expressions (2014), Formal proof development |
| [64] | Pan, G.; Sattler, U.; Vardi, M. Y., Bdd-based decision procedures for the modal logic K, J. Appl. Non-Class. Log., 16, 1-2, 169-208 (2006) · Zbl 1184.68466 |
| [65] | Ramakrishnan, R.; Bothner, P.; Srivastava, D.; Sudarshan, S., CORAL - a database programming language, (Workshop on Deductive Databases (1990)) |
| [66] | Ramakrishnan, R.; Srivastava, D.; Sudarshan, S., CORAL - Control, Relations and Logic, (VLDB ’92: Proceedings of the 18th International Conference on Very Large Data Bases (1992), Morgan Kaufmann Publishers Inc.: Morgan Kaufmann Publishers Inc. San Francisco, CA, USA), 238-250 |
| [67] | Chimenti, D.; Gamboa, R.; Krishnamurthy, R.; Naqvi, S. A.; Tsur, S.; Zaniolo, C., The LDL system prototype, IEEE Trans. Knowl. Data Eng., 2, 1, 76-90 (1990) |
| [68] | Naqvi, S.; Tsur, S., A Logical Language for Data and Knowledge Bases (1989), Computer Science Press |
| [69] | Whaley, J.; Lam, M. S., Cloning-based context-sensitive pointer alias analysis using binary decision diagrams, (Proc. PLDI ’04 (2004)), 131-144 |
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.
