Georg Gottlob
Skip Abstract Section
Abstract
We present Datalog LITE, a new deductive query language with a linear-time model-checking algorithm, that is, linear time data complexity and program complexity. Datalog LITE is a variant of Datalog that uses stratified negation, restricted variable occurrences and a limited form of universal quantification in rule bodies.Despite linear-time evaluation, Datalog LITE is highly expressive: It encompasses popular modal and temporal logics such as CTL or the alternation-free μ-calculus. In fact, these formalisms have natural presentations as fragments of Datalog LITE. Further, Datalog LITE is equivalent to the alternation-free portion of guarded fixed-point logic. Consequently, linear-time model checking algorithms for all mentioned logics are obtained in a unified way.The results are complemented by inexpressibility proofs to the effect that linear-time fragments of stratified Datalog have too limited expressive power.
- ABADI,M.AND MANNA, Z. 1989. Temporal logic programming. J. Logic Prog. 8, 3, 277-295.]] Google Scholar
Digital Library
- ABITEBOUL, S., HULL, R., AND VIANU, V. 1995. Foundations of Databases. Addison-Wesley, Reading, Mass.]] Google ScholarDigital Library
- ABITEBOUL, S., VIANU, V., FORDHAM,B.S.,AND YESHA, Y. 1998. Relational transducers for electronic commerce. In Proceedings of the Seventeenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems. J. Paredaens, Ed. ACM Press. New York, pp. 179-187.]] Google ScholarDigital Library
- ANDREKA, H., VAN BENTHEM,J.,AND NEMETI, I. 1998. Modal languages and bounded fragments of predicate logic. J. Philos. Logic 27, 217-274.]]Google ScholarCross Ref
- APT, K. R., BLAIR,H.A.,AND WALKER, A. 1988. Towards a theory of declarative knowledge. In Foundations of DD and LP, J. Minker, Ed. pp. 89-148.]] Google ScholarDigital Library
- BAUDINET, M. 1989a. Logic programming semantics: Techniques and applications. Ph.D. dissertation, Stanford Univ., Stanford, Calif.]] Google ScholarDigital Library
- BAUDINET, M. 1989b. Temporal logic programming is complete and expressive. In Proceedings of the ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. ACM, New York, pp. 276-280.]] Google ScholarDigital Library
- BAUDINET, M. 1992. A simple proof of the completeness of temporal logic programming. In Intensional Logics for Programming. L. F. del Cerro and M. Penttonen, Eds. Oxford University Press, Oxford, England.]]Google Scholar
- BAUDINET, M. 1995. On the expressiveness of temporal logic programming. Inf. Comput. 117,2, 157-180.]] Google ScholarDigital Library
- BAUDINET, M., CHOMICKI,J.,AND WOLPER, P. 1993. Temporal deductive databases. In Temporal Databases. A. Tansel, J. Clifford, S. Gadia, S. Jajodia, A. Segev, and R. Snodgrass, Eds. Benjamin/Cummings.]]Google Scholar
- BERMAN, K. A., SCHLIPF,J.S.,AND FRANCO, J. V. 1995. Computing well-founded semantics faster. In LPNMR'95, V. Marek and A. Nerode, Eds. Lecture Notes in Computer Science. Springer-Verlag, New York, pp. 113-126.]] Google ScholarDigital Library
- BERWANGER, D. 2000. Games and model checking for guarded logics. Diplomarbeit, RWTH Aachen.]]Google Scholar
- BIERE, A., CIMATTI, A., CLARKE, E., AND ZHU, Y. 1999. Symbolic model checking without BDDs. In TACAS. Springer-Verlag, New York, 193-207.]] Google ScholarDigital Library
- BRYANT, R. E. 1986. Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35, 8, 677-691.]] Google ScholarDigital Library
- BURCH, J. R., CLARKE, E. M., MCMILLAN, K. L., DILL,D.L.,AND HWANG, L. J. 1992. Symbolic model checking: 10 20 states and beyond. Inf. Comput. 98, 2, 142-170.]] Google ScholarDigital Library
- CERI, S., GOTTLOB,G.,AND TANCA, L. 1990. Logic Programming and Databases. Surveys in Computer Science. Springer-Verlag, New York.]] Google ScholarDigital Library
- CHARATONIK,W.AND PODELSKI, A. 1998. Set-based analysis of reactive infinite-state systems. In TACAS'98. B. Steffen, Ed. Lecture Notes in Computer Services, vol, 1384. Springer- Verlag, New York.]] Google ScholarDigital Library
- CHOMICKI, J. 1990a. Functional deductive databases: Query processing in the presence of limited function symbols. Ph.D., Rutgers Univ.]] Google ScholarDigital Library
- CHOMICKI, J. 1990b. Polynomial-time computable queries in temporal deductive databases. In Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS). ACM, New York, pp. 379-391.]] Google ScholarDigital Library
- CHOMICKI,J.AND IMIELINSKI, T. 1988. Temporal deductive databases and infinite objects. In Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS). ACM, New York, pp. 61-73.]] Google ScholarDigital Library
- CHOMICKI,J.AND IMIELINSKI, T. 1989. Relational specifications of infinite query answers. In Proceedings of the ACM SIGMOD International Conference on Management of Data. ACM, New York, pp. 174-183.]] Google ScholarDigital Library
- CLARKE,E.AND EMERSON, E. A. 1981. Design and synthesis of synchronization skeletons using branching time temporal logic. In Logics of Programs: Workshop. Lecture Notes in Computer Science, vol. 131. Springer-Verlag, New York, pp. 52-71.]] Google ScholarDigital Library
- CLARKE, E., GRUMBERG, O., JHA, S., LU,Y.,AND VEITH, H. 2000a. Counterexample-guided abstraction refinement. In Computer-Aided Verification (CAV) 2000. Lecture Notes in Computer Science, vol. 1855. Springer-Verlag, New York. (Full version available as Technical Report CMU-CS-00- 103, Carnegie Mellon University).]] Google ScholarDigital Library
- CLARKE, E., GRUMBERG,O.,AND PELED, D. 2000b. Model Checking. MIT Press, Cambridge, Mass.]] Google ScholarDigital Library
- CLARKE,E.AND SCHLINGLOFF, H. 2000. Model checking. In Handbook of Automated Reasoning. J. Robinson and A. Voronkov, Eds. Elsevier, North-Holland, Amsterdam, The Netherlands, pp. 1635-1790.]] Google ScholarDigital Library
- CLARKE, E. M., GRUMBERG,O.,AND LONG, D. E. 1994. Model checking and abstraction. ACMTrans. Prog. Lang. Syst. (TOPLAS) 16, 5 (Sept.) 1512-1542.]] Google ScholarDigital Library
- CODD, E. 1972. Relational completeness of database sublanguages. In Courant Computer Science Symposium 6: Database Systems, R. Rustin, Ed. vol. 3. Prentice-Hall, Englewood Cliffs, NJ, pp. 65-98.]]Google Scholar
- CONSENS,M.P.AND MENDELZON, A. O. 1993. Low-complexity aggregation in GraphLog and Datalog. Theoret. Comput. Sci. 116, 95-116.]] Google ScholarDigital Library
- COURCELLE, B. 1990. Graph rewriting: An algebraic and logic approach. In Handbook of Theoretical Computer Science, Vol. B. Elsevier, North-Holland, Amsterdam, The Netherlands, pp. 193-242.]] Google ScholarDigital Library
- CUI, B., DONG, Y., DU, X., KUMAR,K.N.,RAMAKRISHNAN, C. R., RAMAKRISHNAN,I.V., ROYCHOUDHURY, A., SMOLKA,S.A.,AND WARREN, D. S. 1998. Logic programming and model checking. In PLAP/ALP'98. C. Palamidessi, H. Glaser, and K. Meinke, Eds. Lecture Notes in Computer Science, vol. 1490. Springer-Verlag, New York, pp. 1-20.]] Google ScholarDigital Library
- DAHLHAUS, E. 1987. Skolem normal forms concerning the least fixpoint. In Computation Theory and Logic. Lecture Notes in Computer Science, vol. 270. Springer-Verlag, New York, pp. 101-106.]] Google ScholarDigital Library
- DANTSIN, E., EITER, T., GOTTLOB,G.,AND VORONKOV, A. 2001. Complexity and expressive power of logic programming. ACM Comput. Surv., to appear.]] Google ScholarDigital Library
- DOWLING,W.F.AND GALLIER, J. H. 1984. Linear-time algorithms for testing the satisfiability of propositional Horn formulae. J. Logic Prog. 1, 3 (Oct.), 267-284.]]Google ScholarCross Ref
- EBBINGHAUS, H.-D. AND FLUM, J. 1999. Finite Model Theory (2nd edition). Springer-Verlag, New York.]]Google Scholar
- EITER, T., GOTTLOB,G.,AND VEITH, H. 1997. Modular logic programming and generalized quantifiers. In LPNMR'97. J. Dix, U. Furbach, and A. Nerode, Eds. Lecture Notes in Computer Science, vol. 1265. Springer-Verlag, New York, pp. 290-309.]] Google ScholarDigital Library
- EITER, T., GOTTLOB,G.,AND VEITH, H. 1999. Generalized quantifiers in logic programs. In Proceedings of the ESSLLI Workshop on Generalized Quantifiers (Aix-en-Provence), France, J. Vaananen, Ed. Lecture Notes in Computer Science, vol. 1754. Springer-Verlag, New York.]] Google ScholarDigital Library
- EMERSON, E. 1990. Temporal and modal logic. In Handbook of Theoretical Computer Science. Vol. B., J. van Leeuven, Ed. Elsevier, North-Holland, Amsterdam, The Netherlands, pp. 995- 1072.]] Google ScholarDigital Library
- FLUM, J. 1999. On the (infinite) model theory of fixed-point logics. In Models, algebras, and proofs. X. Caicedo and C. Montenegro, Eds. Number 2003 in Lecture Notes in Pure and Applied Mathematics Series. Marcel Dekker, pp. 67-75.]]Google Scholar
- GELDER,A.V.,ROSS,K.A.,AND SCHLIPF, J. S. 1991. The well-founded semantics for general logic programs. J. ACM 38, 3 (July), 620-650.]] Google ScholarDigital Library
- GOTTLOB, G., GR~DEL, E., AND VEITH, H. 2000. Linear-time datalog and branching time logic. In Logic-Based Artificial Intelligence, J. Minker, Ed. Kluwer, pp. 443-468.]] Google ScholarDigital Library
- GOTTLOB, G., LEONE,N.,AND VEITH, H. 1999. Succinctness as a source of complexity in logical formalisms. Ann. Pure Appl. Logic 97(1-3), 231-260.]]Google ScholarCross Ref
- GRADEL, E. 1992. On transitive closure logic. In CSL 91. Lecture Notes in Computer Science, vol. 626. Springer-Verlag, New York, pp. 149-163.]] Google ScholarDigital Library
- GRADEL, E. 1999a. Decision procedures for guarded logics. In Automated Deduction-CADE16. Proceedings of 16th International Conference on Automated Deduction (Trento, Italy). Lecture Notes in Artificial Intelligence, vol. 1632. Springer-Verlag, New York.]] Google ScholarDigital Library
- GRADEL, E. 1999b. On the restraining power of guards. J. Symb. Logic 64, 1719-1742.]]Google ScholarCross Ref
- GRADEL, E. 1999c. Why are modal logics so robustly decidable? Bull. EATCS 68, 90-103.]]Google Scholar
- GRADEL,E.AND WALUKIEWICZ, I. 1999. Guarded fixed point logic. In Proceedings of the 14th IEEE Symposium on Logic in Computer Science. G. Longo, Ed. IEEE Computer Society Press, Los Alamitos, Calif., pp. 45-54.]] Google ScholarDigital Library
- IMMERMAN, N. 1988. Nondeterministic space is closed under complementation. SIAM J. Com-put. 17, 5, 935-938.]] Google ScholarDigital Library
- IMMERMAN,N.AND VARDI, M. Y. 1997. Model checking and transitive-closure logic. In Proceedings of the CAV 1997. O. Grumberg, Ed. Lecture Notes in Computer Science, vol. 1254. Springer-Verlag, New York, pp. 291-302.]] Google ScholarDigital Library
- ITAI,A.AND MAKOWSKY, J. A. 1987. Unification as a complexity measure for logic programming. J. Logic Prog. 4, 2 (June), 105-117.]] Google ScholarDigital Library
- JANIN,D.AND WALUKIEWICZ, I. 1996. On the expressive completeness of the propositional mucalculus with respect to monadic second order logic. In CONCUR 96. Lecture Notes in Computer Science, vol. 1119. Springer-Verlag, New York, pp. 263-277.]] Google ScholarDigital Library
- JURDZINSKI, M. 2000. Small progress measures for solving parity games. In STACS 2000, Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer Science. Lecture Notes in Computer Science, vol. 1770. Springer-Verlag, New York, pp. 290-301.]] Google ScholarDigital Library
- KOLAITIS, P. G. 1990. Implicit definability on finite structures and unambiguous computations. Inf. Comput. 90, 50-66.]] Google ScholarDigital Library
- KOZEN, D. 1983. Results on the propositional calculus. Theoret. Comput. Sci. 27, 3 (Dec.), 333- 354.]]Google ScholarCross Ref
- KURSHAN, R. P. 1994. Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton, N.J.]] Google ScholarDigital Library
- LIU, X., RAMAKRISHNAN,C.,AND SMOLKA, S. 1998. Fully local and efficient evaluation of alternating fixed points. In TACAS'98. Lecture Notes in Computer Science, vol. 1384. Springer-Verlag, New York.]] Google ScholarDigital Library
- MCMILLAN, K. L. 1993. Symbolic Model Checking. Kluwer.]] Google ScholarDigital Library
- MINOUX, M. 1988. LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation. Inf. Proc. Lett. 29, 1 (15 Sept.), 1-12.]] Google ScholarDigital Library
- MORET,B.AND SHAPIRO, H. 1990. Algorithms from P to NP. Benjamin/Cummings.]]Google Scholar
- MURAKAMI, M. 1990. A declarative semantics of flat guarded Horn clauses for programs with perpetual processes. Theoret. Comput. Sci. 75, 1-2 (25 Sept.), 67-83.]] Google ScholarDigital Library
- PELED, D. A., PRATT,V.R.,AND HOLZMANN,G.J.,EDS. 1997. Partial Order Methods in Verification. DIMACS series, vol. 29. American Mathematical Society, Providence, R.I.]]Google Scholar
- RAMAKRISHNAN,Y.S.,RAMAKRISHNAN, C. R., RAMAKRISHNAN,I.V.,SMOLKA, S. A., SWIFT,T.,AND WARREN, D. S. 1997. Efficient model checking using tabled resolution. In Proceedings of the CAV'97, O. Grumberg, Ed. Lectures Notes in Computer Science, vol. 1254. Springer-Verlag, New York, pp. 143-154.]] Google ScholarDigital Library
- SEESE, D. 1996. Linear time computable problems and first-order descriptions. Math. Struct. Comput. Sci. 6, 6 (Dec.), 505-526.]]Google ScholarCross Ref
- ULLMAN, J. D. 1989. Principles of Data Base Systems. Computer Science Press.]] Google ScholarDigital Library
- VAN EMDE BOAS, P. 1990. Machine models and simulation. In Handbook of Theoretical Computer Science, vol. A. J. van Leeuven, Ed. Elsevier, North-Holland, Amsterdam, The Netherlands, pp. 1-66.]] Google ScholarDigital Library
- VARDI, M. 1982. Complexity of relational query languages. In Proceedings of the 14th Annual ACM Symposium on Theory of Computing (San Francisco, Calif.). ACM, New York, pp. 137-146.]] Google ScholarDigital Library
- VARDI, M. Y. 1998. Reasoning about the past with two-way automata. In ICALP, K. G. Larsen, S. Skyum, and G. Winskel, Eds. Lecture Notes in Computer Science, vol. 1443. Springer-Verlag, New York, pp. 628-641.]] Google ScholarDigital Library
- VARDI,M.AND WOLPER, P. 1994. Reasoning about infinite computations. Inf. Comput. 115, 1, 1-37.]] Google ScholarDigital Library
- WOLPER, P. 1983. Temporal logic can be more expressive. Inf. Cont. 56, 1-2, 72-99.]]Google ScholarCross Ref
Index Terms
- Datalog LITE: a deductive query language with linear time model checking
Recommendations
On temporal logic versus datalog
Logic and complexity in computer scienceWe provide a direct and modular translation from the temporal logics CTL, ETL, FCTL (CTL extended with the ability to express fairness) and the Modal µ-calculus to Monadic inf-Datalog with built-in predicates. We call it inf-Datalog because the ...
Clausal resolution in a logic of rational agency
A resolution based proof system for a Temporal Logic of Possible Belief is presented. This logic is the combination of the branching-time temporal logic CTL (representing change over time) with the modal logic KD45 (representing belief). Such ...
Disjunctive datalog with existential quantifiers: Semantics, decidability, and complexity issues
Datalog is one of the best-known rule-based languages, and extensions of it are used in a wide context of applications. An important Datalog extension is Disjunctive Datalog , which significantly increases the expressivity of the basic language. ...
Comments