2023
Report
Open Access
On bisimilarity for polyhedral models and SLCS - Preliminary version
Ciancia V., Gabelaia D., Latella D., Massink M., De Vink E. P.
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.Source: ISTI Technical Report, ISTI-2023-TR/003, 2023
DOI: 10.32079/isti-tr-2023/003
Metrics:
Ciancia V., Gabelaia D., Latella D., Massink M., De Vink E. P.
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.Source: ISTI Technical Report, ISTI-2023-TR/003, 2023
DOI: 10.32079/isti-tr-2023/003
Metrics:
See at:
ISTI Repository 
| CNR ExploRA
2023
Conference article
Open Access
Minimisation of spatial models using branching bisimilarity
Ciancia V., Groote J. F., Latella D., Massink M., De Vink E. P.
Spatial logic and spatial model checking have great potential 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 another 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 Labelled 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.Source: FM'23 - 25th International Symposium on Formal Methods, pp. 263–281, Luebeck, Germany, 6-10/03/2023
DOI: 10.1007/978-3-031-27481-7_16
Metrics:
Ciancia V., Groote J. F., Latella D., Massink M., De Vink E. P.
Spatial logic and spatial model checking have great potential 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 another 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 Labelled 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.Source: FM'23 - 25th International Symposium on Formal Methods, pp. 263–281, Luebeck, Germany, 6-10/03/2023
DOI: 10.1007/978-3-031-27481-7_16
Metrics:
See at:
ISTI Repository | CNR ExploRA
2023
Report
Unknown
THE D.3.2.1 - AA@THE User needs, technical requirements and specifications
Pratali L., Campana M. G., Delmastro F., Di Martino F., Pescosolido L., Barsocchi P., Broccia G., Ciancia V., Gennaro C., Girolami M., Lagani G., La Rosa D., Latella D., Magrini M., Manca M., Massink M., Mattioli A., Moroni D., Palumbo F., Paradisi P., Paternò F., Santoro C., Sebastiani L., Vairo C.
Deliverable D3.2.1 del progetto PNRR Ecosistemi ed innovazione - THESource: ISTI Project Report, THE, D3.2, 2023
Pratali L., Campana M. G., Delmastro F., Di Martino F., Pescosolido L., Barsocchi P., Broccia G., Ciancia V., Gennaro C., Girolami M., Lagani G., La Rosa D., Latella D., Magrini M., Manca M., Massink M., Mattioli A., Moroni D., Palumbo F., Paradisi P., Paternò F., Santoro C., Sebastiani L., Vairo C.
Deliverable D3.2.1 del progetto PNRR Ecosistemi ed innovazione - THESource: ISTI Project Report, THE, D3.2, 2023
See at: CNR ExploRA
2023
Conference article
Open Access
On bisimilarity for polyhedral models and SLCS
Ciancia V., Gabelaia D., Latella D., Massink M., De Vink E. P.
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.Source: DisCoTec 2023 - 43rd IFIP WG 6.1 International Conference, FORTE 2023 Held as Part of the 18th International Federated Conference on Distributed Computing Techniques, pp. 132–151, Lisbon, Portugal, 19-23/06/2023
DOI: 10.1007/978-3-031-35355-0_9
Metrics:
Ciancia V., Gabelaia D., Latella D., Massink M., De Vink E. P.
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.Source: DisCoTec 2023 - 43rd IFIP WG 6.1 International Conference, FORTE 2023 Held as Part of the 18th International Federated Conference on Distributed Computing Techniques, pp. 132–151, Lisbon, Portugal, 19-23/06/2023
DOI: 10.1007/978-3-031-35355-0_9
Metrics:
See at:
ISTI Repository | link.springer.com 
| CNR ExploRA
2023
Software
Unknown
A toolchain for strategy synthesis with spatial properties - Complementary material
Basile D., Ter Beek M. H., Bussi L., Ciancia V.
This is the complementary material for our paper ``A Toolchain for Strategy Synthesis with Spatial Properties'' accepted for publication at the Journal of Software Tools and Technology Transfer. This repository contains a permanent snapshot of https://github.com/contractautomataproject/CATLib_PngConverter/tree/ec0938043146b008bbbcb4ed3ec79c06dd2e47d6DOI: 10.5281/zenodo.8220527
Metrics:
Basile D., Ter Beek M. H., Bussi L., Ciancia V.
This is the complementary material for our paper ``A Toolchain for Strategy Synthesis with Spatial Properties'' accepted for publication at the Journal of Software Tools and Technology Transfer. This repository contains a permanent snapshot of https://github.com/contractautomataproject/CATLib_PngConverter/tree/ec0938043146b008bbbcb4ed3ec79c06dd2e47d6DOI: 10.5281/zenodo.8220527
Metrics:
See at: CNR ExploRA
2023
Report
Open Access
SLCS on face-poset models and bisimilarities on quasi-discrete closure models
Ciancia V., Latella D., Massink M.
We define SLCS\eta, a weaker logic than SLCS\gamma, and we interpret it on face-poset models. We show the relationship between the equivalence induced by the two logics, namely =SLCS\gamma and =SLCS\eta and bisimilarities of finite closure models proposed in the literature.Source: 10.32079/ISTI-TR-2023/009, 2023
DOI: 10.32079/isti-tr-2023/009
Metrics:
Ciancia V., Latella D., Massink M.
We define SLCS\eta, a weaker logic than SLCS\gamma, and we interpret it on face-poset models. We show the relationship between the equivalence induced by the two logics, namely =SLCS\gamma and =SLCS\eta and bisimilarities of finite closure models proposed in the literature.Source: 10.32079/ISTI-TR-2023/009, 2023
DOI: 10.32079/isti-tr-2023/009
Metrics:
See at:
ISTI Repository | CNR ExploRA
2023
Journal article
Open Access
A toolchain for strategy synthesis with spatial properties
Basile D., Ter Beek M. H, Bussi L., Ciancia V.
We present an application of strategy synthesis to enforce spatial properties. This is achieved by implementing a toolchain that enables the tools \texttt{CATLib} and \texttt{VoxLogicA} to interact in a fully automated way. The Contract Automata Library (\texttt{CATLib}) is aimed at both composition and strategy synthesis of games modelled in a dialect of finite state automata. The Voxel-based Logical Analyser (\texttt{VoxLogicA}) is a spatial model checker for the verification of properties expressed using the Spatial Logic of Closure Spaces on pixels of digital images. We provide examples of strategy synthesis on automata encoding motion of agents in spaces represented by images, as well as a proof-of-concept realistic example based on a case study from the railway domain. The strategies are synthesised with \texttt{CAT\-Lib}, while the properties to enforce are defined by means of spatial model checking of the images with \texttt{VoxLogicA}. The combination of spatial model checking with strategy synthesis provides a toolchain for checking and enforcing mobility properties in multi-agent systems in which location plays an important role, like in many collective adaptive systems. We discuss the toolchain's performance also considering several recent improvements.Source: International journal on software tools for technology transfer (Print) 25 (2023): 641–658. doi:10.1007/s10009-023-00730-1
DOI: 10.1007/s10009-023-00730-1
Metrics:
Basile D., Ter Beek M. H, Bussi L., Ciancia V.
We present an application of strategy synthesis to enforce spatial properties. This is achieved by implementing a toolchain that enables the tools \texttt{CATLib} and \texttt{VoxLogicA} to interact in a fully automated way. The Contract Automata Library (\texttt{CATLib}) is aimed at both composition and strategy synthesis of games modelled in a dialect of finite state automata. The Voxel-based Logical Analyser (\texttt{VoxLogicA}) is a spatial model checker for the verification of properties expressed using the Spatial Logic of Closure Spaces on pixels of digital images. We provide examples of strategy synthesis on automata encoding motion of agents in spaces represented by images, as well as a proof-of-concept realistic example based on a case study from the railway domain. The strategies are synthesised with \texttt{CAT\-Lib}, while the properties to enforce are defined by means of spatial model checking of the images with \texttt{VoxLogicA}. The combination of spatial model checking with strategy synthesis provides a toolchain for checking and enforcing mobility properties in multi-agent systems in which location plays an important role, like in many collective adaptive systems. We discuss the toolchain's performance also considering several recent improvements.Source: International journal on software tools for technology transfer (Print) 25 (2023): 641–658. doi:10.1007/s10009-023-00730-1
DOI: 10.1007/s10009-023-00730-1
Metrics:
See at:
ISTI Repository | ISTI Repository | CNR ExploRA
2022
Report
Open Access
Minimisation of spatial models using branching bisimilarity (extended version)
Ciancia V., Groote J. F., Latella D., Massink M., De Vink E. P.
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.Source: ISTI Technical Report, ISTI-2022-TR/027, 2022
DOI: 10.32079/isti-tr-2022/027
Metrics:
Ciancia V., Groote J. F., Latella D., Massink M., De Vink E. P.
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.Source: ISTI Technical Report, ISTI-2022-TR/027, 2022
DOI: 10.32079/isti-tr-2022/027
Metrics:
See at:
ISTI Repository | CNR ExploRA
2022
Contribution to conference
Open Access
Towards a GUI for declarative medical image analysis: cognitive and memory load issues
Broccia G., Ciancia V., Latella D., Massink M.
In medical imaging, (semi-)automatic image analysis techniques have been proposed to support the current time-consuming and cognitively demanding practice of manual segmentation of regions of interest (ROIs). The recently proposed image query language ImgQL, based on spatial logic and model checking, represents segmentation methods as concise, domain-oriented, human-readable procedures aimed at domain experts rather than technologists, and has been validated in several case studies. Such efforts are directed towards a human-centred Artificial Intelligence methodology. To this aim, we complemented the ongoing research line with a study of the Human-Computer Interaction aspects. In this work we investigate the design of a graphical user interface (GUI) prototype that supports the analysis procedure with minimal impact on the focus and the memory load of domain experts.Source: HCII 2022 - 24th International Conference on Human-Computer Interaction, pp. 103–111, Online conference, 26/06-01/07/2022
DOI: 10.1007/978-3-031-06388-6_14
Metrics:
Broccia G., Ciancia V., Latella D., Massink M.
In medical imaging, (semi-)automatic image analysis techniques have been proposed to support the current time-consuming and cognitively demanding practice of manual segmentation of regions of interest (ROIs). The recently proposed image query language ImgQL, based on spatial logic and model checking, represents segmentation methods as concise, domain-oriented, human-readable procedures aimed at domain experts rather than technologists, and has been validated in several case studies. Such efforts are directed towards a human-centred Artificial Intelligence methodology. To this aim, we complemented the ongoing research line with a study of the Human-Computer Interaction aspects. In this work we investigate the design of a graphical user interface (GUI) prototype that supports the analysis procedure with minimal impact on the focus and the memory load of domain experts.Source: HCII 2022 - 24th International Conference on Human-Computer Interaction, pp. 103–111, Online conference, 26/06-01/07/2022
DOI: 10.1007/978-3-031-06388-6_14
Metrics:
See at:
ISTI Repository | ISTI Repository | link.springer.com | CNR ExploRA
2022
Contribution to book
Open Access
Back-and-forth in space: on logics and bisimilarity in closure spaces
Ciancia V., Latella D., Massink M., De Vink E. P.
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.Source: A Journey from Process Algebra via Timed Automata to Model Learning, edited by Jansen N., Stoelinga M., van den Bos P., pp. 98–115, 2022
DOI: 10.1007/978-3-031-15629-8_6
Metrics:
Ciancia V., Latella D., Massink M., De Vink E. P.
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.Source: A Journey from Process Algebra via Timed Automata to Model Learning, edited by Jansen N., Stoelinga M., van den Bos P., pp. 98–115, 2022
DOI: 10.1007/978-3-031-15629-8_6
Metrics:
See at:
ISTI Repository | link.springer.com | CNR ExploRA
2022
Report
Open Access
Back-and-forth in space: on logics and bisimilarity in closure spaces. Preliminary Extended Version
Ciancia V., Latella D., Massink M., De Vink E. P.
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.Source: ISTI Technical Report, ISTI-TR-2022/018, 2022
DOI: 10.32079/isti-tr-2022/018
Metrics:
Ciancia V., Latella D., Massink M., De Vink E. P.
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.Source: ISTI Technical Report, ISTI-TR-2022/018, 2022
DOI: 10.32079/isti-tr-2022/018
Metrics:
See at:
ISTI Repository | CNR ExploRA
2022
Conference article
Open Access
An experimental toolchain for strategy synthesis with spatial properties
Basile D., Ter Beek M. H., Ciancia V.
We investigate the application of strategy synthesis to enforce spatial properties. The Contract Automata Library (CATLib) performs both composition and strategy synthesis of games modelled in a dialect of finite state automata. The Voxel-based Logical Analyser (VoxLogicA) is a spatial model checker that allows the verification of properties expressed using the Spatial Logic of Closure Spaces on pixels of digital images. In this paper, we explore the integration of these two tools. We provide a basic example of strategy synthesis on automata encoding motion of agents in spaces represented by images. The strategy is synthesised with CATLib, whilst the properties to enforce are defined by means of spatial model checking of the images with VoxLogicA.Source: ISoLA'22 - 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, pp. 142–164, Rhodes, Greece, 24-28/10/2022
DOI: 10.1007/978-3-031-19759-8_10
Metrics:
Basile D., Ter Beek M. H., Ciancia V.
We investigate the application of strategy synthesis to enforce spatial properties. The Contract Automata Library (CATLib) performs both composition and strategy synthesis of games modelled in a dialect of finite state automata. The Voxel-based Logical Analyser (VoxLogicA) is a spatial model checker that allows the verification of properties expressed using the Spatial Logic of Closure Spaces on pixels of digital images. In this paper, we explore the integration of these two tools. We provide a basic example of strategy synthesis on automata encoding motion of agents in spaces represented by images. The strategy is synthesised with CATLib, whilst the properties to enforce are defined by means of spatial model checking of the images with VoxLogicA.Source: ISoLA'22 - 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, pp. 142–164, Rhodes, Greece, 24-28/10/2022
DOI: 10.1007/978-3-031-19759-8_10
Metrics:
See at:
ISTI Repository | link.springer.com | CNR ExploRA
2022
Contribution to book
Open Access
Towards model checking video streams using VoxLogicA on GPUs
Bussi L., Ciancia V., Gadducci F., Latella D., Massink M.
We present a feasibility study on the use of spatial logic model checking for real-time analysis of high-resolution video streams with the tool VoxLogicA. VoxLogicA is a voxel-based image analyser based on the Spatial Logic for Closure Spaces, a logic catered to deal with properties of spatial structures such as topological spaces, graphs and polyhedra. The underlying language includes operators to model proximity and reachability. We demonstrate, via the analysis of a series of video frames from a well-known video game, that it is possible to analyse high-resolution videos in real-time by exploiting the speed-up of VoxLogicA-GPU, a recently developed GPU-based version of the tool, which is 1-2 orders of magnitude faster than its previous iteration. Potential applications of real-time video analysis include medical imaging applications such as ultrasound exams, and other video-based diagnostic techniques. More broadly speaking, this work can be the first step towards novel information retrieval methods suitable to find information in a declarative way, in possibly large collections of video streams.Source: From Data to Models and Back, edited by Bowles J., Broccia G., Pellungrini R., pp. 78–90, 2022
DOI: 10.1007/978-3-031-16011-0_6
Metrics:
Bussi L., Ciancia V., Gadducci F., Latella D., Massink M.
We present a feasibility study on the use of spatial logic model checking for real-time analysis of high-resolution video streams with the tool VoxLogicA. VoxLogicA is a voxel-based image analyser based on the Spatial Logic for Closure Spaces, a logic catered to deal with properties of spatial structures such as topological spaces, graphs and polyhedra. The underlying language includes operators to model proximity and reachability. We demonstrate, via the analysis of a series of video frames from a well-known video game, that it is possible to analyse high-resolution videos in real-time by exploiting the speed-up of VoxLogicA-GPU, a recently developed GPU-based version of the tool, which is 1-2 orders of magnitude faster than its previous iteration. Potential applications of real-time video analysis include medical imaging applications such as ultrasound exams, and other video-based diagnostic techniques. More broadly speaking, this work can be the first step towards novel information retrieval methods suitable to find information in a declarative way, in possibly large collections of video streams.Source: From Data to Models and Back, edited by Bowles J., Broccia G., Pellungrini R., pp. 78–90, 2022
DOI: 10.1007/978-3-031-16011-0_6
Metrics:
See at:
ISTI Repository | link.springer.com | CNR ExploRA
2022
Conference article
Closed Access
On binding in the spatial logics for closure spaces
Bussi L., Ciancia V., Gadducci F., Latella D., Massink M.
We present two different extensions of the spatial logic for closure spaces (SLCS), and its spatio-temporal variant (?SLCS), with spa- tial quantification operators. The first concerns the existential quantifi- cation on individual points of a space. The second concerns the quantifi- cation on sets of points. The latter amounts to a form of quantification over atomic propositions, thus without the full power of second order logic. The spatial quantification operators are useful for reasoning about the existence of particular spatial objects in a space, their spatial rela- tion with respect to other spatial objects, and, in the spatio-temporal setting, to reason about the dynamic evolution of such spatial objects in time and space, including reasoning about newly introduced items. In this preliminary study we illustrate the expressiveness of the operators by means of several small, but representative, examples.Source: ISoLA 2022 - 11th International Symposium, pp. 479–497, Rhodes, Greece, 22-30/10/2022
DOI: 10.1007/978-3-031-19849-6_27
Metrics:
Bussi L., Ciancia V., Gadducci F., Latella D., Massink M.
We present two different extensions of the spatial logic for closure spaces (SLCS), and its spatio-temporal variant (?SLCS), with spa- tial quantification operators. The first concerns the existential quantifi- cation on individual points of a space. The second concerns the quantifi- cation on sets of points. The latter amounts to a form of quantification over atomic propositions, thus without the full power of second order logic. The spatial quantification operators are useful for reasoning about the existence of particular spatial objects in a space, their spatial rela- tion with respect to other spatial objects, and, in the spatio-temporal setting, to reason about the dynamic evolution of such spatial objects in time and space, including reasoning about newly introduced items. In this preliminary study we illustrate the expressiveness of the operators by means of several small, but representative, examples.Source: ISoLA 2022 - 11th International Symposium, pp. 479–497, Rhodes, Greece, 22-30/10/2022
DOI: 10.1007/978-3-031-19849-6_27
Metrics:
See at:
link.springer.com | CNR ExploRA
2022
Report
Open Access
On the expressive power of IMLC and ISLCS
Ciancia V., Latella D., Massink M., De Vink E. P.
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.Source: ISTI Technical Report, ISTI-2022-TR/021, 2022
DOI: 10.32079/isti-tr-2022/021
Metrics:
Ciancia V., Latella D., Massink M., De Vink E. P.
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.Source: ISTI Technical Report, ISTI-2022-TR/021, 2022
DOI: 10.32079/isti-tr-2022/021
Metrics:
See at:
ISTI Repository | CNR ExploRA
2022
Journal article
Open Access
Geometric model checking of continuous space
Bezhanishvili N., Ciancia V., Gabelaia D., Grilletti G., Latella D., Massink M.
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.Source: Logical Methods in Computer Science 18 (2022): 7:1–7:38. doi:10.46298/LMCS-18(4:7)2022
DOI: 10.46298/lmcs-18(4:7)2022
Metrics:
Bezhanishvili N., Ciancia V., Gabelaia D., Grilletti G., Latella D., Massink M.
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.Source: Logical Methods in Computer Science 18 (2022): 7:1–7:38. doi:10.46298/LMCS-18(4:7)2022
DOI: 10.46298/lmcs-18(4:7)2022
Metrics:
See at:
lmcs.episciences.org | ISTI Repository | CNR ExploRA
2021
Conference article
Open Access
Feasibility of Spatial Model Checking for Nevus Segmentation
Belmonte G., Broccia G., Ciancia V., Latella D., Massink M.
Recently developed spatial and spatio-temporal model checking techniques have a wide range of application domains, among which large scale distributed systems as well as 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 may facilitate the work of professionals in this domain, while supporting explainability, easy replicability and exchange of medical image analysis methods. In recent work, spatial model-checking has been applied to the 3D contouring of brain tumours and related oedema in magnetic resonance images of the brain. In the present paper we address the contouring of 2D images of nevi. One of the challenges of contouring nevi is that they show considerable inhomogeneity in shape, colour, texture and size. In addition these images often include also extraneous elements such as hairs, patches and rulers. To deal with this challenge we explore the use of a texture similarity operator in combination with spatial logic operators. We investigate the feasibility of our technique on images of a large public database. We compare the results with associated ground truth segmentation provided by domain experts; the results are very promising, both from the quality and from the performance point of view.Source: FormaliSE: International Conference on Formal Methods in Software Engineering, pp. 1–12, 18-21/05/2021
DOI: 10.1109/formalise52586.2021.00007
Metrics:
Belmonte G., Broccia G., Ciancia V., Latella D., Massink M.
Recently developed spatial and spatio-temporal model checking techniques have a wide range of application domains, among which large scale distributed systems as well as 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 may facilitate the work of professionals in this domain, while supporting explainability, easy replicability and exchange of medical image analysis methods. In recent work, spatial model-checking has been applied to the 3D contouring of brain tumours and related oedema in magnetic resonance images of the brain. In the present paper we address the contouring of 2D images of nevi. One of the challenges of contouring nevi is that they show considerable inhomogeneity in shape, colour, texture and size. In addition these images often include also extraneous elements such as hairs, patches and rulers. To deal with this challenge we explore the use of a texture similarity operator in combination with spatial logic operators. We investigate the feasibility of our technique on images of a large public database. We compare the results with associated ground truth segmentation provided by domain experts; the results are very promising, both from the quality and from the performance point of view.Source: FormaliSE: International Conference on Formal Methods in Software Engineering, pp. 1–12, 18-21/05/2021
DOI: 10.1109/formalise52586.2021.00007
Metrics:
See at:
ISTI Repository | www.computer.org | CNR ExploRA
2021
Report
Open Access
Geometric Model Checking of Continuous Space
Bezhanishvili N., Ciancia V., Gabelaia D., Grilletti G., Latella D., Massink M.
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.Source: Research report, IT- MaTTerS, PRIN 2017FTXR7S, 2021
Bezhanishvili N., Ciancia V., Gabelaia D., Grilletti G., Latella D., Massink M.
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.Source: Research report, IT- MaTTerS, PRIN 2017FTXR7S, 2021
See at:
arxiv.org | ISTI Repository | CNR ExploRA
2021
Report
Open Access
On Bisimilarities for Closure Spaces - Preliminary Version
Ciancia V., Latella D., Massink M., De Vink E.
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.Source: Research report, ITMaTTerS, PRIN 2017FTXR7S, 2021
Ciancia V., Latella D., Massink M., De Vink E.
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.Source: Research report, ITMaTTerS, PRIN 2017FTXR7S, 2021
See at:
arxiv.org | ISTI Repository | CNR ExploRA
2021
Conference article
Open Access
Towards a spatial model checker on GPU
Bussi L., Ciancia V., Gadducci F.
The tool VoxLogicA merges the state-of-the-art library of computational imaging algorithms ITK with the combination of declarative specification and optimised execution provided by spatial logic model checking. The analysis of an existing benchmark for segmentation of brain tumours via a simple logical specification reached very high accuracy. We introduce a new, GPU-based version of VoxLogicA and present preliminary results on its implementation, scalability, and applications.Source: FORTE 2021 - 41st International Conference on Formal Techniques for Distributed Objects, Components, and Systems, pp. 188–196, Online conference, 15-17/06/2021
DOI: 10.1007/978-3-030-78089-0_12
Metrics:
Bussi L., Ciancia V., Gadducci F.
The tool VoxLogicA merges the state-of-the-art library of computational imaging algorithms ITK with the combination of declarative specification and optimised execution provided by spatial logic model checking. The analysis of an existing benchmark for segmentation of brain tumours via a simple logical specification reached very high accuracy. We introduce a new, GPU-based version of VoxLogicA and present preliminary results on its implementation, scalability, and applications.Source: FORTE 2021 - 41st International Conference on Formal Techniques for Distributed Objects, Components, and Systems, pp. 188–196, Online conference, 15-17/06/2021
DOI: 10.1007/978-3-030-78089-0_12
Metrics:
See at:
ISTI Repository | link.springer.com | CNR ExploRA
2021
Conference article
Closed Access
A hands-on introduction to spatial model checking using VoxLogicA
Ciancia V., Belmonte G., Latella D., Massink M.
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.Source: SPIN 2021 - 27th International Symposium on Model Checking Software, pp. 22–41, Online conference, 12/07/2021
DOI: 10.1007/978-3-030-84629-9_2
Metrics:
Ciancia V., Belmonte G., Latella D., Massink M.
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.Source: SPIN 2021 - 27th International Symposium on Model Checking Software, pp. 22–41, Online conference, 12/07/2021
DOI: 10.1007/978-3-030-84629-9_2
Metrics:
See at:
link.springer.com | CNR ExploRA
2021
Conference article
Open Access
Spatial Model Checking for Smart Stations: Research Challenges
Ter Beek M. H., Ciancia V., Latella D., Massink M., Spagnolo G. O.
In this position paper, we discuss the introduction of spatial verification techniques in an application scenario from smart stations, viz. analysing the user experience with respect to the lighting conditions of station areas. This is a case study in industrial projects. We discuss three challenging use cases for the application of spatial model checking in this setting. First, we envision how to use the spatial model checker VoxLogicA, which can analyse both 2D and 3D voxel-based maps, to explore the areas that users can visit in a station area and to characterise them with respect to their illumination conditions. This is aimed at monitoring a smart station. We also ideate statistical spatio-temporal model checking of the design of energy-saving protocols, exploiting the modelling of user preferences. Finally, we discuss the idea of quantifying the impact of design changes, based on the logs of smart stations, to identify and measure the incidence of undesired events (e.g. non-illuminated platforms where a train is passing by) before and after each change.Source: FMICS 2021 - 26th International Conference on Formal Methods for Industrial Critical Systems, pp. 39–47, Online conference, 24-26/08/2021
DOI: 10.1007/978-3-030-85248-1_3
Metrics:
Ter Beek M. H., Ciancia V., Latella D., Massink M., Spagnolo G. O.
In this position paper, we discuss the introduction of spatial verification techniques in an application scenario from smart stations, viz. analysing the user experience with respect to the lighting conditions of station areas. This is a case study in industrial projects. We discuss three challenging use cases for the application of spatial model checking in this setting. First, we envision how to use the spatial model checker VoxLogicA, which can analyse both 2D and 3D voxel-based maps, to explore the areas that users can visit in a station area and to characterise them with respect to their illumination conditions. This is aimed at monitoring a smart station. We also ideate statistical spatio-temporal model checking of the design of energy-saving protocols, exploiting the modelling of user preferences. Finally, we discuss the idea of quantifying the impact of design changes, based on the logs of smart stations, to identify and measure the incidence of undesired events (e.g. non-illuminated platforms where a train is passing by) before and after each change.Source: FMICS 2021 - 26th International Conference on Formal Methods for Industrial Critical Systems, pp. 39–47, Online conference, 24-26/08/2021
DOI: 10.1007/978-3-030-85248-1_3
Metrics:
See at:
ISTI Repository | link.springer.com | CNR ExploRA
2021
Report
Open Access
A graphical user interface for medical image analysis with declarative spatial logic - Cognitive and memory load evaluation
Broccia G., Ciancia V., Latella D., Massink M.
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.Source: ISTI Technical Report, ISTI-2021-TR/012, pp.1–39, 2021
DOI: 10.32079/isti-tr-2021/012
Metrics:
Broccia G., Ciancia V., Latella D., Massink M.
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.Source: ISTI Technical Report, ISTI-2021-TR/012, pp.1–39, 2021
DOI: 10.32079/isti-tr-2021/012
Metrics:
See at:
ISTI Repository | CNR ExploRA
2021
Conference article
Open Access
Querying medical imaging datasets using spatial logics (Position paper)
Belmonte G., Broccia G., Bussi L., Ciancia V., Latella D., Massink M.
Nowadays a plethora of health data is available for clinical and research usage. Such existing datasets can be augmented through artificial-intelligence-based methods by automatic, personalised annotations and recommendations. This huge amount of data lends itself to new usage scenarios outside the boundaries where it was created; just to give some examples: to aggregate data sources in order to make research work more relevant; to incorporate a diversity of datasets in training of Machine Learning algorithms; to support expert decisions in telemedicine. In such a context, there is a growing need for a paradigm shift towards means to interrogate medical databases in a semantically meaningful way, fulfilling privacy and legal requirements, and transparently with respect to ethical concerns. In the specific domain of Medical Imaging, in this paper we sketch a research plan devoted to the definition and implementation of query languages that can unambiguously express semantically rich queries on possibly multi-dimensional images, in a human-readable, expert-friendly and concise way. Our approach is based on querying images using Topological Spatial Logics, building upon a novel spatial model checker called VoxLogicA, to execute such queries in a fully automated way.Source: MEDI 2021 - Advances in Model and Data Engineering in the Digitalization Era, pp. 285–301, Tallinn, Estonia, 21-23/06/2021
DOI: 10.1007/978-3-030-87657-9_22
Metrics:
Belmonte G., Broccia G., Bussi L., Ciancia V., Latella D., Massink M.
Nowadays a plethora of health data is available for clinical and research usage. Such existing datasets can be augmented through artificial-intelligence-based methods by automatic, personalised annotations and recommendations. This huge amount of data lends itself to new usage scenarios outside the boundaries where it was created; just to give some examples: to aggregate data sources in order to make research work more relevant; to incorporate a diversity of datasets in training of Machine Learning algorithms; to support expert decisions in telemedicine. In such a context, there is a growing need for a paradigm shift towards means to interrogate medical databases in a semantically meaningful way, fulfilling privacy and legal requirements, and transparently with respect to ethical concerns. In the specific domain of Medical Imaging, in this paper we sketch a research plan devoted to the definition and implementation of query languages that can unambiguously express semantically rich queries on possibly multi-dimensional images, in a human-readable, expert-friendly and concise way. Our approach is based on querying images using Topological Spatial Logics, building upon a novel spatial model checker called VoxLogicA, to execute such queries in a fully automated way.Source: MEDI 2021 - Advances in Model and Data Engineering in the Digitalization Era, pp. 285–301, Tallinn, Estonia, 21-23/06/2021
DOI: 10.1007/978-3-030-87657-9_22
Metrics:
See at:
ISTI Repository | link.springer.com | link.springer.com | CNR ExploRA
2020
Report
Open Access
Towards spatial bisimilarity for closure models: logical and coalgebraic characterisations
Ciancia V., Latella D., Massink M., De Vink E.
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.Source: ISTI Technical Reports 015/2020, 2020, 2020
DOI: 10.32079/isti-tr-2020/015
Metrics:
Ciancia V., Latella D., Massink M., De Vink E.
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.Source: ISTI Technical Reports 015/2020, 2020, 2020
DOI: 10.32079/isti-tr-2020/015
Metrics:
See at:
ISTI Repository | CNR ExploRA
2020
Report
Open Access
Using spatial logic and model checking for nevus segmentation
Belmonte G., Broccia G., Ciancia V., Latella D., Massink M.
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.Source: ISTI Technical Reports 2020/017, 2020
DOI: 10.32079/isti-tr-2020/017
Metrics:
Belmonte G., Broccia G., Ciancia V., Latella D., Massink M.
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.Source: ISTI Technical Reports 2020/017, 2020
DOI: 10.32079/isti-tr-2020/017
Metrics:
See at:
ISTI Repository | CNR ExploRA
2020
Report
Open Access
A spatial model checker in GPU (extended version)
Bussi L., Ciancia V., Gadducci F.
The tool voxlogica merges the state-of-the-art library of computational imaging algorithms ITK with the combination of declarative specification and optimised execution provided by spatial logic model checking. The analysis of an existing benchmark for segmentation of brain tumours via a simple logical specification reached state-of-the-art accuracy. We present a new, GPU-based version of voxlogica and discuss its implementation, scalability, and applications.Source: ISTI Research report, IT- MaTTerS, 2020
Bussi L., Ciancia V., Gadducci F.
The tool voxlogica merges the state-of-the-art library of computational imaging algorithms ITK with the combination of declarative specification and optimised execution provided by spatial logic model checking. The analysis of an existing benchmark for segmentation of brain tumours via a simple logical specification reached state-of-the-art accuracy. We present a new, GPU-based version of voxlogica and discuss its implementation, scalability, and applications.Source: ISTI Research report, IT- MaTTerS, 2020
See at:
arxiv.org | ISTI Repository | CNR ExploRA
2019
Conference article
Open Access
VoxLogicA: a spatial model checker for declarative image analysis
Belmonte G., Ciancia V., Latella D., Massink M.
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 easy replicability. Furthermore, due to a two-orders-of-magnitude speedup compared to the existing generalpurpose 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.Source: TACAS 2019 - 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 281–298, Prague, Czech Republic, 06-11 April 2019
DOI: 10.1007/978-3-030-17462-0_16
Metrics:
Belmonte G., Ciancia V., Latella D., Massink M.
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 easy replicability. Furthermore, due to a two-orders-of-magnitude speedup compared to the existing generalpurpose 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.Source: TACAS 2019 - 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 281–298, Prague, Czech Republic, 06-11 April 2019
DOI: 10.1007/978-3-030-17462-0_16
Metrics:
See at:
doi.org | link.springer.com | link.springer.com | ISTI Repository | CNR ExploRA
2019
Contribution to book
Open Access
Embedding RCC8D in the collective spatial logic CSLCS
Ciancia V., Latella D., Massink M.
Discrete mereotopology is a logical theory for the specification of qualitative spatial functions and relations defined over a discrete space, intended as a set of basic elements, the pixels, with an adjacency relation defined over it. The notions of interest are that of region, intended as an arbitrary aggregate of pixels, and of specific relations between regions. The mereotopological theory RCC8D extends the mereological theory RCC5D--a theory of region parthood for discrete spaces--with the topological notion of connection and the remaining relations (disconnection, external connection, tangential and nontangential proper parthood and their inverses). In this paper, we propose an encoding of RCC8D into CSLCS, the collective extension of the Spatial Logic of Closure Spaces SLCS. We show how topochecker, a model-checker for CSLCS, can be used for effectively checking the existence of a RCC8D relation between two given regions of a discrete space.Source: Models, Languages, and Tools for Concurrent and Distributed Programming - Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday, edited by Michele Boreale; Flavio Corradini; Michele Loreti; Rosario Pugliese, pp. 260–277. Cham Heidelberg New York Dordrecht London: Springer, 2019
DOI: 10.1007/978-3-030-21485-2_15
Metrics:
Ciancia V., Latella D., Massink M.
Discrete mereotopology is a logical theory for the specification of qualitative spatial functions and relations defined over a discrete space, intended as a set of basic elements, the pixels, with an adjacency relation defined over it. The notions of interest are that of region, intended as an arbitrary aggregate of pixels, and of specific relations between regions. The mereotopological theory RCC8D extends the mereological theory RCC5D--a theory of region parthood for discrete spaces--with the topological notion of connection and the remaining relations (disconnection, external connection, tangential and nontangential proper parthood and their inverses). In this paper, we propose an encoding of RCC8D into CSLCS, the collective extension of the Spatial Logic of Closure Spaces SLCS. We show how topochecker, a model-checker for CSLCS, can be used for effectively checking the existence of a RCC8D relation between two given regions of a discrete space.Source: Models, Languages, and Tools for Concurrent and Distributed Programming - Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday, edited by Michele Boreale; Flavio Corradini; Michele Loreti; Rosario Pugliese, pp. 260–277. Cham Heidelberg New York Dordrecht London: Springer, 2019
DOI: 10.1007/978-3-030-21485-2_15
Metrics:
See at:
ISTI Repository | doi.org | link.springer.com | CNR ExploRA
2019
Contribution to book
Open Access
Innovating Medical Image Analysis via Spatial Logics
Belmonte G., Ciancia V., Latella D., Massink M.
Current computer-assisted medical imaging for the planning of radiotherapy requires high-level mathematical and computational skills. These are often paired with the case-by-case integration of highly specialised technologies. The lack of modularity at the right level of abstraction in this field hinders research, collaboration and transfer of expertise among medical physicists, engineers and technicians. The longer term aim of the introduction of spatial logics and spatial model checking in medical imaging is to provide an open platform introducing declarative medical image analysis. This will provide domain experts with a convenient and very concise way to specify contouring and segmentation operations, grounded on the solid mathematical foundations of Topological Spatial Logics. We show preliminary results, obtained using the spatial model checker VoxLogicA, for the automatic identification of specific brain tissues in a healthy brain and we discuss a selection of challenges for spatial model checking for medical imaging.Source: From Software Engineering to Formal Methods and Tools, and Back, edited by ter Beek M.H.; Fantechi A.; Semini L. (eds.), pp. 85–109. Berlin: Springer, 2019
DOI: 10.1007/978-3-030-30985-5_7
Metrics:
Belmonte G., Ciancia V., Latella D., Massink M.
Current computer-assisted medical imaging for the planning of radiotherapy requires high-level mathematical and computational skills. These are often paired with the case-by-case integration of highly specialised technologies. The lack of modularity at the right level of abstraction in this field hinders research, collaboration and transfer of expertise among medical physicists, engineers and technicians. The longer term aim of the introduction of spatial logics and spatial model checking in medical imaging is to provide an open platform introducing declarative medical image analysis. This will provide domain experts with a convenient and very concise way to specify contouring and segmentation operations, grounded on the solid mathematical foundations of Topological Spatial Logics. We show preliminary results, obtained using the spatial model checker VoxLogicA, for the automatic identification of specific brain tissues in a healthy brain and we discuss a selection of challenges for spatial model checking for medical imaging.Source: From Software Engineering to Formal Methods and Tools, and Back, edited by ter Beek M.H.; Fantechi A.; Semini L. (eds.), pp. 85–109. Berlin: Springer, 2019
DOI: 10.1007/978-3-030-30985-5_7
Metrics:
See at:
ISTI Repository | doi.org | link.springer.com | CNR ExploRA
2019
Journal article
Open Access
Spatial logics and model checking for medical imaging
Banci Buonamici F., Belmonte G., Ciancia V., Latella D., Massink M.
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 distance-based 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 an example of analysis of Magnetic Resonance images: segmentation of glioblastoma and its oedema.Source: International journal on software tools for technology transfer (Internet) 22 (2019): 195–217. doi:10.1007/s10009-019-00511-9
DOI: 10.1007/s10009-019-00511-9
Metrics:
Banci Buonamici F., Belmonte G., Ciancia V., Latella D., Massink M.
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 distance-based 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 an example of analysis of Magnetic Resonance images: segmentation of glioblastoma and its oedema.Source: International journal on software tools for technology transfer (Internet) 22 (2019): 195–217. doi:10.1007/s10009-019-00511-9
DOI: 10.1007/s10009-019-00511-9
Metrics:
See at:
ISTI Repository | International Journal on Software Tools for Technology Transfer | link.springer.com | CNR ExploRA
2019
Contribution to conference
Closed Access
VoxLogicA: Voxel-based Logical Analyser
Belmonte G., Ciancia V., Latella D., Massink M.
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.Source: ESMRMB 2019, 36th Annual Scientific Meeting, pp. 417–418, Rotterdam, 3/10/2019-5/10/2019
DOI: 10.1007/s10334-019-00756-0
Project(s): B-Q MINDED
Metrics:
Belmonte G., Ciancia V., Latella D., Massink M.
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.Source: ESMRMB 2019, 36th Annual Scientific Meeting, pp. 417–418, Rotterdam, 3/10/2019-5/10/2019
DOI: 10.1007/s10334-019-00756-0
Project(s): B-Q MINDED
Metrics:
See at:
Magnetic Resonance Materials in Physics Biology and Medicine | link.springer.com | CNR ExploRA
2019
Contribution to book
Open Access
Omega-Automata: A Coalgebraic Perspective on Regular omega-Languages
Ciancia V., Venema Y.
In this work, we provide a simple coalgebraic characterisation of regular ?-languages based on languages of lassos, and prove a number of related mathematical results, framed into the theory of a new kind of automata called Ohm-automata. In earlier work we introduced Ohm-automata as two-sorted structures that naturally operate on lassos, pairs of words encoding ultimately periodic streams (infinite words). Here we extend the scope of these Ohm-automata by proposing them as a new kind of acceptor for arbitrary streams. We prove that Ohm-automata are expressively complete for the regular ?-languages. We show that, due to their coalgebraic nature, Ohm-automata share some attractive properties with deterministic automata operating on finite words, properties that other types of stream automata lack. In particular, we provide a simple, coalgebraic definition of bisimilarity between Ohm-automata that exactly captures language equivalence and allows for a simple minimization procedure. We also prove a coalgebraic Myhill-Nerode style theorem for lasso languages, and use this result, in combination with a closure property on stream languages called lasso determinacy, to give a characterization of regular ?-languages.Source: 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019), pp. 5:1–5:18, 2019
DOI: 10.4230/lipics.calco.2019.5
Metrics:
Ciancia V., Venema Y.
In this work, we provide a simple coalgebraic characterisation of regular ?-languages based on languages of lassos, and prove a number of related mathematical results, framed into the theory of a new kind of automata called Ohm-automata. In earlier work we introduced Ohm-automata as two-sorted structures that naturally operate on lassos, pairs of words encoding ultimately periodic streams (infinite words). Here we extend the scope of these Ohm-automata by proposing them as a new kind of acceptor for arbitrary streams. We prove that Ohm-automata are expressively complete for the regular ?-languages. We show that, due to their coalgebraic nature, Ohm-automata share some attractive properties with deterministic automata operating on finite words, properties that other types of stream automata lack. In particular, we provide a simple, coalgebraic definition of bisimilarity between Ohm-automata that exactly captures language equivalence and allows for a simple minimization procedure. We also prove a coalgebraic Myhill-Nerode style theorem for lasso languages, and use this result, in combination with a closure property on stream languages called lasso determinacy, to give a characterization of regular ?-languages.Source: 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019), pp. 5:1–5:18, 2019
DOI: 10.4230/lipics.calco.2019.5
Metrics:
See at:
drops.dagstuhl.de | ISTI Repository | CNR ExploRA
2019
Journal article
Open Access
VoxLogicA: a Spatial-Logic based tool for Declarative Image Analysis
Belmonte G., Ciancia V., Latella D., Massink M.
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.Source: ERCIM news 118 (2019): 12–13.
Project(s): QUANTICOL
Belmonte G., Ciancia V., Latella D., Massink M.
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.Source: ERCIM news 118 (2019): 12–13.
Project(s): QUANTICOL
See at:
ercim-news.ercim.eu | ISTI Repository | CNR ExploRA
2018
Journal article
Open Access
Spatio-temporal model checking of vehicular movement in public transport systems
Ciancia V., Gilmore S., Grilletti G., Latella D., Loreti M., Massink M.
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.Source: International journal on software tools for technology transfer (Internet) 20 (2018): 289–311. doi:10.1007/s10009-018-0483-8
DOI: 10.1007/s10009-018-0483-8
Project(s): QUANTICOL
Metrics:
Ciancia V., Gilmore S., Grilletti G., Latella D., Loreti M., Massink M.
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.Source: International journal on software tools for technology transfer (Internet) 20 (2018): 289–311. doi:10.1007/s10009-018-0483-8
DOI: 10.1007/s10009-018-0483-8
Project(s): QUANTICOL
Metrics:
See at:
Archivio istituzionale della ricerca - Università di Camerino | ISTI Repository | International Journal on Software Tools for Technology Transfer | Edinburgh Research Explorer | NARCIS | International Journal on Software Tools for Technology Transfer | CNR ExploRA
2018
Journal article
Open Access
Qualitative and quantitative monitoring of spatio-temporal properties with SSTL
Nenzi L., Bortolussi L., Ciancia V., Loreti M., Massink M.
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.Source: Logical Methods in Computer Science 14 (2018): 1–38. doi:10.23638/LMCS-14(4:2)2018
DOI: 10.23638/lmcs-14(4:2)2018
DOI: 10.48550/arxiv.1706.09334
Project(s): QUANTICOL
Metrics:
Nenzi L., Bortolussi L., Ciancia V., Loreti M., Massink M.
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.Source: Logical Methods in Computer Science 14 (2018): 1–38. doi:10.23638/LMCS-14(4:2)2018
DOI: 10.23638/lmcs-14(4:2)2018
DOI: 10.48550/arxiv.1706.09334
Project(s): QUANTICOL
Metrics:
See at:
arXiv.org e-Print Archive | Archivio istituzionale della ricerca - Università di Trieste | Archivio istituzionale della ricerca - Università di Camerino | Episciences | ISTI Repository | doi.org | doi.org | CNR ExploRA
2018
Conference article
Open Access
Statistical model checking of a moving block railway signalling scenario with Uppaal SMC. Experience and Outlook
Basile D., Ter Beek M. H., Ciancia V.
We present an experience in modelling and statistical model checking a satellite-based moving block signalling scenario from the railway industry with Uppaal SMC. This demonstrates the usability and applicability of Uppaal SMC in the railway domain. We also propose a promising direction for future work, in which we envision spatio-temporal analysis with Uppaal SMC.Source: ISoLA'18 - 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, pp. 372–391, Limassol, Cyprus, 5-9 November 2018
DOI: 10.1007/978-3-030-03421-4_24
Project(s): ASTRail
Metrics:
Basile D., Ter Beek M. H., Ciancia V.
We present an experience in modelling and statistical model checking a satellite-based moving block signalling scenario from the railway industry with Uppaal SMC. This demonstrates the usability and applicability of Uppaal SMC in the railway domain. We also propose a promising direction for future work, in which we envision spatio-temporal analysis with Uppaal SMC.Source: ISoLA'18 - 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, pp. 372–391, Limassol, Cyprus, 5-9 November 2018
DOI: 10.1007/978-3-030-03421-4_24
Project(s): ASTRail
Metrics:
See at:
ISTI Repository | doi.org | link.springer.com | CNR ExploRA
2017
Report
Open Access
QUANTICOL - The QUANTICOL software tool suite for modelling smart cities (Final)
Ciancia V., Latella D., Massink M., Nenzi L., Tribastone M., Vandin A.
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.Source: Project report, QUANTICOL, Deliverable D5.3, 2017
Project(s): QUANTICOL
Ciancia V., Latella D., Massink M., Nenzi L., Tribastone M., Vandin A.
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.Source: Project report, QUANTICOL, Deliverable D5.3, 2017
Project(s): QUANTICOL
See at:
ISTI Repository | CNR ExploRA
2017
Report
Open Access
QUANTICOL - A quantitative approach to management and design of collective and adaptive behaviours
Massink M., Ter Beek M. H., Bortolussi L., Ciancia V., Gnesi S., Hillston J., Latella D., Loreti M., Tribastone M., Vandin A.
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.Source: Project report, QUANTICOL, Deliverable D3.3, 2017
Project(s): QUANTICOL
Massink M., Ter Beek M. H., Bortolussi L., Ciancia V., Gnesi S., Hillston J., Latella D., Loreti M., Tribastone M., Vandin A.
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.Source: Project report, QUANTICOL, Deliverable D3.3, 2017
Project(s): QUANTICOL
See at:
blog.inf.ed.ac.uk | ISTI Repository | CNR ExploRA
2017
Report
Open Access
ISTI Young Research Award 2017
Barsocchi P., Basile D., Candela L., Ciancia V., Delle Piane M., Esuli A., Ferrari A., Girardi M., Guidotti R., Lonetti F., Moroni D., Nardini F. M., Rinzivillo S., Vadicamo L.
The ISTI Young Researcher Award is an award for young people of Institute of Information Science and Technologies (ISTI) with high scientific production. In particular, the award is granted to young staff members (less than 35 years old) by assessing the yearly scientific production of the year preceding the award. This report documents procedure and results of the 2017 edition of the award.Source: ISTI Technical reports, 2017
Barsocchi P., Basile D., Candela L., Ciancia V., Delle Piane M., Esuli A., Ferrari A., Girardi M., Guidotti R., Lonetti F., Moroni D., Nardini F. M., Rinzivillo S., Vadicamo L.
The ISTI Young Researcher Award is an award for young people of Institute of Information Science and Technologies (ISTI) with high scientific production. In particular, the award is granted to young staff members (less than 35 years old) by assessing the yearly scientific production of the year preceding the award. This report documents procedure and results of the 2017 edition of the award.Source: ISTI Technical reports, 2017
See at:
ISTI Repository | CNR ExploRA
2017
Journal article
Restricted
Exploring nominal cellular automata
Bolognesi T., Ciancia V.
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".Source: Journal of Logical and Algebraic Methods in Programming [online] 93 (2017): 23–41. doi:10.1016/j.jlamp.2017.08.001
DOI: 10.1016/j.jlamp.2017.08.001
Project(s): QUANTICOL
Metrics:
Bolognesi T., Ciancia V.
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".Source: Journal of Logical and Algebraic Methods in Programming [online] 93 (2017): 23–41. doi:10.1016/j.jlamp.2017.08.001
DOI: 10.1016/j.jlamp.2017.08.001
Project(s): QUANTICOL
Metrics:
See at:
Journal of Logical and Algebraic Methods in Programming | www.sciencedirect.com | CNR ExploRA
2017
Report
Open Access
QUANTICOL - The QUANTICOL software tool suite for modelling smart cities
Ciancia V., Latella D., Massink M.
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.Source: Project report, QUANTICOL, Deliverable D5.3, 2017
Project(s): QUANTICOL
Ciancia V., Latella D., Massink M.
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.Source: Project report, QUANTICOL, Deliverable D5.3, 2017
Project(s): QUANTICOL
See at:
blog.inf.ed.ac.uk | ISTI Repository | CNR ExploRA
2017
Report
Restricted
QUANTICOL - Combining spatial verification with model reduction and relating local and global views
Massink M., Ter Beek M., Bortolussi L., Ciancia V., Gnesi S., Hillston J., Latella D., Loreti M., Tribastone M., Vandin A.
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.Source: Project report, QUANTICOL, Deliverable D3.3, 2017
Project(s): QUANTICOL
Massink M., Ter Beek M., Bortolussi L., Ciancia V., Gnesi S., Hillston J., Latella D., Loreti M., Tribastone M., Vandin A.
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.Source: Project report, QUANTICOL, Deliverable D3.3, 2017
Project(s): QUANTICOL
See at:
blog.inf.ed.ac.uk | CNR ExploRA
2017
Report
Open Access
Spatial model checking for medical imaging - Preliminary version
Banci Bonamici F., Belmonte G., Ciancia V., Latella D., Massink M.
The application of the topochecker spatial-model-cheker to medical imaging is described.Source: ISTI Technical reports, 2017
Project(s): QUANTICOL
Banci Bonamici F., Belmonte G., Ciancia V., Latella D., Massink M.
The application of the topochecker spatial-model-cheker to medical imaging is described.Source: ISTI Technical reports, 2017
Project(s): QUANTICOL
See at:
ISTI Repository | CNR ExploRA
2017
Contribution to journal
Open Access
A topological method for automatic segmentation of glioblastoma in MR FLAIR for radiotherapy
Belmonte G., Ciancia V., Latella D., Massink M., Biondi M., De Otto G., Nardone V., Rubino G., Vanzi E., Banci Buonamici F.
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.Source: Magma (New York, N.Y.) 30 (2017): 437–438. doi:10.1007/s10334-017-0634-z
DOI: 10.1007/s10334-017-0634-z
Metrics:
Belmonte G., Ciancia V., Latella D., Massink M., Biondi M., De Otto G., Nardone V., Rubino G., Vanzi E., Banci Buonamici F.
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.Source: Magma (New York, N.Y.) 30 (2017): 437–438. doi:10.1007/s10334-017-0634-z
DOI: 10.1007/s10334-017-0634-z
Metrics:
See at:
Magnetic Resonance Materials in Physics Biology and Medicine | Magnetic Resonance Materials in Physics Biology and Medicine | link.springer.com | CNR ExploRA
2016
Report
Open Access
On-the-fly mean-field model-checking for attribute-based coordination preliminary version. Quanticol technical report TR-QC-01-2016
Ciancia V., Latella D., Massink M.
Typical Collective Adaptive Systems (CAS) consist of a large number of interacting objects that coordinate their activities in a decentralised and often implicit way. The design of such systems is challenging. It requires scalable analysis tools and techniques to check properties of proposed system designs before they are put into operation. A promising technique is Fast Mean- Field Approximated Model-checking. In particular, the FlyFast model-checker uses an on-the-fly algorithm for bounded PCTL model-checking of selected individuals in the context of very large populations whose global behaviour is approximated using deterministic limit techniques. Recently, specific modelling languages have been proposed for CAS. A key feature of such languages is the attribute-based interaction paradigm. In this paper we present a simple non value-passing version of an attribute-based coordination language as a front-end for FlyFast. Its formal probabilistic semantics is provided and a translation to the original FlyFast language is presented and proved correct. Application examples are also provided.Source: ISTI Technical reports, 2016
Project(s): QUANTICOL
Ciancia V., Latella D., Massink M.
Typical Collective Adaptive Systems (CAS) consist of a large number of interacting objects that coordinate their activities in a decentralised and often implicit way. The design of such systems is challenging. It requires scalable analysis tools and techniques to check properties of proposed system designs before they are put into operation. A promising technique is Fast Mean- Field Approximated Model-checking. In particular, the FlyFast model-checker uses an on-the-fly algorithm for bounded PCTL model-checking of selected individuals in the context of very large populations whose global behaviour is approximated using deterministic limit techniques. Recently, specific modelling languages have been proposed for CAS. A key feature of such languages is the attribute-based interaction paradigm. In this paper we present a simple non value-passing version of an attribute-based coordination language as a front-end for FlyFast. Its formal probabilistic semantics is provided and a translation to the original FlyFast language is presented and proved correct. Application examples are also provided.Source: ISTI Technical reports, 2016
Project(s): QUANTICOL
See at:
ISTI Repository | CNR ExploRA
2016
Report
Open Access
ISTI young research award 2016
Barsocchi P., Candela L., Ciancia V., Dellepiane M., Esuli A., Girardi M., Girolami M., Guidotti R., Lonetti F., Malomo L., Moroni D., Nardini F. M., Palumbo F., Pappalardo L., Pascali M. A., Rinzivillo S.
The ISTI Young Researcher Award is an award for young people of Institute of Information Science and Technologies (ISTI) with high scientific production. In particular, the award is granted to young staff members (less than 35 years old) by assessing the yearly scientific production of the year preceding the award. This report documents procedure and results of the 2016 edition of the award.Source: ISTI Technical reports, 2016
Barsocchi P., Candela L., Ciancia V., Dellepiane M., Esuli A., Girardi M., Girolami M., Guidotti R., Lonetti F., Malomo L., Moroni D., Nardini F. M., Palumbo F., Pappalardo L., Pascali M. A., Rinzivillo S.
The ISTI Young Researcher Award is an award for young people of Institute of Information Science and Technologies (ISTI) with high scientific production. In particular, the award is granted to young staff members (less than 35 years old) by assessing the yearly scientific production of the year preceding the award. This report documents procedure and results of the 2016 edition of the award.Source: ISTI Technical reports, 2016
See at:
ISTI Repository | CNR ExploRA
2016
Conference article
Open Access
On-the-fly mean-field model-checking for attribute-based coordination
Ciancia V., Latella D., Massink M.
Typical Collective Adaptive Systems (CAS) consist of a large number of interacting objects that coordinate their activities in a decentralised and often implicit way. The design of such systems is challenging, as it requires scalable analysis tools and methods to check properties of proposed system designs before they are put into operation. A promising technique is Fast Mean-Field Approximated Model-checking. The FlyFast model-checker uses an on-the-fly algorithm for bounded PCTL model-checking of selected individuals in the context of very large populations whose global behaviour is approximated using deterministic limit techniques. Recently, specific modelling languages have been proposed for CAS. A key feature of such languages is the attribute-based interaction paradigm. In this paper we present an attribute-based coordination language as a front-end for FlyFast. Its formal probabilistic semantics is provided and a translation to the original FlyFast language is given and proved correct. Application examples are also provided.Source: COORDINATION 2016 - DisCoTec 2016 - Coordination Models and Languages. 18th IFIP WG 6.1 International Conference, pp. 67–83, Heraklion, Crete, Greece, 6-9 June 2016
DOI: 10.1007/978-3-319-39519-7_5
Project(s): QUANTICOL
Metrics:
Ciancia V., Latella D., Massink M.
Typical Collective Adaptive Systems (CAS) consist of a large number of interacting objects that coordinate their activities in a decentralised and often implicit way. The design of such systems is challenging, as it requires scalable analysis tools and methods to check properties of proposed system designs before they are put into operation. A promising technique is Fast Mean-Field Approximated Model-checking. The FlyFast model-checker uses an on-the-fly algorithm for bounded PCTL model-checking of selected individuals in the context of very large populations whose global behaviour is approximated using deterministic limit techniques. Recently, specific modelling languages have been proposed for CAS. A key feature of such languages is the attribute-based interaction paradigm. In this paper we present an attribute-based coordination language as a front-end for FlyFast. Its formal probabilistic semantics is provided and a translation to the original FlyFast language is given and proved correct. Application examples are also provided.Source: COORDINATION 2016 - DisCoTec 2016 - Coordination Models and Languages. 18th IFIP WG 6.1 International Conference, pp. 67–83, Heraklion, Crete, Greece, 6-9 June 2016
DOI: 10.1007/978-3-319-39519-7_5
Project(s): QUANTICOL
Metrics:
See at:
hal.inria.fr | ISTI Repository | doi.org | Hyper Article en Ligne | link.springer.com | CNR ExploRA
2016
Contribution to book
Open Access
Spatial logic and spatial model checking for closure spaces
Ciancia V., Latella D., Loreti M., Massink M.
Spatial aspects of computation are 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 concurrent systems; however, properties of space are typically not explicitly taken into account. This tutorial provides an introduction to recent work on a topology-inspired approach to formal verification of spatial properties depending upon (physical) space. A logic is presented, stemming from the tradition of topological interpretations of modal logics, dating back to earlier logicians such as Tarski, where modalities describe neighbourhood. These topological definitions are lifted to the more general setting of closure spaces, also encompassing discrete, graph-based structures. The present tutorial illustrates the extension of the framework with a spatial surrounded operator, leading to the spatial logic for closure spaces SLCS, and its combination with the temporal logic CTL, leading to STLCS. The interplay of space and time permits one to define complex spatio-temporal properties. Both for the spatial and the spatio-temporal fragment efficient model-checking algorithms have been developed and their use on a number of case studies and examples is illustrated.Source: Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems, edited by Bernardo M., De Nicola R., Hillston J., pp. 156–201, 2016
DOI: 10.1007/978-3-319-34096-8_6
Project(s): QUANTICOL
Metrics:
Ciancia V., Latella D., Loreti M., Massink M.
Spatial aspects of computation are 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 concurrent systems; however, properties of space are typically not explicitly taken into account. This tutorial provides an introduction to recent work on a topology-inspired approach to formal verification of spatial properties depending upon (physical) space. A logic is presented, stemming from the tradition of topological interpretations of modal logics, dating back to earlier logicians such as Tarski, where modalities describe neighbourhood. These topological definitions are lifted to the more general setting of closure spaces, also encompassing discrete, graph-based structures. The present tutorial illustrates the extension of the framework with a spatial surrounded operator, leading to the spatial logic for closure spaces SLCS, and its combination with the temporal logic CTL, leading to STLCS. The interplay of space and time permits one to define complex spatio-temporal properties. Both for the spatial and the spatio-temporal fragment efficient model-checking algorithms have been developed and their use on a number of case studies and examples is illustrated.Source: Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems, edited by Bernardo M., De Nicola R., Hillston J., pp. 156–201, 2016
DOI: 10.1007/978-3-319-34096-8_6
Project(s): QUANTICOL
Metrics:
See at:
ISTI Repository | doi.org | link.springer.com | CNR ExploRA
2016
Conference article
Open Access
From collective adaptive systems to human centric computation and back: spatial model checking for medical imaging
Belmonte G., Ciancia V., Latella D., Massink M.
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.Source: FORECAST 2016 - Workshop on FORmal methods for the quantitative Evaluation of Collective Adaptive SysTems, pp. 81–92, Vienna, Austria, 8 July 2016
DOI: 10.4204/eptcs.217.10
DOI: 10.48550/arxiv.1607.02235
Project(s): QUANTICOL
Metrics:
Belmonte G., Ciancia V., Latella D., Massink M.
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.Source: FORECAST 2016 - Workshop on FORmal methods for the quantitative Evaluation of Collective Adaptive SysTems, pp. 81–92, Vienna, Austria, 8 July 2016
DOI: 10.4204/eptcs.217.10
DOI: 10.48550/arxiv.1607.02235
Project(s): QUANTICOL
Metrics:
See at:
arXiv.org e-Print Archive | Electronic Proceedings in Theoretical Computer Science | Electronic Proceedings in Theoretical Computer Science | Electronic Proceedings in Theoretical Computer Science | eptcs.web.cse.unsw.edu.au | ISTI Repository | doi.org | CNR ExploRA
2016
Conference article
Open Access
Nominal cellular automata
Bolognesi T., Ciancia V.
The 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. A preliminary investigation of the relations between Nominal Cellular Automata and Wolfram's Elementary Cellular Automata is also carried out.Source: ICE 2016 - 9th Interaction and Concurrency Experience, pp. 24–35, Heraklion, Crete, Greece, 8-9 June 2016
DOI: 10.4204/eptcs.223.2
DOI: 10.48550/arxiv.1608.03320
Project(s): QUANTICOL
Metrics:
Bolognesi T., Ciancia V.
The 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. A preliminary investigation of the relations between Nominal Cellular Automata and Wolfram's Elementary Cellular Automata is also carried out.Source: ICE 2016 - 9th Interaction and Concurrency Experience, pp. 24–35, Heraklion, Crete, Greece, 8-9 June 2016
DOI: 10.4204/eptcs.223.2
DOI: 10.48550/arxiv.1608.03320
Project(s): QUANTICOL
Metrics:
See at:
arXiv.org e-Print Archive | Electronic Proceedings in Theoretical Computer Science | Electronic Proceedings in Theoretical Computer Science | Electronic Proceedings in Theoretical Computer Science | eptcs.web.cse.unsw.edu.au | ISTI Repository | doi.org | CNR ExploRA
2016
Journal article
Open Access
Model checking spatial logics for closure spaces
Ciancia V., Latella D., Loreti M., Massink M.
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.Source: Logical Methods in Computer Science 12 (2016): 1–51. doi:10.2168/LMCS-12(4:2)2016
DOI: 10.2168/lmcs-12(4:2)2016
DOI: 10.48550/arxiv.1609.06513
Project(s): QUANTICOL
Metrics:
Ciancia V., Latella D., Loreti M., Massink M.
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.Source: Logical Methods in Computer Science 12 (2016): 1–51. doi:10.2168/LMCS-12(4:2)2016
DOI: 10.2168/lmcs-12(4:2)2016
DOI: 10.48550/arxiv.1609.06513
Project(s): QUANTICOL
Metrics:
See at:
arXiv.org e-Print Archive | Logical Methods in Computer Science | Archivio istituzionale della ricerca - Università di Camerino | Episciences | Logical Methods in Computer Science | ISTI Repository | doi.org | CNR ExploRA
2016
Conference article
Open Access
A tool-chain for statistical spatio-temporal model checking of bike sharing systems
Ciancia V., Latella D., Massink M., Paskauskas R., Vandin A.
Prominent examples of collective systems are often encountered when analysing smart cities and smart transportation systems. We propose a novel modelling and analysis approach combining statistical model checking, spatio-temporal logics, and simulation. The proposed methodology is applied to modelling and statistical analysis of user behaviour in bike sharing systems. We present a tool-chain that integrates the statistical analysis toolkit MultiVeStA, the spatio-temporal model checker topochecker, and a bike sharing systems simulator based on Markov renewal processes. The obtained tool allows one to estimate, up to a user-specified precision, the likelihood of specific spatio-temporal formulas, such as the formation of clusters of full stations and their temporal evolution.Source: Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. 7th International Symposium, pp. 657–673, Corfu, Greece, 10-14 October 2016
DOI: 10.1007/978-3-319-47166-2_46
Project(s): QUANTICOL
Metrics:
Ciancia V., Latella D., Massink M., Paskauskas R., Vandin A.
Prominent examples of collective systems are often encountered when analysing smart cities and smart transportation systems. We propose a novel modelling and analysis approach combining statistical model checking, spatio-temporal logics, and simulation. The proposed methodology is applied to modelling and statistical analysis of user behaviour in bike sharing systems. We present a tool-chain that integrates the statistical analysis toolkit MultiVeStA, the spatio-temporal model checker topochecker, and a bike sharing systems simulator based on Markov renewal processes. The obtained tool allows one to estimate, up to a user-specified precision, the likelihood of specific spatio-temporal formulas, such as the formation of clusters of full stations and their temporal evolution.Source: Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. 7th International Symposium, pp. 657–673, Corfu, Greece, 10-14 October 2016
DOI: 10.1007/978-3-319-47166-2_46
Project(s): QUANTICOL
Metrics:
See at:
ISTI Repository | doi.org | link.springer.com | CNR ExploRA
2016
Report
Open Access
ProgettISTI 2016
Banterle F., Barsocchi P., Candela L., Carlini E., Carrara F., Cassarà P., Ciancia V., Cintia P., Dellepiane M., Esuli A., Gabrielli L., Germanese D., Girardi M., Girolami M., Kavalionak H., Lonetti F., Lulli A., Moreo Fernandez A., Moroni D., Nardini F. M., Monteiro De Lira V. C., Palumbo F., Pappalardo L., Pascali M. A., Reggianini M., Righi M., Rinzivillo S., Russo D., Siotto E., Villa A.
ProgettISTI research project grant is an award for members of the Institute of Information Science and Technologies (ISTI) to provide support for innovative, original and multidisciplinary projects of high quality and potential. The choice of theme and the design of the research are entirely up to the applicants yet (i) the theme must fall under the ISTI research topics, (ii) the proposers of each project must be of diverse laboratories of the Institute and must contribute different expertise to the project idea, and (iii) project proposals should have a duration of 12 months. This report documents the procedure, the proposals and the results of the 2016 edition of the award. In this edition, ten project proposals have been submitted and three of them have been awarded.Source: ISTI Technical reports, 2016
Banterle F., Barsocchi P., Candela L., Carlini E., Carrara F., Cassarà P., Ciancia V., Cintia P., Dellepiane M., Esuli A., Gabrielli L., Germanese D., Girardi M., Girolami M., Kavalionak H., Lonetti F., Lulli A., Moreo Fernandez A., Moroni D., Nardini F. M., Monteiro De Lira V. C., Palumbo F., Pappalardo L., Pascali M. A., Reggianini M., Righi M., Rinzivillo S., Russo D., Siotto E., Villa A.
ProgettISTI research project grant is an award for members of the Institute of Information Science and Technologies (ISTI) to provide support for innovative, original and multidisciplinary projects of high quality and potential. The choice of theme and the design of the research are entirely up to the applicants yet (i) the theme must fall under the ISTI research topics, (ii) the proposers of each project must be of diverse laboratories of the Institute and must contribute different expertise to the project idea, and (iii) project proposals should have a duration of 12 months. This report documents the procedure, the proposals and the results of the 2016 edition of the award. In this edition, ten project proposals have been submitted and three of them have been awarded.Source: ISTI Technical reports, 2016
See at:
ISTI Repository | CNR ExploRA
2016
Report
Open Access
Scalable verification for spatial stochastic logics
Bortolussi L., Ciancia V., Gilmore S., Hillston J., Latella D., Loreti M., Massink M., Nenzi L., Paskauskas R., Tribastone M., Tschaikowski M.
This Internal Report describes the status of the work performed in the project on the extension of the theoretical foundations of scalable model-checking approaches with suitable notions of spatial verification. Various forms of scalable model-checking were developed during the first phase of Task 3.1 of WP3, including those based on mean-field and fluid flow techniques, and were presented in Deliverable 3.1. The focus of the present report is on forms of spatial verification based on model-checking techniques in which the effect of inhomogeneous spatial distribution of objects is taken into account. Several spatial logics have been developed and explored. The Spatial Logic for Closure Spaces (SLCS) is based on the formal framework of closure spaces. The latter include topological spaces but also discrete spaces such as graphs and therefore form a promising candidate for a uniform framework to develop spatial logics that can be applied to the various spatial representations presented in the deliverables of WP2. Closure spaces come with a well-developed theory and some powerful operators that turned out to be very useful both for the definition of the semantics of SLCS and for the development of spatial and spatio-temporal modelchecking algorithms. The spatial operators of SLCS have been also added to the Signal Temporal Logic (STL) to obtain Spatial Signal Temporal Logic (SSTL). In this case the spatial operators have been extended with spatial bounds based on distance measures and a quantitative semantics has been provided that is used to evaluate the robustness of the spatio-temporal formulas for signals. Spatial and spatio-temporal performance analysis measures have been explored for a simple PALOMA model of a group of robots and for a bike sharing model based on Markov Renewal Processes. The latter provides a simulation model of bike-sharing systems that includes users as agents. It also generates simulation traces with spatio-temporal information on bike stations that can be analysed using the prototype spatiotemporal model checkers that have been developed in the context of the project. A partial-differential approximation has been developed for spatial stochastic process algebra. The approach is validated on the well-known Lotka-Volterra model and shows an advantage in terms of computational efficiency compared to traditional numerical solutions. Finally, for what concerns scalable verification, the innovative model-checking approaches based on fluid approximation and on-the-fly mean-field techniques have been finalised. For the latter a prototype modelchecker, FlyFast, has been made available, which was described in Deliverable 5.2. QUANTICOLSource: ISTI Technical reports, 2016
Project(s): QUANTICOL
Bortolussi L., Ciancia V., Gilmore S., Hillston J., Latella D., Loreti M., Massink M., Nenzi L., Paskauskas R., Tribastone M., Tschaikowski M.
This Internal Report describes the status of the work performed in the project on the extension of the theoretical foundations of scalable model-checking approaches with suitable notions of spatial verification. Various forms of scalable model-checking were developed during the first phase of Task 3.1 of WP3, including those based on mean-field and fluid flow techniques, and were presented in Deliverable 3.1. The focus of the present report is on forms of spatial verification based on model-checking techniques in which the effect of inhomogeneous spatial distribution of objects is taken into account. Several spatial logics have been developed and explored. The Spatial Logic for Closure Spaces (SLCS) is based on the formal framework of closure spaces. The latter include topological spaces but also discrete spaces such as graphs and therefore form a promising candidate for a uniform framework to develop spatial logics that can be applied to the various spatial representations presented in the deliverables of WP2. Closure spaces come with a well-developed theory and some powerful operators that turned out to be very useful both for the definition of the semantics of SLCS and for the development of spatial and spatio-temporal modelchecking algorithms. The spatial operators of SLCS have been also added to the Signal Temporal Logic (STL) to obtain Spatial Signal Temporal Logic (SSTL). In this case the spatial operators have been extended with spatial bounds based on distance measures and a quantitative semantics has been provided that is used to evaluate the robustness of the spatio-temporal formulas for signals. Spatial and spatio-temporal performance analysis measures have been explored for a simple PALOMA model of a group of robots and for a bike sharing model based on Markov Renewal Processes. The latter provides a simulation model of bike-sharing systems that includes users as agents. It also generates simulation traces with spatio-temporal information on bike stations that can be analysed using the prototype spatiotemporal model checkers that have been developed in the context of the project. A partial-differential approximation has been developed for spatial stochastic process algebra. The approach is validated on the well-known Lotka-Volterra model and shows an advantage in terms of computational efficiency compared to traditional numerical solutions. Finally, for what concerns scalable verification, the innovative model-checking approaches based on fluid approximation and on-the-fly mean-field techniques have been finalised. For the latter a prototype modelchecker, FlyFast, has been made available, which was described in Deliverable 5.2. QUANTICOLSource: ISTI Technical reports, 2016
Project(s): QUANTICOL
See at:
ISTI Repository | CNR ExploRA
2016
Report
Open Access
On spatio-temporal model-checking of vehicular movement in public transport systems
Ciancia V., Gilmore S., Grilletti G., Latella D., Loreti M., Massink M.
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.Source: ISTI Technical reports, 2016
Project(s): QUANTICOL
Ciancia V., Gilmore S., Grilletti G., Latella D., Loreti M., Massink M.
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.Source: ISTI Technical reports, 2016
Project(s): QUANTICOL
See at:
ISTI Repository | CNR ExploRA
2016
Report
Open Access
Model checking spatial logics for closure spaces. Extended version
Ciancia V., Latella D., Loreti M., Massink M.
Spatial aspects of computation are becoming increasingly relevant in Computer Science, es- pecially in the eld of collective adaptive systems and when dealing with systems distributed in physical space. Traditional formal verication techniques are well suited to analyse the temporal evolution of programs; however, properties of space are typically not taken into account explic- itly. We present a topology-based approach to formal verication of spatial properties depending upon physical space. We dene 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 denitions to the more general setting of closure spaces, also encompassing discrete, graph-based structures. We extend the framework with a spa- tial 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 dene ecient model checking procedures, both for the individual and the collective spatial fragments of the logic and provide a proof-of-concept tool.Source: ISTI Technical reports, 2016
Project(s): QUANTICOL
Ciancia V., Latella D., Loreti M., Massink M.
Spatial aspects of computation are becoming increasingly relevant in Computer Science, es- pecially in the eld of collective adaptive systems and when dealing with systems distributed in physical space. Traditional formal verication techniques are well suited to analyse the temporal evolution of programs; however, properties of space are typically not taken into account explic- itly. We present a topology-based approach to formal verication of spatial properties depending upon physical space. We dene 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 denitions to the more general setting of closure spaces, also encompassing discrete, graph-based structures. We extend the framework with a spa- tial 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 dene ecient model checking procedures, both for the individual and the collective spatial fragments of the logic and provide a proof-of-concept tool.Source: ISTI Technical reports, 2016
Project(s): QUANTICOL
See at:
ISTI Repository | CNR ExploRA
2016
Journal article
Open Access
Spatio-temporal model-checking for collective adaptive systems
Ciancia V., Latella D., Loreti M., Massink M.
Spatial aspects of computation are becoming increasingly relevant when dealing with systems distributed in physical space. Traditional formal verification techniques are well suited to analyse the temporal evolution of system models; however, properties of space are typically not taken into account explicitly. In this position paper we briefly review some of the recent developments of spatial and spatio-temporal model-checking in the context of the European research project QUANTICOL funded by the FET-Proactive programme on Fundamentals of Collective Adaptive Systems. We illustrate some typical applications of spatial and spatio-temporal model checking on collective adaptive systems and provide an outline for further developments.Source: Ada user journal 37 (2016): 223–227.
Project(s): QUANTICOL
Ciancia V., Latella D., Loreti M., Massink M.
Spatial aspects of computation are becoming increasingly relevant when dealing with systems distributed in physical space. Traditional formal verification techniques are well suited to analyse the temporal evolution of system models; however, properties of space are typically not taken into account explicitly. In this position paper we briefly review some of the recent developments of spatial and spatio-temporal model-checking in the context of the European research project QUANTICOL funded by the FET-Proactive programme on Fundamentals of Collective Adaptive Systems. We illustrate some typical applications of spatial and spatio-temporal model checking on collective adaptive systems and provide an outline for further developments.Source: Ada user journal 37 (2016): 223–227.
Project(s): QUANTICOL
See at:
ISTI Repository | www.ada-europe.org | CNR ExploRA
2016
Contribution to book
Open Access
From urelements to computation: A journey through applications of Fraenkel's permutation model in computer science
Ciancia V.
Around 1922-1938, a new permutation model of set theory was defined. The permutation model served as a counterexample in the first proof of independence of the Axiom of Choice from the other axioms of Zermelo-Fraenkel set theory. Almost a century later, a model introduced as part of a proof in abstract mathematics fostered a plethora of research results, ranging from the area of syntax and semantics of programming languages to minimization algorithms and automated verification of systems. Among these results, we find Lawvere-style algebraic syntax with binders, final-coalgebra semantics with resource allocation, and minimization algorithms for mobile systems. These results are also obtained in various different ways, by describing, in terms of category theory, a number of models equivalent to the permutation model. We aim at providing both a brief history of some of these developments, and a mild introduction to the recent research line of "nominal computation theory", where the essential notion of name is declined in several different ways.Source: History and Philosophy of Computing. HaPoC 2015. IFIP Advances in Information and Communication Technology, edited by Gadducci F.; Tavosanis M., pp. 141–155, 2016
DOI: 10.1007/978-3-319-47286-7_10
Project(s): QUANTICOL, ASCENS
Metrics:
Ciancia V.
Around 1922-1938, a new permutation model of set theory was defined. The permutation model served as a counterexample in the first proof of independence of the Axiom of Choice from the other axioms of Zermelo-Fraenkel set theory. Almost a century later, a model introduced as part of a proof in abstract mathematics fostered a plethora of research results, ranging from the area of syntax and semantics of programming languages to minimization algorithms and automated verification of systems. Among these results, we find Lawvere-style algebraic syntax with binders, final-coalgebra semantics with resource allocation, and minimization algorithms for mobile systems. These results are also obtained in various different ways, by describing, in terms of category theory, a number of models equivalent to the permutation model. We aim at providing both a brief history of some of these developments, and a mild introduction to the recent research line of "nominal computation theory", where the essential notion of name is declined in several different ways.Source: History and Philosophy of Computing. HaPoC 2015. IFIP Advances in Information and Communication Technology, edited by Gadducci F.; Tavosanis M., pp. 141–155, 2016
DOI: 10.1007/978-3-319-47286-7_10
Project(s): QUANTICOL
, ASCENS Metrics:
See at:
hal.inria.fr | doi.org | link-springer-com-443.webvpn.fjmu.edu.cn | CNR ExploRA
2015
Conference article
Open Access
Qualitative and quantitative monitoring of spatio-temporal properties
Nenzi L., Bortolussi L., Ciancia V., Loreti M., Massink M.
We address the specification and verification of spatio-temporal behaviours of complex systems, extending Signal Spatio-Temporal Logic (SSTL) with a spatial operator capable of specifying topological properties in a discrete space. The latter is modelled as a weighted graph, and provided with a boolean and a quantitative semantics. Furthermore, we define efficient monitoring algorithms for both the boolean and the quantitative semantics. These are implemented in a Java tool available online. We illustrate the expressiveness of SSTL and the effectiveness of the monitoring procedures on the formation of patterns in a Turing reaction-diffusion system.Source: RV 2015 - Runtime Verification 2015. 6th International Conference, pp. 21–37, Vienna, Austria, 22 - 25 September 2015
DOI: 10.1007/978-3-319-23820-3_2
Project(s): QUANTICOL
Metrics:
Nenzi L., Bortolussi L., Ciancia V., Loreti M., Massink M.
We address the specification and verification of spatio-temporal behaviours of complex systems, extending Signal Spatio-Temporal Logic (SSTL) with a spatial operator capable of specifying topological properties in a discrete space. The latter is modelled as a weighted graph, and provided with a boolean and a quantitative semantics. Furthermore, we define efficient monitoring algorithms for both the boolean and the quantitative semantics. These are implemented in a Java tool available online. We illustrate the expressiveness of SSTL and the effectiveness of the monitoring procedures on the formation of patterns in a Turing reaction-diffusion system.Source: RV 2015 - Runtime Verification 2015. 6th International Conference, pp. 21–37, Vienna, Austria, 22 - 25 September 2015
DOI: 10.1007/978-3-319-23820-3_2
Project(s): QUANTICOL
Metrics:
See at:
arts.units.it | Archivio istituzionale della ricerca - Università di Trieste | ISTI Repository | doi.org | link.springer.com | CNR ExploRA
2015
Contribution to book
Open Access
An experimental spatio-temporal model checker
Ciancia V., Grilletti G., Latella D., Loreti M., Massink M.
In this work we present a spatial extension of the global model checking algorithm of the temporal logic CTL. This classical veri- fication framework is augmented with ideas coming from the tradition of topological spatial logics. More precisely, we add to CTL the operators of the Spatial Logic of Closure Spaces, including the surrounded operator, with its intended meaning of a point being surrounded by entities sat- isfying a specific property. The interplay of space and time permits one to define complex spatio-temporal properties. The model checking algo- rithm that we propose features no particular efficiency optimisations, as it is meant to be a reference specification of a family of more efficient algorithms that are planned for future work. Its complexity depends on the product of temporal states and points of the space. Nevertheless, a prototype model checker has been implemented, made available, and used for experimentation of the application of spatio-temporal verifica- tion in the field of collective adaptive systems.Source: Software Engineering and Formal Methods, edited by Domenico Bianculli, Radu Calinescu, Bernhard Rumpe, pp. 297–311, 2015
DOI: 10.1007/978-3-662-49224-6_24
Project(s): QUANTICOL
Metrics:
Ciancia V., Grilletti G., Latella D., Loreti M., Massink M.
In this work we present a spatial extension of the global model checking algorithm of the temporal logic CTL. This classical veri- fication framework is augmented with ideas coming from the tradition of topological spatial logics. More precisely, we add to CTL the operators of the Spatial Logic of Closure Spaces, including the surrounded operator, with its intended meaning of a point being surrounded by entities sat- isfying a specific property. The interplay of space and time permits one to define complex spatio-temporal properties. The model checking algo- rithm that we propose features no particular efficiency optimisations, as it is meant to be a reference specification of a family of more efficient algorithms that are planned for future work. Its complexity depends on the product of temporal states and points of the space. Nevertheless, a prototype model checker has been implemented, made available, and used for experimentation of the application of spatio-temporal verifica- tion in the field of collective adaptive systems.Source: Software Engineering and Formal Methods, edited by Domenico Bianculli, Radu Calinescu, Bernhard Rumpe, pp. 297–311, 2015
DOI: 10.1007/978-3-662-49224-6_24
Project(s): QUANTICOL
Metrics:
See at:
ISTI Repository | doi.org | link.springer.com | CNR ExploRA
2015
Conference article
Open Access
Exploring spatio-temporal properties of bike-sharing systems
Ciancia V., Latella D., Massink M., Paskauskas R.
In this paper we explore the combination of novel spatio-temporal model-checking techniques, and of a recently developed model-based approach to the study of bike sharing systems, in order to detect, visualize and investigate potential problems with bike sharing system configurations. In particular the formation and dynamics of clusters of full stations is explored. Such clusters are likely to be related to the difficulties of users to find suitable parking places for their hired bikes and show up as surprisingly long cycling trips in the trip duration statistics of real bike sharing systems of both small and large cities. Spatio- temporal analysis of the pattern formation may help to explain the phenomenon and possibly lead to alternative bike repositioning strategies aiming at the reduction of the size of such clusters and improving the quality of service.Source: IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, pp. 74–79, Cambridge, MA, USA, 21-25/09/2015
DOI: 10.1109/sasow.2015.17
Project(s): QUANTICOL
Metrics:
Ciancia V., Latella D., Massink M., Paskauskas R.
In this paper we explore the combination of novel spatio-temporal model-checking techniques, and of a recently developed model-based approach to the study of bike sharing systems, in order to detect, visualize and investigate potential problems with bike sharing system configurations. In particular the formation and dynamics of clusters of full stations is explored. Such clusters are likely to be related to the difficulties of users to find suitable parking places for their hired bikes and show up as surprisingly long cycling trips in the trip duration statistics of real bike sharing systems of both small and large cities. Spatio- temporal analysis of the pattern formation may help to explain the phenomenon and possibly lead to alternative bike repositioning strategies aiming at the reduction of the size of such clusters and improving the quality of service.Source: IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, pp. 74–79, Cambridge, MA, USA, 21-25/09/2015
DOI: 10.1109/sasow.2015.17
Project(s): QUANTICOL
Metrics:
See at:
ISTI Repository | doi.org | ieeexplore.ieee.org | CNR ExploRA
2015
Report
Open Access
An attribute-based front-end for FlyFast
Ciancia V., Latella D., Massink M.
TypicalCollectiveAdaptiveSystems(CAS)consistofalarge number of interacting objects that coordinate their activities in a decen- tralised and often implicit way. The design of such systems is challenging. It requires scalable analysis tools and techniques to check properties of proposed system designs before they are put into operation. A promising technique is Fast Mean-Field Approximated Model-checking. In particu- lar, the FlyFast model-checker uses an on-the-fly algorithm for bounded PCTL model-checking of selected individuals in the context of very large populations whose behaviour is approximated using deterministic limit techniques. Recently, specific modelling languages have been proposed for CAS. A key feature of such languages is the attribute-based interac- tion paradigm. In this paper we present an attribute-based coordination language as a front-end for FlyFast. Its formal probabilistic semantics is provided and a translation to the original FlyFast language is presented and proved correct.Source: ISTI Technical reports, 2015
Project(s): QUANTICOL
Ciancia V., Latella D., Massink M.
TypicalCollectiveAdaptiveSystems(CAS)consistofalarge number of interacting objects that coordinate their activities in a decen- tralised and often implicit way. The design of such systems is challenging. It requires scalable analysis tools and techniques to check properties of proposed system designs before they are put into operation. A promising technique is Fast Mean-Field Approximated Model-checking. In particu- lar, the FlyFast model-checker uses an on-the-fly algorithm for bounded PCTL model-checking of selected individuals in the context of very large populations whose behaviour is approximated using deterministic limit techniques. Recently, specific modelling languages have been proposed for CAS. A key feature of such languages is the attribute-based interac- tion paradigm. In this paper we present an attribute-based coordination language as a front-end for FlyFast. Its formal probabilistic semantics is provided and a translation to the original FlyFast language is presented and proved correct.Source: ISTI Technical reports, 2015
Project(s): QUANTICOL
See at:
ISTI Repository | CNR ExploRA
2015
Report
Open Access
QUANTICOL - CAS-SCEL semantics and implementation
Ciancia V., De Nicola R., Hillston J., Latella D., Loreti M., Massink M.
At the end of the first year of the QUANTICOL project, we identified the linguistic primitives and the interaction patterns (such as broadcast communication or anonymous interaction) that are needed to model the QUANTICOL case studies and, more generally, in Collective Adaptive Systems (CAS) design. Starting from these primitives and interaction patterns, in the second reporting period, we have worked on the definition of syntax and semantics of the CAS-SCEL language that we named CARMA (Collective Adaptive Resource-sharing Markovian Agents). CARMA is a language specifically developed for the specification and analysis of CAS, with the specific objective to support quantitive evaluation and verification. CARMA combines the lessons learnt from other stochastic process algebras such as PEPA [21], EMPA [2], MTIPP [20] and MoDEST [3], with those learnt from languages specifically designed to model CAS, such as SCEL [13], the AbC calculus [1], PALOMA [14], and the Attributed Pi calculus [22], which feature attribute-based communication and explicit representation of locations. To support simulation of CARMA models a prototype simulator has been also developed. This simulator, which has been implemented in Java, can be used to perform stochastic simulation and can be used as the basis for implementing other analysis techniques. An Eclipse plug-in for supporting specification and analysis of CAS in CARMA has also been developed. Thanks to this plug-in, CARMA systems can be specified by means of an appropriate high-level language. The high level specification is mapped to a process algebra to enable qualitative and quantitive analysis of CAS during system development by following specific design workflows and analysis pathways. In this deliverable we will describe the so-called CARMA Specification Language while in D5.2 an overview of the CARMA Eclipse Plug-in, together with an example of use, is provided. In this document, we first introduce the syntax of CARMA and its operational semantics; then we describe the CARMA tools and show how the formalism can be used to support the quantitative analysis of a simple scenario. Then, we provide a brief illustration of how CARMA could be extended in order to provide a flexible and structured mechanism for defining common spatial aspects of CAS. The document ends with a description of the direction of future work and the relationship with the work done in the other workpackages of the project.Source: Project report, QUANTICOL, Deliverable D4.2, 2015
Project(s): QUANTICOL
Ciancia V., De Nicola R., Hillston J., Latella D., Loreti M., Massink M.
At the end of the first year of the QUANTICOL project, we identified the linguistic primitives and the interaction patterns (such as broadcast communication or anonymous interaction) that are needed to model the QUANTICOL case studies and, more generally, in Collective Adaptive Systems (CAS) design. Starting from these primitives and interaction patterns, in the second reporting period, we have worked on the definition of syntax and semantics of the CAS-SCEL language that we named CARMA (Collective Adaptive Resource-sharing Markovian Agents). CARMA is a language specifically developed for the specification and analysis of CAS, with the specific objective to support quantitive evaluation and verification. CARMA combines the lessons learnt from other stochastic process algebras such as PEPA [21], EMPA [2], MTIPP [20] and MoDEST [3], with those learnt from languages specifically designed to model CAS, such as SCEL [13], the AbC calculus [1], PALOMA [14], and the Attributed Pi calculus [22], which feature attribute-based communication and explicit representation of locations. To support simulation of CARMA models a prototype simulator has been also developed. This simulator, which has been implemented in Java, can be used to perform stochastic simulation and can be used as the basis for implementing other analysis techniques. An Eclipse plug-in for supporting specification and analysis of CAS in CARMA has also been developed. Thanks to this plug-in, CARMA systems can be specified by means of an appropriate high-level language. The high level specification is mapped to a process algebra to enable qualitative and quantitive analysis of CAS during system development by following specific design workflows and analysis pathways. In this deliverable we will describe the so-called CARMA Specification Language while in D5.2 an overview of the CARMA Eclipse Plug-in, together with an example of use, is provided. In this document, we first introduce the syntax of CARMA and its operational semantics; then we describe the CARMA tools and show how the formalism can be used to support the quantitative analysis of a simple scenario. Then, we provide a brief illustration of how CARMA could be extended in order to provide a flexible and structured mechanism for defining common spatial aspects of CAS. The document ends with a description of the direction of future work and the relationship with the work done in the other workpackages of the project.Source: Project report, QUANTICOL, Deliverable D4.2, 2015
Project(s): QUANTICOL
See at:
ISTI Repository | CNR ExploRA
2015
Report
Open Access
A unified view of spatial representation and analysis techniques
Galpin V., Bortolussi L., Ciancia V., Feng C., Gast N., Hillston J., Massink M., Latella D., Tribastone M., Tschaikowski M.
This report presents an overview of spatial representations and analysis techniques within the context of the QUANTICOL project. It first recaps the spatial classification of mathematical models from Deliverable 2.1 and compares this with an abstract data type approach to space proposed for the Carma language in the technical report TR-QC-01-2015. Based on the guidelines presented in Deliverable 2.1, together with recent research within the project, the report focuses on two types of discrete-space models: population discrete-space models and individual discrete-space models, both of which involve a graph over locations. In both types, we restrict our focus to time-homogeneous systems where graph structure is static. When considering analysis techniques, transformations between mathematical models are important as these permit the application of different analysis techniques. The relevant transformations within the QUANTICOL project are aggregation, disaggregation, fluidisation, discretisation and hybridisation. These mostly support abstraction but some can also lead to more detailed models. The report considers analysis techniques that apply specifically to population discrete-space models, and those that apply specifically to individual discrete-space models. A technique for transforming individual (1-dimensional) continuous-space models to population discrete-space models is presented. Some analyses are applicable to both types of model including spatial model checking, modelling of crowding and analyses that combine techniques and work with hybrid models. The report concludes by considering whether space is a special attribute, the relevance of the various analysis techniques for QUANTICOL and Carma, and proposing research topics for the remainder of Task 2.1. These include application of existing results in the context of the QUANTICOL case studies, a location aggregation technique, further investigation of techniques already considered in the project and the possibility of developing hybrid techniques that abstract from parts of the model but consider other parts in a detailed fashion.Source: ISTI Technical reports, 2015
Project(s): QUANTICOL
Galpin V., Bortolussi L., Ciancia V., Feng C., Gast N., Hillston J., Massink M., Latella D., Tribastone M., Tschaikowski M.
This report presents an overview of spatial representations and analysis techniques within the context of the QUANTICOL project. It first recaps the spatial classification of mathematical models from Deliverable 2.1 and compares this with an abstract data type approach to space proposed for the Carma language in the technical report TR-QC-01-2015. Based on the guidelines presented in Deliverable 2.1, together with recent research within the project, the report focuses on two types of discrete-space models: population discrete-space models and individual discrete-space models, both of which involve a graph over locations. In both types, we restrict our focus to time-homogeneous systems where graph structure is static. When considering analysis techniques, transformations between mathematical models are important as these permit the application of different analysis techniques. The relevant transformations within the QUANTICOL project are aggregation, disaggregation, fluidisation, discretisation and hybridisation. These mostly support abstraction but some can also lead to more detailed models. The report considers analysis techniques that apply specifically to population discrete-space models, and those that apply specifically to individual discrete-space models. A technique for transforming individual (1-dimensional) continuous-space models to population discrete-space models is presented. Some analyses are applicable to both types of model including spatial model checking, modelling of crowding and analyses that combine techniques and work with hybrid models. The report concludes by considering whether space is a special attribute, the relevance of the various analysis techniques for QUANTICOL and Carma, and proposing research topics for the remainder of Task 2.1. These include application of existing results in the context of the QUANTICOL case studies, a location aggregation technique, further investigation of techniques already considered in the project and the possibility of developing hybrid techniques that abstract from parts of the model but consider other parts in a detailed fashion.Source: ISTI Technical reports, 2015
Project(s): QUANTICOL
See at:
ISTI Repository | CNR ExploRA
2015
Report
Open Access
Qualitative and quantitative monitoring of spatio-temporal properties. Extended version
Nenzi L., Bortolussi L., Ciancia V., Loreti M., Massink M.
We address the specification and verification of spatio-temporal behaviours of complex systems, extending Signal Spatio-Temporal Logic (SSTL) with a spatial operator capable of specifying topological properties in a discrete space. The latter is modelled as a weighted graph, and provided with a boolean and a quantitative semantics. Furthermore, we define efficient monitoring algorithms for both the boolean and the quantitative semantics. These are implemented in a Java tool available online. We illustrate the expressiveness of SSTL and the effectiveness of the monitoring procedures on the formation of patterns in a Turing reaction-diffusion system. Keywords: Signal Spatio-Temporal Logic, Boolean Semantics, Quantitative Semantics, Monitoring Algorithms, Weighted Graphs, Turing Patterns.Source: ISTI Technical reports, 2015
Project(s): QUANTICOL
Nenzi L., Bortolussi L., Ciancia V., Loreti M., Massink M.
We address the specification and verification of spatio-temporal behaviours of complex systems, extending Signal Spatio-Temporal Logic (SSTL) with a spatial operator capable of specifying topological properties in a discrete space. The latter is modelled as a weighted graph, and provided with a boolean and a quantitative semantics. Furthermore, we define efficient monitoring algorithms for both the boolean and the quantitative semantics. These are implemented in a Java tool available online. We illustrate the expressiveness of SSTL and the effectiveness of the monitoring procedures on the formation of patterns in a Turing reaction-diffusion system. Keywords: Signal Spatio-Temporal Logic, Boolean Semantics, Quantitative Semantics, Monitoring Algorithms, Weighted Graphs, Turing Patterns.Source: ISTI Technical reports, 2015
Project(s): QUANTICOL
See at:
ISTI Repository | CNR ExploRA
2015
Report
Open Access
On space in CARMA
Ciancia V., Latella D., Massink M.
A discussion on embedding space in CARMA is provided and a solution based on Closure Spaces is proposed. An example is shown.Source: ISTI Technical reports, 2015
Project(s): QUANTICOL
Ciancia V., Latella D., Massink M.
A discussion on embedding space in CARMA is provided and a solution based on Closure Spaces is proposed. An example is shown.Source: ISTI Technical reports, 2015
Project(s): QUANTICOL
See at:
ISTI Repository | CNR ExploRA
2014
Report
Open Access
Logics of space and time
Ciancia V., Latella D., Massink M.
We review some literature in the field of spatial logics. The selection of papers we make is intended as an introductory guide in this broad area. In perspective, this review should be expanded in the future and become tailored to the use of spatial reasoning in the context of population models and their ODE / PDE approximations. The application to keep in mind is the analysis of population models where individuals are scattered over a spatial structure. In this context, typically, space is intended to be multi-dimensional, discrete or continuous; it may be useful to think in terms of Euclidean spaces, but also graph-based relational models may be the subject of spatial reasoning. Furthermore, metrics, measures, probabilities and rates may also be part of the requirements of an analysis methodology.Source: ISTI Technical reports, 2014
Project(s): QUANTICOL
Ciancia V., Latella D., Massink M.
We review some literature in the field of spatial logics. The selection of papers we make is intended as an introductory guide in this broad area. In perspective, this review should be expanded in the future and become tailored to the use of spatial reasoning in the context of population models and their ODE / PDE approximations. The application to keep in mind is the analysis of population models where individuals are scattered over a spatial structure. In this context, typically, space is intended to be multi-dimensional, discrete or continuous; it may be useful to think in terms of Euclidean spaces, but also graph-based relational models may be the subject of spatial reasoning. Furthermore, metrics, measures, probabilities and rates may also be part of the requirements of an analysis methodology.Source: ISTI Technical reports, 2014
Project(s): QUANTICOL
See at:
milner.inf.ed.ac.uk | ISTI Repository | CNR ExploRA
2014
Contribution to book
Restricted
Quantitative Evaluation of Enforcement Strategies
Ciancia V., Martinelli F., Matteucci I., Morisset C.
A security enforcement mechanism runs in parallel with a system to check and modify its run-time behaviour, so that it satisfies some security policy. For each policy, several enforcement strategies are possible, usually reflecting trade-offs one has to make to satisfy the policy. To evaluate them, multiple dimensions, such as security, cost of implementation, or cost of attack, must be taken into account. We propose a formal framework for the quantification of enforcement strategies, extending the notion of controller processes (mimicking the well-known edit automata) with weights on transitions, valued in a semiring.Source: Foundations and Practice of Security. 6th International Symposium. Revised Selected Papers, edited by Jean Luc Danger, Mourad Debbabi, Jean-Yves Marion, Joaquin Garcia-Alfaro, Nur Zincir Heywood, pp. 178–186, 2014
DOI: 10.1007/978-3-319-05302-8_11
Metrics:
Ciancia V., Martinelli F., Matteucci I., Morisset C.
A security enforcement mechanism runs in parallel with a system to check and modify its run-time behaviour, so that it satisfies some security policy. For each policy, several enforcement strategies are possible, usually reflecting trade-offs one has to make to satisfy the policy. To evaluate them, multiple dimensions, such as security, cost of implementation, or cost of attack, must be taken into account. We propose a formal framework for the quantification of enforcement strategies, extending the notion of controller processes (mimicking the well-known edit automata) with weights on transitions, valued in a semiring.Source: Foundations and Practice of Security. 6th International Symposium. Revised Selected Papers, edited by Jean Luc Danger, Mourad Debbabi, Jean-Yves Marion, Joaquin Garcia-Alfaro, Nur Zincir Heywood, pp. 178–186, 2014
DOI: 10.1007/978-3-319-05302-8_11
Metrics:
See at:
doi.org | link.springer.com | CNR ExploRA
2014
Report
Open Access
Specifying and verifying properties of space. Extended Version.
Ciancia V., Latella D., Loreti M., Massink M.
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; however, 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 the more general setting of closure spaces, 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.Source: ISTI Technical reports, 2014
Project(s): QUANTICOL
Ciancia V., Latella D., Loreti M., Massink M.
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; however, 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 the more general setting of closure spaces, 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.Source: ISTI Technical reports, 2014
Project(s): QUANTICOL
See at:
milner.inf.ed.ac.uk | ISTI Repository | CNR ExploRA
2014
Conference article
Open Access
Specifying and Verifying Properties of Space
Ciancia V., Latella D., Loreti M., Massink M.
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.Source: Theoretical Computer Science, pp. 222–235, Roma, 1-3 Settembre 2014
DOI: 10.1007/978-3-662-44602-7_18
Project(s): QUANTICOL, ASCENS
Metrics:
Ciancia V., Latella D., Loreti M., Massink M.
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.Source: Theoretical Computer Science, pp. 222–235, Roma, 1-3 Settembre 2014
DOI: 10.1007/978-3-662-44602-7_18
Project(s): QUANTICOL
, ASCENS Metrics:
See at:
link.springer.com | doi.org | Hyper Article en Ligne | www.scopus.com | CNR ExploRA
2014
Journal article
Open Access
A Quantitative Approach to the Design and Analysis of Collective Adaptive Systems for Smart Cities
Ter Beek M. H., Bortolussi L., Ciancia V., Gnesi S., Hillston J., Latella D., Massink M.
It's smart to be fair. Researchers from the Formal Methods and Tools group of ISTI-CNR are working on scalable analysis techniques to support smart applications for the efficient and equitable sharing of resources in the cities of our future. The research is being carried out under the European FET-Proactive project, QUANTICOL.Source: ERCIM news 98 (2014): 32–32.
Project(s): QUANTICOL
Ter Beek M. H., Bortolussi L., Ciancia V., Gnesi S., Hillston J., Latella D., Massink M.
It's smart to be fair. Researchers from the Formal Methods and Tools group of ISTI-CNR are working on scalable analysis techniques to support smart applications for the efficient and equitable sharing of resources in the cities of our future. The research is being carried out under the European FET-Proactive project, QUANTICOL.Source: ERCIM news 98 (2014): 32–32.
Project(s): QUANTICOL
See at:
ercim-news.ercim.eu | CNR ExploRA
2014
Conference article
Restricted
Data verification for collective adaptive systems: spatial model-checking of vehicle location data
Ciancia V., Gilmore S., Latella D., Loreti M., Massink M.
In this paper we present the use of a novel spa- tial model-checker to detect problems in the data which an adaptive system gathers in order to inform future action. We categorise received data as being plausible, implausible, possible or problematic. Data correctness is essential to ensure correct functionality in systems which adapt in response to data and our categorisation influences the degree of caution which should be used in acting in response to this received data. We illustrate the theory with a concrete example of detecting errors in vehicle location data for buses in the city of Edinburgh. Vehicle location data is visualised symbolically on a street map, and categories of problems identified by the spatial model-checker are rendered by repainting the symbols for vehicles in different colours.Source: FoCAS Workshp @ SASO - 2014 IEEE Eighth International Conference on Self-Adaptive and Self-Organizing Systems Workshops, pp. 32–37, Imperial College, London, UK, 8 September 2014
DOI: 10.1109/sasow.2014.16
Project(s): QUANTICOL
Metrics:
Ciancia V., Gilmore S., Latella D., Loreti M., Massink M.
In this paper we present the use of a novel spa- tial model-checker to detect problems in the data which an adaptive system gathers in order to inform future action. We categorise received data as being plausible, implausible, possible or problematic. Data correctness is essential to ensure correct functionality in systems which adapt in response to data and our categorisation influences the degree of caution which should be used in acting in response to this received data. We illustrate the theory with a concrete example of detecting errors in vehicle location data for buses in the city of Edinburgh. Vehicle location data is visualised symbolically on a street map, and categories of problems identified by the spatial model-checker are rendered by repainting the symbols for vehicles in different colours.Source: FoCAS Workshp @ SASO - 2014 IEEE Eighth International Conference on Self-Adaptive and Self-Organizing Systems Workshops, pp. 32–37, Imperial College, London, UK, 8 September 2014
DOI: 10.1109/sasow.2014.16
Project(s): QUANTICOL
Metrics:
See at:
doi.org | ieeexplore.ieee.org | CNR ExploRA
2014
Report
Open Access
QUANTICOL - D6.1 - Dissemination plan for the project
Gilmore S., Ter Beek M. H., Bortolussi L., Ciancia V., Galpin V., Hillston J., Massink M., Tribastone M.
This document sets out the dissemination plan for the QUANTICOL project. The project has ambitions to see its research outputs and results disseminated widely in academia and beyond. We present here our plan to achieve this goal and review the progress on the plan which has been achieved in the rst year of the project. This gives an insight into how we see the plan being developed and implemented in later years of the project.Source: Project report, QUANTICOL, Deliverable D6.1, 2014
Project(s): QUANTICOL
Gilmore S., Ter Beek M. H., Bortolussi L., Ciancia V., Galpin V., Hillston J., Massink M., Tribastone M.
This document sets out the dissemination plan for the QUANTICOL project. The project has ambitions to see its research outputs and results disseminated widely in academia and beyond. We present here our plan to achieve this goal and review the progress on the plan which has been achieved in the rst year of the project. This gives an insight into how we see the plan being developed and implemented in later years of the project.Source: Project report, QUANTICOL, Deliverable D6.1, 2014
Project(s): QUANTICOL
See at:
blog.inf.ed.ac.uk | ISTI Repository | CNR ExploRA
2014
Other
Open Access
A Quantitative Approach to the Design and Analysis of Collective Adaptive Systems for Smart Cities
Ter Beek M. H., Bortolussi L., Ciancia V., Gnesi S., Hillston J., Latella D., Massink M.
It's smart to be fair. Researchers from the Formal Methods and Tools group of ISTI-CNR are working on scalable analysis techniques to support smart applications for the efficient and equitable sharing of resources in the cities of our future. The research is being carried out under the European FET-Proactive project, QUANTICOL.Project(s): QUANTICOL
Ter Beek M. H., Bortolussi L., Ciancia V., Gnesi S., Hillston J., Latella D., Massink M.
It's smart to be fair. Researchers from the Formal Methods and Tools group of ISTI-CNR are working on scalable analysis techniques to support smart applications for the efficient and equitable sharing of resources in the cities of our future. The research is being carried out under the European FET-Proactive project, QUANTICOL.Project(s): QUANTICOL
See at:
ercim-news.ercim.eu | ISTI Repository | CNR ExploRA
2014
Report
Unknown
QUANTICOL - A preliminary investigation of capturing spatial information for CAS
Galpin V., Bortolussi L., Ciancia V., Clark A., De Nicola R., Feng C., Gilmore S., Gast N., Hillston J., Lluch-Lafuente A., Loreti M., Massink M., Nenzi L., Reijsbergen D., Senni V., Tiezzi F., Tribastone M., Tschaikowski M.
Space is important in the QUANTICOL project because the project case studies include smart transport, and quantitative modelling of transport has inherent spatial aspects. This deliverable presents a review of the literature about spatial modelling within and beyond computer science, and a classification of the different approaches reviewed. The objective of the classification is to make clear what approaches are available and how they differ from each other. This will be used to guide future work on spatial approaches within the project. Furthermore, the classification enables the identification of the approaches that have been used in the initial work on case studies in the realm of smart transport. This deliverable rst identifies the aspects of non-spatial modelling that are important in the context of the QUANTICOL project. Time can be modelled in a discrete or continuous manner. States can be discrete, representing attributes of an individual. For example, when considering bike sharing, inUse (busy), onStand (idle) or atWorkshop (under repair) might be appropriate states for a bike. Alternatively, states can be continuous representing an attribute (for example, seat height). In the case of discrete states, it is possible to perform aggregation by considering populations, namely how many individuals are in each state, and to acquire an understanding of the overall behaviour of the population, rather than of individuals. Mean-field techniques can be employed to transform a discrete population approach to one that considers continuous populations that approximate the discrete approach. To this context, space is introduced. Space can be discrete and described by a graph of locations. Depending on the structure of the graph and the parameters associated with locations and movement between locations, discrete space can be classified as regular or homogeneous. Space can be seen as continuous: as Euclidean space in one, two or three dimensions. Space can also be considered abstractly as topological space, whether discrete or continuous and this approach allows for reasoning about concepts such as adjacency and neighbourhoods. This deliverable describes the modelling techniques that are currently available for the different combinations of time, state, aggregation and space, giving both a tabular classification as well as high-level and formal descriptions of the techniques. For each representation, examples are given of its use in different disciplines, including ecology, biology, epidemiology and computer science. In particular, the modelling goals are considered for these techniques, and compared with the goals of the QUANTICOL project. This deliverable also has the aim of identifying disparate uses of terminology in various approaches. Both current and future case studies relevant to the project are classified in terms of how they use time, state, aggregation and space and nally conclusions are presented taking into account the literature reviewed, what has been modelled and what the goals of the project are for modelling of smart transport. The preliminary guidelines arising from the review and classification are to focus on patch models and associated techniques although continuous space models of individuals may be important in certain cases. Items proposed for further research are understanding and developing mean-field techniques, spatial and non-spatial moment closure methods and hybrid spatial approaches. The document closes with a future work plan for Work Package 2.Source: Project report, QUANTICOL, Deliverable D2.1, 2014
Project(s): QUANTICOL
Galpin V., Bortolussi L., Ciancia V., Clark A., De Nicola R., Feng C., Gilmore S., Gast N., Hillston J., Lluch-Lafuente A., Loreti M., Massink M., Nenzi L., Reijsbergen D., Senni V., Tiezzi F., Tribastone M., Tschaikowski M.
Space is important in the QUANTICOL project because the project case studies include smart transport, and quantitative modelling of transport has inherent spatial aspects. This deliverable presents a review of the literature about spatial modelling within and beyond computer science, and a classification of the different approaches reviewed. The objective of the classification is to make clear what approaches are available and how they differ from each other. This will be used to guide future work on spatial approaches within the project. Furthermore, the classification enables the identification of the approaches that have been used in the initial work on case studies in the realm of smart transport. This deliverable rst identifies the aspects of non-spatial modelling that are important in the context of the QUANTICOL project. Time can be modelled in a discrete or continuous manner. States can be discrete, representing attributes of an individual. For example, when considering bike sharing, inUse (busy), onStand (idle) or atWorkshop (under repair) might be appropriate states for a bike. Alternatively, states can be continuous representing an attribute (for example, seat height). In the case of discrete states, it is possible to perform aggregation by considering populations, namely how many individuals are in each state, and to acquire an understanding of the overall behaviour of the population, rather than of individuals. Mean-field techniques can be employed to transform a discrete population approach to one that considers continuous populations that approximate the discrete approach. To this context, space is introduced. Space can be discrete and described by a graph of locations. Depending on the structure of the graph and the parameters associated with locations and movement between locations, discrete space can be classified as regular or homogeneous. Space can be seen as continuous: as Euclidean space in one, two or three dimensions. Space can also be considered abstractly as topological space, whether discrete or continuous and this approach allows for reasoning about concepts such as adjacency and neighbourhoods. This deliverable describes the modelling techniques that are currently available for the different combinations of time, state, aggregation and space, giving both a tabular classification as well as high-level and formal descriptions of the techniques. For each representation, examples are given of its use in different disciplines, including ecology, biology, epidemiology and computer science. In particular, the modelling goals are considered for these techniques, and compared with the goals of the QUANTICOL project. This deliverable also has the aim of identifying disparate uses of terminology in various approaches. Both current and future case studies relevant to the project are classified in terms of how they use time, state, aggregation and space and nally conclusions are presented taking into account the literature reviewed, what has been modelled and what the goals of the project are for modelling of smart transport. The preliminary guidelines arising from the review and classification are to focus on patch models and associated techniques although continuous space models of individuals may be important in certain cases. Items proposed for further research are understanding and developing mean-field techniques, spatial and non-spatial moment closure methods and hybrid spatial approaches. The document closes with a future work plan for Work Package 2.Source: Project report, QUANTICOL, Deliverable D2.1, 2014
Project(s): QUANTICOL
See at: CNR ExploRA
2014
Report
Unknown
QUANTICOL - Foundations of scalable verification for stochastic logics
Massink M., Bortolussi L., Ciancia V., Hillston J., Lluch-Lafuente A., Latella D., Loreti M., Reijsbergen D., Vandin A.
This deliverable reports on the study of the theoretical foundations of scalable model checking approaches, including those based on mean-eld and uid ow techniques, addressing the rst phase of Task 3.1. Model checking has been widely recognised as a powerful approach to the automatic verication of concurrent and distributed systems. It consists of an ecient procedure that, given an abstract model of the behaviour of the system, decides whether that model satises properties of interest, typically expressed using a form of temporal logic. Despite their success, scalability of model checking procedures has always been a concern due to the potential combinatorial explosion of the state space that needs to be searched. This is particularly an issue when analysing large collective adaptive systems that typically consist of a large number of independent, communicating objects. This deliverable reports on the theoretical foundations of several novel scalable model checking approaches that have been developed during the rst year of the QUANTICOL project to address the challenge of scalability. A rst approach concerns Fluid Model Checking. This approach exploits uid ow approximations and fast simulation techniques in a global model checking algorithm to verify continuous stochastic logic properties of an individual object, or a few objects, in the context of large population models. The approach has been extended considering steady state properties and a method has been developed to lift local properties to global collective ones exploiting the central limit theorem. The second approach concerns mean-eld fast probabilistic model checking. This approach exploits mean-eld approximation and fast simulation in a discrete time probabilistic setting. Furthermore, it combines the above mentioned techniques with on-the- y model checking techniques. The asymptotic correctness of the approach is outlined and the use of the prototype implementation of the algorithm, developed during the rst year of the QUANTICOL Project, is brie y illustrated on a variant of the bike-sharing case study. A third approach concerns a novel and ecient statistical model checking technique and tool to deal with uncertainty in the values of model parameters in a statistically sound way. The approach is based also on recent advances in machine learning and pattern recognition. Finally, we report on a literature study that was conducted on spatial logics and that is complementing the work on spatial representations in Work Package 2, in preparation for the future extension of the scalable model checking techniques addressing properties of spatially inhomogeneous collective adaptive systems.Source: Project report, QUANTICOL, Deliverable D1.0, 2014
Project(s): QUANTICOL
Massink M., Bortolussi L., Ciancia V., Hillston J., Lluch-Lafuente A., Latella D., Loreti M., Reijsbergen D., Vandin A.
This deliverable reports on the study of the theoretical foundations of scalable model checking approaches, including those based on mean-eld and uid ow techniques, addressing the rst phase of Task 3.1. Model checking has been widely recognised as a powerful approach to the automatic verication of concurrent and distributed systems. It consists of an ecient procedure that, given an abstract model of the behaviour of the system, decides whether that model satises properties of interest, typically expressed using a form of temporal logic. Despite their success, scalability of model checking procedures has always been a concern due to the potential combinatorial explosion of the state space that needs to be searched. This is particularly an issue when analysing large collective adaptive systems that typically consist of a large number of independent, communicating objects. This deliverable reports on the theoretical foundations of several novel scalable model checking approaches that have been developed during the rst year of the QUANTICOL project to address the challenge of scalability. A rst approach concerns Fluid Model Checking. This approach exploits uid ow approximations and fast simulation techniques in a global model checking algorithm to verify continuous stochastic logic properties of an individual object, or a few objects, in the context of large population models. The approach has been extended considering steady state properties and a method has been developed to lift local properties to global collective ones exploiting the central limit theorem. The second approach concerns mean-eld fast probabilistic model checking. This approach exploits mean-eld approximation and fast simulation in a discrete time probabilistic setting. Furthermore, it combines the above mentioned techniques with on-the- y model checking techniques. The asymptotic correctness of the approach is outlined and the use of the prototype implementation of the algorithm, developed during the rst year of the QUANTICOL Project, is brie y illustrated on a variant of the bike-sharing case study. A third approach concerns a novel and ecient statistical model checking technique and tool to deal with uncertainty in the values of model parameters in a statistically sound way. The approach is based also on recent advances in machine learning and pattern recognition. Finally, we report on a literature study that was conducted on spatial logics and that is complementing the work on spatial representations in Work Package 2, in preparation for the future extension of the scalable model checking techniques addressing properties of spatially inhomogeneous collective adaptive systems.Source: Project report, QUANTICOL, Deliverable D1.0, 2014
Project(s): QUANTICOL
See at: CNR ExploRA
2014
Report
Unknown
Specifying and verifying properties of space
Ciancia V., Latella D., Loreti M., Massink M.
The interplay between process behaviour and spatial aspects of computation has become more and more relevant in Computer Science, especially in the eld of collective adaptive systems, but also, more generally, when dealing with systems distributed in physical space. Traditional verica- tion techniques are well suited to analyse the temporal evolution of programs; however, properties of space are typically not explicitly taken into account. We propose a methodology to verify prop- erties depending upon physical space. We dene 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 denitions to the more general setting of closure spaces, also encompassing discrete, graph-based structures. We further extend the frame- work with a spatial until operator, and dene an ecient model checking procedure, implemented in a proof-of-concept tool.Source: ISTI Technical reports, 2014
Project(s): QUANTICOL
Ciancia V., Latella D., Loreti M., Massink M.
The interplay between process behaviour and spatial aspects of computation has become more and more relevant in Computer Science, especially in the eld of collective adaptive systems, but also, more generally, when dealing with systems distributed in physical space. Traditional verica- tion techniques are well suited to analyse the temporal evolution of programs; however, properties of space are typically not explicitly taken into account. We propose a methodology to verify prop- erties depending upon physical space. We dene 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 denitions to the more general setting of closure spaces, also encompassing discrete, graph-based structures. We further extend the frame- work with a spatial until operator, and dene an ecient model checking procedure, implemented in a proof-of-concept tool.Source: ISTI Technical reports, 2014
Project(s): QUANTICOL
See at: CNR ExploRA
2014
Report
Unknown
A spatio-temporal model-checker
Ciancia V., Grilletti G., Latella D., Loreti M., Massink M.
We define a spatio-temporal logic, the Spatio-temporal Logic of Closure Spaces (STLCS). The logic is interpreted on Kripke models, in which each state has an associated closure space. The logic extends CTL with spatial operators, in the spirit of topological modal logic. More specifically, we add to CTL the operators of the Spatial Logic of Closure Spaces, including the spatial until operator, with its intended meaning of a point being surrounded by entities satisfying a specific property. The interplay of space and time permits one to define complex spatio-temporal properties. We present a simple model-checking algorithm for STLCS, which has been implemented in a prototype tool.Source: ISTI Technical reports, 2014
Project(s): QUANTICOL
Ciancia V., Grilletti G., Latella D., Loreti M., Massink M.
We define a spatio-temporal logic, the Spatio-temporal Logic of Closure Spaces (STLCS). The logic is interpreted on Kripke models, in which each state has an associated closure space. The logic extends CTL with spatial operators, in the spirit of topological modal logic. More specifically, we add to CTL the operators of the Spatial Logic of Closure Spaces, including the spatial until operator, with its intended meaning of a point being surrounded by entities satisfying a specific property. The interplay of space and time permits one to define complex spatio-temporal properties. We present a simple model-checking algorithm for STLCS, which has been implemented in a prototype tool.Source: ISTI Technical reports, 2014
Project(s): QUANTICOL
See at: CNR ExploRA
2013
Conference article
Open Access
Interaction and observation: categorical semantics of reactive systems trough dialgebras
Ciancia V.
We use dialgebras, generalising both algebras and coalgebras, as a complement of the standard coalgebraic framework, aimed at describing the semantics of an interactive system by the means of reaction rules. In this model, interaction is built-in, and semantic equivalence arises from it, instead of being determined by a (possibly difficult) understanding of the side effects of a component in isolation. Behavioural equivalence in dialgebras is determined by how a given process interacts with the others, and the obtained observations. We develop a technique to inter-define categories of dialgebras of different functors, that in particular permits us to compare a standard coalgebraic semantics and its dialgebraic counterpart. We exemplify the framework using the CCS and the ?-calculus. Remarkably, the dialgebra giving semantics to the ?-calculus does not require the use of presheaf categories.Source: CALCO 2013 - 5th Conference on Algebra and Coalgebra in Computer Science, pp. 110–125, Warsaw, Poland, 3-6 Settembre 2013
DOI: 10.1007/978-3-642-40206-7_10
DOI: 10.48550/arxiv.1209.5903
Project(s): QUANTICOL
Metrics:
Ciancia V.
We use dialgebras, generalising both algebras and coalgebras, as a complement of the standard coalgebraic framework, aimed at describing the semantics of an interactive system by the means of reaction rules. In this model, interaction is built-in, and semantic equivalence arises from it, instead of being determined by a (possibly difficult) understanding of the side effects of a component in isolation. Behavioural equivalence in dialgebras is determined by how a given process interacts with the others, and the obtained observations. We develop a technique to inter-define categories of dialgebras of different functors, that in particular permits us to compare a standard coalgebraic semantics and its dialgebraic counterpart. We exemplify the framework using the CCS and the ?-calculus. Remarkably, the dialgebra giving semantics to the ?-calculus does not require the use of presheaf categories.Source: CALCO 2013 - 5th Conference on Algebra and Coalgebra in Computer Science, pp. 110–125, Warsaw, Poland, 3-6 Settembre 2013
DOI: 10.1007/978-3-642-40206-7_10
DOI: 10.48550/arxiv.1209.5903
Project(s): QUANTICOL
Metrics:
See at:
arXiv.org e-Print Archive | arxiv.org | doi.org | doi.org | link.springer.com | CNR ExploRA