Search

Deliverable D3.2.1 del progetto PNRR Ecosistemi ed innovazione - THE

The notion of bisimilarity plays an important role in concurrency theory. It provides formal support to the idea of processes having "equivalent behaviour" and is a powerful tool for model reduction. Furthermore, bisimilarity typically coincides with logical equivalence of an appropriate modal logic enabling model checking to be applied on reduced models. Recently, notions of bisimilarity have been proposed also for models of space, including those based on polyhedra. The latter are central in many domains of application that exploit mesh processing and typically consist of millions of cells, the basic components of face-poset models, discrete representations of polyhedral models. This paper builds on the polyhedral semantics of the Spatial Logic for Closure Spaces (SLCS) for which the geometric spatial model checker PolyLogicA has been de- veloped, that is based on face-poset models. We propose a novel notion of spatial bisimilarity, called plus-minus-bisimilarity, for face-poset models. We show that it coincides with logical equivalence induced by SLCS on such models. The latter corresponds to logical equivalence (based on SLCS) on polyhedra which, in turn, coincides with simplicial bisimilarity, a notion of bisimilarity for continuous spaces.

The notion of bisimilarity plays an important role in con- currency theory. It provides formal support to the idea of processes hav- ing "equivalent behaviour" and is a powerful tool for model reduction. Furthermore, bisimilarity typically coincides with logical equivalence of an appropriate modal logic enabling model checking to be applied on reduced models. Recently, notions of bisimilarity have been proposed also for models of space, including those based on polyhedra. The latter are central in many domains of application that exploit mesh processing and typically consist of millions of cells, the basic components of face- poset models, discrete representations of polyhedral models. This paper builds on the polyhedral semantics of the Spatial Logic for Closure Spaces (SLCS) for which the geometric spatial model checker PolyLogicA has been developed, that is based on face-poset models. We propose a novel notion of spatial bisimilarity for face-poset models, called ±-bisimilarity. We show that it coincides with logical equivalence induced by SLCS on such models. The latter corresponds to logical equivalence with respect to SLCS on polyhedra which, in turn, coincides with simplicial bisimilarity, a notion of bisimilarity for continuous spaces.

Spatial logic and spatial model checking have great poten- tial for traditional computer science domains and beyond. Reasoning about space involves two different conditional reachability modalities: a forward reachability, similar to that used in temporal logic, and a backward modality representing that a point can be reached from an- other point, under certain conditions. Since spatial models can be huge, suitable model minimisation techniques are crucial for efficient model checking. An effective minimisation method for the recent notion of spatial Compatible Path (CoPa)-bisimilarity is proposed, and shown to be correct. The core of our method is the encoding of Closure Models as La- belled Transition Systems, enabling minimisation algorithms for branching bisimulation to compute CoPa equivalence classes. Initial validation via benchmark examples demonstrates a promising speed-up in model checking of spatial properties for models of realistic size. Detailed proofs of all results are provided.

We adapt the standard notion of bisimilarity for topological models to closure models and refine it for quasi-discrete closure models. We also define an additional, weaker notion of bisimilarity that is based on paths in space and expresses a form of conditional reachability in a way that is reminiscent of Stuttering Equivalence on transition systems. For each bisimilarity we provide a characterisation with respect to a suitable spatial logic. In this report, the detailed proofs of all the results we present are also included.

In these notes we prove that, in quasi-discrete closure models, the ISLCS forward (backword) conditional reachability operator can be expressed using a (possibly) infinite disjunction of nested formulas using only conjunction and the IMLC backward (forward) proximity operator.

Revised Selected Papers of FSEN 2021

Topological Spatial Model Checking is a recent paradigm that combines Model Checking with the topological interpretation of Modal Logic. The Spatial Logic of Closure Spaces, SLCS, extends Modal Logic with reachability connectives that, in turn, can be used for expressing interesting spatial properties, such as "being near to" or "being surrounded by". SLCS constitutes the kernel of a solid logical framework for reasoning about discrete space, such as graphs and digital images, interpreted as quasi discrete closure spaces. In particular, the spatial model checker VoxLogicA, that uses an extended version of SLCS, has been used successfully in the domain of medical imaging. However, SLCS is not restricted to discrete space. Following a recently developed geometric semantics of Modal Logic, we show that it is possible to assign an interpretation to SLCS in continuous space, admitting a model checking procedure, by resorting to models based on polyhedra. In medical imaging such representations of space are increasingly relevant, due to recent developments of 3D scanning and visualisation techniques that exploit mesh processing. We demonstrate feasibility of our approach via a new tool, PolyLogicA, aimed at ecient verication of SLCS formulas on polyhedra, while inheriting some well-established optimization techniques already adopted in VoxLogicA. Finally, we cater for a geometric definition of bisimilarity, proving that it characterises logical equivalence.

This volume contains the selected and revised versions of papers that have been presented at three international workshops co-located with the 18th edition of the International Conference on Software Engineering and Formal Methods (SEFM 2020). Because of the COVID-19 pandemic, both the conference and the workshops were held virtually. They were hosted by the Centre for Mathematics and Informatics (CWI) in Amsterdam, The Netherlands, and took place on September 14- 17, 2020. The SEFM 2020 international conference offered a virtual interactive platform for leading researchers and practitioners from academia, industry, and government to advance the state of the art in formal methods, to facilitate their uptake in the software industry, and to encourage their integration within practical software engineering methods and tools.

Closure spaces are a generalisation of topological spaces obtained by removing the idempotence requirement on the closure operator. We adapt the standard notion of bisimilarity for topological models, namely Topo-bisimilarity, to closure models|we call the resulting equivalence CM-bisimilarity|and rene it for quasi-discrete closure models. We also dene two additional notions of bisimilarity that are based on paths on space, namely Path-bisimilarity and Compatible Path-bisimilarity, CoPa-bisimilarity for short. The former expresses (unconditional) reachability, the latter renes it in a way that is reminishent of Stuttering Equivalence on transition systems. For each bisimilarity we provide a logical characterisation, using variants of SLCS.We also address the issue of (space) minimisation via the three equivalences.

Preface to the proceedings of FSEN 2021

This paper provides a tutorial-style introduction, and a guide, to the recent advancements in spatial model checking that have made some relevant results possible. Among these, we mention fully automated segmentation of regions of interest in medical images by short, unambiguous spatial-logical specifications. This tutorial is aimed both at domain experts in medical imaging who would like to learn simple (scripting-alike) techniques for image analysis, making use of a modern, declarative language, and at experts in Formal Methods in Computer Science and Model Checking who would like to grasp how the theory of Spatial Logic and Model Checking has been turned into logic-based, dataset-oriented imaging techniques.

Logic based (semi-)automatic contouring in Medical Imaging has shown to be a very promising and versatile technique that can potentially greatly facilitate the work of different professionals in this domain while supporting explainability, easy replicability and exchange of medical image analysis methods. In such a context there is a clear need of a prototype Graphical User Interface (GUI) support for professionals which is usable, understandable and which reduces unnecessary cognitive load to the minimum, so that the focus of attention can remain on the main, critical, tasks such as image segmentation in support of planning of radiotherapy. In this paper we introduce a first proposal for a graphical user interface for the segmentation of medical images via the spatial logic based analyser VoxLogicA. Since both the logic approach to image analysis and its application in medical imaging are completely new, this is the first step in an iterative development process that will involve various analysis and development techniques, including empirical research and formal analysis. In the current work we analyse the GUI with a focus on the cognitive and memory load aspects which are critical in this domain of application.

The topological interpretation of modal logics provides descriptive languages and proof systems for reasoning about points of topological spaces. Recent work has been devoted to model checking of spatial logics on discrete spatial structures, such as finite graphs and digital images, with applications in various case studies including medical image analysis. These recent developments required a generalisation step, from topological spaces to closure spaces. In this work we initiate the study of bisimilarity and minimisation algorithms that are consistent with the closure spaces semantics. For this purpose we employ coalgebraic models. We present a coalgebraic definition of bisimilarity for quasi-discrete models, which is adequate with respect to a spatial logic with reachability operators, complemented by a free and open-source minimisation tool for finite models. We also discuss the non-quasi-discrete case, by providing a generalisation of the well-known set-theoretical notion of topo-bisimilarity, and a categorical definition, in the same spirit as the coalgebraic rendition of neighbourhood frames, but employing the covariant power set functor, instead of the contravariant one. We prove its adequacy with respect to infinitary modal logic.

Spatial and spatio-temporal model checking techniques have a wide range of application domains, among which large scale distributed systems and signal and image analysis. In the latter domain, automatic and semi-automatic contouring in Medical Imaging has shown to be a very promising and versatile application that can greatly facilitate the work of professionals in this domain, while supporting explainability, easy replicability and exchange of medical image analysis methods. In recent work we have applied this model-checking technique to the (3D) contouring of tumours and related oedema in magnetic resonance images of the brain. In the current work we address the contouring of (2D) images of nevi. One of the challenges of treating nevi images is their considerable inhomogeneity in shape, colour, texture and size. To deal with this challenge we use a texture similarity operator, in combination with spatial logic operators. We apply our technique on images of a large public database and compare the results with associated ground truth segmentation provided by domain experts.

Gossip protocols form the basis of many smart collective adaptive systems. They are a class of fully decentralised, simple but robust protocols for the distribution of information throughout large scale networks with hundreds or thousands of nodes. Mean field analysis methods have made it possible to approximate and analyse performance aspects of such large scale protocols in an efficient way. Taking the gossip shuffle protocol as a benchmark, we evaluate a recently developed refined mean field approach. We illustrate the gain in accuracy this can provide for the analysis of medium size models analysing two key performance measures. We also show that refined mean field analysis requires special attention to correctly capture the coordination aspects of the gossip shuffle protocol.

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.

This book constitutes the thoroughly refereed post-conference proceedings of the 8th International Conference on Fundamentals of Software Engineering, FSEN 2019, held in Tehran, Iran, in May 2019. The 14 full papers and 3 short papers presented in this volume were carefully reviewed and selected from 47 submissions. The topics of interest in FSEN span over all aspects of formal methods, especially those related to advancing the application of formal methods in the software industry and promoting their integration with practical engineering techniques. The papers are organized in topical sections on agent based systems, theorem proving, learning, verification, distributed algorithms, and program analysis.

VoxLogicA [1] is a free and open source, multi-platform tool, catering for a novel approach to image segmentation, bringing in ideas from formal methods in software engineering, rapid-development, and declarative programming languages, that have been successful in other domains. In a few lines of code, complex analyses can be specified, translating domain knowledge into logical properties. For instance, in brain tumor segmentation, logical properties encode facts such as ''the oedema touches the tumor'', or ''the tumor contains hyperintense areas; furthermore, very intense areas that are very close to hyperintense ones, are part of the tumor''. Such constraints are extremely effective at filtering noise in automated analysis. The logical core is extended by including imaging primitives, e.g., texture similarity or image normalisation. The language is ''a query language for image analysis''. Its innovation potential can be compared to that of the ''Structured Query Language'' SQL, that revolutionised automated data analysis, by permitting queries on large datasets to be designed by experts of the domain to which the data belongs, instead of computer programmers.

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 efficient monitoring algorithms have been developed. As such, it is suitable for real-time verification 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 satisfies 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-Diffusion system and spatio-temporal aspects of a large bike-sharing system., Comment: 36 pages with 13 figures

FuTS, state-to-function transition systems are generalizations of labeled transition systems and of familiar notions of quantitative semantical models as continuous-time Markov chains, interactive Markov chains, and Markov automata. A general scheme for the definition of a notion of strong bisimulation associated with a FuTS is proposed. It is shown that this notion of bisimulation for a FuTS coincides with the coalgebraic notion of behavioral equivalence associated to the functor on Set given by the type of the FuTS. For a series of concrete quantitative semantical models the notion of bisimulation as reported in the literature is proven to coincide with the notion of quantitative bisimulation obtained from the scheme. The comparison includes models with orthogonal behaviour, like interactive Markov chains, and with multiple levels of behavior, like Markov automata. As a consequence of the general result relating FuTS bisimulation and behavioral equivalence we obtain, in a systematic way, a coalgebraic underpinning of all quantitative bisimulations discussed., Comment: In Proceedings QAPL 2015, arXiv:1509.08169

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

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

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.

Coordination Models and Languages. 19th IFIP WG 6.1 International Conference, COORDINATION 2017 Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017 Neuchâtel, Switzerland, June 19-22, 2017, Proceedings

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.

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.

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.

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.

A topological method for automatic segmentation of glioblastoma in MR FLAIR for radiotherapy is presented. The method is based on spatial logics and spatial model-checking.

Preface

In this paper we present the use of a novel spatio-temporal model-checker to detect problems in the data and operation of an adaptive system. We categorise received data as being plausible, implausible, possible or problematic. Data correctness is essential to ensure behavioural correctness in systems which adapt in response to data and our categorisation suggests the degree of caution which should be used in acting in response to this received 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 behavioural phenomenon of clumping", the undesired reduction of separation between subsequent buses serving the same route. Vehicle location data is visualised symbolically on a street map, and categories of problems identied by the spatial part of the model-checker are rendered by repainting the symbols for vehicles in dierent colours. 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.