Register automata (RAs) are finite automata extended with a finite set of registers to store and compare data from an infinite domain. We study the concept of synchronizing data words in RAs: Does there exist a data word that sends all states of the RA to a single state? For deterministic RAs with k registers (k-DRAs), we prove that inputting data words with 2k+1 distinct data, from the infinite data domain, is sufficient to synchronize. We show that the synchronizing problem for DRAs is in general PSPACE-complete, and is NLOGSPACE-complete for 1-DRAs. For nondeterministic RAs (NRAs), we show that Ackermann(n) distinct data (where n is the size of the RA) might be necessary to synchronize. The synchronizing problem for NRAs is in general undecidable, however, we establish Ackermann-completeness of the problem for 1-NRAs. Our most substantial achievement is proving NEXPTIME-completeness of the length-bounded synchronizing problem for NRAs (length encoded in binary). A variant of this last construction allows to prove that the bounded universality problem for NRAs is coNEXPTIME-complete.
Let v(F) denote the number of vertices in a fixed connected pattern graph F. We show an infinite family of patterns F such that the existence of a subgraph isomorphic to F is expressible by a first-order sentence of quantifier depth (2/3)v(F)+1, assuming that the host graph is sufficiently large and connected. On the other hand, this is impossible for any F with using less than (2/3)v(F)-2 first-order variables.
Enhancing Datalog with existential quantification gives rise to Datalog^E, a powerful knowledge representation language widely used in ontology-based query answering. In this setting, a conjunctive query is evaluated over a Datalog^E program consisting of extensional data paired with so-called existential rules. Due to their high expressiveness, such rules make the evaluation of queries undecidable, even when the latter are atomic. Decidable Datalog^E fragments have been proposed in the literature (e.g., weakly-acyclic and weakly-guarded); but they pay the price of a higher computational complexity, hindering the implementation of effective systems. Conversely, the results in this paper demonstrate that it is definitely possible to enable fast yet powerful query answering over existential rules, ensuring decidability without any complexity overhead. On the theoretical side, we define the class of parsimonious programs which guarantees decidability of atomic queries. We then strengthen this class to strongly parsimonious programs ensuring decidability also for conjunctive queries. Since parsimony is an undecidable property, we single out Shy, an easily recognizable class of strongly parsimonious programs that generalizes Datalog while preserving its complexity even under conjunctive query evaluation. Shy generalizes also the class of linear existential programs, while it is uncomparable to the other main classes ensuring decidability. On the practical side, we exploit our results to implement DLV^E, an effective system for query answering over parsimonious existential rules. To asses its efficiency, we carry out an experimental analysis, comparing DLV^E against state-of-the-art systems for ontology-based query answering. The results confirm the effectiveness of DLV^E, which outperforms all other systems.
In alternating-time temporal logic ATL*, agents with perfect recall assign choices to sequences of states, i.e., to possible finite histories of the game. However, when a nested strategic modality is interpreted, the new strategy does not take into account the previous sequence of events. It is as if agents collect their observations in the nested game again from scratch, thus effectively forgetting what they observed before. Intuitively, it does not fit the assumption of agents having perfect recall of the past. In this paper, we investigate the alternative semantics for ATL* where the past is not forgotten in nested games. We show that the standard semantics of ATL* coincides with the truly perfect recall semantics in case of agents with perfect information. On the other hand, the two semantics differ significantly if agents have imperfect information about the state of the game. The same applies to the standard vs. truly perfect recall semantics of ATL* with persistent strategies. We compare the relevant variants of ATL* by looking at their their expressive power, sets of validities, and feasibility of model checking.