License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2014.653
URN: urn:nbn:de:0030-drops-48787
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2014/4878/
Go to the corresponding LIPIcs Volume Portal


Abdulla, Parosh Aziz ; Atig, Mohamed Faouzi ; Kara, Ahmet ; Rezine, Othmane

Verification of Dynamic Register Automata

pdf-format:
54.pdf (0.6 MB)


Abstract

We consider the verification problem for Dynamic Register Automata (DRA). DRA extend classical register automata by process creation. In this setting, each process is equipped with a finite set of registers in which the process IDs of other processes can be stored. A process can communicate with processes whose IDs are stored in its registers and can send them the content of its registers. The state reachability problem asks whether a DRA reaches a configuration where at least one process is in an error state. We first show that this problem is in general undecidable. This result holds even when we restrict the analysis to configurations where the maximal length of the simple paths in their underlying (un)directed communication graphs are bounded by some constant. Then we introduce the model of degenerative DRA which allows non-deterministic reset of the registers. We prove that for every given DRA, its corresponding degenerative one has the same set of reachable states. While the state reachability of a degenerative DRA remains undecidable, we show that the problem becomes decidable with nonprimitive recursive complexity when we restrict the analysis to strongly bounded configurations, i.e. configurations whose underlying undirected graphs have bounded simple paths. Finally, we consider the class of strongly safe DRA, where all the reachable configurations are assumed to be strongly bounded. We show that for strongly safe DRA, the state reachability problem becomes decidable.

BibTeX - Entry

@InProceedings{abdulla_et_al:LIPIcs:2014:4878,
  author =	{Parosh Aziz Abdulla and Mohamed Faouzi Atig and Ahmet Kara and Othmane Rezine},
  title =	{{Verification of  Dynamic Register Automata}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{653--665},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Venkatesh Raman and S. P. Suresh},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2014/4878},
  URN =		{urn:nbn:de:0030-drops-48787},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.653},
  annote =	{Keywords: Verification, Reachability problem, Register automata}
}

Keywords: Verification, Reachability problem, Register automata
Collection: 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)
Issue Date: 2014
Date of publication: 12.12.2014


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI