×

On temporal logic versus Datalog. (English) Zbl 1019.03021

Summary: We provide a direct and modular translation from the temporal logics CTL, ETL, FCTL (CTL extended with the ability to express fairness) and the modal \(\mu\)-calculus to monadic inf-Datalog with built-in predicates. We call it inf-Datalog because the semantics we provide is a little different from the conventional Datalog least fixed-point semantics, in that some recursive rules (corresponding to least fixed points) are allowed to unfold only finitely many times, whereas others (corresponding to greatest fixed points) are allowed to unfold infinitely many times.
We characterize the fragments of monadic inf-Datalog that have the same expressive power as modal logic (resp. CTL, alternation-free modal \(\mu\)-calculus and modal \(\mu\)-calculus). Our translation is interesting because it is direct and succinct. Moreover the fragments of monadic inf-Datalog that we have exhibited have very simple syntactic characterizations as subsets of what we call modal inf-Datalog programs.

MSC:

03B70 Logic in computer science
68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
68N17 Logic programming

Software:

Datalog; Oz
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abiteboul, S.; Hull, R.; Vianu, V., Foundations of Databases (1995), Addison-Wesley: Addison-Wesley New York · Zbl 0848.68031
[2] Andreka, H.; Bethem, van; Nemeti, I., Modal languages and bounded fragments of predicate logic, J. Philos. Logic, 27, 217-274 (1998) · Zbl 0919.03013
[3] Arnold, A., Finite Transition Systems, Semantics of communicating systems, C.A.R. Hoare International series (1994), Prentice-Hall: Prentice-Hall London
[4] Arnold, A.; Niwiński, D., Rudiments of \(μ\)-calculus, Studies in Logic and the Foundations of Mathematics, Vol. 146 (2001), Elsevier Science: Elsevier Science North-Holland, Amsterdam · Zbl 0968.03002
[5] Bradfield, J., Fixpoint alternation: arithmetic, transition systems, and the binary tree, in: Theoretical Informatics and Applications, 33, 341-356 (1999) · Zbl 0945.68126
[6] Bradfield, J.; Stirling, C., Modal logics and \(μ\)-calculi: an introduction, (Bergstra, J.; Ponse, A.; Smolka, S., Handbook of Process Algebra (2001), Elsevier: Elsevier North-Holland, Amsterdam), 293-332 · Zbl 1002.03021
[7] Charatonik, W.; Podelski, A., Set-based analysis of reactive infinite-state systems, (TACAS’98, Lecture Notes in Computer Science (1998), Springer: Springer Berlin), 358-375
[8] E.M. Clarke, E.A. Emerson, A.P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM TOPLAS, Vol. 8, 1986, pp. 244-263.; E.M. Clarke, E.A. Emerson, A.P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM TOPLAS, Vol. 8, 1986, pp. 244-263. · Zbl 0591.68027
[9] Corsini, M.-M.; Rauzy, A., Toupiethe \(μ\)-calculus over finite domains as a constraint language, J. Automat. Reason., 19, 2, 143-171 (1997) · Zbl 0941.03532
[10] (Cui, B.; Dong, Y.; Du, X.; Kumar, K. N.; Ramakrishnan, C. R.; Ramakrishnan, I. V.; Roychoudhury, A.; Smolka, S. A.; Warren, D. S., Logic programming and model checking, in PLAP/ALP’98. Logic programming and model checking, in PLAP/ALP’98, Lecture Notes in Computer Science, Vol. 85 (1998), Springer: Springer Berlin), 1-20
[11] Dam, M., \(CTL^*\) and E \(CTL^*\) as fragments of the modal \(μ\)-calculus, Theoret. Comput. Sci., 126, 77-96 (1994) · Zbl 0798.03018
[12] Emerson, E., Temporal and modal logic, Handbook of Theoret. Comput. Sci., 2, 997-1072 (1990) · Zbl 0900.03030
[13] Emerson, E., Model checking and the \(μ\)-calculus, (Immerman, N.; Kolaitis, Ph., Descriptive Complexity and Finite Models (1997), American Mathematical Society: American Mathematical Society Providence, RI) · Zbl 0877.03020
[14] Emerson, E. A.; Clarke, E. M., Characterizing correctness properties of parallel programs using fixpoints, (ICALP’80. ICALP’80, Lecture Notes in Computer Science, Vol. 85 (1980), Springer: Springer Berlin), 169-181 · Zbl 0456.68016
[15] Emerson, E. A.; Halpern, J. Y., Sometimes and not never revisitedon branching versus linear time, J. Assoc. Comput., 33, 1, 151-178 (1986) · Zbl 0629.68020
[16] E.A. Emerson, C.L. Lei, Efficient model checking in fragments of the propositional \(μ\); E.A. Emerson, C.L. Lei, Efficient model checking in fragments of the propositional \(μ\)
[17] E.A. Emerson, C.L. Lei, Modalities for model checking: branching time logic strikes back, Sci. Comput. Programming (1987) 275-306.; E.A. Emerson, C.L. Lei, Modalities for model checking: branching time logic strikes back, Sci. Comput. Programming (1987) 275-306. · Zbl 0615.68019
[18] Fariñas del Cerro, L.; Penttonen, M., A note on the complexity of the satisfiability of modal Horn clauses, Logic Programming, 4, 1-10 (1987) · Zbl 0624.03010
[19] Gottlob, G.; Grädel, E.; Veith, H., Datalog LITEtemporal versus deductive reasoning in verification, ACM Trans. Comput. Logic, 3, 39-74 (2002)
[20] (Hafer, T.; Thomas, W., Computation tree logic \(CTL^*\) and path quantifiers in the monadic theory of the binary tree, ICALP’87. Computation tree logic \(CTL^*\) and path quantifiers in the monadic theory of the binary tree, ICALP’87, Lecture Notes in Computer Science, Vol. 267 (1987), Springer: Springer Berlin), 269-279 · Zbl 0632.03027
[21] Immermann, N.; Vardi, M., Model checking and transitive-closure logic, (CAV’97. CAV’97, Lecture Notes in Computer Science, Vol. 1254 (1997), Springer: Springer Berlin), 291-302
[22] D. Janin, G. Lenzi, Relating levels of the \(μ\); D. Janin, G. Lenzi, Relating levels of the \(μ\)
[23] D. Janin, I. Walukiewicz, On the expressive completeness of the propositional \(μ\); D. Janin, I. Walukiewicz, On the expressive completeness of the propositional \(μ\)
[24] Kozen, D., Results on the propositional \(μ\)-calculus, Theoret. Comput. Sci., 27, 333-354 (1983) · Zbl 0553.03007
[25] Kupferman, O.; Vardi, M.; Wolper, P., An automata-theoretic approach to branching-time model checking, JACM, 47, 2, 312-360 (2000) · Zbl 1133.68376
[26] L. Lamport, Sometimes is sometimes “not never”-on the temporal logic of programs, in: Proceedings of the Seventh ACM Symposium on Principles of Programming Languages, 1980, pp. 174-185.; L. Lamport, Sometimes is sometimes “not never”-on the temporal logic of programs, in: Proceedings of the Seventh ACM Symposium on Principles of Programming Languages, 1980, pp. 174-185.
[27] Manna, Z.; Pnueli, A., The Temporal Logic of Reactive and Concurrent Systems: Specification (1992), Springer: Springer Berlin
[28] F. Moller, A. Rabinovich, On the expressive power of \(CTL^*\); F. Moller, A. Rabinovich, On the expressive power of \(CTL^*\) · Zbl 1019.03023
[29] L.A. Nguyen, The Modal Query Language MDatalog, Fundamenta Informaticae, http://www.mimuw.edu.pl/ nguyen/; L.A. Nguyen, The Modal Query Language MDatalog, Fundamenta Informaticae, http://www.mimuw.edu.pl/ nguyen/ · Zbl 0991.68021
[30] Niwiński, D., Fixed point characterization of infinite behavior of finite-state systems, TCS Fundamental Study, Theoret. Comput. Sci., 189, 1-69 (1997) · Zbl 0893.68102
[31] D. Park, Fixpoint induction and proof of program semantics, in: Machine Intelligence, Vol. 5, Edinburgh University Press (1969) 59-78.; D. Park, Fixpoint induction and proof of program semantics, in: Machine Intelligence, Vol. 5, Edinburgh University Press (1969) 59-78. · Zbl 0219.68007
[32] A. Pnueli, The temporal logic of programs, in: Proceedings of the 18th IEEE Symposium on Foundation of Computer Science, 1977, pp. 46-57.; A. Pnueli, The temporal logic of programs, in: Proceedings of the 18th IEEE Symposium on Foundation of Computer Science, 1977, pp. 46-57.
[33] Ramakrishnan, Y. S.; Ramakrishnan, C. R.; Ramakrishnan, I. V.; Smolka, S. A.; Swift, T.; Warren, D. S., Efficient model checking using tabled resolution, (CAV’97. CAV’97, Lecture Notes in Computer Science, Vol. 1254 (1997), Springer: Springer Berlin), 143-154
[34] Thomas, W., Automata on infinite objects, Handbook Theoret. Comput. Sci., 1, 133-191 (1990) · Zbl 0900.68316
[35] Ullman, J. D., Implementation of logical query languages for databases, ACM Trans. Database Systems, 10, 3, 289-321 (1985) · Zbl 0573.68060
[36] Ullman, J. D., Database and Knowledge-Base Systems, Vols. I and II (1989), Computer Science Press: Computer Science Press Rockville, MD
[37] M. Vardi, P. Wolper, An automata-theoretic approach to automatic program verification, Proceedings of the First Symposium on Logic in Computer Science, 1986, pp. 322-331.; M. Vardi, P. Wolper, An automata-theoretic approach to automatic program verification, Proceedings of the First Symposium on Logic in Computer Science, 1986, pp. 322-331.
[38] Vardi, M. Y.; Wolper, P., Reasoning about infinite computation, Inform. Comput., 115, 1, 1-37 (1994) · Zbl 0827.03009
[39] T. Wilke, \(CTL^+\); T. Wilke, \(CTL^+\) · Zbl 0952.03017
[40] P. Wolper, Temporal logic can be more expressive, in: Proceedings of the 22nd IEEE Symposium on Foundations of Computer Science, 1981, pp. 340-348.; P. Wolper, Temporal logic can be more expressive, in: Proceedings of the 22nd IEEE Symposium on Foundations of Computer Science, 1981, pp. 340-348.
[41] P. Wolper, M.Y. Vardi, A.P. Sistla, Reasoning about infinite computation paths, in: Proceedings of the 24th IEEE Symposium on Foundations of Computer Science, Tucson, 1983, pp. 185-194.; P. Wolper, M.Y. Vardi, A.P. Sistla, Reasoning about infinite computation paths, in: Proceedings of the 24th IEEE Symposium on Foundations of Computer Science, Tucson, 1983, pp. 185-194.
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.