Abstract
We investigate the model checking problems for guarded first-order and fixed point logics byreducing them to paritygames. This approach is known to provide good results for the modal μ-calculus and is verycloselyrelated to automata-based methods. To obtain good results also for guarded logics, optimized constructions of games have to be provided.
Further, we studythe structure of paritygames, isolate ‘easy’ cases that admit efficient algorithmic solutions, and determine their relationship to specific fragments of guarded fixed point logics.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
H. Andréka, J. van Benthem, and I. Németi, Modal languages and bounded fragments of predicate logic, Journal of Philosophical Logic, 27 (1998), 217–274.
D. Berwanger, Games and model checking for guarded logics. Diploma thesis, RWTH Aachen, 2000.
R. Bloem, H. Gabow, and F. Somenzi, An algorithm for strongly connected component analysis in n log n symbolic steps, in Formal Methods in Computer Aided Design, LNCS Nr. 1954 (2000), 37–54.
S. Dziembowski, Bounded-variable fixpoint queries are PSPACE-complete, Computer Science Logic CSL 96. LNCS Nr. 1258 (1996), 89–105.
A. Emerson and C. Jutla, Tree automata, mu-calculus and determinacy, in Proc. 32nd IEEE Symp. on Foundations of Computer Science, 1991, 368–377.
A. Emerson and C. Jutla and A. P. Sistla, On model checking for the μ-calculus and its fragments, Theoretical Computer Science 258 (2001), 491–522.
J. Flum, M. Frick, and M. Grohe, Query evaluation via tree-decompositions, in Database Theory-ICDT 2001, LNCS Nr. 1973 (2001), 22–38.
H. Ganzinger, C. Meyer, and M. Veanes, The two-variable guarded fragment with transitive relations, in Proc. 14th IEEE Symp. on Logic in Computer Science, 1999, 24–34.
G. Gottlob, E. Grädel, and H. Veith, Datalog LITE: A deductive query language with linear time model checking, ACM Transactions on Computational Logic, (to appear).
G. Gottlob, N. Leone, and F. Scarcello, Robbers, marshals, and guards: Game theoretic and logical characterizations of hypertree width, in Proc. 20th ACM Symp. on Principles of Database Systems, 2001, 195–201.
E. Grädel, On the restraining power of guards, Journal of Symbolic Logic, 64 (1999), 1719–1742.
E. Grädel, Guarded fixed point logics and the monadic theory of countable trees, to appear in Theoretical Computer Science, (2001).
E. Grädel, Why are modal logics so robustly decidable?, in Current Trends in Theoretical Computer Science. Entering the 21st Century, G. Paun, G. Rozenberg, and A. Salomaa, eds., World Scientific, 2001, 393–498.
E. Grädel and M. Otto, On logics with two variables, Theoretical Computer Science, 224 (1999), 73–113.
E. Grädel and I. Walukiewicz, Guarded fixed point logic, in Proc. 14th IEEE Symp. on Logic in Computer Science, 1999, 45–54.
B. Herwig, Zur Modelltheorie von Lμ. Dissertation, Universität Freiburg, 1989.
M. Jurdzinski, Deciding the winner in parity games is in UP ∩ Co-UP., Information Processing Letters, 68 (1998), 119–124.
M. Jurdziński, Small progress measures for solving parity games, Proceedings of STACS 2000, LNCS Nr. 1770 (2000), 290–301.
V. King, O. Kupferman, and M. Vardi, On the complexity of parity word automata, in Proceedings of FOSSACS 2001, LNCS Nr. 2030 (2001), 276–286.
O. Kupferman, M. Vardi, and P. Wolper, An automata-theoretic approach to branching-time model checking, Journal of the ACM, 47 (2000), 312–360.
C. Stirling, Bisimulation, model checking and other games. Notes for the Mathfit instructional meeting on games and computation. Edinburgh, 1997.
M. Vardi, On the complexity of bounded-variable queries, in Proc. 14th ACM Symp. on Principles of Database Systems, 1995, 266–267.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Berwanger, D., Grädel, E. (2001). Games and Model Checking for Guarded Logics. In: Nieuwenhuis, R., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2001. Lecture Notes in Computer Science(), vol 2250. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45653-8_5
Download citation
DOI: https://doi.org/10.1007/3-540-45653-8_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42957-9
Online ISBN: 978-3-540-45653-7
eBook Packages: Springer Book Archive