A tool-chain for statistical spatio-temporal model checking of bike sharing systems

Vincenzo Ciancia; Diego Latella; Mieke Massink; Rytis Paškauskas; Andrea Vandin

doi:10.1007/978-3-319-47166-2_46

A tool-chain for statistical spatio-temporal model checking of bike sharing systems

Vincenzo Ciancia^*
, Diego Latella
, Mieke Massink
, Rytis Paškauskas
, Andrea Vandin

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

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.

Original language	English
Title of host publication	Leveraging Applications of Formal Methods, Verification and Validation : Foundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings
Number of pages	17
Volume	9952 LNCS
Publisher	Springer Verlag
Publication date	2016
Pages	657-673
ISBN (Print)	9783319471655
DOIs	https://doi.org/10.1007/978-3-319-47166-2_46
Publication status	Published - 2016
Externally published	Yes
Event	7^th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation - Corfu, Greece Duration: 10 Oct 2016 → 14 Oct 2016 Conference number: 7

Conference

Conference	7^th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation
Number	7
Country/Territory	Greece
City	Corfu
Period	10/10/2016 → 14/10/2016

Series	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9952 LNCS
ISSN	0302-9743

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

SDG 11 Sustainable Cities and Communities

Keywords

Collective adaptive systems
MultiVeStA
Spatio-temporal model checking
Statistical model checking

Access to Document

10.1007/978-3-319-47166-2_46

OpenUrl availability

Full text

Cite this

Ciancia, V., Latella, D., Massink, M., Paškauskas, R., & Vandin, A. (2016). A tool-chain for statistical spatio-temporal model checking of bike sharing systems. In Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings (Vol. 9952 LNCS, pp. 657-673). Springer Verlag. https://doi.org/10.1007/978-3-319-47166-2_46

Ciancia, Vincenzo ; Latella, Diego ; Massink, Mieke et al. / A tool-chain for statistical spatio-temporal model checking of bike sharing systems. Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings. Vol. 9952 LNCS Springer Verlag, 2016. pp. 657-673 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 9952 LNCS).

@inproceedings{32af2094bfe345e5a124800446e2f84d,

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.",

keywords = "Collective adaptive systems, MultiVeStA, Spatio-temporal model checking, Statistical model checking",

author = "Vincenzo Ciancia and Diego Latella and Mieke Massink and Rytis Pa{\v s}kauskas and Andrea Vandin",

year = "2016",

doi = "10.1007/978-3-319-47166-2\_46",

language = "English",

isbn = "9783319471655",

volume = "9952 LNCS",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "657--673",

booktitle = "Leveraging Applications of Formal Methods, Verification and Validation",

address = "Germany",

note = "7<sup>th</sup> International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016 ; Conference date: 10-10-2016 Through 14-10-2016",

}

Ciancia, V, Latella, D, Massink, M, Paškauskas, R & Vandin, A 2016, A tool-chain for statistical spatio-temporal model checking of bike sharing systems. in Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings. vol. 9952 LNCS, Springer Verlag, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9952 LNCS, pp. 657-673, 7^th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, Corfu, Greece, 10/10/2016. https://doi.org/10.1007/978-3-319-47166-2_46

A tool-chain for statistical spatio-temporal model checking of bike sharing systems. / Ciancia, Vincenzo; Latella, Diego; Massink, Mieke et al.
Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings. Vol. 9952 LNCS Springer Verlag, 2016. p. 657-673 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 9952 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - A tool-chain for statistical spatio-temporal model checking of bike sharing systems

AU - Ciancia, Vincenzo

AU - Latella, Diego

AU - Massink, Mieke

AU - Paškauskas, Rytis

AU - Vandin, Andrea

N1 - Conference code: 7

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

KW - Collective adaptive systems

KW - MultiVeStA

KW - Spatio-temporal model checking

KW - Statistical model checking

U2 - 10.1007/978-3-319-47166-2_46

DO - 10.1007/978-3-319-47166-2_46

M3 - Article in proceedings

AN - SCOPUS:84993950068

SN - 9783319471655

VL - 9952 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 657

EP - 673

BT - Leveraging Applications of Formal Methods, Verification and Validation

PB - Springer Verlag

T2 - 7<sup>th</sup> International Symposium on Leveraging Applications of Formal Methods, Verification and Validation

Y2 - 10 October 2016 through 14 October 2016

ER -

Ciancia V, Latella D, Massink M, Paškauskas R, Vandin A. A tool-chain for statistical spatio-temporal model checking of bike sharing systems. In Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Proceedings. Vol. 9952 LNCS. Springer Verlag. 2016. p. 657-673. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 9952 LNCS). doi: 10.1007/978-3-319-47166-2_46

A tool-chain for statistical spatio-temporal model checking of bike sharing systems

Abstract

Conference

UN SDGs

Keywords

Access to Document

OpenUrl availability

Fingerprint

Cite this