Parameterized model checking problems

Stéphane Demri
LSV, ENS de Cachan
Friday, 18 June, 2004 (All day)

Parameterized complexity is a theoretical framework developed by Downey and Fellows for studying problems where complexity depends differently on the size n of the input and on some other parameter k that varies less in some sense. An introduction of this framework is the first part of the talk.

Then, a wide variety of model checking problems for non-flat systems under the light of parameterized complexity, taking the number of synchronized components as a parameter, is presented. In model checking, the state explosion problem occurs when one checks a non-flat system, i.e. a system implicitly described as a synchronized product of elementary subsystems.

Precise complexity measures (in the parameterized sense) for most of such parameterised model-checking problems, and evidence that the results are robust are given along the talk.