Automating Reasoning About Large (Collective Adaptive) Systems and Space
- Day - Time: 18 November 2016, h.10:30
- Place: Area della Ricerca CNR di Pisa - Room: C-29
Speakers
Referent
Abstract
Collective Adaptive System (CAS) are often composed of very large numbers of relatively simple agents, so that modelling these systems, analysing them or rigorously reasoning about them faces serious scalability issues. Another feature of CAS is their spatial distribution; formal and automated reasoning about space and spatial properties is a challenge per se in the area of logics and related verification techniques, e.g. model-checking. In this talk two examples of useful analysis techniques based on solid mathematical theories are discussed as well as the software tools which have been built for supporting such techniques. The first technique is Scalable Approximated Population DTMC Model-checking. The second one is Spatial Model-checking for Closure Spaces. Both techniques have been developed in the context of the EU funded project QUANTICOL.