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 Ciancia | 1 | 96 | 10.80 |
Diego Latella | 2 | 1168 | 113.42 |
Mieke Massink | 3 | 1095 | 87.58 |
Rytis Paskauskas | 4 | 9 | 0.84 |
Andrea Vandin | 5 | 201 | 21.36 |