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.

Adding Data Registers to Parameterized Networks with Broadcast

Traverso, Riccardo
2016-01-01

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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/307070
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact