Showing 1–22 of 22 results for author: Latella, D

Weak Simplicial Bisimilarity for Polyhedral Models and SLCS_eta -- Extended Version

Authors: Nick Bezhanishvili, Vincenzo Ciancia, David Gabelaia, Mamuka Jibladze, Diego Latella, Mieke Massink, Erik P. de Vink

Abstract: In the context of spatial logics and spatial model checking for polyhedral models -- mathematical basis for visualisations in continuous space -- we propose a weakening of simplicial bisimilarity. We additionally propose a corresponding weak notion of $\pm$-bisimilarity on cell-poset models, a discrete representation of polyhedral models. We show that two points are weakly simplicial bisimilar iff… ▽ More In the context of spatial logics and spatial model checking for polyhedral models -- mathematical basis for visualisations in continuous space -- we propose a weakening of simplicial bisimilarity. We additionally propose a corresponding weak notion of $\pm$-bisimilarity on cell-poset models, a discrete representation of polyhedral models. We show that two points are weakly simplicial bisimilar iff their repesentations are weakly $\pm$-bisimilar. The advantage of this weaker notion is that it leads to a stronger reduction of models than its counterpart that was introduced in our previous work. This is important, since real-world polyhedral models, such as those found in domains exploiting mesh processing, typically consist of large numbers of cells. We also propose SLCS_eta, a weaker version of the Spatial Logic for Closure Spaces (SLCS) on polyhedral models, and we show that the proposed bisimilarities enjoy the Hennessy-Milner property: two points are weakly simplicial bisimilar iff they are logically equivalent for SLCS_eta. Similarly, two cells are weakly $\pm$-bisimilar iff they are logically equivalent in the poset-model interpretation of SLCS_eta. This work is performed in the context of the geometric spatial model checker PolyLogicA and the polyhedral semantics of SLCS. △ Less

Submitted 9 April, 2024; originally announced April 2024.

On Bisimilarity for Quasi-discrete Closure Spaces

Authors: Vincenzo Ciancia, Diego Latella, Mieke Massink, Erik P. de Vink

Abstract: Closure spaces, a generalisation of topological spaces, have shown to be a convenient theoretical framework for spatial model checking. The closure operator of closure spaces and quasi-discrete closure spaces induces a notion of neighborhood akin to that of topological spaces that build on open sets. For closure models and quasi-discrete closure models, in this paper we present three notions of bi… ▽ More Closure spaces, a generalisation of topological spaces, have shown to be a convenient theoretical framework for spatial model checking. The closure operator of closure spaces and quasi-discrete closure spaces induces a notion of neighborhood akin to that of topological spaces that build on open sets. For closure models and quasi-discrete closure models, in this paper we present three notions of bisimilarity that are logically characterised by corresponding modal logics with spatial modalities: (i) CM-bisimilarity for closure models (CMs) is shown to generalise Topo-bisimilarity for topological models. CM-bisimilarity corresponds to equivalence with respect to the infinitary modal logic IML that includes the modality ${\cal N}$ for ``being near''. (ii) CMC-bisimilarity, with `CMC' standing for CM-bisimilarity with converse, refines CM-bisimilarity for quasi-discrete closure spaces, carriers of quasi-discrete closure models. Quasi-discrete closure models come equipped with two closure operators, Direct ${\cal C}$ and Converse ${\cal C}$, stemming from the binary relation underlying closure and its converse. CMC-bisimilarity, is captured by the infinitary modal logic IMLC including two modalities, Direct ${\cal N}$ and Converse ${\cal N}$, corresponding to the two closure operators. (iii) CoPa-bisimilarity on quasi-discrete closure models, which is weaker than CMC-bisimilarity, is based on the notion of compatible paths. The logical counterpart of CoPa-bisimilarity is the infinitary modal logic ICRL with modalities Direct $ζ$ and Converse $ζ$, whose semantics relies on forward and backward paths, respectively. It is shown that CoPa-bisimilarity for quasi-discrete closure models relates to divergence-blind stuttering equivalence for Kripke structures. △ Less

Submitted 7 December, 2023; v1 submitted 27 January, 2023; originally announced January 2023.

Comments: 32 pages, 14 figures

MSC Class: 03B44; 03B70 ACM Class: F.4.1; D.2.4

On Bisimilarities for Closure Spaces - Preliminary Version

Authors: Vincenzo Ciancia, Diego Latella, Mieke Massink Erik de Vink

Abstract: 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 refine it for quasi-discrete closure models. We also define two additional notions of bisimilar… ▽ More 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 refine it for quasi-discrete closure models. We also define 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 refines it in a way that is reminishent of Stuttering Equivalence on transition systems. For each bisimilarity we provide a logical characterisation, using variants of the Spatial Logic for Closure Spaces (SLCS). We also address the issue of (space) minimisation via the three equivalences. △ Less

Submitted 14 May, 2021; originally announced May 2021.

MSC Class: 68Q60 ACM Class: F.4.1; D.2.4; I.2.4; I.4.6

Geometric Model Checking of Continuous Space

Authors: Nick Bezhanishvili, Vincenzo Ciancia, David Gabelaia, Gianluca Grilletti, Diego Latella, Mieke Massink

Abstract: Topological Spatial Model Checking is a recent paradigm where model checking techniques are developed for 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… ▽ More Topological Spatial Model Checking is a recent paradigm where model checking techniques are developed for 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. Following a recently developed geometric semantics of Modal Logic, we propose an interpretation of SLCS in continuous space, admitting a geometric spatial model checking procedure, by resorting to models based on polyhedra. Such representations of space are increasingly relevant in many domains of application, due to recent developments of 3D scanning and visualisation techniques that exploit mesh processing. We introduce PolyLogicA, a geometric spatial model checker for SLCS formulas on polyhedra and demonstrate feasibility of our approach on two 3D polyhedral models of realistic size. Finally, we introduce a geometric definition of bisimilarity, proving that it characterises logical equivalence. △ Less

Submitted 21 November, 2022; v1 submitted 13 May, 2021; originally announced May 2021.

MSC Class: 68Q60 ACM Class: F.4.1; D.2.4; I.2.4; I.3.6; I.4.6; I.5.4

Journal ref: Logical Methods in Computer Science, Volume 18, Issue 4 (November 22, 2022) lmcs:9060

Using Spatial Logic and Model Checking for Nevus Segmentation

Authors: Gina Belmonte, Giovanna Broccia, Vincenzo Ciancia, Diego Latella, Mieke Massink

Abstract: 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 ex… ▽ More 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. △ Less

Submitted 24 December, 2020; originally announced December 2020.

Towards Spatial Bisimilarity for Closure Models: Logical and Coalgebraic Characterisations

Authors: Vincenzo Ciancia, Diego Latella, Mieke Massink, Erik de Vink

Abstract: 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 ge… ▽ More 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. △ Less

Submitted 12 May, 2020; originally announced May 2020.

Refined Mean Field Analysis of the Gossip Shuffle Protocol -- extended version --

Authors: Nicolas Gast, Diego Latella, Mieke Massink

Abstract: 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. Tak… ▽ More 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. △ Less

Submitted 16 April, 2020; originally announced April 2020.

Comments: This paper is an extended version of a short paper accepted for the LNCS proceedings of COORDINATION 2020

Spatial Logics and Model Checking for Medical Imaging (Extended Version)

Authors: Fabrizio Banci Buonamici, Gina Belmonte, Vincenzo Ciancia, Diego Latella, Mieke Massink

Abstract: Recent research on spatial and spatio-temporal model checking provides novel image analysis methodologies, rooted in logical methods for topological spaces. Medical Imaging (MI) is a field where such methods show potential for ground-breaking innovation. Our starting point is SLCS, the Spatial Logic for Closure Spaces -- Closure Spaces being a generalisation of topological spaces, covering also di… ▽ More Recent research on spatial and spatio-temporal model checking provides novel image analysis methodologies, rooted in logical methods for topological spaces. Medical Imaging (MI) is a field where such methods show potential for ground-breaking innovation. Our starting point is SLCS, the Spatial Logic for Closure Spaces -- Closure Spaces being a generalisation of topological spaces, covering also discrete space structures -- and topochecker, a model-checker for SLCS (and extensions thereof). We introduce the logical language ImgQL ("Image Query Language"). ImgQL extends SLCS with logical operators describing distance and region similarity. The spatio-temporal model checker topochecker is correspondingly enhanced with state-of-the-art algorithms, borrowed from computational image processing, for efficient implementation of distancebased operators, namely distance transforms. Similarity between regions is defined by means of a statistical similarity operator, based on notions from statistical texture analysis. We illustrate our approach by means of two examples of analysis of Magnetic Resonance images: segmentation of glioblastoma and its oedema, and segmentation of rectal carcinoma. △ Less

Submitted 14 November, 2018; originally announced November 2018.

VoxLogicA: a Spatial Model Checker for Declarative Image Analysis (Extended Version)

Authors: Gina Belmonte, Vincenzo Ciancia, Diego Latella, Mieke Massink

Abstract: 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. We explore a new domain, namely (semi-)automatic contouring in Medical Imaging, introducing the tool VoxLogicA which merges the state-of-the-art library of computational imaging algorithms ITK with the unique combination of decla… ▽ More 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. We explore a new domain, namely (semi-)automatic contouring in Medical Imaging, introducing the tool VoxLogicA which merges the state-of-the-art library of computational imaging algorithms ITK with the unique combination of declarative specification and optimised execution provided by spatial logic model checking. The result is a rapid, logic based analysis development methodology. The analysis of an existing benchmark of medical images for segmentation of brain tumours shows that simple VoxLogicA analysis can reach state-of-the-art accuracy, competing with best-in-class algorithms, with the advantage of explainability and replicability. Furthermore, due to a two-orders-of-magnitude speedup compared to the existing general-purpose spatio-temporal model checker topochecker, VoxLogicA enables interactive development of analysis of 3D medical images, which can greatly facilitate the work of professionals in this domain. △ Less

Submitted 14 November, 2018; originally announced November 2018.

A refined mean field approximation of synchronous discrete-time population models

Authors: Nicolas Gast, Diego Latella, Mieke Massink

Abstract: Mean field approximation is a popular method to study the behaviour of stochastic models composed of a large number of interacting objects. When the objects are asynchronous, the mean field approximation of a population model can be expressed as an ordinary differential equation. When the objects are (clock-) synchronous the mean field approximation is a discrete time dynamical system. We focus on… ▽ More Mean field approximation is a popular method to study the behaviour of stochastic models composed of a large number of interacting objects. When the objects are asynchronous, the mean field approximation of a population model can be expressed as an ordinary differential equation. When the objects are (clock-) synchronous the mean field approximation is a discrete time dynamical system. We focus on the latter.We study the accuracy of mean field approximation when this approximation is a discrete-time dynamical system. We extend a result that was shown for the continuous time case and we prove that expected performance indicators estimated by mean field approximation are $O(1/N)$-accurate. We provide simple expressions to effectively compute the asymptotic error of mean field approximation, for finite time-horizon and steady-state, and we use this computed error to propose what we call a \emph{refined} mean field approximation. We show, by using a few numerical examples, that this technique improves the quality of approximation compared to the classical mean field approximation, especially for relatively small population sizes. △ Less

Submitted 20 July, 2018; originally announced July 2018.

Journal ref: Performance Evaluation, Elsevier, 2018

Design and Optimisation of the FlyFast Front-end for Attribute-based Coordination

Authors: Diego Latella, Mieke Massink

Abstract: 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-chec… ▽ More 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. △ Less

Submitted 13 July, 2017; originally announced July 2017.

Comments: In Proceedings QAPL 2017, arXiv:1707.03668

Journal ref: EPTCS 250, 2017, pp. 92-110

Model Checking Spatial Logics for Closure Spaces

Authors: Vincenzo Ciancia, Diego Latella, Michele Loreti, Mieke Massink

Abstract: Spatial aspects of computation are becoming increasingly relevant in Computer Science, especially in the field of collective adaptive systems and when dealing with systems distributed in physical space. Traditional formal verification techniques are well suited to analyse the temporal evolution of programs; however, properties of space are typically not taken into account explicitly. We present a… ▽ More Spatial aspects of computation are becoming increasingly relevant in Computer Science, especially in the field of collective adaptive systems and when dealing with systems distributed in physical space. Traditional formal verification techniques are well suited to analyse the temporal evolution of programs; however, properties of space are typically not taken into account explicitly. We present a topology-based approach to formal verification of spatial properties depending upon physical space. We define an appropriate logic, stemming from the tradition of topological interpretations of modal logics, dating back to earlier logicians such as Tarski, where modalities describe neighbourhood. We lift the topological definitions to the more general setting of closure spaces, also encompassing discrete, graph-based structures. We extend the framework with a spatial surrounded operator, a propagation operator and with some collective operators. The latter are interpreted over arbitrary sets of points instead of individual points in space. We define efficient model checking procedures, both for the individual and the collective spatial fragments of the logic and provide a proof-of-concept tool. △ Less

Submitted 7 October, 2016; v1 submitted 21 September, 2016; originally announced September 2016.

ACM Class: D.2.4; F.3.1; F.3.2

Journal ref: Logical Methods in Computer Science, Volume 12, Issue 4 (April 27, 2017) lmcs:2067

From Collective Adaptive Systems to Human Centric Computation and Back: Spatial Model Checking for Medical Imaging

Authors: Gina Belmonte, Vincenzo Ciancia, Diego Latella, Mieke Massink

Abstract: Recent research on formal verification for Collective Adaptive Systems (CAS) pushed advancements in spatial and spatio-temporal model checking, and as a side result provided novel image analysis methodologies, rooted in logical methods for topological spaces. Medical Imaging (MI) is a field where such technologies show potential for ground-breaking innovation. In this position paper, we present a… ▽ More Recent research on formal verification for Collective Adaptive Systems (CAS) pushed advancements in spatial and spatio-temporal model checking, and as a side result provided novel image analysis methodologies, rooted in logical methods for topological spaces. Medical Imaging (MI) is a field where such technologies show potential for ground-breaking innovation. In this position paper, we present a preliminary investigation centred on applications of spatial model checking to MI. The focus is shifted from pure logics to a mixture of logical, statistical and algorithmic approaches, driven by the logical nature intrinsic to the specification of the properties of interest in the field. As a result, novel operators are introduced, that could as well be brought back to the setting of CAS. △ Less

Submitted 8 July, 2016; originally announced July 2016.

Comments: In Proceedings FORECAST 2016, arXiv:1607.02001

ACM Class: D.2.4 model checking; F.4.1 modal logic; J.3 medical information systems

Journal ref: EPTCS 217, 2016, pp. 81-92

On Formal Methods for Collective Adaptive System Engineering. {Scalable Approximated, Spatial} Analysis Techniques. Extended Abstract

Authors: Diego Latella

Abstract: In this extended abstract a view on the role of Formal Methods in System Engineering is briefly presented. Then 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-c… ▽ More In this extended abstract a view on the role of Formal Methods in System Engineering is briefly presented. Then 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. △ Less

Submitted 8 July, 2016; originally announced July 2016.

Comments: In Proceedings FORECAST 2016, arXiv:1607.02001

Journal ref: EPTCS 217, 2016, pp. 53-61

Bisimulation of Labelled State-to-Function Transition Systems Coalgebraically

Authors: Diego Latella, Mieke Massink, Erik P De Vink

Abstract: Labeled state-to-function transition systems, FuTS for short, are characterized by transitions which relate states to functions of states over general semirings, equipped with a rich set of higher-order operators. As such, FuTS constitute a convenient modeling instrument to deal with process languages and their quantitative extensions in particular. In this paper, the notion of bisimulation induc… ▽ More Labeled state-to-function transition systems, FuTS for short, are characterized by transitions which relate states to functions of states over general semirings, equipped with a rich set of higher-order operators. As such, FuTS constitute a convenient modeling instrument to deal with process languages and their quantitative extensions in particular. In this paper, the notion of bisimulation induced by a FuTS is addressed from a coalgebraic point of view. A correspondence result is established stating that FuTS-bisimilarity coincides with behavioural equivalence of the associated functor. As generic examples, the equivalences underlying substantial fragments of major examples of quantitative process algebras are related to the bisimilarity of specific FuTS. The examples range from a stochastic process language, PEPA, to a language for Interactive Markov Chains, IML, a (discrete) timed process language, TPC, and a language for Markov Automata, MAL. The equivalences underlying these languages are related to the bisimilarity of their specific FuTS. By the correspondence result coalgebraic justification of the equivalences of these calculi is obtained. The specific selection of languages, besides covering a large variety of process interaction models and modelling choices involving quantities, allows us to show different classes of FuTS, namely so-called simple FuTS, combined FuTS, nested FuTS, and general FuTS. △ Less

Submitted 21 December, 2015; v1 submitted 18 November, 2015; originally announced November 2015.

Journal ref: Logical Methods in Computer Science, Volume 11, Issue 4 (December 22, 2015) lmcs:1617

A Definition Scheme for Quantitative Bisimulation

Authors: Diego Latella, Mieke Massink, Erik de Vink

Abstract: 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 coin… ▽ More 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. △ Less

Submitted 28 September, 2015; originally announced September 2015.

Comments: In Proceedings QAPL 2015, arXiv:1509.08169

ACM Class: D.2.4, F.3.2

Journal ref: EPTCS 194, 2015, pp. 63-78

CARMA: Collective Adaptive Resource-sharing Markovian Agents

Authors: Luca Bortolussi, Rocco De Nicola, Vashti Galpin, Stephen Gilmore, Jane Hillston, Diego Latella, Michele Loreti, Mieke Massink

Abstract: In this paper we present CARMA, a language recently defined to support specification and analysis of collective adaptive systems. CARMA is a stochastic process algebra equipped with linguistic constructs specifically developed for modelling and programming systems that can operate in open-ended and unpredictable environments. This class of systems is typically composed of a huge number of interact… ▽ More In this paper we present CARMA, a language recently defined to support specification and analysis of collective adaptive systems. CARMA is a stochastic process algebra equipped with linguistic constructs specifically developed for modelling and programming systems that can operate in open-ended and unpredictable environments. This class of systems is typically composed of a huge number of interacting agents that dynamically adjust and combine their behaviour to achieve specific goals. A CARMA model, termed a collective, consists of a set of components, each of which exhibits a set of attributes. To model dynamic aggregations, which are sometimes referred to as ensembles, CARMA provides communication primitives that are based on predicates over the exhibited attributes. These predicates are used to select the participants in a communication. Two communication mechanisms are provided in the CARMA language: multicast-based and unicast-based. In this paper, we first introduce the basic principles of CARMA and then we show how our language can be used to support specification with a simple but illustrative example of a socio-technical collective adaptive system. △ Less

Submitted 28 September, 2015; originally announced September 2015.

Comments: In Proceedings QAPL 2015, arXiv:1509.08169

ACM Class: C.4; B.8.2

Journal ref: EPTCS 194, 2015, pp. 16-31

On-the-fly Probabilistic Model Checking

Authors: Diego Latella, Michele Loreti, Mieke Massink

Abstract: Model checking approaches can be divided into two broad categories: global approaches that determine the set of all states in a model M that satisfy a temporal logic formula f, and local approaches in which, given a state s in M, the procedure determines whether s satisfies f. When s is a term of a process language, the model checking procedure can be executed "on-the-fly", driven by the syntactic… ▽ More Model checking approaches can be divided into two broad categories: global approaches that determine the set of all states in a model M that satisfy a temporal logic formula f, and local approaches in which, given a state s in M, the procedure determines whether s satisfies f. When s is a term of a process language, the model checking procedure can be executed "on-the-fly", driven by the syntactical structure of s. For certain classes of systems, e.g. those composed of many parallel components, the local approach is preferable because, depending on the specific property, it may be sufficient to generate and inspect only a relatively small part of the state space. We propose an efficient, on-the-fly, PCTL model checking procedure that is parametric with respect to the semantic interpretation of the language. The procedure comprises both bounded and unbounded until modalities. The correctness of the procedure is shown and its efficiency is compared with a global PCTL model checker on representative applications. △ Less

Submitted 27 October, 2014; originally announced October 2014.

Comments: In Proceedings ICE 2014, arXiv:1410.7013

ACM Class: F.3.1; D.2.4

Journal ref: EPTCS 166, 2014, pp. 45-59

Specifying and Verifying Properties of Space - Extended Version

Authors: Vincenzo Ciancia, Diego Latella, Michele Loreti, Mieke Massink

Abstract: The interplay between process behaviour and spatial aspects of computation has become more and more relevant in Computer Science, especially in the field of collective adaptive systems, but also, more generally, when dealing with systems distributed in physical space. Traditional verification techniques are well suited to analyse the temporal evolution of programs; properties of space are typicall… ▽ More The interplay between process behaviour and spatial aspects of computation has become more and more relevant in Computer Science, especially in the field of collective adaptive systems, but also, more generally, when dealing with systems distributed in physical space. Traditional verification techniques are well suited to analyse the temporal evolution of programs; properties of space are typically not explicitly taken into account. We propose a methodology to verify properties depending upon physical space. We define an appropriate logic, stemming from the tradition of topological interpretations of modal logics, dating back to earlier logicians such as Tarski, where modalities describe neighbourhood. We lift the topological definitions to a more general setting, also encompassing discrete, graph-based structures. We further extend the framework with a spatial until operator, and define an efficient model checking procedure, implemented in a proof-of-concept tool. △ Less

Submitted 26 June, 2014; v1 submitted 24 June, 2014; originally announced June 2014.

Comments: Presented at "Theoretical Computer Science" 2014, Rome

Stochastically timed predicate-based communication primitives for autonomic computing

Authors: Diego Latella, Michele Loreti, Mieke Massink, Valerio Senni

Abstract: Predicate-based communication allows components of a system to send messages and requests to ensembles of components that are determined at execution time through the evaluation of a predicate, in a multicast fashion. Predicate-based communication can greatly simplify the programming of autonomous and adaptive systems. We present a stochastically timed extension of the Software Component Ensembl… ▽ More Predicate-based communication allows components of a system to send messages and requests to ensembles of components that are determined at execution time through the evaluation of a predicate, in a multicast fashion. Predicate-based communication can greatly simplify the programming of autonomous and adaptive systems. We present a stochastically timed extension of the Software Component Ensemble Language (SCEL) that was introduced in previous work. Such an extension raises a number of non-trivial design and formal semantics issues with different options as possible solutions at different levels of abstraction. We discuss four of these options, of which two in more detail. We provide a formal semantics definition and an illustration of the use of the language modeling a bike sharing system, together with some preliminary analysis of the system performance. △ Less

Submitted 8 June, 2014; originally announced June 2014.

Comments: In Proceedings QAPL 2014, arXiv:1406.1567

Journal ref: EPTCS 154, 2014, pp. 1-16

On-the-fly Fast Mean-Field Model-Checking: Extended Version

Authors: Diego Latella, Michele Loreti, Mieke Massink

Abstract: A novel, scalable, on-the-fly model-checking procedure is presented to verify bounded PCTL properties of selected individuals in the context of very large systems of independent interacting objects. The proposed procedure combines on-the-fly model checking techniques with deterministic mean-field approximation in discrete time. The asymptotic correctness of the procedure is shown and some results… ▽ More A novel, scalable, on-the-fly model-checking procedure is presented to verify bounded PCTL properties of selected individuals in the context of very large systems of independent interacting objects. The proposed procedure combines on-the-fly model checking techniques with deterministic mean-field approximation in discrete time. The asymptotic correctness of the procedure is shown and some results of the application of a prototype implementation of the FlyFast model-checker are presented. △ Less

Submitted 12 December, 2013; originally announced December 2013.

Bisimulation of Labeled State-to-Function Transition Systems of Stochastic Process Languages

Authors: D. Latella, M. Massink, E. P. de Vink

Abstract: Labeled state-to-function transition systems, FuTS for short, admit multiple transition schemes from states to functions of finite support over general semirings. As such they constitute a convenient modeling instrument to deal with stochastic process languages. In this paper, the notion of bisimulation induced by a FuTS is proposed and a correspondence result is proven stating that FuTS-bisimulat… ▽ More Labeled state-to-function transition systems, FuTS for short, admit multiple transition schemes from states to functions of finite support over general semirings. As such they constitute a convenient modeling instrument to deal with stochastic process languages. In this paper, the notion of bisimulation induced by a FuTS is proposed and a correspondence result is proven stating that FuTS-bisimulation coincides with the behavioral equivalence of the associated functor. As generic examples, the concrete existing equivalences for the core of the process algebras ACP, PEPA and IMC are related to the bisimulation of specific FuTS, providing via the correspondence result coalgebraic justification of the equivalences of these calculi. △ Less

Submitted 6 September, 2012; originally announced September 2012.

Comments: In Proceedings ACCAT 2012, arXiv:1208.4301

ACM Class: F.3.2

Journal ref: EPTCS 93, 2012, pp. 23-43