Skip to main content
SpringerLink
Log in

Verification of Buffered Dynamic Register Automata

  • Conference paper
  • First Online:
Networked Systems (NETYS 2015)

Part of the book series: Lecture Notes in Computer Science ((LNCCN,volume 9466))

Included in the following conference series:

Abstract

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.

Supported by the Uppsala Programming for Multicore Architectures Research Center (UPMARC) and the Programming Platform for Future Wireless Sensor Networks Project (PROFUN). The third author acknowledges the financial support by the German DFG under grant SCHW 678/4-2.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  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)

    Chapter  Google Scholar 

  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. 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. 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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. Ding, G.: Subgraphs and well quasi ordering. J. Graph Theory 16(5), 489–502 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  10. Figueira, D.: Alternating register automata on finite words and trees. Logical Methods in Computer Science 8(1), 22 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  11. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theor. Comput. Sci. 256(1–2), 63–92 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. Kaminski, M., Francez, N.: Finite-memory automata. Theor. Comput. Sci. 134(2), 329–363 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  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. Meyer, R.: On boundedness in depth in the pi-calculus. In: IFIP TCS, pp. 477–489 (2008)

    Google Scholar 

  17. Neven, F., Schwentick, T., Vianu, V.: Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Log. 5(3), 403–435 (2004)

    Article  MathSciNet  Google Scholar 

  18. Sakamoto, H., Ikeda, D.: Intractability of decision problems for finite-memory automata. Theor. Comput. Sci. 231(2), 297–308 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  19. Tzevelekos, N.: Fresh-register automata. In: POPL. ACM (2011)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Uppsala University, Uppsala, Sweden

    Parosh Aziz Abdulla, Mohamed Faouzi Atig & Othmane Rezine

  2. TU Dortmund University, Dortmund, Germany

    Ahmet Kara

Authors
  1. Parosh Aziz Abdulla
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mohamed Faouzi Atig
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ahmet Kara
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Othmane Rezine
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Othmane Rezine .

Editor information

Editors and Affiliations

  1. Université Paris Diderot, Paris Cedex 13, France

    Ahmed Bouajjani

  2. Université Paris Diderot, Paris Cedex 13, France

    Hugues Fauconnier

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Abdulla, P.A., Atig, M.F., Kara, A., Rezine, O. (2015). Verification of Buffered Dynamic Register Automata. In: Bouajjani, A., Fauconnier, H. (eds) Networked Systems . NETYS 2015. Lecture Notes in Computer Science(), vol 9466. Springer, Cham. https://doi.org/10.1007/978-3-319-26850-7_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-26850-7_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-26849-1

  • Online ISBN: 978-3-319-26850-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation