Document Open Access Logo

The Fixed-Parameter Tractability of Model Checking Concurrent Systems

Author Stefan Göller

Thumbnail PDF


  • Filesize: 0.59 MB
  • 16 pages

Document Identifiers

Author Details

Stefan Göller

Cite AsGet BibTex

Stefan Göller. The Fixed-Parameter Tractability of Model Checking Concurrent Systems. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 332-347, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2013)


We study the fixed-parameter complexity of model checking temporal logics on concurrent systems that are modeled as the product of finite systems and where the size of the formula is the parameter. We distinguish between asynchronous product and synchronous product. Sometimes it is possible to show that there is an algorithm for this with running time (\sum_i T_i|)O(1) * f(|\phi|), where the T_i are the component systems and \phi is the formula and f is computable function, thus model checking is fixed-parameter tractable when the size of the formula is the parameter. In this paper we concern ourselves with the question, provided fixed-parameter tractability is known, whether it holds for an elementary function f. Negative answers to this question are provided for modal logic and EF logic: Depending on the mode of synchronization we show the non-existence of such an elementary function f under different assumptions from (parameterized) complexity theory.
  • Model Checking
  • Concurrent Systems
  • Parameterized Complexity


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail