2026
Conference article
Open Access
Model checking in space with applications to medical image analysis: Invited abstract
Belmonte Gina, Ciancia Vincenzo, Latella Diego, Massink Mieke
Model checking has traditionally focused on the analysis of the behaviour of concurrent systems. In this invited abstract, instead, we focus on spatial model checking. We briefly motivate its development and its application in the domain of medical imaging, providing a gentle guide to our recent work on that topic and future research lines.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16504, pp. 3-18. Turin, Italy, 11–16 April 2026
DOI: 10.1007/978-3-032-22774-4_1
Project(s): Ecosystems of Innovation, Project “Tuscany Health Ecosystem” (THE), Model Checking for Polyhedral Logic, Stendhal, T-LADIES
Metrics:
Belmonte Gina, Ciancia Vincenzo, Latella Diego, Massink Mieke
Model checking has traditionally focused on the analysis of the behaviour of concurrent systems. In this invited abstract, instead, we focus on spatial model checking. We briefly motivate its development and its application in the domain of medical imaging, providing a gentle guide to our recent work on that topic and future research lines.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16504, pp. 3-18. Turin, Italy, 11–16 April 2026
DOI: 10.1007/978-3-032-22774-4_1
Project(s): Ecosystems of Innovation, Project “Tuscany Health Ecosystem” (THE), Model Checking for Polyhedral Logic, Stendhal, T-LADIES
Metrics:
See at:
CNR IRIS 
| link.springer.com | CNR IRIS 
| CNR IRIS
2026
Contribution to book
Open Access
Practical polyhedral model checking. A gentle introduction
Andriaccioyuri, Ciancia Vincenzo, Latella Diego, Massink Mieke
We illustrate the potential of spatial model checking of poly- hedral models on a number of selected examples. In computer graphics polyhedral models can be commonly found in the form of triangular sur- face meshes or tetrahedral volume meshes. Polyhedral model checking is used to analyse spatial properties of interest of such models expressed in a suitable spatial logic. For this work we use the recently developed geo- metric spatial model checker PolyLogicA, the visualiser PolyVisualizer and the polyhedral semantics of the Spatial Logic for Closure Spaces SLCS.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16470, pp. 138-159
DOI: 10.1007/978-3-032-12484-5_8
DOI: https://doi.org/10.1007/978-3-032-12484-5_8
Project(s): Ecosystems of Innovation, Project “Tuscany Health Ecosystem” (THE), Model Checking for Polyhedral Logic, Stendhal, T-LADIES
Metrics:
Andriaccioyuri, Ciancia Vincenzo, Latella Diego, Massink Mieke
We illustrate the potential of spatial model checking of poly- hedral models on a number of selected examples. In computer graphics polyhedral models can be commonly found in the form of triangular sur- face meshes or tetrahedral volume meshes. Polyhedral model checking is used to analyse spatial properties of interest of such models expressed in a suitable spatial logic. For this work we use the recently developed geo- metric spatial model checker PolyLogicA, the visualiser PolyVisualizer and the polyhedral semantics of the Spatial Logic for Closure Spaces SLCS.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 16470, pp. 138-159
DOI: 10.1007/978-3-032-12484-5_8
DOI: https://doi.org/10.1007/978-3-032-12484-5_8
Project(s): Ecosystems of Innovation, Project “Tuscany Health Ecosystem” (THE), Model Checking for Polyhedral Logic, Stendhal, T-LADIES
Metrics:
2026
Journal article
Open Access
Weak simplicial bisimilarity and minimisation for polyhedral model checking
Bezhanishvili Nick, Bussi Laura, Ciancia Vincenzo, Gabelaia David, Jibladze Mamuka, Latella Diego, Massink Mieke, De Vink Erik P.
The work described 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 polyhedral models is given by cell poset models, which are amenable to geometric spatial model checking on polyhedral models using the logical language SLCSη, a weaker version of SLCS. In this work we show that the mapping from polyhedral models to cell poset models preserves and reflects SLCSη. We also propose weak simplicial bisimilarity on polyhedral models and weak ±-bisimilarity on cell poset models, where by ``weak'' we mean that the relevant equivalence is coarser than the corresponding one for SLCS, leading to a greater reduction of the size of models and thus to more efficient model checking. We show that the proposed bisimilarities enjoy the Hennessy-Milner property, i.e. 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η. Furthermore we present a model minimisation procedure and prove that it correctly computes the minimal model with respect to weak ±-bisimilarity, i.e. with respect to logical equivalence of SLCSη. The procedure works via an encoding into LTSs and then exploits branching bisimilarity on those LTSs, exploiting the minimisation capabilities as included in the mCRL2 toolset. Various examples show the effectiveness of the approach.Source: LOGICAL METHODS IN COMPUTER SCIENCE, vol. 22 (issue 1), pp. 6:1-6:49
DOI: 10.46298/lmcs-22(1:6)2026
Project(s): Model Checking for Polyhedral Logic, Spatio-Temporal Enhancement of Neural nets for Deeply Hierarchical Automatised Logic, Tuscany Health Ecosystem, Typeful Language Adaptations for Dynamic, Interacting and Evolving Sysems
Metrics:
Bezhanishvili Nick, Bussi Laura, Ciancia Vincenzo, Gabelaia David, Jibladze Mamuka, Latella Diego, Massink Mieke, De Vink Erik P.
The work described 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 polyhedral models is given by cell poset models, which are amenable to geometric spatial model checking on polyhedral models using the logical language SLCSη, a weaker version of SLCS. In this work we show that the mapping from polyhedral models to cell poset models preserves and reflects SLCSη. We also propose weak simplicial bisimilarity on polyhedral models and weak ±-bisimilarity on cell poset models, where by ``weak'' we mean that the relevant equivalence is coarser than the corresponding one for SLCS, leading to a greater reduction of the size of models and thus to more efficient model checking. We show that the proposed bisimilarities enjoy the Hennessy-Milner property, i.e. 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η. Furthermore we present a model minimisation procedure and prove that it correctly computes the minimal model with respect to weak ±-bisimilarity, i.e. with respect to logical equivalence of SLCSη. The procedure works via an encoding into LTSs and then exploits branching bisimilarity on those LTSs, exploiting the minimisation capabilities as included in the mCRL2 toolset. Various examples show the effectiveness of the approach.Source: LOGICAL METHODS IN COMPUTER SCIENCE, vol. 22 (issue 1), pp. 6:1-6:49
DOI: 10.46298/lmcs-22(1:6)2026
Project(s): Model Checking for Polyhedral Logic, Spatio-Temporal Enhancement of Neural nets for Deeply Hierarchical Automatised Logic, Tuscany Health Ecosystem, Typeful Language Adaptations for Dynamic, Interacting and Evolving Sysems
Metrics:
See at:
CNR IRIS | lmcs.episciences.org | CNR IRIS
2025
Contribution to book
Open Access
Ten years of spatial model checking
Ciancia V., Latella D., Massink M.
Model checking has traditionally focused on the analysis of the behaviour of concurrent systems. When addressing more complex systems, such as large-scale collective adaptive systems, it quickly becomes clear that a focus on spatial aspects of such systems is as much relevant as the behavioural aspects. We provide a guided tour through the various research directions that this new focus on space has generated and is about to generate in the future.DOI: 10.1007/978-3-031-85134-6
Project(s): Ecosystems of Innovation, Project “Tuscany Health Ecosystem” (THE), Model Checking for Polyhedral Logic, Stendhal, T-LADIES
Metrics:
Ciancia V., Latella D., Massink M.
Model checking has traditionally focused on the analysis of the behaviour of concurrent systems. When addressing more complex systems, such as large-scale collective adaptive systems, it quickly becomes clear that a focus on spatial aspects of such systems is as much relevant as the behavioural aspects. We provide a guided tour through the various research directions that this new focus on space has generated and is about to generate in the future.DOI: 10.1007/978-3-031-85134-6
Project(s): Ecosystems of Innovation, Project “Tuscany Health Ecosystem” (THE), Model Checking for Polyhedral Logic, Stendhal, T-LADIES
Metrics:
See at:
CNR IRIS | link.springer.com | CNR IRIS | CNR IRIS
2025
Journal article
Open Access
On bisimilarity for quasi-discrete closure spaces
Ciancia V., Latella D., Massink M., De Vink E. P.
Closure spaces, a generalisation of topological spaces, have shown to be a convenient theoretical framework for spatial model-checking. The closure operator of closure spaces and quasi-discrete closure spaces induces a notion of neighbourhood akin to that of topological spaces that build on open sets. For closure models and quasi-discrete closure models, in this paper we present three notions of bisimilarity that are logically characterised by corresponding modal logics with spatial modalities: (i) CM-bisimilarity for closure models (CMs) is shown to generalise topo-bisimilarity for topological models and to be an instantiation of neighbourhood bisimilarity, when CMs are seen as (augmented) neighbourhood models. CM-bisimilarity corresponds to equivalence with respect to the infinitary modal logic IML that includes the modality N for “being near to”. (ii) CMC-bisimilarity, with CMC standing for CM-bisimilarity with converse, refines CM-bisimilarity for quasi-discrete closure spaces, carriers of quasi-discrete closure models. Quasi-discrete closure models come equipped with two closure operators, forward C and backward C, stemming from the binary relation underlying closure and its converse. CMC-bisimilarity, is captured by the infinitary modal logic IMLC including two modalities, forward N and backward N , corresponding to the two closure operators. (iii) CoPa-bisimilarity on quasi-discrete closure models, which is weaker than CMC-bisimilarity, is based on the notion of compatible paths. The logical counterpart of CoPa-bisimilarity is the infinitary modal logic ICRL with modalities forward ζ and backward ζ whose semantics relies on forward and backward paths, respectively. It is shown that CoPa-bisimilarity for quasi-discrete closure models relates to divergence-blind stuttering equivalence for Kripke models.Source: LOGICAL METHODS IN COMPUTER SCIENCE, vol. 21 (issue 3)
DOI: 10.46298/lmcs-21(3:21)2025
DOI: https://doi.org/10.46298/lmcs-21(3:21)2025
Project(s): Model Checking for Polyhedral Logic, Spatio-Temporal Enhancement of Neural nets for Deeply Hierarchical Automatised Logic, Tuscany Health Ecosystem, Typeful Language Adaptations for Dynamic, Interacting and Evolving Sysems
Metrics:
Ciancia V., Latella D., Massink M., De Vink E. P.
Closure spaces, a generalisation of topological spaces, have shown to be a convenient theoretical framework for spatial model-checking. The closure operator of closure spaces and quasi-discrete closure spaces induces a notion of neighbourhood akin to that of topological spaces that build on open sets. For closure models and quasi-discrete closure models, in this paper we present three notions of bisimilarity that are logically characterised by corresponding modal logics with spatial modalities: (i) CM-bisimilarity for closure models (CMs) is shown to generalise topo-bisimilarity for topological models and to be an instantiation of neighbourhood bisimilarity, when CMs are seen as (augmented) neighbourhood models. CM-bisimilarity corresponds to equivalence with respect to the infinitary modal logic IML that includes the modality N for “being near to”. (ii) CMC-bisimilarity, with CMC standing for CM-bisimilarity with converse, refines CM-bisimilarity for quasi-discrete closure spaces, carriers of quasi-discrete closure models. Quasi-discrete closure models come equipped with two closure operators, forward C and backward C, stemming from the binary relation underlying closure and its converse. CMC-bisimilarity, is captured by the infinitary modal logic IMLC including two modalities, forward N and backward N , corresponding to the two closure operators. (iii) CoPa-bisimilarity on quasi-discrete closure models, which is weaker than CMC-bisimilarity, is based on the notion of compatible paths. The logical counterpart of CoPa-bisimilarity is the infinitary modal logic ICRL with modalities forward ζ and backward ζ whose semantics relies on forward and backward paths, respectively. It is shown that CoPa-bisimilarity for quasi-discrete closure models relates to divergence-blind stuttering equivalence for Kripke models.Source: LOGICAL METHODS IN COMPUTER SCIENCE, vol. 21 (issue 3)
DOI: 10.46298/lmcs-21(3:21)2025
DOI: https://doi.org/10.46298/lmcs-21(3:21)2025
Project(s): Model Checking for Polyhedral Logic, Spatio-Temporal Enhancement of Neural nets for Deeply Hierarchical Automatised Logic, Tuscany Health Ecosystem, Typeful Language Adaptations for Dynamic, Interacting and Evolving Sysems
Metrics:
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
DOI: https://doi.org/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
DOI: https://doi.org/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
DOI: https://doi.org/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
DOI: https://doi.org/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
DOI: https://doi.org/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
DOI: https://doi.org/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: https://doi.org/10.32079/isti-tr-2023/003
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: https://doi.org/10.32079/isti-tr-2023/003
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
DOI: https://doi.org/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
DOI: https://doi.org/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: https://doi.org/10.32079/isti-tr-2023/009
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: https://doi.org/10.32079/isti-tr-2023/009
DOI: 10.32079/isti-tr-2023/009
Metrics:
See at:
CNR IRIS | ISTI Repository | CNR IRIS | CNR IRIS
2023
Other
Open Access
D3.2.1: AA@THE User needs, technical requirements and specifications
Lorenza Pratali, Franca Delmastro, Mattia Campana, Flavio Di Martino, Loreto Pescosolido, Paolo Barsocchi, Giovanna Broccia, Vincenzo Ciancia, Claudio Gennaro, Michele Girolami, Gabriele Lagani, Diego Latella, Massimo Magrini, Marco Manca, Mieke Massink, Andrea Mattioli, Davide Moroni, Filippo Palumbo, Paolo Paradisi, Fabio Paternò, Laura Sebastiani, Claudio Vairo, Carmelina Santoro, Davide La Rosa
The objective of this deliverable is to compile a comprehensive report that describes the user needs, requirements, and technical specifications necessary to successfully implement the pilot study. To achieve this, it is crucial to establish contacts with specific associations and medical experts, which, collaboratively, will help to establish exclusion and inclusion criteria for the target population of healthy adults. Furthermore, another related objective is to define the different categories of users that will interact with the system and their specific needs. This holistic approach will ensure that the system is designed and developed to satisfy the diverse needs of the users and be aligned with the goals of the project. To achieve the milestone M3.2.1, we made significant progresses in the definition of the pilot study for the AA@THE subproject. One of our key achievements is the successful description of users’ needs, requirements, and technical specifications necessary for the study. We worked closely with both a specialized association of personal trainers for Adapted Physical Activity (APA) for older adults, already active in the area of Pisa, and the medical partner who played a crucial role in providing valuable insights and expertise to establish exclusion and inclusion criteria for the target population of healthy adults. In this milestone, we also defined the activities and services that we intend to offer. Specifically, we plan to provide technological systems aimed at monitoring physical and cognitive training processes, as well as stability evaluations, by instrumenting a gym dedicated to active and healthy ageing, which is located within the CNR research area in Pisa. Additionally, we will conduct sleep, nutrition, and sedentary assessments at the volunteers' homes. Furthermore, we successfully defined the different user categories involved in the study. To facilitate the recruitment process and people engagement, on January 17th 2023, we organized an open day in collaboration with the gym association where we presented the overall objectives of the project and we collected feedbacks from a group of healthy adults over 65, already involved in APA training. This allowed us to gain a comprehensive understanding of the users' specific needs in terms of system interactions, thus establishing the system requirements and technical specifications of the AA@THE ecosystem. In parallel, a specific action on “Automatic Support of Medical Image Analysis” has been initiated by members of the “Formal Methods and Tools” group at CNR-ISTI. Such an action aims at leveraging Formal Methods in Computer Science, Logic and Model Checking to augment state-of-the-art machine learning techniques for automatic medical image analysis, enabling end-users to make specific assumptions on the level of accountability and affordability of the system. The methodology is based on a strict intertwining between theory and experimentation, with the development of new theoretical foundations for model reduction and efficient model checking, and experimentation and finalization of a graphical user interface that is being evaluated from the points of view of usability and of cognitive load. Moreover, the design and implementation of a suitable GUI able to support the analysis of medical images has been conducted and tested with small groups of people derived from the hospital in Lucca. The proposed GUI prototype has been evaluated from a cognitive point of view in order to allow easy employment with little training, for general practitioners and caregivers who may lack the technical skills required to use fully-fledged medical imaging programs.Project(s): Tuscany Health Ecosystem
Lorenza Pratali, Franca Delmastro, Mattia Campana, Flavio Di Martino, Loreto Pescosolido, Paolo Barsocchi, Giovanna Broccia, Vincenzo Ciancia, Claudio Gennaro, Michele Girolami, Gabriele Lagani, Diego Latella, Massimo Magrini, Marco Manca, Mieke Massink, Andrea Mattioli, Davide Moroni, Filippo Palumbo, Paolo Paradisi, Fabio Paternò, Laura Sebastiani, Claudio Vairo, Carmelina Santoro, Davide La Rosa
The objective of this deliverable is to compile a comprehensive report that describes the user needs, requirements, and technical specifications necessary to successfully implement the pilot study. To achieve this, it is crucial to establish contacts with specific associations and medical experts, which, collaboratively, will help to establish exclusion and inclusion criteria for the target population of healthy adults. Furthermore, another related objective is to define the different categories of users that will interact with the system and their specific needs. This holistic approach will ensure that the system is designed and developed to satisfy the diverse needs of the users and be aligned with the goals of the project. To achieve the milestone M3.2.1, we made significant progresses in the definition of the pilot study for the AA@THE subproject. One of our key achievements is the successful description of users’ needs, requirements, and technical specifications necessary for the study. We worked closely with both a specialized association of personal trainers for Adapted Physical Activity (APA) for older adults, already active in the area of Pisa, and the medical partner who played a crucial role in providing valuable insights and expertise to establish exclusion and inclusion criteria for the target population of healthy adults. In this milestone, we also defined the activities and services that we intend to offer. Specifically, we plan to provide technological systems aimed at monitoring physical and cognitive training processes, as well as stability evaluations, by instrumenting a gym dedicated to active and healthy ageing, which is located within the CNR research area in Pisa. Additionally, we will conduct sleep, nutrition, and sedentary assessments at the volunteers' homes. Furthermore, we successfully defined the different user categories involved in the study. To facilitate the recruitment process and people engagement, on January 17th 2023, we organized an open day in collaboration with the gym association where we presented the overall objectives of the project and we collected feedbacks from a group of healthy adults over 65, already involved in APA training. This allowed us to gain a comprehensive understanding of the users' specific needs in terms of system interactions, thus establishing the system requirements and technical specifications of the AA@THE ecosystem. In parallel, a specific action on “Automatic Support of Medical Image Analysis” has been initiated by members of the “Formal Methods and Tools” group at CNR-ISTI. Such an action aims at leveraging Formal Methods in Computer Science, Logic and Model Checking to augment state-of-the-art machine learning techniques for automatic medical image analysis, enabling end-users to make specific assumptions on the level of accountability and affordability of the system. The methodology is based on a strict intertwining between theory and experimentation, with the development of new theoretical foundations for model reduction and efficient model checking, and experimentation and finalization of a graphical user interface that is being evaluated from the points of view of usability and of cognitive load. Moreover, the design and implementation of a suitable GUI able to support the analysis of medical images has been conducted and tested with small groups of people derived from the hospital in Lucca. The proposed GUI prototype has been evaluated from a cognitive point of view in order to allow easy employment with little training, for general practitioners and caregivers who may lack the technical skills required to use fully-fledged medical imaging programs.Project(s): Tuscany Health Ecosystem
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: https://doi.org/10.32079/isti-tr-2022/027
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: https://doi.org/10.32079/isti-tr-2022/027
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: https://doi.org/10.32079/isti-tr-2022/018
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: https://doi.org/10.32079/isti-tr-2022/018
DOI: 10.32079/isti-tr-2022/018
Metrics:
See at:
CNR IRIS | ISTI Repository | CNR IRIS