Agenda

Département
Langue
Date
Thématique
2025

septembre

  • 11:00
    12: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.

    https://algodist.labri.fr/index.php/Main/GT

    LaBRI 178
  • 13:00
    14: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:00
    14: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:00
    12:00

    Arthur Lunven (UBx Service Innovation)

    Title: Les missions de service Innovation et AAP Prématuration

    https://algodist.labri.fr/index.php/Main/GT

    LaBRI 178
  • 14:00
    15: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