Skip to main content
SpringerLink
Log in

Model Checking Dynamic Distributed Systems

  • 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:

  • 608 Accesses

Abstract

We consider distributed systems with dynamic process creation. We use data words to model behaviors of such systems. Data words are words where positions also contain some data values from an infinite domain. The data values are seen as the process identities. We use an automata with a stack and registers to model a distributed system with dynamic process creation. The non-emptiness checking of these automata is NP-Complete. While satisfiability of first order logic over data words is undecidable, we show that model checking such an automata against full MSO logic (with data equality and comparison predicates) is decidable.

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., Kara, A., Rezine, O.: Verification of dynamic register automata. In: Raman, V., Suresh, S.P. (eds.) FSTTCS 2014. LIPIcs, vol. 20, pp. 653–665. Leibniz-Zentrum für Informatik (2014)

    Google Scholar 

  2. Alur, R., Madhusudan, P.: Adding nesting structure to words. J. ACM 56(3), 1–43 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  3. Atig, M.F., Bouajjani, A., Qadeer, S.: Context-bounded analysis for concurrent programs with dynamic creation of threads. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 107–123. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  4. Bojańczyk, M., David, C., Muscholl, A., Schwentick, T., Segoufin, L.: Two-variable logic on data words. ACM Trans. Comput. Log. 12(4), 27 (2011)

    MathSciNet  MATH  Google Scholar 

  5. Bollig, B.: An automaton over data words that captures EMSO logic. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 171–186. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  6. Bollig, B.: Logic for Communicating Automata with Parameterized Topology. In: CSL/LICS 2014, chap. 18. ACM Press (2014)

    Google Scholar 

  7. Bollig, B., Cyriac, A., Gastin, P., Narayan Kumar, K.: Model checking languages of data words. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol. 7213, pp. 391–405. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  8. Bollig, B., Gastin, P., Kumar, A.: Parameterized communicating automata: complementation and model checking. In: Raman, V., Suresh, S.P. (eds.) FSTTCS 2014. LIPIcs, vol. 20, pp. 625–637. Leibniz-Zentrum für Informatik (2014)

    Google Scholar 

  9. Bollig, B., Gastin, P., Schubert, J.: Parameterized verification of communicating automata under context bounds. In: Ouaknine, J., Potapov, I., Worrell, J. (eds.) RP 2014. LNCS, vol. 8762, pp. 45–57. Springer, Heidelberg (2014)

    Google Scholar 

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

  11. Demri, S., Lazić, R.: LTL with the freeze quantifier and register automata. ACM Trans. Comput. Logic 10(3), 16 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  12. Demri, S., Lazić, R.S., Sangnier, A.: Model checking freeze LTL over one-counter automata. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 490–504. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  13. Demri, S., Sangnier, A.: When model-checking freeze LTL over counter machines becomes decidable. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 176–190. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  14. Leucker, M., Madhusudan, P., Mukhopadhyay, S.: Dynamic message sequence charts. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 253–264. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Uppsala University, Uppsala, Sweden

    C. Aiswarya

Authors
  1. C. Aiswarya
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to C. Aiswarya .

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

Aiswarya, C. (2015). Model Checking Dynamic Distributed Systems. 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_4

Download citation

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

  • 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