LRDE : comment y aller Amphi IP11
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.
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.