Lanciani, Roberta (2017) Stochastic Approximations in Model Checking: A New Scalable Approach to Collective Systems Verification. Advisor: De Nicola, Prof. Rocco. Coadvisor: Bortolussi, Prof. Luca . pp. 123. [IMT PhD Thesis]
|
Text
Lanciani_phdthesis.pdf - Published Version Available under License Creative Commons Attribution No Derivatives. Download (2MB) | Preview |
Abstract
A collective system is a complex model comprised of a large number of individual entities, whose interaction gives rise to non-trivial emergent behaviours. The automatic verification of the intrinsically noisy dynamics of this type of models, by means of Stochastic Model Checking techniques, is severely hampered by the large size of their state space. In this project, we consider a new scalable and effective technique to validate the performance of these systems, based on Stochastic Approximations of the dynamics of the model. In this context, this works merges and extends the few preliminary results available in the literature at the beginning of this project and defines some interesting contributions leading the investigation in two major directions. First, we consider various types of Stochastic Approximations to accurately capture the probabilistic noise that characterises the evolution of collective systems when the number of individuals in the population is limited (mesoscopic collective systems). Second, we extend the set of properties that can be validated exploiting the efficiency of Stochastic Approximations. In particular, we consider requirements on the behaviour of the individuals (local properties), of the population (global properties) and of the individuals in the global context (local-to-global properties). Moreover, we develop procedures to verify the dynamics of time-critical systems. Finally, we prove the theoretical results that guarantee the quality of the developed model checking procedures, showing the asymptotic convergence of the results and the exactness in the limit of an infinite population size.
| Item Type: | IMT PhD Thesis |
|---|---|
| Subjects: | Q Science > QA Mathematics > QA75 Electronic computers. Computer science |
| PhD Course: | Computer Decision and System Science |
| Identification Number: | https://doi.org/10.6092/imtlucca/e-theses/224 |
| NBN Number: | urn:nbn:it:imtlucca-27251 |
| Date Deposited: | 08 Aug 2017 10:49 |
| URI: | http://e-theses.imtlucca.it/id/eprint/224 |
Actions (login required, only for staff repository)
 |
View Item |
