A tool-chain for statistical spatio-temporal model checking of bike sharing systems
Ciancia V, Latella D, Massink M, Paskauskas R, Vandin A
Bike-sharing Statistical Model-checking Smart cities F.4.1 MATHEMATICAL LOGIC AND FORMAL LANGUAGES. Mathematical Logic Spatial Logics Model-checking D.2.4 SOFTWARE ENGINEERING. Software/Program Verification Spatial Logics
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.
Metrics
Cited in SectionsSee how this article has been cited at scite.ai
scite shows how a scientific paper has been cited by providing the context of the citation, a classification describing whether it supports, mentions, or contrasts the cited claim, and a label indicating in which section the citation was made.
Back to previous page
@inproceedings{oai:it.cnr:prodotti:359672,
title = {A tool-chain for statistical spatio-temporal model checking of bike sharing systems},
author = {Ciancia V and Latella D and Massink M and Paskauskas R and Vandin A},
doi = {10.1007/978-3-319-47166-2_46},
year = {2016}
}
0000-0003-1314-0574
A Tool-Chain for Statistical Spatio-Temporal Model Checking of Bike Sharing Systems
Analysing Spatial Properties on Neighbourhood Spaces
Statistical Model Checking of Hazards in an Autonomous Tramway Positioning System
Statistical Model Checking of a Moving Block Railway Signalling Scenario with Uppaal SMC
