License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.STACS.2012.148
URN: urn:nbn:de:0030-drops-34214
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3421/
Go to the corresponding LIPIcs Volume Portal

Göller, Stefan ; Widjaja Lin, Anthony

Concurrency Makes Simple Theories Hard

pdf-format:
37.pdf (0.6 MB)

Abstract

A standard way of building concurrent systems is by composing several
individual processes by product operators. We show that even the simplest notion of product operators (i.e. asynchronous products) suffices to increase the complexity of model checking simple logics like Hennessy-Milner (HM) logic and its extension with the reachability operator (EF-logic) from PSPACE to nonelementary. In particular, this nonelementary jump happens for EF-logic when we consider individual processes represented by pushdown systems (indeed, even with only one control state). Using this result, we prove nonelementary lower bounds on the size of formula decompositions provided by Feferman-Vaught (de)compositional methods for HM and EF logics, which reduce theories of asynchronous products to theories of the components. Finally, we show that the same nonelementary lower bounds also hold when we consider the relativization of such compositional methods to finite systems.

BibTeX - Entry

@InProceedings{gller_et_al:LIPIcs:2012:3421,
  author =	{Stefan G{\"o}ller and Anthony Widjaja Lin},
  title =	{{Concurrency Makes Simple Theories Hard}},
  booktitle =	{29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)},
  pages =	{148--159},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-35-4},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{14},
  editor =	{Christoph D{\"u}rr and Thomas Wilke},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3421},
  URN =		{urn:nbn:de:0030-drops-34214},
  doi =		{10.4230/LIPIcs.STACS.2012.148},
  annote =	{Keywords: Modal Logic, Model Checking, Asynchronous Product, Pushdown Systems, Feferman-Vaught, Nonelementary lower bounds}
}

Keywords: Modal Logic, Model Checking, Asynchronous Product, Pushdown Systems, Feferman-Vaught, Nonelementary lower bounds
Collection: 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)
Issue Date: 2012
Date of publication: 24.02.2012

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