2024
Contribution to book
Restricted
Measured causes: adding time and probability to true concurrency
Brinksma E., Langerak R., Latella D., Massink M.
In this paper we briefly discuss ten papers by Joost-Pieter Katoen on quantitative extensions of causality models from the period 1994--2001 that all resulted from collaboration with Pisa and/or Twente.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15262, pp. 297-308
DOI: 10.1007/978-3-031-75778-5_14
Project(s): Formal Methods in Software Engineering 2.0
Metrics:
Brinksma E., Langerak R., Latella D., Massink M.
In this paper we briefly discuss ten papers by Joost-Pieter Katoen on quantitative extensions of causality models from the period 1994--2001 that all resulted from collaboration with Pisa and/or Twente.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15262, pp. 297-308
DOI: 10.1007/978-3-031-75778-5_14
Project(s): Formal Methods in Software Engineering 2.0
Metrics:
2024
Other
Open Access
Weak ±-minimisation for model checking polyhedra
Bezhanishvili N., Bussi L., Ciancia V., Gabelaia D., Jibladze M., Latella D., Massink M., De Vink E. P.
The work in this paper builds on the polyhedral semantics of the Spatial Logic for Closure Spaces (SLCS), and the geometric spatial model checker PolyLogicA. Polyhedral models are central in domains that exploit mesh processing, such as 3D computer graphics. A discrete representation of polyhedra is given by face-poset models, which are amenable to spatial model checking using the logical language SLCSη and PolyLogicA. In this work, we propose a procedure that computes the minimal model with respect to weak ±-bisimilarity – that is SLCSη- logical equivalence – via a translation to LTSs and branching bisimilarity. Because of its reduced size, the minimal model makes geometric model checking more efficient. We provide a preliminary experimental valida- tion of the approach exploiting the minimization capabilities of mCRL2.DOI: 10.32079/isti-tr-2024/002
Project(s): Model Checking for Polyhedral Logic
Metrics:
Bezhanishvili N., Bussi L., Ciancia V., Gabelaia D., Jibladze M., Latella D., Massink M., De Vink E. P.
The work in this paper builds on the polyhedral semantics of the Spatial Logic for Closure Spaces (SLCS), and the geometric spatial model checker PolyLogicA. Polyhedral models are central in domains that exploit mesh processing, such as 3D computer graphics. A discrete representation of polyhedra is given by face-poset models, which are amenable to spatial model checking using the logical language SLCSη and PolyLogicA. In this work, we propose a procedure that computes the minimal model with respect to weak ±-bisimilarity – that is SLCSη- logical equivalence – via a translation to LTSs and branching bisimilarity. Because of its reduced size, the minimal model makes geometric model checking more efficient. We provide a preliminary experimental valida- tion of the approach exploiting the minimization capabilities of mCRL2.DOI: 10.32079/isti-tr-2024/002
Project(s): Model Checking for Polyhedral Logic
Metrics:
2024
Conference article
Open Access
Weak simplicial bisimilarity for polyhedral models and SLCSη
Bezhanishvili N., Ciancia V., Gabelaia D., Jibladze M., Latella D., Massink M., De Vink E. P.
In the context of spatial logics and spatial model checking for polyhedral models — mathematical basis for visualisations in continuous space — we propose a weakening of simplicial bisimilarity. We addition- ally propose a corresponding weak notion of ±-bisimilarity on cell-poset models, discrete representation of polyhedral models. We show that two points are weakly simplicial bisimilar iff their representations are weakly ±-bisimilar. The advantage of this weaker notion is that it leads to a stronger reduction of models than its counterpart that was introduced in our previous work. This is important, since real-world polyhedral mod- els, such as those found in domains exploiting mesh processing, typically consist of large numbers of cells. We also propose SLCSη, a weaker ver- sion of the Spatial Logic for Closure Spaces (SLCS) on polyhedral models, and we show that the proposed bisimilarities enjoy the Hennessy-Milner property: two points are weakly simplicial bisimilar iff they are logically equivalent for SLCSη. Similarly, two cells are weakly ±-bisimilar iff they are logically equivalent in the poset-model interpretation of SLCSη. This work is performed in the context of the geometric spatial model checker PolyLogicA and the polyhedral semantics of SLCS.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 14678, pp. 20-38. Groningen, NL, 17-21/06/2024
DOI: 10.1007/978-3-031-62645-6_2
Metrics:
Bezhanishvili N., Ciancia V., Gabelaia D., Jibladze M., Latella D., Massink M., De Vink E. P.
In the context of spatial logics and spatial model checking for polyhedral models — mathematical basis for visualisations in continuous space — we propose a weakening of simplicial bisimilarity. We addition- ally propose a corresponding weak notion of ±-bisimilarity on cell-poset models, discrete representation of polyhedral models. We show that two points are weakly simplicial bisimilar iff their representations are weakly ±-bisimilar. The advantage of this weaker notion is that it leads to a stronger reduction of models than its counterpart that was introduced in our previous work. This is important, since real-world polyhedral mod- els, such as those found in domains exploiting mesh processing, typically consist of large numbers of cells. We also propose SLCSη, a weaker ver- sion of the Spatial Logic for Closure Spaces (SLCS) on polyhedral models, and we show that the proposed bisimilarities enjoy the Hennessy-Milner property: two points are weakly simplicial bisimilar iff they are logically equivalent for SLCSη. Similarly, two cells are weakly ±-bisimilar iff they are logically equivalent in the poset-model interpretation of SLCSη. This work is performed in the context of the geometric spatial model checker PolyLogicA and the polyhedral semantics of SLCS.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 14678, pp. 20-38. Groningen, NL, 17-21/06/2024
DOI: 10.1007/978-3-031-62645-6_2
Metrics:
See at:
IRIS Cnr 
| IRIS Cnr | IRIS Cnr | doi.org 
| CNR IRIS | CNR IRIS
2024
Conference article
Open Access
Towards hybrid-AI in imaging using VoxLogicA
Belmonte G., Bussi L., Ciancia V., Latella D., Massink M.
We present the design of a meta-programming system for hybrid AI, integrating spatial model checking and machine learning. The proposed system architecture blends together different programming languages and execution technologies using a simplified, declarative meta-language. The design features a global-model-checking-alike execution model, backed up by a microservices architecture. The system is meant to be a follow up to the spatial model checker VoxLogicA currently used for research on declarative medical image analysis, aimed at explainable by construction artificial intelligence.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15222, pp. 205-221. Crete, Greece, 27-31/10/2024
DOI: 10.1007/978-3-031-75387-9_13
Project(s): -Spatio-Temporal Enhancement of Neural nets for Deeply Hierarchical Automatised Logic, Formal Methods in Software Engineering 2.0, Model Checking for Polyhedral Logic, PRIN T-LADIES, Tuscany Health Ecosystem
Metrics:
Belmonte G., Bussi L., Ciancia V., Latella D., Massink M.
We present the design of a meta-programming system for hybrid AI, integrating spatial model checking and machine learning. The proposed system architecture blends together different programming languages and execution technologies using a simplified, declarative meta-language. The design features a global-model-checking-alike execution model, backed up by a microservices architecture. The system is meant to be a follow up to the spatial model checker VoxLogicA currently used for research on declarative medical image analysis, aimed at explainable by construction artificial intelligence.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 15222, pp. 205-221. Crete, Greece, 27-31/10/2024
DOI: 10.1007/978-3-031-75387-9_13
Project(s): -Spatio-Temporal Enhancement of Neural nets for Deeply Hierarchical Automatised Logic, Formal Methods in Software Engineering 2.0, Model Checking for Polyhedral Logic, PRIN T-LADIES, Tuscany Health Ecosystem
Metrics:
2023
Other
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.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.DOI: 10.32079/isti-tr-2023/003
Metrics:
See at:
CNR IRIS | ISTI Repository | CNR IRIS
2023
Conference article
Open Access
Minimisation of spatial models using branching bisimilarity
Ciancia V, Groote Jf, Latella D, Massink M, De Vink Ep
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.DOI: 10.1007/978-3-031-27481-7_16
Metrics:
Ciancia V, Groote Jf, Latella D, Massink M, De Vink Ep
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.DOI: 10.1007/978-3-031-27481-7_16
Metrics:
See at:
CNR IRIS | ISTI Repository | CNR IRIS | CNR IRIS
2023
Contribution to book
Open Access
Caratteristiche, prospettive e problematicità dell'Intelligenza Artificiale
Latella D, Siroli Gp, Tamburrini G
Breve introduzione ai concetti fondamentali sui quali si basa l'intelligenza artificiale e alle problematiche alle quali il suo uso, specie in contesti critici, puo' dare origine. Viene data una breve introduzione storica e di inquadramento. Si approfondiscono alcuni aspetti dell'apprendimento automatico e si discutono alcuni suoi limiti e problematicità.
Latella D, Siroli Gp, Tamburrini G
Breve introduzione ai concetti fondamentali sui quali si basa l'intelligenza artificiale e alle problematiche alle quali il suo uso, specie in contesti critici, puo' dare origine. Viene data una breve introduzione storica e di inquadramento. Si approfondiscono alcuni aspetti dell'apprendimento automatico e si discutono alcuni suoi limiti e problematicità.
See at:
CNR IRIS | ISTI Repository | series.francoangeli.it | CNR IRIS
2023
Other
Restricted
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 - THE
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 - THE
2023
Conference article
Open Access
On bisimilarity for polyhedral models and SLCS
Ciancia V, Gabelaia D, Latella D, Massink M, De Vink Ep
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.DOI: 10.1007/978-3-031-35355-0_9
Metrics:
Ciancia V, Gabelaia D, Latella D, Massink M, De Vink Ep
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.DOI: 10.1007/978-3-031-35355-0_9
Metrics:
See at:
CNR IRIS | link.springer.com | ISTI Repository | CNR IRIS | CNR IRIS | CNR IRIS
2023
Other
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.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.DOI: 10.32079/isti-tr-2023/009
Metrics:
See at:
CNR IRIS | ISTI Repository | CNR IRIS | CNR IRIS
2022
Other
Open Access
Minimisation of spatial models using branching bisimilarity (extended version)
Ciancia V, Groote Jf, Latella D, Massink M, De Vink Ep
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.DOI: 10.32079/isti-tr-2022/027
Metrics:
Ciancia V, Groote Jf, Latella D, Massink M, De Vink Ep
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.DOI: 10.32079/isti-tr-2022/027
Metrics:
See at:
CNR IRIS | ISTI Repository | CNR IRIS
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: COMMUNICATIONS IN COMPUTER AND INFORMATION SCIENCE (PRINT), 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: COMMUNICATIONS IN COMPUTER AND INFORMATION SCIENCE (PRINT), pp. 103-111. Online conference, 26/06-01/07/2022
DOI: 10.1007/978-3-031-06388-6_14
Metrics:
See at:
CNR IRIS | link.springer.com | ISTI Repository | ISTI Repository | CNR IRIS | CNR IRIS | CNR IRIS
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 Ep
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.DOI: 10.1007/978-3-031-15629-8_6
Metrics:
Ciancia V, Latella D, Massink M, De Vink Ep
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.DOI: 10.1007/978-3-031-15629-8_6
Metrics:
See at:
CNR IRIS | link.springer.com | ISTI Repository | CNR IRIS | CNR IRIS
2022
Other
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 Ep
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.DOI: 10.32079/isti-tr-2022/018
Metrics:
Ciancia V, Latella D, Massink M, De Vink Ep
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.DOI: 10.32079/isti-tr-2022/018
Metrics:
See at:
CNR IRIS | ISTI Repository | CNR IRIS
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.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.DOI: 10.1007/978-3-031-16011-0_6
Metrics:
See at:
CNR IRIS | link.springer.com | ISTI Repository | CNR IRIS | CNR IRIS
2022
Conference article
Open 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.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.DOI: 10.1007/978-3-031-19849-6_27
Metrics:
See at:
CNR IRIS | link.springer.com | CNR IRIS | CNR IRIS
2022
Other
Open Access
On the expressive power of IMLC and ISLCS
Ciancia V, Latella D, Massink M, De Vink Ep
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.DOI: 10.32079/isti-tr-2022/021
Metrics:
Ciancia V, Latella D, Massink M, De Vink Ep
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.DOI: 10.32079/isti-tr-2022/021
Metrics:
See at:
CNR IRIS | ISTI Repository | CNR IRIS
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, vol. 18 (issue 4), pp. 7:1-7:38
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, vol. 18 (issue 4), pp. 7:1-7:38
DOI: 10.46298/lmcs-18(4:7)2022
Metrics:
See at:
CNR IRIS | lmcs.episciences.org | ISTI Repository | CNR IRIS
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.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.DOI: 10.1109/formalise52586.2021.00007
Metrics:
See at:
CNR IRIS | ISTI Repository | www.computer.org | CNR IRIS | CNR IRIS
2021
Other
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.
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.
See at:
arxiv.org | CNR IRIS | ISTI Repository | CNR IRIS