Efficient synthesis and verification of parametrised timed systems

Overview & Synopsis

In this thesis, we are interested in efficiently verifying timed systems modelled by time Petri nets (TPNs) and also in synthesising parameters in their parametric extension, the parametric time Petri nets (PTPNs). First, we study the problem of reachability of a given marking, then we focus on synthesising controller for a reachability objective, as long as a safety objective. To achieve this goal, we use an abstraction of the state space called parametric state-class graph, regrouping states of the PTPN in state classes that can be represented in matrix form through tropical Parametric Difference Bound Matrices (tPDBMs). All the necessary operations for our verification (semi-)algorithms can be efficiently computed using these tPDBMs. These (semi-)algorithms are implemented into the tool Roméo, that we will use to illustrated two things on case-studies: first, the efficiency of using tPDBMs compared to other usual representations of state classes to check the reachability of a marking, then the synthesis of a strategy for the controller.