Verification of Buffered Dynamic Register Automata

  • Parosh Aziz Abdulla
  • Mohamed Faouzi Atig
  • Ahmet Kara
  • Othmane RezineEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9466)


We consider the verification problem for Communicating Register Automata (BDRA) which extend classical register automata by process creation. In this setting, each process is equipped with a mailbox (i.e., a channel) in which received messages can be stored. Moreover, each process has a finite number of registers in which IDs of other processes can be stored. A process can send messages to the mailbox of the processes whose IDs are stored in its registers and can send them the content of its registers. The state reachability problem asks whether a BDRA reaches a configuration where at least one process is in an error state. In this paper, we study the decidability of the reachability problem for different kind of channels and we provide a complete characterisation of the (un)decidable subclasses in this generalised setting.


Formal verification Distributed systems 


  1. 1.
    Abdulla, P.A., Atig, M.F., Rezine, O.: Verification of directed acyclic ad hoc networks. In: Beyer, D., Boreale, M. (eds.) FORTE 2013 and FMOODS 2013. LNCS, vol. 7892, pp. 193–208. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  2. 2.
    Abdulla, P., Cerans, K., Jonsson, B., Tsay, Y.: General decidability theorems for infinite-state systems. In: LICS 1996, pp. 313–321. IEEE Computer Society (1996)Google Scholar
  3. 3.
    Abdulla, P.A., Atig, M.F., Kara, A., Rezine, O.: Verification of dynamic register automata. In: FSTTCS 2014, pp. 653–665 (2014)Google Scholar
  4. 4.
    Benedikt, M., Ley, C., Puppis, G.: Automata vs. logics on data words. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 110–124. Springer, Heidelberg (2010) CrossRefGoogle Scholar
  5. 5.
    Bollig, B., Cyriac, A., Hélouët, L., Kara, A., Schwentick, T.: Dynamic communicating automata and branching high-level MSCs. In: Dediu, A.-H., Martín-Vide, C., Truthe, B. (eds.) LATA 2013. LNCS, vol. 7810, pp. 177–189. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  6. 6.
    Bollig, B., Hélouët, L.: Realizability of dynamic MSC languages. In: Ablayev, F., Mayr, E.W. (eds.) CSR 2010. LNCS, vol. 6072, pp. 48–59. Springer, Heidelberg (2010) CrossRefGoogle Scholar
  7. 7.
    Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of ad hoc networks. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 313–327. Springer, Heidelberg (2010) CrossRefGoogle Scholar
  8. 8.
    Demri, S., Lazic, R.: LTL with the freeze quantifier and register automata. In: LICS, pp. 17–26. IEEE Computer Society (2006)Google Scholar
  9. 9.
    Ding, G.: Subgraphs and well quasi ordering. J. Graph Theory 16(5), 489–502 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Figueira, D.: Alternating register automata on finite words and trees. Logical Methods in Computer Science 8(1), 22 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theor. Comput. Sci. 256(1–2), 63–92 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Grigore, R., Distefano, D., Petersen, R.L., Tzevelekos, N.: Runtime verification based on register automata. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 260–276. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  13. 13.
    Jurdzinski, M., Lazic, R.: Alternation-free modal mu-calculus for data trees. In: LICS, pp. 131–140. IEEE Computer Society (2007)Google Scholar
  14. 14.
    Kaminski, M., Francez, N.: Finite-memory automata. Theor. Comput. Sci. 134(2), 329–363 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Lazić, R.S.: Safely freezing LTL. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 381–392. Springer, Heidelberg (2006) Google Scholar
  16. 16.
    Meyer, R.: On boundedness in depth in the pi-calculus. In: IFIP TCS, pp. 477–489 (2008)Google Scholar
  17. 17.
    Neven, F., Schwentick, T., Vianu, V.: Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Log. 5(3), 403–435 (2004)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Sakamoto, H., Ikeda, D.: Intractability of decision problems for finite-memory automata. Theor. Comput. Sci. 231(2), 297–308 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Tzevelekos, N.: Fresh-register automata. In: POPL. ACM (2011)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  • Parosh Aziz Abdulla
    • 1
  • Mohamed Faouzi Atig
    • 1
  • Ahmet Kara
    • 2
  • Othmane Rezine
    • 1
    Email author
  1. 1.Uppsala UniversityUppsalaSweden
  2. 2.TU Dortmund UniversityDortmundGermany

Personalised recommendations