Prof. Giuseppe De Giacomo (University of Oxford)

Linear Temporal Logics on Finite Traces

In this talk we look at temporal logics on traces that are assumed to be finite, as typical of action planning in Artificial Intelligence and of process modeling in Business Process Management.  Having to deal with finite traces has been considered a sort of accident in much of the AI and BPM literature, and standard temporal logics (on infinite traces) have been hacked to fit this assumption. Only recently a specific interest in studying the impact of such an assumption emerged.  We will survey linear temporal logics on finite traces, including LTLf, LDLf, and pure-past LTL, reviewing the main results on Satisfiability, Verification, and Synthesis. The talk will also draw connections with work in AI Planning, Non-Markovian Decision Processes, Reinforcement Learning, and BPM Declarative Process Modeling. The main catch is that working with these logics can be based on the manipulation of regular automata on finite strings, simplifying greatly reasoning and especially synthesis.

Break

Prof. Dmitry Chistikov (University of Warwick)

Making elementary decisions about natural numbers

This talk will be an introduction to logical theories of arithmetic given from a discrete mathematics and computer science perspective. In particular, I will talk about:

* periodic and ultimately periodic sets of natural numbers,

* how to decide the truth value of logical statements that involve linear inequalities, Boolean connectives, and quantifiers that range over natural numbers (formally: in the first-order theory of natural numbers with addition),

* how these ideas and methods extend to other arithmetic theories (including some recent research results).

Prof. Stefan Kiefer (University of Oxford)

On unambiguous finite automata

Finite automata are fundamental for automated verification. A nondeterministic finite automaton is called unambiguous if every accepted word has only one accepting run. Thus, unambiguous automata are in between deterministic and nondeterministic automata. They are naturally connected to linear algebra and combinatorics. The infinite-word version of unambiguous automata, unambiguous Büchi automata, can be used to model check Markov chains. These algorithms are both mathematically elegant and practically efficient for the verification of probabilistic systems. Based on new connections to communication complexity, there has been recent progress around state minimisation and the complexity of language operations on unambiguous automata.