| Date |
13-11-2012 |
| Number |
DISI-TR-12-05 |
| Title |
On the Coverability Problem for Asynchronous Broadcast Networks (Extended and Revised Version) |
| Authors |
Giorgio Delzanno and Riccardo Traverso |
| Bibtex Entry |
|
| E-mail |
delzanno@disi.unige.it |
| Link |
http://www.disi.unige.it/person/DelzannoG/Papers/dt12rev.pdf |
| Abstract |
We study verification problems for networks in which nodes communicate via
asynchronous broadcast messages.
This type of communication is achieved by using a distributed model in which
nodes have a local buffer.
We present here a formal model based on communicating automata with different
type of mailboxes (bags/queues).
We give preliminary results on decidability and undecidability of verification
problems formulated in terms of coverability for an initial parametric configuration.
The decision problems that we consider naturally model the search of an initial topology
that may lead to an error state in the protocol.
We study these problems by considering different policies for handling local
buffers such as unordered, fifo and lossy fifo queues.
Note:
A preliminary version based on WSTS-theory but no complexity results and incomplete undecidability proofs
is available at the URL:
http://www.disi.unige.it/person/DelzannoG/Papers/dt12.pdf (6/11/12)
An extended abstract of the preliminary results appeared at ICTCS 2012. |
