CNR Author
operator:
and / or
Typology
operator:
and / or
Language
operator:
and / or
Date
operator:
and / or
Rights
operator:
and / or
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
Restricted
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
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
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
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
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
Contribution to book
Open Access
Towards model checking video streams using VoxLogicA on GPUs
Bussi L, Ciancia V, Gadducci F, Latella D, Massink M
We present a feasibility study on the use of spatial logic model checking for real-time analysis of high-resolution video streams with the tool VoxLogicA. VoxLogicA is a voxel-based image analyser based on the Spatial Logic for Closure Spaces, a logic catered to deal with properties of spatial structures such as topological spaces, graphs and polyhedra. The underlying language includes operators to model proximity and reachability. We demonstrate, via the analysis of a series of video frames from a well-known video game, that it is possible to analyse high-resolution videos in real-time by exploiting the speed-up of VoxLogicA-GPU, a recently developed GPU-based version of the tool, which is 1-2 orders of magnitude faster than its previous iteration. Potential applications of real-time video analysis include medical imaging applications such as ultrasound exams, and other video-based diagnostic techniques. More broadly speaking, this work can be the first step towards novel information retrieval methods suitable to find information in a declarative way, in possibly large collections of video streams.DOI: 10.1007/978-3-031-16011-0_6
Metrics:
Bussi L, Ciancia V, Gadducci F, Latella D, Massink M
We present a feasibility study on the use of spatial logic model checking for real-time analysis of high-resolution video streams with the tool VoxLogicA. VoxLogicA is a voxel-based image analyser based on the Spatial Logic for Closure Spaces, a logic catered to deal with properties of spatial structures such as topological spaces, graphs and polyhedra. The underlying language includes operators to model proximity and reachability. We demonstrate, via the analysis of a series of video frames from a well-known video game, that it is possible to analyse high-resolution videos in real-time by exploiting the speed-up of VoxLogicA-GPU, a recently developed GPU-based version of the tool, which is 1-2 orders of magnitude faster than its previous iteration. Potential applications of real-time video analysis include medical imaging applications such as ultrasound exams, and other video-based diagnostic techniques. More broadly speaking, this work can be the first step towards novel information retrieval methods suitable to find information in a declarative way, in possibly large collections of video streams.DOI: 10.1007/978-3-031-16011-0_6
Metrics:
See at:
CNR IRIS | link.springer.com | ISTI Repository | CNR IRIS | CNR IRIS
2022
Conference article
Open Access
On binding in the spatial logics for closure spaces
Bussi L, Ciancia V, Gadducci F, Latella D, Massink M
We present two different extensions of the spatial logic for closure spaces (SLCS), and its spatio-temporal variant (?SLCS), with spa- tial quantification operators. The first concerns the existential quantifi- cation on individual points of a space. The second concerns the quantifi- cation on sets of points. The latter amounts to a form of quantification over atomic propositions, thus without the full power of second order logic. The spatial quantification operators are useful for reasoning about the existence of particular spatial objects in a space, their spatial rela- tion with respect to other spatial objects, and, in the spatio-temporal setting, to reason about the dynamic evolution of such spatial objects in time and space, including reasoning about newly introduced items. In this preliminary study we illustrate the expressiveness of the operators by means of several small, but representative, examples.DOI: 10.1007/978-3-031-19849-6_27
Metrics:
Bussi L, Ciancia V, Gadducci F, Latella D, Massink M
We present two different extensions of the spatial logic for closure spaces (SLCS), and its spatio-temporal variant (?SLCS), with spa- tial quantification operators. The first concerns the existential quantifi- cation on individual points of a space. The second concerns the quantifi- cation on sets of points. The latter amounts to a form of quantification over atomic propositions, thus without the full power of second order logic. The spatial quantification operators are useful for reasoning about the existence of particular spatial objects in a space, their spatial rela- tion with respect to other spatial objects, and, in the spatio-temporal setting, to reason about the dynamic evolution of such spatial objects in time and space, including reasoning about newly introduced items. In this preliminary study we illustrate the expressiveness of the operators by means of several small, but representative, examples.DOI: 10.1007/978-3-031-19849-6_27
Metrics:
See at:
CNR IRIS | link.springer.com | CNR IRIS | CNR IRIS
2021
Conference article
Open Access
Querying medical imaging datasets using spatial logics (Position paper)
Belmonte G, Broccia G, Bussi L, Ciancia V, Latella D, Massink M
Nowadays a plethora of health data is available for clinical and research usage. Such existing datasets can be augmented through artificial-intelligence-based methods by automatic, personalised annotations and recommendations. This huge amount of data lends itself to new usage scenarios outside the boundaries where it was created; just to give some examples: to aggregate data sources in order to make research work more relevant; to incorporate a diversity of datasets in training of Machine Learning algorithms; to support expert decisions in telemedicine. In such a context, there is a growing need for a paradigm shift towards means to interrogate medical databases in a semantically meaningful way, fulfilling privacy and legal requirements, and transparently with respect to ethical concerns. In the specific domain of Medical Imaging, in this paper we sketch a research plan devoted to the definition and implementation of query languages that can unambiguously express semantically rich queries on possibly multi-dimensional images, in a human-readable, expert-friendly and concise way. Our approach is based on querying images using Topological Spatial Logics, building upon a novel spatial model checker called VoxLogicA, to execute such queries in a fully automated way.DOI: 10.1007/978-3-030-87657-9_22
Metrics:
Belmonte G, Broccia G, Bussi L, Ciancia V, Latella D, Massink M
Nowadays a plethora of health data is available for clinical and research usage. Such existing datasets can be augmented through artificial-intelligence-based methods by automatic, personalised annotations and recommendations. This huge amount of data lends itself to new usage scenarios outside the boundaries where it was created; just to give some examples: to aggregate data sources in order to make research work more relevant; to incorporate a diversity of datasets in training of Machine Learning algorithms; to support expert decisions in telemedicine. In such a context, there is a growing need for a paradigm shift towards means to interrogate medical databases in a semantically meaningful way, fulfilling privacy and legal requirements, and transparently with respect to ethical concerns. In the specific domain of Medical Imaging, in this paper we sketch a research plan devoted to the definition and implementation of query languages that can unambiguously express semantically rich queries on possibly multi-dimensional images, in a human-readable, expert-friendly and concise way. Our approach is based on querying images using Topological Spatial Logics, building upon a novel spatial model checker called VoxLogicA, to execute such queries in a fully automated way.DOI: 10.1007/978-3-030-87657-9_22
Metrics:
See at:
CNR IRIS | link.springer.com | ISTI Repository | CNR IRIS | CNR IRIS | link.springer.com