Logic for Communicating Automata with Parameterized Topology - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport Année : 2013

Logic for Communicating Automata with Parameterized Topology

Résumé

Communicating automata (CA) are a fundamental model of systems where a fixed finite number of processes communicate via message exchange through FIFO channels. In this paper, we introduce a parameterized version of CA (PCA). The parameter is the underlying communication topology, in which processes are linked via interfaces and arranged as graphs of bounded degree such as ranked trees, grids, rings, or pipelines. A given PCA can be run on any such topology. We provide Büchi-Elgot-Trakhtenbrot theorems for PCA, continuing the logical study that has established characterizations of classical CA in terms of (fragments of) monadic second-order (MSO) logic. In particular, we give translations of existential MSO logic to PCA that are correct for large and natural classes of topologies. Our main result relies on a locality theorem for first-order logic due to Schwentick and Barthelmann, and it uses, as a black-box, a construction by Genest, Kuske, and Muscholl from the non-parameterized case.
Fichier principal
Vignette du fichier
parameterized.pdf (546.74 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-00872807 , version 1 (14-10-2013)
hal-00872807 , version 2 (21-01-2014)

Identifiants

  • HAL Id : hal-00872807 , version 1

Citer

Benedikt Bollig. Logic for Communicating Automata with Parameterized Topology. 2013. ⟨hal-00872807v1⟩
340 Consultations
275 Téléchargements

Partager

Gmail Facebook X LinkedIn More