Concurrency Makes Simple Theories Hard

Authors Stefan Göller, Anthony Widjaja Lin

Thumbnail PDF


  • Filesize: 0.57 MB
  • 12 pages

Document Identifiers

Author Details

Stefan Göller
Anthony Widjaja Lin

Cite AsGet BibTex

Stefan Göller and Anthony Widjaja Lin. Concurrency Makes Simple Theories Hard. In 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 14, pp. 148-159, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


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.
  • Modal Logic
  • Model Checking
  • Asynchronous Product
  • Pushdown Systems
  • Feferman-Vaught
  • Nonelementary lower bounds


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail