Related papers: What's Decidable about (Atomic) Polymorphism
The \emph{Orbit Problem} consists of determining, given a linear transformation $A$ on $\mathbb{Q}^d$, together with vectors $x$ and $y$, whether the orbit of $x$ under repeated applications of $A$ can ever reach $y$. This problem was…
Constraint LTL, a generalisation of LTL over Presburger constraints, is often used as a formal language to specify the behavior of operational models with constraints. The freeze quantifier can be part of the language, as in some real-time…
In this note we prove the following results: $\bullet$ If a finitely presented group $G$ admits a strongly aperiodic SFT, then $G$ has decidable word problem. More generally, for f.g. groups that are not recursively presented, there exists…
The problem of linking the structure of a finite linear dynamical system with its dynamics is well understood when the phase space is a vector space over a finite field. The cycle structure of such a system can be described by the…
We show that a holomorphic eta quotient has only finitely many factors. We also provide an algorithm for checking irreducibility of holomorphic eta quotients by constructing an upper bound for the minimum of the levels of the proper factors…
We consider the model checking problem of infinite state systems given in the form of parameterized discrete timed networks with multiple clocks. We show that this problem is decidable with respect to specifications given by B- or…
We prove that the problem of deciding whether a given morphic sequence is uniformly recurrent is decidable. The proof uses decidability of HD0L periodicity problem, which was recently proved in papers of F.Durand and I.Mitrofanov.
Does a given a set of polyominoes tile some rectangle? We show that this problem is undecidable. In a different direction, we also consider tiling a cofinite subset of the plane. The tileability is undecidable for many variants of this…
The rewriting system sigma is the set of rules propagating explicit substitutions in the lambda-calculus with explicit substitutions. In this note, we prove the undecidability of unification modulo sigma.
Recent work by Faizal et al. (2025) claims that G\"odelian undecidability of non-algorithmic truths in our universe imply the impossibility of a formal, algorithmic simulation of the universe. This paper clarifies the distinction between…
Recently, symbolic structures were proposed as finite representations of potentially infinite first-order structures, where Linear Integer Arithmetic terms and formulas define the domain and interpretations of a structure. We generalize…
We call a group $G$ {\it algorithmically finite} if no algorithm can produce an infinite set of pairwise distinct elements of $G$. We construct examples of recursively presented infinite algorithmically finite groups and study their…
Controlling hybrid systems is mostly very challenging due to the variety of dynamics these systems can exhibit. Inspired by the concept of differential flatness of nonlinear continuous systems and their inherent invertibility property, the…
An integral of a group $G$ is a group $H$ whose commutator subgroup is isomorphic to $G$. In this paper, we prove that the integrability of a finite group is a decidable problem.
The study of word equations (or the existential theory of equations over free monoids) is a central topic in mathematics and theoretical computer science. The problem of deciding whether a given word equation has a solution was shown to be…
Recently, the separated fragment (SF) has been introduced and proved to be decidable. Its defining principle is that universally and existentially quantified variables may not occur together in atoms. The known upper bound on the time…
The Fairness, Accountability, and Transparency in Machine Learning (FAT-ML) literature proposes a varied set of group fairness metrics to measure discrimination against socio-demographic groups that are characterized by a protected feature,…
The satisfiability problem of hybrid logics with the downarrow binder is known to be undecidable. This initiated a research program on decidable and tractable fragments. In this paper, we investigate the effect of restricting the…
Morrill and Valentin in the paper "Computational coverage of TLG: Nonlinearity" considered an extension of the Lambek calculus enriched by a so-called "exponential" modality. This modality behaves in the "relevant" style, that is, it allows…
It is undecidable whether the language recognized by a probabilistic finite automaton is empty. Several other undecidability results, in particular regarding problems about matrix products, are based on this important theorem. We present…