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
Other
Open Access
ISTI-day 2025 Proceedings
Del Corso G., Pedrotti A., Federico G., Gennaro C., Carrara F., Amato G., Di Benedetto M., Gabrielli E., Belli D., Matrullo Z., Miori V., Tolomei G., Waheed T., Marchetti E., Calabrò A., Rossetti G., Stella M., Cazabet R., Abramski K., Cau E., Citraro S., Failla A., Mesina V., Morini V., Pansanella V., Colantonio S., Germanese D., Pascali M. A., Bianchi L., Messina N., Falchi F., Barsellotti L., Pacini G., Cassese M., Puccetti G., Esuli A., Volpi L., Moreo A., Sebastiani F., Sperduti G., Nguyen D., Broccia G., Ter Beek M. H., Ferrari A., Massink M., Belmonte G., Ciancia V., Papini O., Canapa G., Catricalà B., Manca M., Paternò F., Santoro C., Zedda E., Gallo S., Maenza S., Mattioli A., Simeoli L., Rucci D., Carlini E., Dazzi P., Kavalionak H., Mordacchini M., Rulli C., Muntean Cristina Ioana, Nardini F. M., Perego R., Rocchietti G., Lettich F., Renso C., Pugliese C., Casini G., Haldimann J., Meyer T., Assante M., Candela L., Dell'Amico A., Frosini L., Mangiacrapa F., Oliviero A., Pagano P., Panichi G., Peccerillo B., Procaccini M., Mannocci A., Manghi P., Lonetti F., Kang D., Di Giandomenico F., Jee E., Lazzini G., Conti F., Scopigno R., D'Acunto M., Moroni D., Cafiso M., Paradisi P., Callieri M., Pavoni G., Corsini M., De Falco A., Sala F., Saraceni Q., Gattiglia G.
ISTI-Day is an annual information and networking event organized by the Institute of Information Science and Technologies "A. Faedo" (ISTI) of the Italian National Research Council (CNR). This event features an opening talk of the Director of the Dept. DIITET (Emilio F. Campana) as well as an overview of the Institute's activities presented by the ISTI Director (Roberto Scopigno). Those institutional segments are complemented by dedicated presentations and round tables featuring former staff members, as well as internal and external collaborators. To foster a network of knowledge and collaboration among newcomers, the 2025 ISTI Day edition also includes a large poster session that provides a comprehensive overview of current research activities. Each of the 13 laboratories contributes 1–3 posters, highlighting the most innovative work and offering early-career researchers a platform for discussion. Thus these proceedings include the posters selected for ISTI-Day 2025, reflecting the diverse and innovative nature of the Institute's research.
Del Corso G., Pedrotti A., Federico G., Gennaro C., Carrara F., Amato G., Di Benedetto M., Gabrielli E., Belli D., Matrullo Z., Miori V., Tolomei G., Waheed T., Marchetti E., Calabrò A., Rossetti G., Stella M., Cazabet R., Abramski K., Cau E., Citraro S., Failla A., Mesina V., Morini V., Pansanella V., Colantonio S., Germanese D., Pascali M. A., Bianchi L., Messina N., Falchi F., Barsellotti L., Pacini G., Cassese M., Puccetti G., Esuli A., Volpi L., Moreo A., Sebastiani F., Sperduti G., Nguyen D., Broccia G., Ter Beek M. H., Ferrari A., Massink M., Belmonte G., Ciancia V., Papini O., Canapa G., Catricalà B., Manca M., Paternò F., Santoro C., Zedda E., Gallo S., Maenza S., Mattioli A., Simeoli L., Rucci D., Carlini E., Dazzi P., Kavalionak H., Mordacchini M., Rulli C., Muntean Cristina Ioana, Nardini F. M., Perego R., Rocchietti G., Lettich F., Renso C., Pugliese C., Casini G., Haldimann J., Meyer T., Assante M., Candela L., Dell'Amico A., Frosini L., Mangiacrapa F., Oliviero A., Pagano P., Panichi G., Peccerillo B., Procaccini M., Mannocci A., Manghi P., Lonetti F., Kang D., Di Giandomenico F., Jee E., Lazzini G., Conti F., Scopigno R., D'Acunto M., Moroni D., Cafiso M., Paradisi P., Callieri M., Pavoni G., Corsini M., De Falco A., Sala F., Saraceni Q., Gattiglia G.
ISTI-Day is an annual information and networking event organized by the Institute of Information Science and Technologies "A. Faedo" (ISTI) of the Italian National Research Council (CNR). This event features an opening talk of the Director of the Dept. DIITET (Emilio F. Campana) as well as an overview of the Institute's activities presented by the ISTI Director (Roberto Scopigno). Those institutional segments are complemented by dedicated presentations and round tables featuring former staff members, as well as internal and external collaborators. To foster a network of knowledge and collaboration among newcomers, the 2025 ISTI Day edition also includes a large poster session that provides a comprehensive overview of current research activities. Each of the 13 laboratories contributes 1–3 posters, highlighting the most innovative work and offering early-career researchers a platform for discussion. Thus these proceedings include the posters selected for ISTI-Day 2025, reflecting the diverse and innovative nature of the Institute's research.
See at:
CNR IRIS | www.isti.cnr.it | CNR IRIS
2025
Journal article
Open Access
Symbolic and hybrid AI for brain tissue segmentation using spatial model checking
Belmonte G., Ciancia V., Massink M.
Segmentation of 3D medical images, and brain segmentation in particular, is an important topic in neuroimaging and in radiotherapy. Overcoming the current, time consuming, practise of manual delineation of brain tumours and providing an accurate, explainable, and replicable method of segmentation of the tumour area and related tissues is therefore an open research challenge. In this paper, we first propose a novel symbolic approach to brain segmentation and delineation of brain lesions based on spatial model checking. This method has its foundations in the theory of closure spaces, a generalisation of topological spaces, and spatial logics. At its core is a high-level declarative logic language for image analysis, ImgQL, and an efficient spatial model checker, VoxLogicA, exploiting state-of-the-art image analysis libraries in its model checking algorithm. We then illustrate how this technique can be combined with Machine Learning techniques leading to a hybrid AI approach that provides accurate and explainable segmentation results. We show the results of the application of the symbolic approach on several public datasets with 3D magnetic resonance (MR) images. Three datasets are provided by the 2017, 2019 and 2020 international MICCAI BraTS Challenges with 210, 259 and 293 MR images, respectively, and the fourth is the BrainWeb dataset with 20 (synthetic) 3D patient images of the normal brain. We then apply the hybrid AI method to the BraTS 2020 training set. Our segmentation results are shown to be in line with the state-of-the-art with respect to other recent approaches, both from the accuracy point of view as well as from the view of computational efficiency, but with the advantage of them being explainable.Source: ARTIFICIAL INTELLIGENCE IN MEDICINE, vol. 167 (issue 103154)
DOI: 10.1016/j.artmed.2025.103154
Project(s): Model Checking for Polyhedral Logic, Spatio-Temporal Enhancement of Neural Nets for Deeply Hierarchical Automatised Logic, Tuscany Health Ecosystem
Metrics:
Belmonte G., Ciancia V., Massink M.
Segmentation of 3D medical images, and brain segmentation in particular, is an important topic in neuroimaging and in radiotherapy. Overcoming the current, time consuming, practise of manual delineation of brain tumours and providing an accurate, explainable, and replicable method of segmentation of the tumour area and related tissues is therefore an open research challenge. In this paper, we first propose a novel symbolic approach to brain segmentation and delineation of brain lesions based on spatial model checking. This method has its foundations in the theory of closure spaces, a generalisation of topological spaces, and spatial logics. At its core is a high-level declarative logic language for image analysis, ImgQL, and an efficient spatial model checker, VoxLogicA, exploiting state-of-the-art image analysis libraries in its model checking algorithm. We then illustrate how this technique can be combined with Machine Learning techniques leading to a hybrid AI approach that provides accurate and explainable segmentation results. We show the results of the application of the symbolic approach on several public datasets with 3D magnetic resonance (MR) images. Three datasets are provided by the 2017, 2019 and 2020 international MICCAI BraTS Challenges with 210, 259 and 293 MR images, respectively, and the fourth is the BrainWeb dataset with 20 (synthetic) 3D patient images of the normal brain. We then apply the hybrid AI method to the BraTS 2020 training set. Our segmentation results are shown to be in line with the state-of-the-art with respect to other recent approaches, both from the accuracy point of view as well as from the view of computational efficiency, but with the advantage of them being explainable.Source: ARTIFICIAL INTELLIGENCE IN MEDICINE, vol. 167 (issue 103154)
DOI: 10.1016/j.artmed.2025.103154
Project(s): Model Checking for Polyhedral Logic, Spatio-Temporal Enhancement of Neural Nets for Deeply Hierarchical Automatised Logic, Tuscany Health Ecosystem
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
Contribution to book
Open Access
A spatial logic with time and quantifiers
Bussi L., Ciancia V., Gadducci F.
Spatial logics are formalisms for expressing topological prop erties of structures based on geometrical entities and relations. In this paper we consider SLCS, the Spatial Logic for Closure Spaces, recently used for describing features of images and video frames. We extend SLCS in two directions. We first introduce first-order quantifiers, rang ing on both individuals and atomic propositions. We then equip the logic with temporal operators, and provide a linear-time semantics over finite traces. The resulting formalism allows to state properties about geomet rical entities whose attributes change along time. For both extensions, we prove the equivalence of their operational semantics with a denotational one.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 14401, pp. 1-19
DOI: 10.1007/978-3-031-51777-8_1
Metrics:
Bussi L., Ciancia V., Gadducci F.
Spatial logics are formalisms for expressing topological prop erties of structures based on geometrical entities and relations. In this paper we consider SLCS, the Spatial Logic for Closure Spaces, recently used for describing features of images and video frames. We extend SLCS in two directions. We first introduce first-order quantifiers, rang ing on both individuals and atomic propositions. We then equip the logic with temporal operators, and provide a linear-time semantics over finite traces. The resulting formalism allows to state properties about geomet rical entities whose attributes change along time. For both extensions, we prove the equivalence of their operational semantics with a denotational one.Source: LECTURE NOTES IN COMPUTER SCIENCE, vol. 14401, pp. 1-19
DOI: 10.1007/978-3-031-51777-8_1
Metrics:
See at:
IRIS Cnr | IRIS Cnr | IRIS Cnr | doi.org | Archivio della Ricerca - Università di Pisa | CNR IRIS | CNR IRIS
2024
Conference article
Open Access
Logics of polyhedral reachability
Bezhanishvili N., Bussi L., Ciancia V., Fernandez-Duque D., Gabelaia D.
Polyhedral semantics is a recently introduced branch of spatial modal logic, in which modal formulas are interpreted as piecewise linear subsets of an Euclidean space. Polyhedral semantics for the basic modal language has already been well investigated. However, for many practical applications of polyhedral semantics, it is advantageous to enrich the basic modal language with a reachability modality. Recently, a language with an Until-like spatial modality has been introduced, with demonstrated applicability to the analysis of 3D meshes via model checking. In this paper, we exhibit an axiom system for this logic, and show that it is complete with respect to polyhedral semantics. The proof consists of two major steps: First, we show that this logic, which is built over Grzegorczyk's system $\mathsf{Grz}$, has the finite model property. Subsequently, we show that every formula satisfied in a finite poset is also satisfied in a polyhedral model, thereby establishing polyhedral completeness.Source: ADVANCES IN MODAL LOGIC, vol. 15. Praga, Czech Republic, 19-23/08/2024
Project(s): Model Checking for Polyhedral Logic, PRIN 2022 STENDHAL, Tuscany Health Ecosystem
Bezhanishvili N., Bussi L., Ciancia V., Fernandez-Duque D., Gabelaia D.
Polyhedral semantics is a recently introduced branch of spatial modal logic, in which modal formulas are interpreted as piecewise linear subsets of an Euclidean space. Polyhedral semantics for the basic modal language has already been well investigated. However, for many practical applications of polyhedral semantics, it is advantageous to enrich the basic modal language with a reachability modality. Recently, a language with an Until-like spatial modality has been introduced, with demonstrated applicability to the analysis of 3D meshes via model checking. In this paper, we exhibit an axiom system for this logic, and show that it is complete with respect to polyhedral semantics. The proof consists of two major steps: First, we show that this logic, which is built over Grzegorczyk's system $\mathsf{Grz}$, has the finite model property. Subsequently, we show that every formula satisfied in a finite poset is also satisfied in a polyhedral model, thereby establishing polyhedral completeness.Source: ADVANCES IN MODAL LOGIC, vol. 15. Praga, Czech Republic, 19-23/08/2024
Project(s): Model Checking for Polyhedral Logic, PRIN 2022 STENDHAL, Tuscany Health Ecosystem
See at:
CNR IRIS | www.cs.cas.cz | 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
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
Software
Metadata Only Access
A toolchain for strategy synthesis with spatial properties - Complementary material
Basile D, Ter Beek Mh, Bussi L, Ciancia V
This is the complementary material for our paper ``A Toolchain for Strategy Synthesis with Spatial Properties'' accepted for publication at the Journal of Software Tools and Technology Transfer. This repository contains a permanent snapshot of https://github.com/contractautomataproject/CATLib_PngConverter/tree/ec0938043146b008bbbcb4ed3ec79c06dd2e47d6DOI: 10.5281/zenodo.8220527
Metrics:
Basile D, Ter Beek Mh, Bussi L, Ciancia V
This is the complementary material for our paper ``A Toolchain for Strategy Synthesis with Spatial Properties'' accepted for publication at the Journal of Software Tools and Technology Transfer. This repository contains a permanent snapshot of https://github.com/contractautomataproject/CATLib_PngConverter/tree/ec0938043146b008bbbcb4ed3ec79c06dd2e47d6DOI: 10.5281/zenodo.8220527
Metrics:
See at:
CNR 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
2023
Journal article
Open Access
A toolchain for strategy synthesis with spatial properties
Basile D, Ter Beek Mh, Bussi L, Ciancia V
We present an application of strategy synthesis to enforce spatial properties. This is achieved by implementing a toolchain that enables the tools \texttt{CATLib} and \texttt{VoxLogicA} to interact in a fully automated way. The Contract Automata Library (\texttt{CATLib}) is aimed at both composition and strategy synthesis of games modelled in a dialect of finite state automata.The Voxel-based Logical Analyser (\texttt{VoxLogicA}) is a spatial model checker for the verification of properties expressed using the Spatial Logic of Closure Spaces on pixels of digital images.We provide examples of strategy synthesis on automata encoding motion of agents in spaces represented by images, as well as a proof-of-concept realistic example based on a case study from the railway domain.The strategies are synthesised with \texttt{CAT\-Lib}, while the properties to enforce are defined by means of spatial model checking of the images with \texttt{VoxLogicA}.The combination of spatial model checking with strategy synthesis provides a toolchain for checking and enforcing mobility properties in multi-agent systems in which location plays an important role, like in many collective adaptive systems.We discuss the toolchain's performance also considering several recent improvements.Source: INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER (PRINT), vol. 25, pp. 641-658
DOI: 10.1007/s10009-023-00730-1
Project(s): Methods and Tools for Trustworthy Smart Systems, Sustainable MobilityNational Research Center, Tuscany Health Ecosystem
Metrics:
Basile D, Ter Beek Mh, Bussi L, Ciancia V
We present an application of strategy synthesis to enforce spatial properties. This is achieved by implementing a toolchain that enables the tools \texttt{CATLib} and \texttt{VoxLogicA} to interact in a fully automated way. The Contract Automata Library (\texttt{CATLib}) is aimed at both composition and strategy synthesis of games modelled in a dialect of finite state automata.The Voxel-based Logical Analyser (\texttt{VoxLogicA}) is a spatial model checker for the verification of properties expressed using the Spatial Logic of Closure Spaces on pixels of digital images.We provide examples of strategy synthesis on automata encoding motion of agents in spaces represented by images, as well as a proof-of-concept realistic example based on a case study from the railway domain.The strategies are synthesised with \texttt{CAT\-Lib}, while the properties to enforce are defined by means of spatial model checking of the images with \texttt{VoxLogicA}.The combination of spatial model checking with strategy synthesis provides a toolchain for checking and enforcing mobility properties in multi-agent systems in which location plays an important role, like in many collective adaptive systems.We discuss the toolchain's performance also considering several recent improvements.Source: INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER (PRINT), vol. 25, pp. 641-658
DOI: 10.1007/s10009-023-00730-1
Project(s): Methods and Tools for Trustworthy Smart Systems, Sustainable MobilityNational Research Center, Tuscany Health Ecosystem
Metrics:
See at:
CNR IRIS | ISTI Repository | 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
Conference article
Open Access
An experimental toolchain for strategy synthesis with spatial properties
Basile D, Ter Beek Mh, 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.DOI: 10.1007/978-3-031-19759-8_10
Metrics:
Basile D, Ter Beek Mh, 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.DOI: 10.1007/978-3-031-19759-8_10
Metrics:
See at:
CNR IRIS | link.springer.com | ISTI Repository | CNR IRIS | CNR IRIS | CNR IRIS