In line with the Autoboz meetings, we will not follow a strict programme. Instead, we ask each of you to bring one interesting open question for us to discuss: please be prepared to talk for ~10 minutes, outlining your problem and the state of the art.
We will start on Monday morning with these short presentations.
For subsequent days, some of us have kindly agreed to give tutorials. Confirmed far are the following.
- Wojciech Czerwiński
- Regular separability problem
I will talk about recent developments on decidability
of separability problem. One of the open problems is to show
decidability of separability of two VASS languages by regular languages.
I will present several its subproblems and sketch techniques, which we used
to solve it. Namely, I will consider regular separability of Z-VASS and one counter languages
and modular separability of VASS reachability sets.
- Petr Jancar
- Equivalences of first-order grammars
The decidability of bisimilarity for first-order grammars is
equivalent to Senizergues' result for pushdown automata (who thus
generalized his famous decidability of DPDA-equivalence).
This result surely belongs to the most involved results in the area of
behavioural equivalences of infinite-state systems.
The plan of the talk is to present a full proof in a new, hopefully
easily understandable, way. This should also highlight the
difference of the general case and the deterministic subcase
(equivalent to the DPDA-problem), the complexity of which still
remains an intriguing open problem.
- Arnaud Sangnier - Fixpoints in VASS: Results and applications
Many verification techniques have been developed for VASS to analyse them and the frontier between the decidable and undecidable problems for them begins to be well known. One interesting point is that the model-checking of linear temporal logics (like LTL or linear mu-calculus) is decidable for this model but this is not anymore the case when considering branching time temporal logics. However some restrictions can be imposed on the logics and on the studied system in order to regain decidability. In this talk, we will present these results concerning the model-checking of VASS and the techniques leading to the decidability results. We will then show how these techniques and results can be used to analyse some extensions of VASS with probabilities, namely probabilistic VASS and VASS Markov Decision Processes.
- Grégoire Sutre, Christoph Haase, Michael Blondin
on Tools for Coverability;
- Sylvain Schmitz
Rackoff revisited: complexity of Coverability;