Model Checking Dynamic Distributed Systems

  • C. AiswaryaEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9466)


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.


  1. 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. 2.
    Alur, R., Madhusudan, P.: Adding nesting structure to words. J. ACM 56(3), 1–43 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 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) CrossRefGoogle Scholar
  4. 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)MathSciNetzbMATHGoogle Scholar
  5. 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) CrossRefGoogle Scholar
  6. 6.
    Bollig, B.: Logic for Communicating Automata with Parameterized Topology. In: CSL/LICS 2014, chap. 18. ACM Press (2014)Google Scholar
  7. 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) CrossRefGoogle Scholar
  8. 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. 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. 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) CrossRefGoogle Scholar
  11. 11.
    Demri, S., Lazić, R.: LTL with the freeze quantifier and register automata. ACM Trans. Comput. Logic 10(3), 16 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 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) CrossRefGoogle Scholar
  13. 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) CrossRefGoogle Scholar
  14. 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) CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.Uppsala UniversityUppsalaSweden

Personalised recommendations