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 
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 | 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 | CNR ExploRA | www.computer.org
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
Embargo
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:
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