
Evènement pour le groupe Séminaire Méthodes Formelles
Date  20200204 14:0015:00 
Titre  Reachability in fixed dimension vector addition systems with states 
Résumé  The reachability problem is a central decision problem for formal verification based on vector addition systems with states (VASS), which are equivalent to Petri nets and form one of the most studied and applied models of concurrency. Reachability for VASS is also interreducible with a plethora of problems from a number of areas of computer science. In spite of recent progress, the complexity of the reachability problem remains unsettled, and it is closely related to the lengths of shortest VASS runs that witness reachability.
We consider VASS of fixed dimension, and obtain three main results. For the first two, we assume that the integers in the input are given in unary, and that the control graph of the given VASS is flat (i.e., without nested cycles). We obtain a family of VASS in dimension 3 whose shortest reachability witnessing runs are exponential, and we show that the reachability problem is NPhard in dimension 7. These results resolve negatively questions that had been posed by the works of Blondin et al. in LICS 2015 and Englert et al. in LICS 2016, and contribute a first construction that distinguishes 3dimensional flat VASS from 2dimensional VASS.
Our third result, by means of a novel family of products of integer fractions, shows that 4dimensional VASS can have doubly exponentially long shortest reachability witnessing runs. The smallest dimension for which this was previously known is 14.
Joint work with Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Filip Mazowiecki. Paper available at https://arxiv.org/abs/2001.04327 
Lieu  178 
Orateur  Jérôme Leroux 
Email  https://www.labri.fr/perso/leroux/ 
Url  CNRS, LaBRI 
Aucun document lié à cet événement. RetourRetour à l'index
 