Undecidability of QLTL with two variables and one monadic predicate letter

We study the algorithmic properties of the quantified linear-time temporal logic QLTL in languages with restrictions on the number of individual variables as well as the number and arity of predicate letters. We prove that the satisfiability problem for QLTL in languages with two individual variables and one monadic predicate letter in Σ 11 -hard. Thus, QLTL is Π 11 -hard, and so not recursively enumerable, in such languages. The resultholds both for the increasing domain and the constant domain semantics and is obtained by reduction from a Σ 11 -hard N×N recurrent tiling problem. It follows from the proof for QLTL that similar results hold for the quantified branching-time temporal logic QCTL, and hence for the quantified alternating-time temporal logic QATL. The result presented in this paper strengthens a result by I. Hodkinson, F. Wolter, and M. Zakharyaschev, who have shown that the satisfiability problem for QLTL is Σ 11 -hard in languages with two individual variablesand an unlimited supply of monadic predicate letters.

Twenty Vertex Model and Domino Tilings of the Aztec Triangle

We show that the number of configurations of the 20 Vertex model on certain domains with domain wall type boundary conditions is equal to the number of domino tilings of Aztec-like triangles, proving a conjecture of the author and Guitter. The result is based on the integrability of the 20 Vertex model and uses a connection to the U-turn boundary 6 Vertex model to re-express the number of 20 Vertex configurations as a simple determinant, which is then related to a Lindström-Gessel-Viennot determinant for the domino tiling problem. The common number of configurations is conjectured to be $2^{n(n-1)/2}\prod_{j=0}^{n-1}\frac{(4j+2)!}{(n+2j+1)!}=1, 4, 60, 3328, 678912...$ The enumeration result is extended to include refinements of both numbers.

Decidability and Periodicity of Low Complexity Tilings

In this paper we study colorings (or tilings) of the two-dimensional grid ${\mathbb {Z}}^{2}$ ℤ 2 . A coloring is said to be valid with respect to a set P of n × m rectangular patterns if all n × m sub-patterns of the coloring are in P. A coloring c is said to be of low complexity with respect to a rectangle if there exist $m,n\in \mathbb {N}$ m , n ∈ ℕ and a set P of n × m rectangular patterns such that c is valid with respect to P and |P|≤ nm. Open since it was stated in 1997, Nivat’s conjecture states that such a coloring is necessarily periodic. If Nivat’s conjecture is true, all valid colorings with respect to P such that |P|≤ mn must be periodic. We prove that there exists at least one periodic coloring among the valid ones. We use this result to investigate the tiling problem, also known as the domino problem, which is well known to be undecidable in its full generality. However, we show that it is decidable in the low-complexity setting. Then, we use our result to show that Nivat’s conjecture holds for uniformly recurrent configurations. These results also extend to other convex shapes in place of the rectangle. After that, we prove that the nm bound is multiplicatively optimal for the decidability of the domino problem, as for all ε > 0 it is undecidable to determine if there exists a valid coloring for a given $m,n\in \mathbb {N}$ m , n ∈ ℕ and set of rectangular patterns P of size n × m such that |P|≤ (1 + ε)nm. We prove a slightly better bound in the case where m = n, as well as constructing aperiodic SFTs of pretty low complexity. This paper is an extended version of a paper published in STACS 2020 (Kari and Moutot 12).