Gregynog is a historic country estate in the middle of nowhere in Wales. It features an early Victorian main hall, grade 1 listed gardens and great walks. The nearest village with pub is Bettws Cedewain, a nice 3 mile walk away. On site, we will have the famous Gregynog home-made cakes and Blayney’s Brew.

Getting there and around

By Train

The local train station is Newtown (Powys), approximately a £12 taxi journey from Gregynog Hall. There are direct trains to Newtown (Powys) from Birmingham International Airport and Birmingham New Street, which take roughly 2h and cost £23 return. See http://www.nationalrail.co.uk.

To ensure that as many of you as possible can share a ride, please share your estimated arrival/departure time HERE.

  • Station Taxis - 01686 621818
  • Pauls Taxis - 01686 624314
  • Ross Taxis - 01686 627600


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 (slides)

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 (slides)

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 deciding 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 (slides)

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: QCover and ICover (slides)

Sylvain Schmitz

Rackoff revisited: complexity of Coverability; (slides)

For the Family Album

Thanks Everyone!