Document Open Access Logo

Verification of Dynamic Register Automata

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

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2014.653.pdf
  • Filesize: 0.58 MB
  • 13 pages

Document Identifiers

Author Details

Parosh Aziz Abdulla
Mohamed Faouzi Atig
Ahmet Kara
Othmane Rezine

Cite As Get BibTex

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) https://doi.org/10.4230/LIPIcs.FSTTCS.2014.653

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.

Subject Classification

Keywords
  • Verification
  • Reachability problem
  • Register automata

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Parosh Aziz Abdula, Mohamed Faouzi Atig, and Othmane Rezine. Verification of directed acyclic ad hoc networks. In FMOODS/FORTE, pages 193-208, 2013. Google Scholar
  2. P. A. Abdulla, K. Cerans, B. Jonsson, and Y. K. Tsay. General decidability theorems for infinite-state systems. In LICS'96, pages 313-321. IEEE Computer Society, 1996. Google Scholar
  3. Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. Inf. Comput., 127(2):91-101, 1996. Google Scholar
  4. Bharat Adsul, Madhavan Mukund, K. Narayan Kumar, and Vasumathi Narayanan. Causal closure for MSC languages. In FSTTCS, volume 3821 of LNCS, pages 335-347. Springer, 2005. Google Scholar
  5. Rajeev Alur, Kousha Etessami, and Mihalis Yannakakis. Realizability and verification of MSC graphs. Theor. Comput. Sci., 331(1):97-114, 2005. Google Scholar
  6. Michael Benedikt, Clemens Ley, and Gabriele Puppis. Automata vs. logics on data words. In CSL, volume 6247 of LNCS, pages 110-124. Springer, 2010. Google Scholar
  7. Benedikt Bollig, Aiswarya Cyriac, Loïc Hélouët, Ahmet Kara, and Thomas Schwentick. Dynamic communicating automata and branching high-level MSCs. In LATA, volume 7810 of LNCS. Springer, 2013. Google Scholar
  8. Benedikt Bollig and Loïc Hélouët. Realizability of dynamic MSC languages. In CSR, volume 6072 of LNCS. Springer, 2010. Google Scholar
  9. Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines. J. ACM, 30(2):323-342, 1983. Google Scholar
  10. G. Delzanno, A. Sangnier, and G. Zavattaro. Parameterized verification of ad hoc networks. In CONCUR'10, volume 6269 of LNCS. Springer, 2010. Google Scholar
  11. G. Delzanno, A. Sangnier, and G. Zavattaro. On the power of cliques in the parameterized verification of ad hoc networks. In FoSSaCS'11, volume 6604 of LNCS, pages 441-455. Springer, 2011. Google Scholar
  12. Giorgio Delzanno, Arnaud Sangnier, and Riccardo Traverso. Parameterized verification of broadcast networks of register automata. In RP, volume 8169 of LNCS. Springer, 2013. Google Scholar
  13. Giorgio Delzanno, Arnaud Sangnier, Riccardo Traverso, and Gianluigi Zavattaro. On the complexity of parameterized reachability in reconfigurable broadcast networks. In FSTTCS, volume 18 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012. Google Scholar
  14. Stéphane Demri and Ranko Lazic. LTL with the freeze quantifier and register automata. In LICS, pages 17-26. IEEE Computer Society, 2006. Google Scholar
  15. D. Figueira. Alternating register automata on finite words and trees. Logical Methods in Computer Science, 8(1), 2012. Google Scholar
  16. A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! Theor. Comput. Sci., 256(1-2):63-92, 2001. Google Scholar
  17. Blaise Genest, Dietrich Kuske, and Anca Muscholl. A kleene theorem and model checking algorithms for existentially bounded communicating automata. Inf. Comput., 204(6):920-956, 2006. Google Scholar
  18. Jesper G. Henriksen, Madhavan Mukund, K. Narayan Kumar, Milind A. Sohoni, and P. S. Thiagarajan. A theory of regular MSC languages. Inf. Comput., 202(1):1-38, 2005. Google Scholar
  19. M. Jurdzinski and R. Lazic. Alternation-free modal mu-calculus for data trees. In LICS, pages 131-140. IEEE Computer Society, 2007. Google Scholar
  20. Michael Kaminski and Nissim Francez. Finite-memory automata. Theor. Comput. Sci., 134(2):329-363, 1994. Google Scholar
  21. Ranko Lazic. Safely freezing LTL. In FSTTCS, volume 4337 of LNCS, pages 381-392. Springer, 2006. Google Scholar
  22. Anca Muscholl and Doron Peled. Message sequence graphs and decision problems on Mazurkiewicz traces. In MFCS, volume 1672 of LNCS, pages 81-91. Springer, 1999. Google Scholar
  23. Frank Neven, Thomas Schwentick, and Victor Vianu. Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Log., 5(3):403-435, 2004. Google Scholar
  24. Hiroshi Sakamoto and Daisuke Ikeda. Intractability of decision problems for finite-memory automata. Theor. Comput. Sci., 231(2):297-308, 2000. Google Scholar
  25. P. Schnoebelen. Revisiting ackermann-hardness for lossy counter machines and reset petri nets. In MFCS, volume 6281 of LNCS, pages 616-628. Springer, 2010. Google Scholar
  26. Anu Singh, C. R. Ramakrishnan, and Scott A. Smolka. Query-based model checking of ad hoc network protocols. In CONCUR, volume 5710 of LNCS, pages 603-619. Springer, 2009. Google Scholar
  27. Anu Singh, C. R. Ramakrishnan, and Scott A. Smolka. A process calculus for mobile ad hoc networks. Sci. Comput. Program., 75(6):440-469, 2010. Google Scholar
  28. Nikos Tzevelekos. Fresh-register automata. In POPL. ACM, 2011. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact