Glioblastomas are among the most common malignant intracranial tumours. Neuroimaging protocols are used before and after treatment to evaluate its effect and to monitor the evolution of the disease. In clinical studies and routine treatment, magnetic resonance images (MRI) are evaluated, largely manually, and based on qualitative criteria such as the presence of hyper-intense tissue in the image. VoxLogicA is an image analysis tool, designed to perform tasks such as identifying brain tumours in 3D magneto-resonance scans. The aim is to have a system that is portable, predictable and reproducible, and requires minimal computing expertise to operate.

In spatially located, large scale systems, time and space dynamics interact and drives the behaviour. Examples of such systems can be found in many smart city applications and Cyber-Physical Systems. In this paper we present the Signal Spatio-Temporal Logic (SSTL), a modal logic that can be used to specify spatio-temporal properties of linear time and discrete space models. The logic is equipped with a Boolean and a quantitative semantics for which ecient monitoring algorithms have been developed. As such, it is suitable for real-time verication of both white box and black box complex systems. These algorithms can also be combined with stochastic model checking routines. SSTL combines the until temporal modality with two spatial modalities, one expressing that something is true somewhere nearby and the other capturing the notion of being surrounded by a region that satises a given spatio-temporal property. The monitoring algorithms are implemented in an open source Java tool. We illustrate the use of SSTL analysing the formation of patterns in a Turing Reaction-Diusion system and spatio-temporal aspects of a large bike-sharing system.

This paper presents our approach to the quantitative modeling and analysis of highly (re)configurable systems, like software product lines. Different combinations of the optional features of such systems give rise to combinatorially many individual system variants. We use a formal modeling language that allows us to model systems with probabilistic behavior, possibly subject to quantitative feature constraints, and able to dynamically install, remove or replace features. Our models are defined in the probabilistic feature-oriented language QFLan, a rich domain specific language (DSL) for systems with variability defined in terms of features. QFLan specifications are automatically encoded in terms of a process algebra whose operational behavior interacts with a store of constraints and with a semantics based on discrete-time Markov chains. Our analysis is based on statistical model checking, which allow us to scale to larger models with respect to precise probabilistic techniques. The analyses we can conduct range from the likelihood of specific behavior to the expected average cost of specific system variants. Our approach is supported by a novel Eclipse-based tool including state-of-the-art DSL utilities for QFLan as well as analysis plug-ins. We provide a number of case studies that have driven and validated the development of our framework.

We present the use of a novel spatio-temporal model checker to detect problems in the data and operation of a collective adaptive system. Data correctness is important to ensure operational correctness in systems which adapt in response to data. We illustrate the theory with several concrete examples, addressing both the detection of errors in vehicle location data for buses in the city of Edinburgh and the undesirable phenomenon of ``clumping'' which occurs when there is not enough separation between subsequent buses serving the same route. Vehicle location data are visualised symbolically on a street map, and categories of problems identified by the spatial part of the model checker are rendered by highlighting the symbols for vehicles or other objects that satisfy a property of interest. Behavioural correctness makes use of both the spatial and temporal aspects of the model checker to determine from a series of observations of vehicle locations whether the system is failing to meet the expected quality of service demanded by system regulators.

This deliverable is an account of the QUANTICOL software tool suite, with application to the smart city scenarios studied in the project. While Deliverable D4.3 focuses on the CARMA language and its implementation with the CARMA Eclipse plug-in, in this deliverable we present software tools developed to support further techniques such as model checking, model order reduction, and reachability analysis. Their integration with the CARMA Eclipse plug-in is discussed in Deliverable D4.3. Instead, here we provide detailed account of such tools as stand-alone products. We present FlyFast, a probabilistic model checker for mean-field models; jSSTL, for the analysis of Signal Spatio-Temporal Logic; ERODE, for the reduction of systems of ordinary differential equations; UTOPIC, for the reachability analysis of nonlinear dynamical systems; and topochecker, a spatio-temporal model checker. While an application of FlyFast to smart cities is presented in D4.3, in this deliverable we discuss an application of jSSTL and ERODE to the verification and reduction, respectively, of a model of a bike-sharing system. Instead, bus transportation systems are studied with topochecker, to detect problems in vehicle location data and clumping in frequent services.

Model-checking is an effective formal verification technique that has also been extended to quantitative logics and models such as PCTL and DTMCs as well as CSL and CTMCs/CTMDPs. Unfortunately, the state-space explosion problem of classical model-checking algorithms affects also quantitative extensions. Mean-field techniques provide approximations of the mean behaviour of large population models. These approximations are deterministic: a unique value of the fractions of agents in each state is computed for each time instant. A drastic reduction of the size of the model is obtained enabling the definition of an efficient model-checking algorithm. This paper is a survey of work we have done in the last few years in the area of mean-field approximated probabilistic model-checking. We start with a brief description of FlyFast, an on-the-fly model checker we have developed for approximated bounded PCTL model-checking, based on mean-field population DTMC approximation. Then we show an example of use of FlyFast in the context of Collective Adaptive Systems. We also discuss two additional interesting front-ends for FlyFast; the first one is a translation from CTMC-based population models and (a fragment of) CSL that allows for approximate probabilistic model-checking in the continuous stochastic time setting; the second one is a translation from a predicate-based process interaction language that allows for probabilistic model-checking of models based on components equipped both with behaviour and with attributes, on which predicates are defined that can be used in component interaction primitives.

Collective Adaptive Systems (CAS) consist of a large number of interacting objects. The design of such systems requires scalable analysis tools and methods, which have necessarily to rely on some form of approximation of the system's actual behaviour. Promising techniques are those based on mean-field approximation. The FlyFast model-checker uses an on-the-fly algorithm for bounded PCTL model-checking of selected individual(s) in the context of very large populations whose global behaviour is approximated using deterministic limit mean-field techniques. Recently, a front-end for FlyFast has been proposed which provides a modelling language, PiFF in the sequel, for the Predicate-based Interaction for FlyFast. In this paper we present details of PiFF design and an approach to state-space reduction based on probabilistic bisimulation for inhomogeneous DTMCs.

The application of the topochecker spatial-model-cheker to medical imaging is described.

This final Deliverable of Work Package 3 describes the main achievements obtained during the last reporting period for all three tasks of the work package (and in part during the second reporting period regarding Task 1.3) concerning the development of the theoretical foundations of novel, scalable and spatial formal analysis tech- niques and the underlying theories to support the design of large scale CAS. During the first two reporting periods of the project a number of innovative analysis techniques have been developed that are highly scalable. Some of these are based on mean field approximation techniques, others involve statistical model checking and machine learning techniques. For all these cases additional model reduction techniques have been developed to further improve scalability of analysis, for example to reduce the number of ordinary differential equations (ODEs) that need to be solved or the number of populations that need to be considered. For what concerns spatial verification several spatial and spatio-temporal logics have been developed for which efficient verifica- tion techniques have been created based on model checking and monitoring techniques. In particular, Spatial Logic for Closure Spaces (SLCS), based on the formal framework of closure spaces, and Spatial Signal Tem- poral Logic (SSTL) extending Signal Temporal Logic (STL) with some of the spatial operators from SLCS in a monitoring setting. Finally, suitable extensions of a software product line engineering (SPLE) approach for CAS were developed, among which family-based verification of behavioural aspects of CAS. In the third and final reporting period all these techniques have been further extended and some combined, implemented and applied to the case studies of the project. Some of the main achievements are: the extension of the fluid model checking algorithms incorporating various kinds of rewards (or costs); study of the condi- tions under which continuous time population models can be analysed based on discrete time mean field model checking techniques; approximation of probabilistic reachability; development of a front-end language for Fly- Fast to deal with components and predicate-based interaction; extension of SLCS with temporal operators and with collective operators; combination of statistical and spatio-temporal model checking; application of an extended version of SLCS on Medical Imaging; combination of SSTL with machine learning; development of CTMC and ODE based behavioural equivalences for CAS and related minimisation algorithms; definition of an efficient family-based model checking procedure for SPLE models; development of a tool for quanti- tative analysis of probabilistic and dynamically reconfigurable SPLE models via statistical model checking; variability-aware software performance models. All these developments are briefly described in the three main sections of this deliverable reflecting the three tasks of Work Package 3.

This deliverable reports on the work completed in the final reporting period on the modelling language at the centre of the QUANTICOL framework, C ARMA . A major focus of the period has been on making modelling with C ARMA accessible to a wide audience of potential users interested in CAS, not just those already familiar with formal modelling with process algebras. To this end we have further developed the C ARMA Specification Language ( CaSL ) and the software tools that support it; we have developed exemplar models, some of which are reported in this deliverable, and extended the suite of tools to offer a modeller different approaches to model analysis. In essence, the CaSL language does not formally extend the expressiveness of C ARMA , but it presents a more programmatic style of modelling, which will be usable by a wider set of people. Space plays a key role in many CAS and we have revisited the support that is offered to faithfully capture the spatial aspects within a model, resulting in improved syntax to assist the modeller and a graphical front end which can be used to automatically generate the spatial aspects of models. In this document we give an account of the key features of CaSL , and present a full account of the language in an appendix. We also discuss a few of the models that have been developed alongside the language development. These served to refine our ideas on how best to support spatial modelling as well as testing the implementation in the Eclipse plug-in supporting CaSL . One of this set of models is completely outside the domain of smart cities, which has been the main focus of our case studies, in order to demonstrate that the modelling pathway that we have developed could be suitable for a wide class of applications beyond smart cities. Of course, to be practically useful a modelling language must be implemented in a robust set of software tools to allow the modeller to construct and analyse the model with confidence. In Section 3 we give an account of the software tools, whilst in Section 4 we describe the design workflow and analysis pathway that is supported in the tools. This takes into account the different phases that a model goes through, from initial design, elaboration, parameterisation and then use as a tool to investigate the behaviour of the system under study. The modeller needs different support at each of these stages and we have sought to provide what is appropriate for each stage, as far as is feasible within the limited time and resource of the project. Building within Eclipse has allowed us to provide many "hidden" features which nevertheless greatly enhance the support for the modeller. These internal checks seek to ensure that CaSL models are free from the type of minor error that can be frustrating and time-consuming during model development. However, once a modeller is fully confident of their model, a graphical user interface can become cumbersome and inconvenient. Thus we also provide a command line interface to support efficient exploitation of models under different experimental frames. Moreover, the results of model analysis are automatically enhanced with metadata to assist with their interpretation and reproducibility. The deliverable concludes with a demonstration of the analysis of CaSL models on two of the scenarios from our smart city case studies. Specifically we consider a mesoscale model of buses within a city, particularly paying attention to the congestion that occurs when multiple routes share the same bus stopes, and issues related to regulatory compliance and appropriate spacing on frequent bus services. In the second example, we consider the key issue related to user satisfaction within urban bike sharing systems - whether a user will find a bike or a slot at a convenient location when they want one. In addition to this document, we also deliver the software tool suite for C ARMA which is available at https://quanticol.github.io

This deliverable is an account of the QUANTICOL software tool suite, with application to the smart city scenarios studied in the project. While Deliverable D4.3 focuses on the CARMA language and its implementation with the CARMA Eclipse plug-in, in this deliverable we present software tools developed to support further techniques such as model checking, model order reduction, and reachability analysis. Their integration with the CARMA Eclipse plug-in is discussed in Deliverable D4.3. Instead, here we provide detailed account of such tools as stand-alone products. We present FlyFast, a probabilistic model checker for mean-field models; jSSTL, for the analysis of Signal Spatio-Temporal Logic; ERODE, for the reduction of systems of ordinary differential equations; UTOPIC, for the reachability analysis of nonlinear dynamical systems; and topochecker, a spatio-temporal model checker. While an application of FlyFast to smart cities is presented in D4.3, in this deliverable we discuss an application of jSSTL and ERODE to the verification and reduction, respectively, of a model of a bike-sharing system. Instead, bus transportation systems are studied with topochecker, to detect problems in vehicle location data and clumping in frequent services.

he emerging field of Nominal Computation Theory is concerned with the theory of Nominal Sets and its applications to Computer Science. We investigate here the impact of nominal sets on the definition of Cellular Automata and on their computational capabilities, with a special focus on the emergent behavioural properties of this new model and their significance in the context of computation-oriented interpretations of physical phenomena. An investigation of the relations between Nominal Cellular Automata and Wolfram's Elementary Cellular Automata is carried out, together with an analysis of interesting particles, exhibiting "nominal" behaviour, in a particular kind of rules, reminiscent of the class of totalistic Cellular Automata, that we call "bagged".

Collective Adaptive Systems (CAS) consist of a large number of interacting objects. The design of such systems requires scalable analysis tools and methods, which have necessarily to rely on some form of approximation of the system's actual behaviour. Promising techniques are those based on mean-field approximation. The FlyFast model-checker uses an on-The-fly algorithm for bounded PCTL model-checking of selected individual(s) in the context of very large populations whose global behaviour is approximated using deterministic limit mean-field techniques. Recently, a front-end for FlyFast has been proposed which provides a modelling language, PiFF in the sequel, for the Predicate-based Interaction for FlyFast. In this paper we present details of PiFF design and an approach to state-space reduction based on probabilistic bisimulation for inhomogeneous DTMCs.

Preface

This final Deliverable of Work Package 3 describes the main achievements obtained during the last reporting period for all three tasks of the work package (and in part during the second reporting period regarding Task 1.3) concerning the development of the theoretical foundations of novel, scalable and spatial formal analysis techniques and the underlying theories to support the design of large scale CAS. During the first two reporting periods of the project a number of innovative analysis techniques have been developed that are highly scalable. Some of these are based on mean field approximation techniques, others involve statistical model checking and machine learning techniques. For all these cases additional model reduction techniques have been developed to further improve scalability of analysis, for example to reduce the number of ordinary differential equations (ODEs) that need to be solved or the number of populations that need to be considered. For what concerns spatial verification several spatial and spatio-temporal logics have been developed for which efficient verification techniques have been created based on model checking and monitoring techniques. In particular, Spatial Logic for Closure Spaces (SLCS), based on the formal framework of closure spaces, and Spatial Signal Temporal Logic (SSTL) extending Signal Temporal Logic (STL) with some of the spatial operators from SLCS in a monitoring setting. Finally, suitable extensions of a software product line engineering (SPLE) approach for CAS were developed, among which family-based verification of behavioural aspects of CAS. In the third and final reporting period all these techniques have been further extended and some combined, implemented and applied to the case studies of the project. Some of the main achievements are: the extension of the fluid model checking algorithms incorporating various kinds of rewards (or costs); study of the conditions under which continuous time population models can be analysed based on discrete time mean field model checking techniques; approximation of probabilistic reachability; development of a front-end language for FlyFast to deal with components and predicate-based interaction; extension of SLCS with temporal operators and with collective operators; combination of statistical and spatio-temporal model checking; application of an extended version of SLCS on Medical Imaging; combination of SSTL with machine learning; development of CTMC and ODE based behavioural equivalences for CAS and related minimisation algorithms; definition of an efficient family-based model checking procedure for SPLE models; development of a tool for quantitative analysis of probabilistic and dynamically reconfigurable SPLE models via statistical model checking; variability-aware software performance models. All these developments are briefly described in the three main sections of this deliverable reflecting the three tasks of Work Package 3.

We present FlyFast, a recently introduced on-the-fly mean field model checker for the verification of time-dependent probabilistic properties of individual objects in the context of large populations. An example of its use is illustrated analysing a push-pull gossip protocol. Such protocols form the basis on top of which many smart collective adaptive systems are built. Typical properties are the replication of a fresh data element throughout a network, the coverage of the network, and the time to convergence.

Family-based model checking targets the simultaneous verification of multiple system variants, a technique to handle feature-based variability that is intrinsic to software product lines (SPLs). We present an approach for family-based verification based on the feature mu-calculus mu-Lf, which combines modalities with feature expressions. This logic is interpreted over featured transition systems, a well-accepted model of SPLs, which allows one to reason over the collective behavior of a number of variants (a family of products). Via an embedding into the modal mu-calculus with data, underpinned by the general-purpose mCRL2 toolset, off-the-shelf tool support for mu-Lf becomes readily available. We illustrate the feasibility of our approach on an SPL benchmark model and show the runtime improvement that family-based model checking with mCRL2 offers with respect to model checking the benchmark product-by-product.

Collective Adaptive Systems (CAS) consist of a large number of interacting objects. The design of such systems requires scalable analysis tools and methods, which have necessarily to rely on some form of approximation of the system's actual behaviour. Promising techniques are those based on mean-field approximation. The FlyFast model-checker uses an on-the- y algorithm for bounded PCTL model-checking of selected individual(s) in the context of very large populations whose global behaviour is approximated using deterministic limit mean-field techniques. Recently, a front-end for FlyFast has been proposed which provides a modelling language, PiFF in the sequel, for the Predicate-based Interaction for FlyFast. In this paper we present details of PiFF design and an approach to state-space reduction based on probabilistic bisimulation for inhomogeneous DTMCs.

Continuous-time Markov decision processes are an important class of models in a wide range of applications, ranging from cyberphysical systems to synthetic biology. A central problem is how to devise a policy to control the system in order to maximise the probability of satisfying a set of temporal logic specifications. Here we present a novel approach based on statistical model checking and an unbiased estimation of a functional gradient in the space of possible policies. The statistical approach has several advantages over conventional approaches based on uniformisation, as it can also be applied when the model is replaced by a black box, and does not suffer from state-space explosion. The use of a stochastic gradient to guide our search considerably improves the efficiency of learning policies. We demonstrate the method on a proof-ofprinciple non-linear population model, showing strong performance in a non-trivial task.

We study the limiting behaviour of stochastic models of populations of interacting agents, as the number of agents goes to infinity. Classical mean-field results have established that this limiting behaviour is described by an ordinary differential equation (ODE) under two conditions: (1) that the dynamics is smooth; and (2) that the population is composed of a finite number of homogeneous sub-populations, each containing a large number of agents. This paper reviews recent work showing what happens if these conditions do not hold. In these cases, it is still possible to exhibit a limiting regime at the price of replacing the ODE by a more complex dynamical system. In the case of non-smooth or uncertain dynamics, the limiting regime is given by a differential inclusion. In the case of multiple population scales, the ODE is replaced by a stochastic hybrid automaton.