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.
@InProceedings{goller_et_al:LIPIcs.STACS.2012.148, author = {G\"{o}ller, Stefan and Widjaja Lin, Anthony}, 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 = {D\"{u}rr, Christoph and Wilke, Thomas}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2012.148}, 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} }
Feedback for Dagstuhl Publishing