Inf-datalog, Modal Logic and Complexities

Eugénie Foustoucos; Irène Guessarian

RAIRO - Theoretical Informatics and Applications (2007)

  • 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 [CITE]. 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 μ-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 43.1 (2007): 1-21. <http://eudml.org/doc/92905>.

@article{Foustoucos2007,
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 [CITE]. 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 μ-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). },
author = {Foustoucos, Eugénie, Guessarian, Irène},
journal = {RAIRO - Theoretical Informatics and Applications},
keywords = {Databases; model-checking; specification languages; performance evaluation.; databases; performance evaluation},
language = {eng},
month = {12},
number = {1},
pages = {1-21},
publisher = {EDP Sciences},
title = {Inf-datalog, Modal Logic and Complexities},
url = {http://eudml.org/doc/92905},
volume = {43},
year = {2007},
}

TY - JOUR
AU - Foustoucos, Eugénie
AU - Guessarian, Irène
TI - Inf-datalog, Modal Logic and Complexities
JO - RAIRO - Theoretical Informatics and Applications
DA - 2007/12//
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 [CITE]. 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 μ-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).
LA - eng
KW - Databases; model-checking; specification languages; performance evaluation.; databases; performance evaluation
UR - http://eudml.org/doc/92905
ER -

References

top
  1. S. Abiteboul, R. Hull and V. Vianu, Foundations of databases. Addison-Wesley (1995).  Zbl0848.68031
  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.68075
  3. A. Arnold and D. Niwiński, Rudiments of µ-calculus. Stud. Logic Found. Math.146, Elsevier Science, North-Holland, Amsterdam (2001).  
  4. J. Bradfield, Fixpoint alternation: Arithmetic, transition systems, and the binary tree. RAIRO-Theor. Inf. Appl.33 (1999) 341–356.  Zbl0945.68126
  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.68118
  6. W. Charatonik, D. McAllester, D. Niwínski, A. Podelski and I. Walukiewicz, The horn Mu-calculus. LICS (1998) 58–69.  Zbl0945.03541
  7. E.M. Clarke, E.A. Emerson and A.P. Sistla, Automatic Verification of finite-state concurrent systems using temporal logic specifications. ACM TOPLAS8 (1986) 244–263.  Zbl0591.68027
  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. E. Emerson, Temporal and modal logic. Handbook of Theoretical Computer Science (1990) 997–1072.  Zbl0900.03030
  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.03020
  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. 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. 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. G. Gottlob, E. Grädel and H. Veith, Datalog LITE: temporal versus deductive reasoning in verification. ACM T. Comput. Log.3 (2002) 39–74.  
  15. A. Griffault and A. Vincent, The Mec 5 model-checker, CAV'04. Lect. Notes Comput. Sci.3114 (2004) 488–491.  Zbl1103.68619
  16. I. Guessarian, E. Foustoucos, T. Andronikos and F. Afrati, On temporal logic versus Datalog. Theor. Comput. Sci.303 (2003) 103–133.  Zbl1019.03021
  17. M. Jurdzinski, Small progress measures for solving parity games. Proc. STACS'2000 (2000) 290–301.  Zbl0962.68111
  18. M. Jurdzinski, M. Paterson and U. Zwick, A Deterministic subexponential algorithm for solving parity games. Proc. SODA (2006) 117–123.  Zbl1192.91013
  19. D. Kozen, Results on the propositional µ-calculus. Theor. Comput. Sci.27 (1983) 333–354.  Zbl0553.03007
  20. A. Mader, The modal µ-calculus, model-checking, equations systems and Gauss elimination. TACAS95 (1995) 44–57.  
  21. D. Park, Finiteness is µ-ineffable. Theor. Comput. Sci.3 (1976) 173–181.  Zbl0353.02027
  22. H. Seidl, Fast and simple nested fixpoints. Inform. Process. Lett.59 (1996) 303–308.  Zbl0900.68458
  23. A. Vincent, Conception et réalisation d'un vérificateur de modèles AltaRica. Ph.D. Thesis, LaBRI, University of Bordeaux 1 (2003)  URIhttp://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.