CNR Author
operator:
and / or
Typology
operator:
and / or
Language
operator:
and / or
Date
operator:
and / or
Rights
operator:
and / or
2014
Other
Restricted
QUANTICOL - Multiscale modelling informed by smart grids
Gast N, Bortolussi L, Jane H, Paskauskas R, Trinabastone M
Multiple scales are inherent to collaborative adaptive systems (CAS). They can be temporal, for example, adjusting the production of a large power plant takes hours while appliances can switched on or of the instant a signal is received. They can also be organizational and represent a hierarchical structure, for example a smart building that contains rooms. Fluid approximations, and in particular mean-field limits, are a powerful tool to conduct a quantitative analysis of large stochastic systems. Yet existing techniques are not well adapted to study multiple-scale behaviour. This deliverable reports on Task 1.1 and 1.2 of Work Package 1. We mainly focus on two aspects: (1) how to define and construct mean-field limits in the presence of multiple scales and (2) what approximations are needed to build efficient control algorithms for smart grids. This deliverable presents results from published papers by the members of the project as well as the relevant literature. Our approach is to develop the theory in a way informed by examples. The results presented in this deliverable are motivated by their applicability to model smart grids and smart buildings. Hence, each section contains at least one concrete example of how the results apply to our case-studies. We rst present a review of model reduction techniques in the presence of multiple time scales. This occurs when the states of some objects evolve at a much faster time scale than others (for example, small electric appliances and big power plants). We compare existing reduction techniques for deterministic dynamical systems, a mature subject, with on-going work on stochastic systems. This review shows that a number of time-scale reduction techniques can be readily applied to mean-field models. It gives us tools to develop the analog for stochastic systems. We then describe the situation when there are multiple population scales. Our basic example is when one centralized controller interacts with many appliances. We show that in such cases, the limit is naturally described by a stochastic hybrid system. We describe how to construct the limit and the limitations of the approach. This technique reduces greatly the complexity of the simulation while maintaining a good accuracy. We develop a novel formalism to describe systems of systems. This can model systems that have a hierarchical organization. This formalism allows us to automatically reduce the complexity of the mean-field equations, by exploiting symmetries in the model. This method can be applied iteratively, to construct hierarchical abstractions of systems. We illustrate our method to describe the behaviour of a collection of smart buildings. In the last section, we demonstrate the use of optimization tools for building control algorithms in electrical systems that have a large production of renewable energy. We model and treat two challenges: large forecast uncertainties and presence of delay due to multiple time scales. We study two directions based on centralized and distributed control. We develop storage and demand/response management policies, where a central controller sends signals to smart users to adapt the consumption to the production. These policies are more robust to forecast errors than existing strategies. To conclude, this work package reports on progress that has been made on the fundamental aspects of multi-scale modeling as well as on advances in the smart-grid case study. This constitutes a rst attempt to build generic tools that will be applicable to the analysis and the optimization of the other case studies. We will continue the development of these generic methods to incorporate spatial behaviour (Work Package 2) and apply these techniques to uid model checking (Work Package 3).Project(s): QUANTICOL
Gast N, Bortolussi L, Jane H, Paskauskas R, Trinabastone M
Multiple scales are inherent to collaborative adaptive systems (CAS). They can be temporal, for example, adjusting the production of a large power plant takes hours while appliances can switched on or of the instant a signal is received. They can also be organizational and represent a hierarchical structure, for example a smart building that contains rooms. Fluid approximations, and in particular mean-field limits, are a powerful tool to conduct a quantitative analysis of large stochastic systems. Yet existing techniques are not well adapted to study multiple-scale behaviour. This deliverable reports on Task 1.1 and 1.2 of Work Package 1. We mainly focus on two aspects: (1) how to define and construct mean-field limits in the presence of multiple scales and (2) what approximations are needed to build efficient control algorithms for smart grids. This deliverable presents results from published papers by the members of the project as well as the relevant literature. Our approach is to develop the theory in a way informed by examples. The results presented in this deliverable are motivated by their applicability to model smart grids and smart buildings. Hence, each section contains at least one concrete example of how the results apply to our case-studies. We rst present a review of model reduction techniques in the presence of multiple time scales. This occurs when the states of some objects evolve at a much faster time scale than others (for example, small electric appliances and big power plants). We compare existing reduction techniques for deterministic dynamical systems, a mature subject, with on-going work on stochastic systems. This review shows that a number of time-scale reduction techniques can be readily applied to mean-field models. It gives us tools to develop the analog for stochastic systems. We then describe the situation when there are multiple population scales. Our basic example is when one centralized controller interacts with many appliances. We show that in such cases, the limit is naturally described by a stochastic hybrid system. We describe how to construct the limit and the limitations of the approach. This technique reduces greatly the complexity of the simulation while maintaining a good accuracy. We develop a novel formalism to describe systems of systems. This can model systems that have a hierarchical organization. This formalism allows us to automatically reduce the complexity of the mean-field equations, by exploiting symmetries in the model. This method can be applied iteratively, to construct hierarchical abstractions of systems. We illustrate our method to describe the behaviour of a collection of smart buildings. In the last section, we demonstrate the use of optimization tools for building control algorithms in electrical systems that have a large production of renewable energy. We model and treat two challenges: large forecast uncertainties and presence of delay due to multiple time scales. We study two directions based on centralized and distributed control. We develop storage and demand/response management policies, where a central controller sends signals to smart users to adapt the consumption to the production. These policies are more robust to forecast errors than existing strategies. To conclude, this work package reports on progress that has been made on the fundamental aspects of multi-scale modeling as well as on advances in the smart-grid case study. This constitutes a rst attempt to build generic tools that will be applicable to the analysis and the optimization of the other case studies. We will continue the development of these generic methods to incorporate spatial behaviour (Work Package 2) and apply these techniques to uid model checking (Work Package 3).Project(s): QUANTICOL
2015
Other
Open Access
Model-based assessment of aspects of user-satisfaction in bicycle sharing systems
Massink M, Paskauskas R
A simulation model for bike-sharing systems is proposed and results of its use are discussed.Project(s): QUANTICOL
Massink M, Paskauskas R
A simulation model for bike-sharing systems is proposed and results of its use are discussed.Project(s): QUANTICOL
See at:
CNR IRIS 
| ISTI Repository | CNR IRIS 
2015
Conference article
Open Access
Exploring spatio-temporal properties of bike-sharing systems
Ciancia V, Latella D, Massink M, Paskauskas R
In this paper we explore the combination of novel spatio-temporal model-checking techniques, and of a recently developed model-based approach to the study of bike sharing systems, in order to detect, visualize and investigate potential problems with bike sharing system configurations. In particular the formation and dynamics of clusters of full stations is explored. Such clusters are likely to be related to the difficulties of users to find suitable parking places for their hired bikes and show up as surprisingly long cycling trips in the trip duration statistics of real bike sharing systems of both small and large cities. Spatio- temporal analysis of the pattern formation may help to explain the phenomenon and possibly lead to alternative bike repositioning strategies aiming at the reduction of the size of such clusters and improving the quality of service.DOI: 10.1109/sasow.2015.17
Project(s): QUANTICOL
Metrics:
Ciancia V, Latella D, Massink M, Paskauskas R
In this paper we explore the combination of novel spatio-temporal model-checking techniques, and of a recently developed model-based approach to the study of bike sharing systems, in order to detect, visualize and investigate potential problems with bike sharing system configurations. In particular the formation and dynamics of clusters of full stations is explored. Such clusters are likely to be related to the difficulties of users to find suitable parking places for their hired bikes and show up as surprisingly long cycling trips in the trip duration statistics of real bike sharing systems of both small and large cities. Spatio- temporal analysis of the pattern formation may help to explain the phenomenon and possibly lead to alternative bike repositioning strategies aiming at the reduction of the size of such clusters and improving the quality of service.DOI: 10.1109/sasow.2015.17
Project(s): QUANTICOL
Metrics:
See at:
CNR IRIS | ieeexplore.ieee.org | ISTI Repository | doi.org | CNR IRIS | CNR IRIS
2016
Conference article
Open Access
A tool-chain for statistical spatio-temporal model checking of bike sharing systems
Ciancia V, Latella D, Massink M, Paskauskas R, Vandin A
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.DOI: 10.1007/978-3-319-47166-2_46
Project(s): QUANTICOL
Metrics:
Ciancia V, Latella D, Massink M, Paskauskas R, Vandin A
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.DOI: 10.1007/978-3-319-47166-2_46
Project(s): QUANTICOL
Metrics:
See at:
CNR IRIS | link.springer.com | ISTI Repository | doi.org | CNR IRIS | CNR IRIS
2016
Other
Open Access
Scalable verification for spatial stochastic logics
Bortolussi L, Ciancia V, Gilmore S, Hillston J, Latella D, Loreti M, Massink M, Nenzi L, Paskauskas R, Tribastone M, Tschaikowski M
This Internal Report describes the status of the work performed in the project on the extension of the theoretical foundations of scalable model-checking approaches with suitable notions of spatial verification. Various forms of scalable model-checking were developed during the first phase of Task 3.1 of WP3, including those based on mean-field and fluid flow techniques, and were presented in Deliverable 3.1. The focus of the present report is on forms of spatial verification based on model-checking techniques in which the effect of inhomogeneous spatial distribution of objects is taken into account. Several spatial logics have been developed and explored. The Spatial Logic for Closure Spaces (SLCS) is based on the formal framework of closure spaces. The latter include topological spaces but also discrete spaces such as graphs and therefore form a promising candidate for a uniform framework to develop spatial logics that can be applied to the various spatial representations presented in the deliverables of WP2. Closure spaces come with a well-developed theory and some powerful operators that turned out to be very useful both for the definition of the semantics of SLCS and for the development of spatial and spatio-temporal modelchecking algorithms. The spatial operators of SLCS have been also added to the Signal Temporal Logic (STL) to obtain Spatial Signal Temporal Logic (SSTL). In this case the spatial operators have been extended with spatial bounds based on distance measures and a quantitative semantics has been provided that is used to evaluate the robustness of the spatio-temporal formulas for signals. Spatial and spatio-temporal performance analysis measures have been explored for a simple PALOMA model of a group of robots and for a bike sharing model based on Markov Renewal Processes. The latter provides a simulation model of bike-sharing systems that includes users as agents. It also generates simulation traces with spatio-temporal information on bike stations that can be analysed using the prototype spatiotemporal model checkers that have been developed in the context of the project. A partial-differential approximation has been developed for spatial stochastic process algebra. The approach is validated on the well-known Lotka-Volterra model and shows an advantage in terms of computational efficiency compared to traditional numerical solutions. Finally, for what concerns scalable verification, the innovative model-checking approaches based on fluid approximation and on-the-fly mean-field techniques have been finalised. For the latter a prototype modelchecker, FlyFast, has been made available, which was described in Deliverable 5.2. QUANTICOLProject(s): QUANTICOL
Bortolussi L, Ciancia V, Gilmore S, Hillston J, Latella D, Loreti M, Massink M, Nenzi L, Paskauskas R, Tribastone M, Tschaikowski M
This Internal Report describes the status of the work performed in the project on the extension of the theoretical foundations of scalable model-checking approaches with suitable notions of spatial verification. Various forms of scalable model-checking were developed during the first phase of Task 3.1 of WP3, including those based on mean-field and fluid flow techniques, and were presented in Deliverable 3.1. The focus of the present report is on forms of spatial verification based on model-checking techniques in which the effect of inhomogeneous spatial distribution of objects is taken into account. Several spatial logics have been developed and explored. The Spatial Logic for Closure Spaces (SLCS) is based on the formal framework of closure spaces. The latter include topological spaces but also discrete spaces such as graphs and therefore form a promising candidate for a uniform framework to develop spatial logics that can be applied to the various spatial representations presented in the deliverables of WP2. Closure spaces come with a well-developed theory and some powerful operators that turned out to be very useful both for the definition of the semantics of SLCS and for the development of spatial and spatio-temporal modelchecking algorithms. The spatial operators of SLCS have been also added to the Signal Temporal Logic (STL) to obtain Spatial Signal Temporal Logic (SSTL). In this case the spatial operators have been extended with spatial bounds based on distance measures and a quantitative semantics has been provided that is used to evaluate the robustness of the spatio-temporal formulas for signals. Spatial and spatio-temporal performance analysis measures have been explored for a simple PALOMA model of a group of robots and for a bike sharing model based on Markov Renewal Processes. The latter provides a simulation model of bike-sharing systems that includes users as agents. It also generates simulation traces with spatio-temporal information on bike stations that can be analysed using the prototype spatiotemporal model checkers that have been developed in the context of the project. A partial-differential approximation has been developed for spatial stochastic process algebra. The approach is validated on the well-known Lotka-Volterra model and shows an advantage in terms of computational efficiency compared to traditional numerical solutions. Finally, for what concerns scalable verification, the innovative model-checking approaches based on fluid approximation and on-the-fly mean-field techniques have been finalised. For the latter a prototype modelchecker, FlyFast, has been made available, which was described in Deliverable 5.2. QUANTICOLProject(s): QUANTICOL
See at:
CNR IRIS | ISTI Repository | CNR IRIS