Checking structural safety for networks of timed automata by acceleration
( Laboratory for Foundations of Computer Science, Edinburgh )
We study the interplay between multiple indistinguishable timed automata processes. The system advances according to global rules which trigger several local changes at once, on a nondeterministically chosen subset of processes. We ask if a given safety property is satisfied regardless of the initial number of processes. I will discuss several variants of this decision problem in the setting of timed-arc Petri nets.
Graduated from the University of Hamburg, Germany (2010, Dipl.Inf.) and Edinburgh (2014, Ph.D.). I spend a year each at LaBRI in Bordeaux, Warwick, and now back at the Laboratory for Foundations of Computer Science in Edinburgh. I am interested in the formal verification of infinite processes and am currently focusing on extensions of vector addition systems. Most of my previous work is on verification games for one-counter systems.