In model checking, the state-explosion problem occurs when one checks a nonflat system, i.e., a system implicitly described as a synchronized product of elementary subsystems. In this paper, we investigate the complexity of a wide variety of model-checking problems for nonflat systems under the light of parameterized complexity, taking the number of synchronized components as a parameter. We provide precise complexity measures (in the parameterized sense) for most of the problems we investigate, and evidence that the results are robust. © 2006 Elsevier Inc. All rights reserved.
CITATION STYLE
Demri, S., Laroussinie, F., & Schnoebelen, P. (2006). A parametric analysis of the state-explosion problem in model checking. Journal of Computer and System Sciences, 72(4), 547–575. https://doi.org/10.1016/j.jcss.2005.11.003
Mendeley helps you to discover research relevant for your work.