Reachability Predicates for Graph Assertions

  • Giorgio DelzannoEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9899)


We introduce a logic-based formalism to specify updates on arbitrary graphs. For the resulting language called GLog, we introduce an assertional language for reasoning about infinite sets of graph configurations in which we use reachability predicates to specify paths of arbitrary length. For the considered assertional language and a restricted class of update rules, we define a symbolic procedure to compute predecessor configurations.


  1. 1.
    Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: acceleration from theory to practice. STTT 10(5), 401–424 (2008)CrossRefGoogle Scholar
  2. 2.
    Bertrand, N., Delzanno, G., König, B., Sangnier, A., Stückrath, J.: On the decidability status of reachability and coverability in graph transformation systems. In: 23rd International Conference on Rewriting Techniques and Applications (RTA 2012), Nagoya, Japan, 28 May – 2 June 2012, pp. 101–116 (2012)Google Scholar
  3. 3.
    Bouajjani, A., Dragoi, C., Enea, C., Jurski, Y., Sighireanu, M.: A generic framework for reasoning about dynamic networks of in nite-state processes. Logical Methods Comput. Sci. 5(2), 1–29 (2009).
  4. 4.
    Das, S., Perkins, C., Belding-Royer, E.: Ad hoc on-demand distance vector (AODV) routing (2003)Google Scholar
  5. 5.
    Delzanno, G.: A logic-based approach to verify distributed protocols. To appear in the Proceedings of CILC (2016)Google Scholar
  6. 6.
    Delzanno, G., Sangnier, A., Traverso, R., Zavattaro, G.: On the complexity of parameterized reachability in recongurable broadcast networks. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012, Hyderabad, India, 15–17 December 2012, pp. 289–300 (2012)Google Scholar
  7. 7.
    Emerson, E.A., Namjoshi, K.S.: On model checking for non-deterministic in nite-state systems. In: Thirteenth Annual IEEE Symposium on Logic in Computer Science, Indianapolis, Indiana, USA, 21–24 June 1998, pp. 70–80 (1998)Google Scholar
  8. 8.
    Fioravanti, F., Pettorossi, A., Proietti, M., Senni, V.: Improving reachability analysis of in nite state systems by specialization. Fundam. Inform. 119(3–4), 281–300 (2012)MathSciNetzbMATHGoogle Scholar
  9. 9.
    German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675–735 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Ghamarian, A.H., de Mol, M., Rensink, A., Zambon, E., Zimakova, M.: Modelling and analysis using groove. STTT 14(1), 15–40 (2012)CrossRefGoogle Scholar
  11. 11.
    König, B., Kozioura, V.: Augur 2 - a new version of a tool for the analysis of graph transformation systems. Electron. Notes Theor. Comput. Sci. 211, 201–210 (2008)CrossRefGoogle Scholar
  12. 12.
    Meyer, R., Strazny, T.: Petruchio: from dynamic networks to nets. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 175–179. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  13. 13.
    Namjoshi, K.S., Trefler, R.J.: Uncovering symmetries in irregular process networks. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 496–514. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  14. 14.
    Stückrath, J.: Uncover: using coverability analysis for verifying graph transformation systems. In: Parisi-Presicce, F., Westfechtel, B. (eds.) ICGT 2015. LNCS, vol. 9151, pp. 266–274. Springer, Heidelberg (2015)CrossRefGoogle Scholar
  15. 15.
  16. 16.
  17. 17.
  18. 18.
  19. 19.
  20. 20.
  21. 21.
  22. 22.

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.DIBRISUniversity of GenovaGenovaItaly

Personalised recommendations