Inf-datalog, modal logic and complexities

Eugénie Foustoucos; Irène Guessarian

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (2009)

  • Volume: 43, Issue: 1, page 1-21
  • ISSN: 0988-3754

Abstract

top
Inf-Datalog extends the usual least fixpoint semantics of Datalog with greatest fixpoint semantics: we defined inf-Datalog and characterized the expressive power of various fragments of inf-Datalog in [16]. In the present paper, we study the complexity of query evaluation on finite models for (various fragments of) inf-Datalog. We deduce a unified and elementary proof that global model-checking (i.e. computing all nodes satisfying a formula in a given structure) has 1. quadratic data complexity in time and linear program complexity in space for C T L and alternation-free modal μ -calculus, and 2. linear-space (data and program) complexities, linear-time program complexity and polynomial-time data complexity for L μ k (modal μ -calculus with fixed alternation-depth at most k ).

How to cite

top

Foustoucos, Eugénie, and Guessarian, Irène. "Inf-datalog, modal logic and complexities." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 43.1 (2009): 1-21. <http://eudml.org/doc/245704>.

@article{Foustoucos2009,
abstract = {Inf-Datalog extends the usual least fixpoint semantics of Datalog with greatest fixpoint semantics: we defined inf-Datalog and characterized the expressive power of various fragments of inf-Datalog in [16]. In the present paper, we study the complexity of query evaluation on finite models for (various fragments of) inf-Datalog. We deduce a unified and elementary proof that global model-checking (i.e. computing all nodes satisfying a formula in a given structure) has 1. quadratic data complexity in time and linear program complexity in space for $CTL$ and alternation-free modal $\mu $-calculus, and 2. linear-space (data and program) complexities, linear-time program complexity and polynomial-time data complexity for $L\mu _k$ (modal $\mu $-calculus with fixed alternation-depth at most $k$).},
author = {Foustoucos, Eugénie, Guessarian, Irène},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},
keywords = {databases; model-checking; specification languages; performance evaluation},
language = {eng},
number = {1},
pages = {1-21},
publisher = {EDP-Sciences},
title = {Inf-datalog, modal logic and complexities},
url = {http://eudml.org/doc/245704},
volume = {43},
year = {2009},
}

TY - JOUR
AU - Foustoucos, Eugénie
AU - Guessarian, Irène
TI - Inf-datalog, modal logic and complexities
JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY - 2009
PB - EDP-Sciences
VL - 43
IS - 1
SP - 1
EP - 21
AB - Inf-Datalog extends the usual least fixpoint semantics of Datalog with greatest fixpoint semantics: we defined inf-Datalog and characterized the expressive power of various fragments of inf-Datalog in [16]. In the present paper, we study the complexity of query evaluation on finite models for (various fragments of) inf-Datalog. We deduce a unified and elementary proof that global model-checking (i.e. computing all nodes satisfying a formula in a given structure) has 1. quadratic data complexity in time and linear program complexity in space for $CTL$ and alternation-free modal $\mu $-calculus, and 2. linear-space (data and program) complexities, linear-time program complexity and polynomial-time data complexity for $L\mu _k$ (modal $\mu $-calculus with fixed alternation-depth at most $k$).
LA - eng
KW - databases; model-checking; specification languages; performance evaluation
UR - http://eudml.org/doc/245704
ER -

References

top
  1. [1] S. Abiteboul, R. Hull and V. Vianu, Foundations of databases. Addison-Wesley (1995). Zbl0848.68031
  2. [2] A. Arnold and P. Crubillé, A linear algorithm to solve fixed-point equations on transition systems. Inform. Process. Lett. 29 (1988) 57–66. Zbl0663.68075MR974202
  3. [3] A. Arnold and D. Niwiński, Rudiments of μ -calculus. Stud. Logic Found. Math. 146, Elsevier Science, North-Holland, Amsterdam (2001). Zbl0968.03002MR1854973
  4. [4] J. Bradfield, Fixpoint alternation: Arithmetic, transition systems, and the binary tree. RAIRO-Theor. Inf. Appl. 33 (1999) 341–356. Zbl0945.68126MR1748660
  5. [5] A. Browne, E. Clarke, S. Jha, D. Long and W. Marrero, An improved algorithm for the evaluation of fixpoint expressions. Theor. Comput. Sci. 178 (1997) 237–255. Zbl0901.68118MR1453852
  6. [6] W. Charatonik, D. McAllester, D. Niwínski, A. Podelski and I. Walukiewicz, The horn Mu-calculus. LICS (1998) 58–69. Zbl0945.03541MR1654520
  7. [7] E.M. Clarke, E.A. Emerson and A.P. Sistla, Automatic Verification of finite-state concurrent systems using temporal logic specifications. ACM TOPLAS 8 (1986) 244–263. Zbl0591.68027
  8. [8] R. Cleaveland and B. Steffan, A linear time model-checking algorithm for the alternation-free modal mu-calculus. Formal Method. Syst. Des. 2 (1993) 121–148. Zbl0772.68038
  9. [9] E. Emerson, Temporal and modal logic. Handbook of Theoretical Computer Science (1990) 997–1072. Zbl0900.03030MR1127201
  10. [10] E. Emerson, Model-Checking and the Mu-Calculus, in Descriptive Complexity and Finite Models, edited by N. Immerman and Ph. Kolaitis, American Mathematical Society (1997). Zbl0877.03020MR1451385
  11. [11] E.A. Emerson and C.L. Lei, Efficient model-checking in fragments of the propositional μ -calculus, in Proc. of 1rst Symposium on Logic in Computer Science (1986) 267–278. 
  12. [12] E. Foustoucos and I. Guessarian, Complexity of Monadic inf-datalog. Application to temporal logic. Extended abstract in Proceedings 4th Panhellenic Logic Symposium (2003) 95–99. 
  13. [13] G. Gottlob and C. Koch, Monadic Datalog and the expressive power of web information extraction languages. Proc. PODS’02 (2002) 17–28. Zbl1316.68045
  14. [14] G. Gottlob, E. Grädel and H. Veith, Datalog LITE: temporal versus deductive reasoning in verification. ACM T. Comput. Log. 3 (2002) 39–74. MR1902106
  15. [15] A. Griffault and A. Vincent, The Mec 5 model-checker, CAV’04. Lect. Notes Comput. Sci. 3114 (2004) 488–491. Zbl1103.68619
  16. [16] I. Guessarian, E. Foustoucos, T. Andronikos and F. Afrati, On temporal logic versus Datalog. Theor. Comput. Sci. 303 (2003) 103–133. Zbl1019.03021MR1990744
  17. [17] M. Jurdzinski, Small progress measures for solving parity games. Proc. STACS’2000 (2000) 290–301. Zbl0962.68111MR1781740
  18. [18] M. Jurdzinski, M. Paterson and U. Zwick, A Deterministic subexponential algorithm for solving parity games. Proc. SODA (2006) 117–123. Zbl1192.91013MR2368806
  19. [19] D. Kozen, Results on the propositional μ -calculus. Theor. Comput. Sci. 27 (1983) 333–354. Zbl0553.03007MR731069
  20. [20] A. Mader, The modal μ -calculus, model-checking, equations systems and Gauss elimination. TACAS 95 (1995) 44–57. 
  21. [21] D. Park, Finiteness is μ -ineffable. Theor. Comput. Sci. 3 (1976) 173–181. Zbl0353.02027MR437297
  22. [22] H. Seidl, Fast and simple nested fixpoints. Inform. Process. Lett. 59 (1996) 303–308. Zbl0900.68458MR1417647
  23. [23] A. Vincent, Conception et réalisation d’un vérificateur de modèles AltaRica. Ph.D. Thesis, LaBRI, University of Bordeaux 1 (2003) http://altarica.labri.fr/Doc/Biblio/Author/VINCENT-A.html 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.