Agenda
septembre
-
11:0012:00
Mohammed Dlimi (Bordeaux-INP; LaBRI (internship))
Title: Thresholds in bounded BIO Petri nets
Abstract:
Mohammed Dlimi will present the results on thresholds for boundedness of Branching Immediate Observation systems. BIO Petri nets have transitions where only one place is an input but not an output, but multiple places can be outputs, or inputs and outputs with the same multiplicity. In terms of protocols, this corresponds to finite-state agents that can observe each other and change the local state, finish the excution or create new agents; while observees stay unaware of being observed. A BIO system (with a fixed initial configuration) is bounded if only a finite number of configurations can be reached.
Two questions were studied during the internship. Specifically, how many tokens can be created within a bounded BIO system of a given size, and how few tokens are needed to demonstrate an unbounded token-producing loop if one exists. The answers to these questions will be presented in the talk.
LaBRI 178 -
13:0014:00
Title: Query Entailment Problem for S.
Abstract: 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 show 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.178 -
13:0014:00
Conjugacy and equivalence of weighted automata
This talk starts with a result witin classical Finite Automata Theory:
'Two regular languages with the same number of words for each length can be mapped one onto the other by a letter-to-letter (finite) transducer'.The notion of generating function of regular languages leads to the
introduction of the model of weighted automata. The conjugacy of weighted automata, a concept borrowed to symbolic dynamics, is then defined and it is shown how the above statement can be derived from the central result of this work: 'Two equivalent weighted automata are conjugate to a third one when the weight semiring is B, N, Z, or any Euclidean domain (and thus any (skew) field)'.The talk is based on a joint work with Marie-Pierre Béal and Sylvain
Lombardy.LaBRI -
11:0012:00
Arthur Lunven (UBx Service Innovation)
Title: Les missions de service Innovation et AAP Prématuration
LaBRI 178 -
14:0015:00
We reduce the model checking problem for a subset of Python to
the satisfiability of a first-order formula over finite words, which is
known to be decidable. The reduction is based on the theory of
polyregular functions, a recently developed generalization of regular
languages to polynomial output string-to-string functions. We
implemented this reduction in a verification tool called PolyCheck, that
can use both automata-based solvers and classical SMT solvers as
backends.This is a joint work with Rafał Stefański that was pursued
at the University of Warsaw, and was published at CAV'2025.LaBRI
octobre
-
10:0014:00
Zoé Varin soutiendra sa thèse, le 20 octobre 2025 à 10h, dans l’amphi du LaBRI.
L’intitulé de sa thèse est : "Modèles discrets et continus de dispersion aléatoire en dimension 1, analyse d'un amarclgorithme d’apprentissage par renforcement".