10:30 am, Lecture Hall 5
Very-Well Structured Transition Systems
Alain Finkel
LSV, CNRS & ENS Paris-Saclay.
08-02-19

---

Abstract

In the past, we provided a framework to conduct forward reachability analyses of WSTS, using finite representations of downwards-closed sets. We further develop this framework to obtain a generic Karp-Miller algorithm for the new class of very-WSTS. This allows us to show that coverability sets of very-WSTS can be computed as their finite ideal decompositions. Under natural effectiveness assumptions, we also show that LTL model checking for very-WSTS is decidable. The termination of our procedure rests on a new notion of acceleration levels, which we study. We characterize those domains that allow for only finitely many accelerations, based on ordinal ranks.

Reference: https://arxiv.org/abs/1710.07258