Title
A Tool-Chain for Statistical Spatio-Temporal Model Checking of Bike Sharing Systems.
Abstract
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.
Year
DOI
Venue
2016
10.1007/978-3-319-47166-2_46
Lecture Notes in Computer Science
Keywords
Field
DocType
Collective adaptive systems,Spatio-temporal model checking,Statistical model checking,MultiVeStA
Model checking,Computer science,Markov chain,Statistical model checking,Smart transportation,Collective adaptive systems,Statistical analysis,Distributed computing
Conference
Volume
ISSN
Citations 
9952
0302-9743
8
PageRank 
References 
Authors
0.47
20
5
Name
Order
Citations
PageRank
Vincenzo Ciancia19610.80
Diego Latella21168113.42
Mieke Massink3109587.58
Rytis Paskauskas490.84
Andrea Vandin520121.36