DROPS

Document

DOI: 10.4230/LIPIcs.LICS.2026.43

Guarded Negation Transitive Closure Logic

Authors: Diego Figueira, Santiago Figueira, and Yoshiki Nakamura

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract

We study the guarded negation fragment of transitive closure logic (GNTC). We show that the satisfiability problem for GNTC is 2ExpTime-complete, by establishing the following reductions: (i) a polynomial-time reduction from the satisfiability problem for GNTC to the satisfiability problem for the unary negation fragment UNTC of GNTC, and (ii) a direct exponential-time reduction from the satisfiability problem for UNTC to the non-emptiness problem for 2-way alternating parity tree automata. Furthermore, we show that the model checking problem for GNTC is 𝖯^NP[𝒪(log² n)]-complete in combined complexity. Our result implies 𝖯^NP[𝒪(log² n)]-completeness for both UNTC and UNFO^reg, which were left open in previous works.

Cite as

Diego Figueira, Santiago Figueira, and Yoshiki Nakamura. Guarded Negation Transitive Closure Logic. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 43:1-43:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{figueira_et_al:LIPIcs.LICS.2026.43,
  author =	{Figueira, Diego and Figueira, Santiago and Nakamura, Yoshiki},
  title =	{{Guarded Negation Transitive Closure Logic}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{43:1--43:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.43},
  URN =		{urn:nbn:de:0030-drops-268302},
  doi =		{10.4230/LIPIcs.LICS.2026.43},
  annote =	{Keywords: Transitive closure logic, Guarded negation, Unary negation, Satisfiability, Model checking}
}

Document

DOI: 10.4230/LIPIcs.STACS.2019.22

Closure Properties of Synchronized Relations

Authors: María Emilia Descotte, Diego Figueira, and Santiago Figueira

Published in: LIPIcs, Volume 126, 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)

Abstract

A standard approach to define k-ary word relations over a finite alphabet A is through k-tape finite state automata that recognize regular languages L over {1, ..., k} x A, where (i,a) is interpreted as reading letter a from tape i. Accordingly, a word w in L denotes the tuple (u_1, ..., u_k) in (A^*)^k in which u_i is the projection of w onto i-labelled letters. While this formalism defines the well-studied class of rational relations, enforcing restrictions on the reading regime from the tapes, which we call synchronization, yields various sub-classes of relations. Such synchronization restrictions are imposed through regular properties on the projection of the language L onto {1, ..., k}. In this way, for each regular language C subseteq {1, ..., k}^*, one obtains a class Rel({C}) of relations. Synchronous, Recognizable, and Length-preserving rational relations are all examples of classes that can be defined in this way. We study basic properties of these classes of relations, in terms of closure under intersection, complement, concatenation, Kleene star and projection. We characterize the classes with each closure property. For the binary case (k=2) this yields effective procedures.

Cite as

María Emilia Descotte, Diego Figueira, and Santiago Figueira. Closure Properties of Synchronized Relations. In 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 126, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{descotte_et_al:LIPIcs.STACS.2019.22,
  author =	{Descotte, Mar{\'\i}a Emilia and Figueira, Diego and Figueira, Santiago},
  title =	{{Closure Properties of Synchronized Relations}},
  booktitle =	{36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)},
  pages =	{22:1--22:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-100-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{126},
  editor =	{Niedermeier, Rolf and Paul, Christophe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2019.22},
  URN =		{urn:nbn:de:0030-drops-102614},
  doi =		{10.4230/LIPIcs.STACS.2019.22},
  annote =	{Keywords: synchronized word relations, rational, closure, characterization, intersection, complement, Kleene star, concatenation}
}

Search Results

Documents authored by Figueira, Santiago

Guarded Negation Transitive Closure Logic

Abstract

Cite as

Closure Properties of Synchronized Relations

Abstract

Cite as

Thanks for your feedback!

Could not send message