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 $\mathsf{P}^{\mathsf{NP}[\mathcal{O}(\log^2 n)]}$-complete in combined complexity. Our result implies $\mathsf{P}^{\mathsf{NP}[\mathcal{O}(\log^2 n)]}$-completeness for both UNTC and $\mathrm{UNFO}^{\mathrm{reg}}$, which were left open in previous works.

Abstract Game comonads provide categorical semantics for comparison games in Finite Model Theory, thus providing an abstract characterization of logical equivalence for a wide range of logics, each one captured through a specific choice of comonad. Motivated by the goal of applying comonadic tools to the study of data-aware logics such as CoreDataXPath, in this work we introduce a generalization of Modal Logic that allows relation symbols of arbitrary arity as atoms of the syntax, which we call Path Predicate Modal Logic or PPML. We motivate this logic as arising from a shift in perspective on a previously studied fragment of CoreDataXPath, called DataGL, and prove that PPML recovers DataGL for a specific choice of signature. We argue that this shift in perspective allows the capturing and designing of new data-aware logics. On the other hand, PPML enjoys an intrinsic motivation in that it extends Modal Logic to predicate over more general models. Having introduced resource-bounded simulation and bisimulation games for PPML together with a proof of the Hennessy–Milner property relating bisimilarity and logical equivalence, we define the PPML comonad, which essentially amounts to an unravelling construction on models of PPML, and prove that it captures these games, following analogous results in the literature. However, we depart from the literature in our proof strategy, since we draw upon the axiomatic framework of arboreal categories, giving intuition for the axioms involved and supplying detailed verifications. Subsequently, we develop the model-theoretical understanding of PPML by making systematic use of the comonadic framework. This includes results such as a tree-model property and an alternative proof of the one-way Hennessy–Milner property using a correspondence between positive PPML formulas and canonical models. We also use the comonadic perspective to establish connections with other logics, such as bounded quantifier rank and bounded variable number fragments of First Order Logic on one side and Basic Modal Logic on the other, and show how the PPML comonad induces a syntax-free characterization of logical equivalence for DataGL, our original motivation. With respect to Basic Modal Logic, a functorial assignment from PPML unravellings into Kripke trees enables us to obtain polynomial-time reductions from PPML problems to their Basic Modal Logic counterparts.

We introduce CPDL+, a family of expressive logics rooted in Propositional Dynamic Logic (PDL). In terms of expressive power, CPDL+strictly contains PDL extended with intersection and converse (a.k.a. ICPDL) as well as Conjunctive Queries (CQ), Conjunctive Regular Path Queries (CRPQ), or some known extensions thereof (Regular Queries and CQPDL). We investigate the expressive power, indistinguishability via bisimulations, satisfiability, and model checking for CPDL+.We argue that natural subclasses of CPDL+can be defined in terms of the tree-width of the underlying graphs of the formulas. We show that the class of CPDL+formulas of tree-width 2 is equivalent to ICPDL, and that it also coincides with CPDL+formulas of tree-width 1. However, beyond tree-width 2, incrementing the tree-width strictly increases the expressive power. We characterize the expressive power for every class of fixed tree-width formulas in terms of a bisimulation game with pebbles. Based on this characterization, we show that CPDL+has a tree-like model property. We prove that the satisfiability problem is decidable in 2EXPTIME on fixed tree-width formulas, coinciding with the complexity of ICPDL. We also exhibit classes for which satisfiability is reduced to EXPTIME. Finally, we establish that the model checking problem for fixed tree-width formulas is in PTIME, contrary to the full class CPDL+.

Working memory capacity can be improved by recoding the memorized information in a condensed form. Here, we tested the theory that human adults encode binary sequences of stimuli in memory using an abstract internal language and a recursive compression algorithm. The theory predicts that the psychological complexity of a given sequence should be proportional to the length of its shortest description in the proposed language, which can capture any nested pattern of repetitions and alternations using a limited number of instructions. Five experiments examine the capacity of the theory to predict human adults' memory for a variety of auditory and visual sequences. We probed memory using a sequence violation paradigm in which participants attempted to detect occasional violations in an otherwise fixed sequence. Both subjective complexity ratings and objective violation detection performance were well predicted by our theoretical measure of complexity, which simply reflects a weighted sum of the number of elementary instructions and digits in the shortest formula that captures the sequence in our language. While a simpler transition probability model, when tested as a single predictor in the statistical analyses, accounted for significant variance in the data, the goodness-of-fit with the data significantly improved when the language-based complexity measure was included in the statistical model, while the variance explained by the transition probability model largely decreased. Model comparison also showed that shortest description length in a recursive language provides a better fit than six alternative previously proposed models of sequence encoding. The data support the hypothesis that, beyond the extraction of statistical knowledge, human sequence coding relies on an internal compression using language-like nested structures.

Finite ontology mediated query answering (FOMQA) is the variant of ontology mediated query answering (OMQA) where the represented world is assumed to be finite, and thus only finite models of the ontology are considered. We study the property of finite-controllability, that is, whether FOMQA and OMQA are equivalent, for fragments of C2RPQ. C2RPQ is the language of conjunctive two-way regular path queries, which can be regarded as the result of adding simple recursion to Conjunctive Queries. For graph classes S, we consider fragments C2RPQ(S) of C2RPQ as the queries whose underlying graph structure is in S. We completely classify the finitely controllable and non-finitely controllable fragments under: inclusion dependencies, (frontier-)guarded rules, frontier-one rules (either with or without constants), and more generally under guarded-negation first-order constraints. For the finitely controllable fragments, we show a reduction to the satisfiability problem for guarded-negation first-order logic, yielding a 2EXPTIME algorithm (in combined complexity) for the corresponding (F)OMQA problem.

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.

Bisimulation provides structural conditions to characterize indistinguishability from an external observer between nodes on labeled graphs. It is a fundamental notion used in many areas, such as verification, graph-structured databases, and constraint satisfaction. However, several current applications use graphs where nodes also contain data (the so called "data graphs"), and where observers can test for equality or inequality of data values (e.g., asking the attribute 'name' of a node to be different from that of all its neighbors). The present work constitutes a first investigation of "data aware" bisimulations on data graphs. We study the problem of computing such bisimulations, based on the observational indistinguishability for XPath ---a language that extends modal logics like PDL with tests for data equality--- with and without transitive closure operators. We show that in general the problem is PSpace-complete, but identify several restrictions that yield better complexity bounds (coNP, PTime) by controlling suitable parameters of the problem, namely the amount of non-locality allowed, and the class of models considered (graphs, DAGs, trees). In particular, this analysis yields a hierarchy of tractable fragments.

During language processing, humans form complex embedded representations from sequential inputs. Here, we ask whether a "geometrical language" with recursive embedding also underlies the human ability to encode sequences of spatial locations. We introduce a novel paradigm in which subjects are exposed to a sequence of spatial locations on an octagon, and are asked to predict future locations. The sequences vary in complexity according to a well-defined language comprising elementary primitives and recursive rules. A detailed analysis of error patterns indicates that primitives of symmetry and rotation are spontaneously detected and used by adults, preschoolers, and adult members of an indigene group in the Amazon, the Munduruku, who have a restricted numerical and geometrical lexicon and limited access to schooling. Furthermore, subjects readily combine these geometrical primitives into hierarchically organized expressions. By evaluating a large set of such combinations, we obtained a first view of the language needed to account for the representation of visuospatial sequences in humans, and conclude that they encode visuospatial sequences by minimizing the complexity of the structured expressions that capture them.

We investigate model theoretic properties of XPath with data (in)equality tests over the class of data trees, i.e., the class of trees where each node contains a label from a finite alphabet and a data value from an infinite domain. We provide notions of (bi)simulations for XPpath logics containing the child, parent, ancestor and descendant axes to navigate the tree. We show that these notions precisely characterize the equivalence relation associated with each logic. We study formula complexity measures consisting of the number of nested axes and nested subformulas in a formula; these notions are akin to the notion of quantifier rank in first-order logic. We show characterization results for fine grained notions of equivalence and (bi)simulation that take into account these complexity measures. We also prove that positive fragments of these logics correspond to the formulas preserved under (non-symmetric) simulations. We show that the logic including the child axis is equivalent to the fragment of first-order logic invariant under the corresponding notion of bisimulation. If upward navigation is allowed the characterization fails but a weaker result can still be established. These results hold both over the class of possibly infinite data trees and over the class of finite data trees. Besides their intrinsic theoretical value, we argue that bi-simulations are useful tools to prove (non)expressivity results for the logics studied here, and we substantiate this claim with examples.

We study the number of changes of the initial segment Zs ↾n for computable approximations of a Martin-Löf random Δ20 set Z. We establish connections between this number of changes and various notions of computability theoretic lowness, as well as the fundamental thesis that, among random sets, randomness is antithetical to computational power. We introduce a new randomness notion, called balanced randomness, which implies that for each computable approximation and each constant c, there are infinitely many n such that Zs ↾n changes more than c2n times. We establish various connections with ω-c.e. tracing and omega;-c.e. jump domination, a new lowness property. We also examine some relationships to randomness theoretic notions of highness, and give applications to the study of (weak) Demuth cuppability.

The minoring ordering between finite sets of (X,≤) is a well quasi-ordering provided (X,≤) is an ω2-well quasi-ordering. We mention some known facts about ω2-well quasi orderings, and we prove some new results about them. We also study some algebraic properties of the minoring well-quasi ordering over finite sets of (X, ≤), such as the behaviour of its order type when the underlying set is a disjoint sum, and give a tight lower bound for its maximal order type in terms of the maximal order type of (X,≤). We also state some observations regarding the upper bound.

International audience

Dickson's Lemma is a simple yet powerful tool widely used in decidability proofs, especially when dealing with counters or related data structures in algorithmics, verification and model-checking, constraint solving, logic, etc. While Dickson's Lemma is well-known, most computer scientists are not aware of the complexity upper bounds that are entailed by its use. This is mainly because, on this issue, the existing literature is not very accessible. We propose a new analysis of the length of bad sequences over (Nk,≤), improving on earlier results and providing upper bounds that are essentially tight. This analysis is complemented by a ``user guide'' explaining through practical examples how to easily derive complexity upper bounds from Dickson's Lemma.

We define the notion of indifferent set with respect to a given class of {0,1}-sequences. Roughly, for a set A in the class, a set of natural numbers I is indifferent for A with respect to the class if it does not matter how we change A at the positions in I: the new sequence continues to be in the given class. We are especially interested in studying those sets that are indifferent with respect to classes containing different types of stochastic sequences. For the class of Martin-Löf random sequences, we show that every random sequence has an infinite indifferent set and that there is no universal indifferent set. We show that indifferent sets must be sparse, in fact sparse enough to decide the halting problem. We prove the existence of co-c.e. indifferent sets, including a co-c.e. set that is indifferent for every 2-random sequence with respect to the class of random sequences. For the class of absolutely normal numbers, we show that there are computable indifferent sets with respect to that class and we conclude that there is an absolutely normal real number in every non-trivial many-one degree.

Abstract We consider the question of randomness of the probability ΩU[X] that an optimal Turing machine U halts and outputs a string in a fixed set X. The main results are as follows: • ΩU[X] is random whenever X is Σn0-complete or Πn0-complete for some n ≥ 2. • However, for n ≥ 2, ΩU[X] is not n-random when X is Σn0 or Πn0. Nevertheless, there exists Δn+10 sets such that ΩU[X] is n-random. • There are Δ20 sets X such that ΩU[X] is rational. Also, for every n ≥ 1, there exists a set X which is Δn+10 and Σn0-hard such that ΩU[X] is not random. We also look at the range of ΩU as an operator. We prove that the set {ΩU[X]: X ⊆ 2≤ω} is a finite union of closed intervals. It follows that for any optimal machine U and any sufficiently small real r, there is a set X ⊆ 2≤ω recursive in ∅′ ⊕ r, such that ΩU[X] = r. The same questions are also considered in the context of infinite computations, and lead to similar results.