Conference paper · Book chapter
A Tool-Chain for Statistical Spatio-Temporal Model Checking of Bike Sharing Systems
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.
| Language: | English |
|---|---|
| Publisher: | Springer International Publishing |
| Year: | 2016 |
| Pages: | 657-673 |
| Proceedings: | International Symposium on Leveraging Applications of Formal Methods |
| Series: | Lecture Notes in Computer Science |
| Journal subtitle: | 7th International Symposium, Isola 2016, Imperial, Corfu, Greece, October 10–14, 2016, Proceedings, Part I |
| ISBN: | 3319471651 , 331947166X , 331947166x , 9783319471655 and 9783319471662 |
| Types: | Conference paper and Book chapter |
| DOI: | 10.1007/978-3-319-47166-2_46 |
Artificial Intelligence (incl. Robotics) Collective adaptive systems Computation by Abstract Devices Computer Science Logics and Meanings of Programs Mathematical Logic and Formal Languages MultiVeStA Programming Languages, Compilers, Interpreters Software Engineering Spatio-temporal model checking Statistical model checking
