Spatio-Temporal Model-Checking of Cyber-Physical Systems Using Graph Queries

  • Hojat KhosrowjerdiEmail author
  • Hamed Nemati
  • Karl Meinke
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 12165)


We explore the application of graph database technology to spatio-temporal model checking of cooperating cyber-physical systems-of- systems such as vehicle platoons. We present a translation of spatio-temporal automata (STA) and the spatio-temporal logic STAL to semantically equivalent property graphs and graph queries respectively. We prove a sound reduction of the spatio-temporal verification problem to graph database query solving. The practicability and efficiency of this approach is evaluated by introducing NeoMC, a prototype implementation of our explicit model checking approach based on Neo4j. To evaluate NeoMC we consider case studies of verifying vehicle platooning models. Our evaluation demonstrates the effectiveness of our approach in terms of execution time and counterexample detection.



This research has been supported by KTH ICT-TNG project STaRT (Spatio-Temporal Planning at Runtime), as well as the German Federal Ministry of Education and Research (BMBF) through funding for the CISPA-Stanford Center for Cybersecurity (FKZ: 13N1S0762).


  1. 1.
    Khosrowjerdi, H., Meinke, K.: Learning-based testing for autonomous systems using spatial and temporal requirements. In: Proceedings of the 1st International Workshop on Machine Learning and Software Engineering in Symbiosis, MASES@ASE 2018, Montpellier, France, 3 September 2018, pp. 6–15 (2018).
  2. 2.
    Kamali, M., Linker, S., Fisher, M.: Modular verification of vehicle platooning with respect to decisions, space and time. In: Artho, C., Ölveczky, P.C. (eds.) FTSCS 2018. CCIS, vol. 1008, pp. 18–36. Springer, Cham (2019). Scholar
  3. 3.
    Schwammberger, M.: An abstract model for proving safety of autonomous urban traffic. Theor. Comput. Sci. 744, 143–169 (2018). Scholar
  4. 4.
    Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994). Scholar
  5. 5.
    Chaochen, Z., Hoare, C., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269–276 (1991). Scholar
  6. 6.
    Haghighi, I., Jones, A., Kong, Z., Bartocci, E., Grosu, R., Belta, C.: Spatel: a novel spatial-temporal logic and its applications to networked systems. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC 2015, Seattle, WA, USA, 14–16 April 2015, pp. 189–198 (2015).
  7. 7.
    Quesel, J.-D., Schäfer, A.: Spatio-temporal model checking for mobile real-time systems. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 347–361. Springer, Heidelberg (2006). Scholar
  8. 8.
    Angles, R., Arenas, M., Barceló, P., Hogan, A., Reutter, J.L., Vrgoc, D.: Foundations of modern query languages for graph databases. ACM Comput. Surv. 50(5), 68:1–68:40 (2017). Scholar
  9. 9.
    Bennaceur, A., Hähnle, R., Meinke, K. (eds.): Machine Learning for Dynamic Software Analysis: Potentials and Limits. LNCS, vol. 11026. Springer, Cham (2018). Scholar
  10. 10.
    Meinke, K., Niu, F.: A learning-based approach to unit testing of numerical software. In: Petrenko, A., Simão, A., Maldonado, J.C. (eds.) ICTSS 2010. LNCS, vol. 6435, pp. 221–235. Springer, Heidelberg (2010). Scholar
  11. 11.
    Meinke, K., Sindhu, M.A.: Incremental learning-based testing for reactive systems. In: Gogolla, M., Wolff, B. (eds.) TAP 2011. LNCS, vol. 6706, pp. 134–151. Springer, Heidelberg (2011). Scholar
  12. 12.
    Webber, J.: A programmatic introduction to neo4j. In: Conference on Systems, Programming, and Applications: Software for Humanity, SPLASH 2012, Tucson, AZ, USA, 21–25 October 2012, pp. 217–218 (2012).
  13. 13.
    Francis, N., et al.: Cypher: an evolving query language for property graphs. In: Proceedings of the 2018 International Conference on Management of Data, SIGMOD Conference 2018, Houston, TX, USA, 10–15 June 2018, pp. 1433–1445 (2018).
  14. 14.
    de la Higuera, C.: Grammatical Inference: Learning Automata and Grammars. Cambridge University Press, (2010). iv + 417 pages, Machine Translation, vol. 24, no. 3–4, pp. 291–293, 2010.
  15. 15.
    Angles, R., Gutiérrez, C.: Survey of graph database models. ACM Comput. Surv. 40(1), 11–139 (2008). Scholar
  16. 16.
    Robinson, I., Webber, J., Eifrem, E.: Graph Databases: New Opportunities for Connected Data, 2nd edn. O’Reilly Media Inc., Sebastopol (2015)Google Scholar
  17. 17.
    Hölsch, J., Schmidt, T., Grossniklaus, M.: On the performance of analytical and pattern matching graph queries in neo4j and a relational database. In: Proceedings of the Workshops of the EDBT/ICDT 2017 Joint Conference (EDBT/ICDT 2017), Venice, Italy, 21–24 March 2017 (2017).
  18. 18.
    Francis, N., et al.: Formal semantics of the language cypher. CoRR, vol. abs/1802.09984 (2018).
  19. 19.
    Junghanns, M., Kießling, M., Averbuch, A., Petermann, A., Rahm, E.: Cypher-based graph pattern matching in gradoop. In: Proceedings of the Fifth International Workshop on Graph Data-management Experiences & Systems, GRADES@SIGMOD/PODS 2017, Chicago, IL, USA, 14–19 May 2017, pp. 3:1–3:8 (2017).
  20. 20.
    Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer, Cham (2018). Scholar
  21. 21.
    Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths (extended abstract). In: 24th Annual Symposium on Foundations of Computer Science, Tucson, Arizona, USA, 7–9 November 1983, pp. 185–194 (1983).
  22. 22.
    Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181–185 (1985). Scholar
  23. 23.
    Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Proceedings of the Symposium on Logic in Computer Science (LICS 1986), Cambridge, Massachusetts, USA, June 16–18, 1986, pp. 332–344 (1986)Google Scholar
  24. 24.
    Búr, M., Szilágyi, G., Vörös, A., Varró, D.: Distributed graph queries for runtime monitoring of cyber-physical systems. In: Russo, A., Schürr, A. (eds.) FASE 2018. LNCS, vol. 10802, pp. 111–128. Springer, Cham (2018). Scholar
  25. 25.
    Meinke, K.: Learning-based testing of cyber-physical systems-of-systems: a platooning study. In: Reinecke, P., Di Marco, A. (eds.) EPEW 2017. LNCS, vol. 10497, pp. 135–151. Springer, Cham (2017). Scholar
  26. 26.
    Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334–342. Springer, Cham (2014). Scholar
  27. 27.
    Holzmann, G.J.: The SPIN Model Checker - Primer and Referencemanual. Addison-Wesley, Boston (2004)Google Scholar
  28. 28.
    Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692–707. Springer, Heidelberg (2015). Scholar
  29. 29.
    Chiarugi, D., Falaschi, M., Hermith, D., Olarte, C.: Verification of spatial and temporal modalities in biochemical systems. Electr. Notes Theor. Comput. Sci. 316, 29–44 (2015). Scholar
  30. 30.
    Parvu, O., Gilbert, D.R.: Automatic validation of computational models using pseudo-3D Spatio-temporal model checking. BMC Syst. Biol. 8, 124 (2014). Scholar
  31. 31.
    Grosu, R., Smolka, S.A., Corradini, F., Wasilewska, A., Entcheva, E., Bartocci, E.: Learning and detecting emergent behavior in networks of cardiac myocytes. Commun. ACM 52(3), 97–105 (2009). Scholar
  32. 32.
    de Oliveira, Í.R., Cugnasca, P.S.: Checking safe trajectories of aircraft using hybrid automata. In: Anderson, S., Felici, M., Bologna, S. (eds.) SAFECOMP 2002. LNCS, vol. 2434, pp. 224–235. Springer, Heidelberg (2002). Scholar
  33. 33.
    Ciancia, V., Grilletti, G., Latella, D., Loreti, M., Massink, M.: An experimental spatio-temporal model checker. In: Bianculli, D., Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9509, pp. 297–311. Springer, Heidelberg (2015). Scholar
  34. 34.
    Ciancia, V., Gilmore, S., Grilletti, G., Latella, D., Loreti, M., Massink, M.: Spatio-temporal model checking of vehicular movement in public transport systems. STTT 20(3), 289–311 (2018). Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.KTH Royal Institute of TechnologyStockholmSweden
  2. 2.Helmholtz Center for Information Security (CISPA)SaarbrückenGermany

Personalised recommendations