文章基本信息

标题：The Fixed-Parameter Tractability of Model Checking Concurrent Systems
本地全文：下载
作者：Stefan G{\"o}ller
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2013
卷号：23
页码：332-347
DOI：10.4230/LIPIcs.CSL.2013.332
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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