A tool-chain for statistical spatio-temporal model checking of bike sharing systems
| Autor: | Diego Latella, Rytis Paškauskas, Vincenzo Ciancia, Andrea Vandin, Mieke Massink |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2016 |
| Předmět: |
Model checking
MultiVeStA Computer science Distributed computing F.4.1 MATHEMATICAL LOGIC AND FORMAL LANGUAGES. Mathematical Logic Statistical Model Checking 02 engineering and technology computer.software_genre Statistical model checking Chain (algebraic topology) 0202 electrical engineering electronic engineering information engineering Collective adaptive systems Statistical analysis Spatial Logics Model-checking Markov chain D.2.4 SOFTWARE ENGINEERING. Software/Program Verification 020207 software engineering Spatio-temporal model checking Smart transportation Spatial Logics Bike sharing 020201 artificial intelligence & image processing Statistical Model-checking Data mining computer Bike-sharing Smart cities |
| Zdroj: | Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. 7th International Symposium, pp. 657–673, Corfu, Greece, 10-14 October 2016 info:cnr-pdr/source/autori:Ciancia V.; Latella D.; Massink M.; Paskauskas R.; Vandin A./congresso_nome:Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. 7th International Symposium/congresso_luogo:Corfu, Greece/congresso_data:10-14 October 2016/anno:2016/pagina_da:657/pagina_a:673/intervallo_pagine:657–673 Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques ISBN: 9783319471655 ISoLA (1) |
| DOI: | 10.1007/978-3-319-47166-2_46 |
| Popis: | Prominent examples of collective systems are often encountered when analysing smart cities and smart transportation systems. We propose a novel modelling and analysis approach combining statistical model checking, spatio-temporal logics, and simulation. The proposed methodology is applied to modelling and statistical analysis of user behaviour in bike sharing systems. We present a tool-chain that integrates the statistical analysis toolkit MultiVeStA, the spatio-temporal model checker topochecker, and a bike sharing systems simulator based on Markov renewal processes. The obtained tool allows one to estimate, up to a user-specified precision, the likelihood of specific spatio-temporal formulas, such as the formation of clusters of full stations and their temporal evolution. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|