Adding Data Registers to Parameterized Networks with Broadcast

Issue title: Reachability Problems for Infinite State Systems

Guest editors: Parosh Aziz Abdulla, Stéphane Demri, Alain Finkel, Jérôme Leroux and Igor Potapov

Article type: Research Article

Authors: Delzanno, Giorgio^{a; *} | Sangnier, Arnaud^b | Traverso, Riccardo^c

Affiliations: [a] DIBRIS, University of Genova, Italy. [email protected] | [b] LIAFA, Univ Paris Diderot, Paris Cité Sorbonne, CNRS, France. [email protected] | [c] FBK, Trento, Italy. [email protected]

Correspondence: [*] Address for correspondence: DIBRIS, University of Genova, Via Dodecaneso, 35 16146 Genova, Italy

Abstract: We study parameterized verification problems for networks of interacting register automata. The network is represented through a graph, and processes may exchange broadcast messages containing data with their neighbours. Upon reception a process can either ignore a sent value, test for equality with a value stored in a register, or simply store the value in a register. We consider safety properties expressed in terms of reachability, from arbitrarily large initial configurations, of a configuration exposing some given control states and patterns. We investigate, in this context, the impact on decidability and complexity of the number of local registers, the number of values carried by a single message, and dynamic reconfigurations of the underlying network.

DOI: 10.3233/FI-2016-1315

Journal: Fundamenta Informaticae, vol. 143, no. 3-4, pp. 287-316, 2016