Séminaires
Séminaire du 18 mai 2018
Lieu
LRDE : comment y aller Amphi IP11
Programme
14h00-15h00: Étienne Renault (LRDE/EPITA), The quest for an efficient LTL model-checking
Abstract : 
Model checking is an automated verification technique that is used for establishing
that a model of a system is correct with respect to some given specification. One of
the most serious problems with model checking in practice is the so-called "state explosion
problem", i.e the state-space of a system can be too large to be processed in a reasonable
time and to be stored on the memory. This problem can be addressed using symbolic or explicit
techniques. In this talk I will focus on the latter one by overviewing the recent
advances in (1) emptiness checks and (2) partial-order reductions.
15h00-15h30 : Mathias Ramparison (LIPN, Université Paris 13), Timed automata with parametric updates
Abstract :
Timed automata (TAs) represent a powerful formalism to model and verify systems where concurrency is intricated with hard timing constraints. However, they can seem limited when dealing with uncertain or unknown timing constants. Several parametric extensions were proposed in the literature, and the vast majority of them leads to the undecidability of the EF-emptiness problem: "is the set of valuations reaching a given location empty?" Here, we study an extension of TAs where clocks can be updated to a parameter. While the EF-emptiness problem is undecidable for rational-valued parameters, it becomes PSPACE-complete for integer-valued parameters. In addition, exact synthesis of the parameter valuations set can be achieved. We also extend these two results to the EF-universality ("are all valuations reaching a given location?"), AF-emptiness ("is the set of valuations such that a given location is unavoidable empty?") and AF-universality ("are all valuations such that a given location is unavoidable?") problems.