Logic for Communicating Automata with Parameterized Topology

Benedikt Bollig 1, 2
2 MEXICO - Modeling and Exploitation of Interaction and Concurrency
Inria Saclay - Ile de France, LSV - Laboratoire Spécification et Vérification [Cachan]
Abstract : We introduce parameterized communicating automata (PCA) as a model of systems where finite-state processes communicate through FIFO channels. Unlike classical communicating automata, a given PCA can be run on any network topology of bounded degree. The topology is thus a parameter of the system. We provide various Büchi-Elgot-Trakhtenbrot theorems for PCA, which roughly read as follows: Given a logical specification \phi and a class of topologies T, there is a PCA that is equivalent to \phi on all topologies from T. We give uniform constructions which allow us to instantiate T with concrete classes such as pipelines, ranked trees, grids, rings, etc. The proofs build on a locality theorem for first-order logic due to Schwentick and Barthelmann, and they exploit concepts from the non-parameterized case, notably a result by Genest, Kuske, and Muscholl.
Complete list of metadatas

Cited literature [25 references]  Display  Hide  Download

Contributor : Benedikt Bollig <>
Submitted on : Tuesday, January 21, 2014 - 1:36:09 PM
Last modification on : Wednesday, December 4, 2019 - 1:26:02 PM
Long-term archiving on: Saturday, April 8, 2017 - 8:53:54 PM


Files produced by the author(s)


  • HAL Id : hal-00872807, version 2



Benedikt Bollig. Logic for Communicating Automata with Parameterized Topology. Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (CSL-LICS'14), Jul 2014, Vienna, Austria. ⟨hal-00872807v2⟩



Record views


Files downloads