1 Search Results for "Rezine, Othmane"

Document

DOI: 10.4230/LIPIcs.FSTTCS.2014.653

Verification of Dynamic Register Automata

Authors: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmet Kara, and Othmane Rezine

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

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.

Cite as

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmet Kara, and Othmane Rezine. Verification of Dynamic Register Automata. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 653-665, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:LIPIcs.FSTTCS.2014.653,
  author =	{Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Kara, Ahmet and Rezine, Othmane},
  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 =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.653},
  URN =		{urn:nbn:de:0030-drops-48787},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.653},
  annote =	{Keywords: Verification, Reachability problem, Register automata}
}

Refine by Author
1 Abdulla, Parosh Aziz
1 Atig, Mohamed Faouzi
1 Kara, Ahmet
1 Rezine, Othmane

Refine by Classification

Refine by Keyword
1 Reachability problem
1 Register automata
1 Verification

Refine by Type
1 document

Refine by Publication Year
1 2014

1 Search Results for "Rezine, Othmane"

Verification of Dynamic Register Automata

Abstract

Cite as

Thanks for your feedback!

Could not send message