Skip to main content
SpringerLink
Log in

Statistical Model Checking for Traffic Models

  • Conference paper
  • First Online:
Formal Methods: Foundations and Applications (SBMF 2021)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 13130))

Included in the following conference series:

Abstract

Statistical Model Checking (SMC) is a popular technique in formal methods for analyzing large stochastic systems. As opposed to the expensive but exact model checking algorithms, this technique allows for a trade-off between accuracy and running time. SMC is based on Monte Carlo sampling of the runs of the stochastic system, and lends itself to stochastic discrete event simulators as well.

In this paper, we use SMC to analyze traffic models like car-following and lane-changing models. We achieve this through an integration of the SMC tool MultiVeStA with the discrete event simulation software for urban mobility, SUMO.

As illustration of the approach and the tool chain, we compare the car-following and lane-changing models against various performance parameters like throughput, emissions and waiting times. Importantly, the use of formal methods allows for formulating and evaluating complex queries that can be asked of the model. The results show the utility of such a tool chain in performing complex quantitative what-if analyses of various traffic models and policies.

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 44.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 59.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. MultiVeStA. https://github.com/andrea-vandin/MultiVeStA/wiki/. Accessed 28 Sept 2021

  2. Simulation of Urban MObility. https://www.eclipse.org/sumo/. Accessed 06 Aug 2021

  3. Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. (TOMACS) 28(1), 6 (2018)

    Article  MathSciNet  Google Scholar 

  4. Agha, G.A., Meseguer, J., Sen, K.: PMaude: rewrite-based specification language for probabilistic object systems. Electron. Notes Theor. Comput. Sci. 153(2), 213–239 (2006)

    Article  Google Scholar 

  5. Ahmed, H.U., Huang, Y., Lu, P.: A review of car-following models and modeling tools for human and autonomous-ready driving behaviors in micro-simulation. Smart Cities 4(1), 314–335 (2021)

    Article  Google Scholar 

  6. AlTurki, M., Meseguer, J.: PVeStA: a parallel statistical model checking and quantitative analysis tool. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 386–392. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22944-2_28

    Chapter  Google Scholar 

  7. Baier, C., Katoen, J.P.: Principles of Model Checking (Representation and Mind Series). The MIT Press, Boston (2008)

    MATH  Google Scholar 

  8. Erdmann, J.: Lane-changing model in SUMO. In: Proceedings of the SUMO 2014 Modeling Mobility with Open Data, vol. 24, May 2014

    Google Scholar 

  9. Erdmann, J.: SUMO’s lane-changing model. In: Behrisch, M., Weber, M. (eds.) Modeling Mobility with Open Data. LNM, pp. 105–123. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-15024-6_7

    Chapter  Google Scholar 

  10. Kanagaraj, V., Asaithambi, G., Kumar, C.N., Srinivasan, K.K., Sivanandan, R.: Evaluation of different vehicle following models under mixed traffic conditions. Proc. Soc. Behav. Sci. 104, 390–401 (2013). 2nd Conference of Transportation Research Group of India (2nd CTRG)

    Google Scholar 

  11. Krauß, S., Wagner, P., Gawron, C.: Metastable states in a microscopic model of traffic flow. Phys. Rev. E 55(5), 5597 (1997)

    Article  Google Scholar 

  12. Lopez, P.A., et al.: Microscopic traffic simulation using sumo. In: The 21st IEEE International Conference on Intelligent Transportation Systems. IEEE, November 2018

    Google Scholar 

  13. Mintsis, E., et al.: TransAID deliverable 3.1 - modelling, simulation and assessment of vehicle automations and automated vehicles’ driver behaviour in mixed traffic, September 2019

    Google Scholar 

  14. Nimal, V.: Statistical approaches for probabilistic model checking. Ph.D. thesis, University of Oxford (2010)

    Google Scholar 

  15. Olstam, J., Tapani, A.: Comparison of car-following models. In: VTI meddelande 960A (2004)

    Google Scholar 

  16. Pourabdollah, M., Bjärkvik, E., Fürer, F., Lindenberg, B., Burgdorf, K.: Calibration and evaluation of car following models using real-world driving data. In: 2017 IEEE 20th International Conference on Intelligent Transportation Systems (ITSC), pp. 1–6 (2017)

    Google Scholar 

  17. Sebastio, S., Vandin, A.: Multivesta: statistical model checking for discrete event simulators. In: Horváth, A., Buchholz, P., Cortellessa, V., Muscariello, L., Squillante, M.S. (eds.) 7th International Conference on Performance Evaluation Methodologies and Tools, ValueTools 2013, pp. 310–315. ICST/ACM (2013)

    Google Scholar 

  18. Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202–215. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27813-9_16

    Chapter  Google Scholar 

  19. Sen, K., Viswanathan, M., Agha, G.A.: VESTA: a statistical model-checker and analyzer for probabilistic systems. In: Second International Conference on the Quantitative Evaluaiton of Systems (QEST 2005), 19–22 September 2005, Torino, Italy, pp. 251–252. IEEE Computer Society (2005)

    Google Scholar 

  20. Thamilselvam, B., Kalyanasundaram, S., Rao, M.V.P.: Scalable coordinated intelligent traffic light controller for heterogeneous traffic scenarios using UPPAAL STRATEGO. In: 2021 International Conference on COMmunication Systems NETworkS (COMSNETS), pp. 404–412 (2021)

    Google Scholar 

  21. Treiber, M., Hennecke, A., Helbing, D.: Congested traffic states in empirical observations and microscopic simulations. Phys. Rev. E 62(2), 1805 (2000)

    Article  Google Scholar 

  22. Wiedemann, R.: Simulation des strassenverkehrsflusses. Institut fur Verkehrswesen der Universitat Karlsruhe (1994)

    Google Scholar 

  23. Younes, H.L.S., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking: an empirical study. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 46–60. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24730-2_4

    Chapter  Google Scholar 

  24. Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223–235. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45657-0_17

    Chapter  MATH  Google Scholar 

Download references

Acknowledgment

Thamilselvam is supported by the project M2Smart: Smart Cities for Emerging Countries based on Sensing, Network and Big Data Analysis of Multimodal Regional Transport System, JST/JICA SATREPS (Program ID JPMJSA1606), Japan and Shubham Parmar is supported by the DST National Mission for Interdisciplinary Cyber-Physical Systems (NM-ICPS), Technology Innovation Hub on Autonomous Navigation and Data Acquisition Systems: TiHAN Foundations at Indian Institute of Technology (IIT) Hyderabad.

Author information

Authors and Affiliations

  1. Department of Computer Science and Engineering, IIT Hyderabad, Sangareddy, India

    B. Thamilselvam, Subrahmanyam Kalyanasundaram, Shubham Parmar & M. V. Panduranga Rao

Authors
  1. B. Thamilselvam
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Subrahmanyam Kalyanasundaram
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Shubham Parmar
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. M. V. Panduranga Rao
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Subrahmanyam Kalyanasundaram .

Editor information

Editors and Affiliations

  1. Departamento de Ciência da Computação, Universidade Federal de Minas Gerais, Belo Horizonte, Minas Gerais, Brazil

    Sérgio Campos

  2. College of Information and Computer Sciences, University of Massachusetts, Amherst, MA, USA

    Marius Minea

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Thamilselvam, B., Kalyanasundaram, S., Parmar, S., Panduranga Rao, M.V. (2021). Statistical Model Checking for Traffic Models. In: Campos, S., Minea, M. (eds) Formal Methods: Foundations and Applications. SBMF 2021. Lecture Notes in Computer Science(), vol 13130. Springer, Cham. https://doi.org/10.1007/978-3-030-92137-8_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-92137-8_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-92136-1

  • Online ISBN: 978-3-030-92137-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation