Home | Search | Help  
Home Page Università di Genova

Technical Report Details

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.

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.
Back to Technical Reports