Document Open Access Logo

Guarded Teams: The Horizontally Guarded Case

Authors Erich Grädel, Martin Otto

PDF
Thumbnail PDF

File

LIPIcs.CSL.2020.22.pdf
  • Filesize: 0.49 MB
  • 17 pages

Document Identifiers

Author Details

Erich Grädel
  • RWTH Aachen University, Germany
Martin Otto
  • Technische Universität Darmstadt, Germany

Acknowledgements

We gratefully acknowledge participation in the programme on Logical Structure in Computation at the Simons Institute in Berkeley in 2016, which provided interesting stimulation towards this work.

Cite AsGet BibTex

Erich Grädel and Martin Otto. Guarded Teams: The Horizontally Guarded Case. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CSL.2020.22

Abstract

Team semantics admits reasoning about large sets of data, modelled by sets of assignments (called teams), with first-order syntax. This leads to high expressive power and complexity, particularly in the presence of atomic dependency properties for such data sets. It is therefore interesting to explore fragments and variants of logic with team semantics that permit model-theoretic tools and algorithmic methods to control this explosion in expressive power and complexity. We combine here the study of team semantics with the notion of guarded logics, which are well-understood in the case of classical Tarski semantics, and known to strike a good balance between expressive power and algorithmic manageability. In fact there are two strains of guardedness for teams. Horizontal guardedness requires the individual assignments of the team to be guarded in the usual sense of guarded logics. Vertical guardedness, on the other hand, posits an additional (or definable) hypergraph structure on relational structures in order to interpret a constraint on the component-wise variability of assignments within teams. In this paper we investigate the horizontally guarded case. We study horizontally guarded logics for teams and appropriate notions of guarded team bisimulation. In particular, we establish characterisation theorems that relate invariance under guarded team bisimulation with guarded team logics, but also with logics under classical Tarski semantics.

Subject Classification

ACM Subject Classification
  • Theory of computation → Finite Model Theory
Keywords
  • Team semantics
  • guarded logics
  • bisimulation
  • characterisation theorems

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. S. Abramsky, J. Kontinen, J. Väänänen, and H. Vollmer, editors. Dependence Logic. Theory and Applications. Birkhäuser, 2016. Google Scholar
  2. H. Andréka, J. van Benthem, and I. Németi. Modal Languages and Bounded Fragments of Predicate Logic. Journal of Philosophical Logic, 27:217-274, 1998. Google Scholar
  3. V. Bárány, G. Gottlob, and M. Otto. Querying the Guarded Fragment. In Proceedings of the 2010 25th Annual IEEE Symposium on Logic in Computer Science, LICS '10, pages 1-10, 2010. Google Scholar
  4. V. Bárány, B. ten Cate, and L. Segoufin. Guarded Negation. J. ACM, 62(3):22:1-22:26, 2015. Google Scholar
  5. M. Benedikt, P. Bourhis, and M. Vanden Boom. Characterizing Definability in Decidable Fixpoint Logics. In 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, pages 107:1-107:14, 2017. Google Scholar
  6. P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. Cambridge University Press, 2001. Google Scholar
  7. H.-D. Ebbinghaus and J. Flum. Finite Model Theory. Springer, 2nd edition, 1999. Google Scholar
  8. H.-D. Ebbinghaus, J. Flum, and W. Thomas. Mathematical Logic. Springer, 1994. Google Scholar
  9. P. Galliani. Inclusion and exclusion in team semantics - On some logics of imperfect information. Annals of Pure and Applied Logic, 163:68-84, 2012. Google Scholar
  10. P. Galliani and L. Hella. Inclusion logic and fixed-point logic. In Computer Science Logic 2013, pages 281-295, 2013. Google Scholar
  11. V. Goranko and M. Otto. Model Theory of Modal Logic. In P. Blackburn, J. van Benthem, and F. Wolter, editors, Handbook of Modal Logic, pages 249-329. Elsevier, 2007. Google Scholar
  12. E. Grädel. On the restraining power of guards. Journal of Symbolic Logic, 64:1719-1742, 1999. Google Scholar
  13. E. Grädel. Guarded fixed point logics and the monadic theory of countable trees. Theoretical Computer Science, 288:129-152, 2002. Google Scholar
  14. E. Grädel, C. Hirsch, and M. Otto. Back and forth between guarded and modal logics. ACM Transactions on Computational Logics, 3:418-463, 2002. Google Scholar
  15. E. Grädel and M. Otto. The Freedoms of (Guarded) Bisimulation. In Trends in Logic: Johan van Benthem on Logical and Informational Dynamics, pages 3-31. Springer, 2014. Google Scholar
  16. E. Grädel and J. Väänänen. Dependence and Independence. Studia Logica, 101(2):399-410, 2013. Google Scholar
  17. E. Grädel and I. Walukiewicz. Guarded fixed point logic. In Proc. 14th IEEE Symp. on Logic in Computer Science, LICS 1999, pages 45-54, 1999. Google Scholar
  18. W. Hodges. Compositional semantics for a logic of imperfect information. Logic Journal of IGPL, 5:539-563, 1997. Google Scholar
  19. I. Hodkinson. Loosely guarded fragment of first-order logic has the finite model property. Studia Logica, 70:205-240, 2002. Google Scholar
  20. J. Kontinen, J. Müller, H. Schnoor, and H. Vollmer. A van Benthem Theorem for Modal Team Semantics. In CSL 2015, pages 277-291, 2015. Google Scholar
  21. J. Kontinen and J. Väänänen. On definability in dependence logic. Journal of Logic, Language, and Information, 18:317-241, 2009. Google Scholar
  22. A. Mann, G. Sandu, and M. Sevenster. Independence-Friendly Logic. A Game-Theoretic Approach, volume 386 of London Mathematical Societay Lecture Notes Series. Cambridge University Press, 2012. Google Scholar
  23. M. Otto. Model theoretic methods for fragments of FO and special classes of (finite) structures. In J. Esparza, C. Michaux, and C. Steinhorn, editors, Finite and Algorithmic Model Theory, volume 379 of LMS Lecture Note Series, pages 271-341. Cambridge University Press, 2011. Google Scholar
  24. M. Otto. Highly acyclic groups, hypergraph covers and the guarded fragment. Journal of the ACM, 59 (1), 2012. Google Scholar
  25. J. Väänänen. Dependence Logic. Cambridge University Press, 2007. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact