License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2013.332
URN: urn:nbn:de:0030-drops-42062
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4206/
Go to the corresponding LIPIcs Volume Portal

Göller, Stefan

The Fixed-Parameter Tractability of Model Checking Concurrent Systems

pdf-format:
26.pdf (0.6 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{gller:LIPIcs:2013:4206,
  author =	{Stefan G{\"o}ller},
  title =	{{The Fixed-Parameter Tractability of Model Checking Concurrent Systems}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{332--347},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Simona Ronchi Della Rocca},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4206},
  URN =		{urn:nbn:de:0030-drops-42062},
  doi =		{10.4230/LIPIcs.CSL.2013.332},
  annote =	{Keywords: Model Checking, Concurrent Systems, Parameterized Complexity}
}

Keywords: Model Checking, Concurrent Systems, Parameterized Complexity
Collection: Computer Science Logic 2013 (CSL 2013)
Issue Date: 2013
Date of publication: 02.09.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI