Evènement pour le groupe Séminaire Méthodes Formelles


Date 2020-12-15  07:00-07:00
TitreReachability in dynamical systems with rounding 
RésuméWe consider reachability in dynamical systems with discrete linear updates, but with fixed decimal precision, i.e., such that values of the system are rounded at each step. Given a matrix M in Q^{d*d}, an initial vector x in Q^d, a granularity g in Q_+ and a rounding operation [·] projecting a vector of Q^d onto another vector whose every entry is a multiple of g, we are interested in the behaviour of the orbit O=<[x],[M[x]],[M[M[x]]],...>, i.e., the trajectory of a linear dynamical system in which the state is rounded after each step. For arbitrary rounding functions with bounded effect, we show that the complexity of deciding point-to-point reachability—whether a given target y in Q^d belongs to O—is PSPACE-complete when no eigenvalue of M has modulus one. We also establish decidability without any restrictions on eigenvalues for several natural classes of rounding functions. Joint work with Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, Amaury Pouly, and Markus A. Whiteland 
LieuOnline 
OrateurEngel Lefaucheux 
Emailhttps://elefauch.github.io/ 
UrlMax-Planck Institute for Software Systems 



Aucun document lié à cet événement.

Retour
Retour à l'index