2026-07-23T22:35:58Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3421 2024-03-06T10:34:10Z ddc:004 open_access

Concurrency Makes Simple Theories Hard Göller, Stefan Widjaja Lin, Anthony Modal Logic Model Checking Asynchronous Product Pushdown Systems Feferman-Vaught Nonelementary lower bounds 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Stefan Göller and Anthony Widjaja Lin 2012 Is Part Of LIPIcs, Volume 14, 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.STACS.2012.148 urn:nbn:de:0030-drops-34214 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2012.148 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode