License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.MFCS.2018.27
URN: urn:nbn:de:0030-drops-96094
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9609/
Go to the corresponding LIPIcs Volume Portal

Lück, Martin

On the Complexity of Team Logic and Its Two-Variable Fragment

pdf-format:
LIPIcs-MFCS-2018-27.pdf (0.6 MB)

Abstract

We study the logic FO(~), the extension of first-order logic with team semantics by unrestricted Boolean negation. It was recently shown to be axiomatizable, but otherwise has not yet received much attention in questions of computational complexity. In this paper, we consider its two-variable fragment FO^2(~) and prove that its satisfiability problem is decidable, and in fact complete for the recently introduced non-elementary class TOWER(poly). Moreover, we classify the complexity of model checking of FO(~) with respect to the number of variables and the quantifier rank, and prove a dichotomy between PSPACE- and ATIME-ALT(exp, poly)-complete fragments. For the lower bounds, we propose a translation from modal team logic MTL to FO^2(~) that extends the well-known standard translation from modal logic ML to FO^2. For the upper bounds, we translate FO(~) to fragments of second-order logic with PSPACE-complete and ATIME-ALT(exp, poly)-complete model checking, respectively.

BibTeX - Entry

@InProceedings{lck:LIPIcs:2018:9609,
  author =	{Martin L{\"u}ck},
  title =	{{On the Complexity of Team Logic and Its Two-Variable Fragment}},
  booktitle =	{43rd International Symposium on Mathematical Foundations  of Computer Science (MFCS 2018)},
  pages =	{27:1--27:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-086-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{117},
  editor =	{Igor Potapov and Paul Spirakis and James Worrell},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9609},
  URN =		{urn:nbn:de:0030-drops-96094},
  doi =		{10.4230/LIPIcs.MFCS.2018.27},
  annote =	{Keywords: team logic, two-variable logic, complexity, satisfiability, model checking}
}

Keywords: team logic, two-variable logic, complexity, satisfiability, model checking
Collection: 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)
Issue Date: 2018
Date of publication: 27.08.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI