Next meeting
Query Entailment Problem for S
(University of Warsaw, Poland)
In description logic, possibly infinite structures are described via an ABox A (i.e. a basic finite structure, to be completed), and an ontology T (or a TBox, a finite set of constraints aiming to complete the ABox). The query entailment problem asks the following: given an ABox A, a TBox T, and a conjunctive query q (= a subgraph), does any structure satisfying A and T necessarily also satisfy the request?
In ALC, the basic description logic (which is nothing more than modal logic in disguise), this problem is well understood, as it is known to be ExpTime-complete in combined complexity, and coNP-complete in data complexity (i.e. with TBox and query fixed) [Lutz '08].
However, the exact complexity for S, the extension of ALC where some roles (= binary relations) are specified to be transitive, was not known yet. The status being that the problem is coNExpTime-hard [Eiter et al. '09] and in 2ExpTime [Calvanese et al. '98]. Two articles in 2009 and 2010 tried to close the gap by proving coNExpTime-completeness in special cases, but the general question remained open.
In this seminar, we finally answer this question by showing that the query entailment problem for S is actually 2-ExpTime complete. In fact, we show that the complexity gap is associated with the number of transitive roles: two distinct transitive roles are enough to get 2-ExpTime-hardness, while the case with only one transitive role (and possibly many non-transitive ones) is in coNExpTime.
This latter case is proven by showing that whenever q is not entailed by (A,T), then there exists a counterexample with a representation of exponential size (while being most certainly infinite). In the talk, we will explain how some variant of automata over infinite trees can be elegantly used in order to obtain such a representation. We will also highlight the crucial difficulties induced by two distinct transitive roles, that were overlooked so far.
Robust timed synthesis
(lacl)
Solving games played on timed automata is a well-known problem and has led to tools and industrial case studies. In these games, the first player (Controller) chooses delays and actions and the second player (Environment) resolves the non-determinism of actions. However, the model of timed automata suffers from mathematical idealizations such as infinite precision of clocks and instantaneous synchronization of actions. To address this issue, we extend the theory of timed games in two directions. First, we study the synthesis of robust strategies for Controller which should be tolerant to adversarially chosen clock imprecisions. Second, we address the case of a stochastic perturbation model where both clock imprecisions and the non-determinism are resolved randomly. Finally we present a notion "repair" where we explain how to recover robustness in non-robust systems.