2013
Conference article
Open Access
Interaction and observation: categorical semantics of reactive systems trough dialgebras
Ciancia V
We use dialgebras, generalising both algebras and coalgebras, as a complement of the standard coalgebraic framework, aimed at describing the semantics of an interactive system by the means of reaction rules. In this model, interaction is built-in, and semantic equivalence arises from it, instead of being determined by a (possibly difficult) understanding of the side effects of a component in isolation. Behavioural equivalence in dialgebras is determined by how a given process interacts with the others, and the obtained observations. We develop a technique to inter-define categories of dialgebras of different functors, that in particular permits us to compare a standard coalgebraic semantics and its dialgebraic counterpart. We exemplify the framework using the CCS and the ?-calculus. Remarkably, the dialgebra giving semantics to the ?-calculus does not require the use of presheaf categories.DOI: 10.1007/978-3-642-40206-7_10
DOI: 10.48550/arxiv.1209.5903
Project(s): QUANTICOL
Metrics:
Ciancia V
We use dialgebras, generalising both algebras and coalgebras, as a complement of the standard coalgebraic framework, aimed at describing the semantics of an interactive system by the means of reaction rules. In this model, interaction is built-in, and semantic equivalence arises from it, instead of being determined by a (possibly difficult) understanding of the side effects of a component in isolation. Behavioural equivalence in dialgebras is determined by how a given process interacts with the others, and the obtained observations. We develop a technique to inter-define categories of dialgebras of different functors, that in particular permits us to compare a standard coalgebraic semantics and its dialgebraic counterpart. We exemplify the framework using the CCS and the ?-calculus. Remarkably, the dialgebra giving semantics to the ?-calculus does not require the use of presheaf categories.DOI: 10.1007/978-3-642-40206-7_10
DOI: 10.48550/arxiv.1209.5903
Project(s): QUANTICOL
Metrics:
See at:
arXiv.org e-Print Archive 
| arxiv.org | doi.org 
| doi.org | CNR IRIS | CNR IRIS | link.springer.com
2019
Contribution to book
Open Access
Omega-Automata: A Coalgebraic Perspective on Regular omega-Languages
Ciancia V, Venema Y
In this work, we provide a simple coalgebraic characterisation of regular ?-languages based on languages of lassos, and prove a number of related mathematical results, framed into the theory of a new kind of automata called Ohm-automata. In earlier work we introduced Ohm-automata as two-sorted structures that naturally operate on lassos, pairs of words encoding ultimately periodic streams (infinite words). Here we extend the scope of these Ohm-automata by proposing them as a new kind of acceptor for arbitrary streams. We prove that Ohm-automata are expressively complete for the regular ?-languages. We show that, due to their coalgebraic nature, Ohm-automata share some attractive properties with deterministic automata operating on finite words, properties that other types of stream automata lack. In particular, we provide a simple, coalgebraic definition of bisimilarity between Ohm-automata that exactly captures language equivalence and allows for a simple minimization procedure. We also prove a coalgebraic Myhill-Nerode style theorem for lasso languages, and use this result, in combination with a closure property on stream languages called lasso determinacy, to give a characterization of regular ?-languages.Source: LEIBNIZ INTERNATIONAL PROCEEDINGS IN INFORMATICS, pp. 5:1-5:18
DOI: 10.4230/lipics.calco.2019.5
Metrics:
Ciancia V, Venema Y
In this work, we provide a simple coalgebraic characterisation of regular ?-languages based on languages of lassos, and prove a number of related mathematical results, framed into the theory of a new kind of automata called Ohm-automata. In earlier work we introduced Ohm-automata as two-sorted structures that naturally operate on lassos, pairs of words encoding ultimately periodic streams (infinite words). Here we extend the scope of these Ohm-automata by proposing them as a new kind of acceptor for arbitrary streams. We prove that Ohm-automata are expressively complete for the regular ?-languages. We show that, due to their coalgebraic nature, Ohm-automata share some attractive properties with deterministic automata operating on finite words, properties that other types of stream automata lack. In particular, we provide a simple, coalgebraic definition of bisimilarity between Ohm-automata that exactly captures language equivalence and allows for a simple minimization procedure. We also prove a coalgebraic Myhill-Nerode style theorem for lasso languages, and use this result, in combination with a closure property on stream languages called lasso determinacy, to give a characterization of regular ?-languages.Source: LEIBNIZ INTERNATIONAL PROCEEDINGS IN INFORMATICS, pp. 5:1-5:18
DOI: 10.4230/lipics.calco.2019.5
Metrics:
See at:
drops.dagstuhl.de | CNR IRIS | ISTI Repository | CNR IRIS
2016
Contribution to book
Open Access
From urelements to computation: A journey through applications of Fraenkel's permutation model in computer science
Ciancia V
Around 1922-1938, a new permutation model of set theory was defined. The permutation model served as a counterexample in the first proof of independence of the Axiom of Choice from the other axioms of Zermelo-Fraenkel set theory. Almost a century later, a model introduced as part of a proof in abstract mathematics fostered a plethora of research results, ranging from the area of syntax and semantics of programming languages to minimization algorithms and automated verification of systems. Among these results, we find Lawvere-style algebraic syntax with binders, final-coalgebra semantics with resource allocation, and minimization algorithms for mobile systems. These results are also obtained in various different ways, by describing, in terms of category theory, a number of models equivalent to the permutation model. We aim at providing both a brief history of some of these developments, and a mild introduction to the recent research line of "nominal computation theory", where the essential notion of name is declined in several different ways.DOI: 10.1007/978-3-319-47286-7_10
Project(s): QUANTICOL, ASCENS
Metrics:
Ciancia V
Around 1922-1938, a new permutation model of set theory was defined. The permutation model served as a counterexample in the first proof of independence of the Axiom of Choice from the other axioms of Zermelo-Fraenkel set theory. Almost a century later, a model introduced as part of a proof in abstract mathematics fostered a plethora of research results, ranging from the area of syntax and semantics of programming languages to minimization algorithms and automated verification of systems. Among these results, we find Lawvere-style algebraic syntax with binders, final-coalgebra semantics with resource allocation, and minimization algorithms for mobile systems. These results are also obtained in various different ways, by describing, in terms of category theory, a number of models equivalent to the permutation model. We aim at providing both a brief history of some of these developments, and a mild introduction to the recent research line of "nominal computation theory", where the essential notion of name is declined in several different ways.DOI: 10.1007/978-3-319-47286-7_10
Project(s): QUANTICOL
, ASCENS Metrics:
See at:
hal.inria.fr | doi.org | CNR IRIS | CNR IRIS | link-springer-com-443.webvpn.fjmu.edu.cn
2021
Conference article
Open Access
Towards a spatial model checker on GPU
Bussi L, Ciancia V, Gadducci F
The tool VoxLogicA merges the state-of-the-art library of computational imaging algorithms ITK with the combination of declarative specification and optimised execution provided by spatial logic model checking. The analysis of an existing benchmark for segmentation of brain tumours via a simple logical specification reached very high accuracy. We introduce a new, GPU-based version of VoxLogicA and present preliminary results on its implementation, scalability, and applications.DOI: 10.1007/978-3-030-78089-0_12
Metrics:
Bussi L, Ciancia V, Gadducci F
The tool VoxLogicA merges the state-of-the-art library of computational imaging algorithms ITK with the combination of declarative specification and optimised execution provided by spatial logic model checking. The analysis of an existing benchmark for segmentation of brain tumours via a simple logical specification reached very high accuracy. We introduce a new, GPU-based version of VoxLogicA and present preliminary results on its implementation, scalability, and applications.DOI: 10.1007/978-3-030-78089-0_12
Metrics:
See at:
CNR IRIS | link.springer.com | ISTI Repository | CNR IRIS | CNR IRIS
2020
Other
Open Access
A spatial model checker in GPU (extended version)
Bussi L, Ciancia V, Gadducci F
The tool voxlogica merges the state-of-the-art library of computational imaging algorithms ITK with the combination of declarative specification and optimised execution provided by spatial logic model checking. The analysis of an existing benchmark for segmentation of brain tumours via a simple logical specification reached state-of-the-art accuracy. We present a new, GPU-based version of voxlogica and discuss its implementation, scalability, and applications.
Bussi L, Ciancia V, Gadducci F
The tool voxlogica merges the state-of-the-art library of computational imaging algorithms ITK with the combination of declarative specification and optimised execution provided by spatial logic model checking. The analysis of an existing benchmark for segmentation of brain tumours via a simple logical specification reached state-of-the-art accuracy. We present a new, GPU-based version of voxlogica and discuss its implementation, scalability, and applications.
See at:
arxiv.org | CNR IRIS | ISTI Repository | CNR IRIS
2014
Contribution to book
Restricted
Quantitative Evaluation of Enforcement Strategies
Ciancia V, Martinelli F, Matteucci I, Morisset C
A security enforcement mechanism runs in parallel with a system to check and modify its run-time behaviour, so that it satisfies some security policy. For each policy, several enforcement strategies are possible, usually reflecting trade-offs one has to make to satisfy the policy. To evaluate them, multiple dimensions, such as security, cost of implementation, or cost of attack, must be taken into account. We propose a formal framework for the quantification of enforcement strategies, extending the notion of controller processes (mimicking the well-known edit automata) with weights on transitions, valued in a semiring.DOI: 10.1007/978-3-319-05302-8_11
Metrics:
Ciancia V, Martinelli F, Matteucci I, Morisset C
A security enforcement mechanism runs in parallel with a system to check and modify its run-time behaviour, so that it satisfies some security policy. For each policy, several enforcement strategies are possible, usually reflecting trade-offs one has to make to satisfy the policy. To evaluate them, multiple dimensions, such as security, cost of implementation, or cost of attack, must be taken into account. We propose a formal framework for the quantification of enforcement strategies, extending the notion of controller processes (mimicking the well-known edit automata) with weights on transitions, valued in a semiring.DOI: 10.1007/978-3-319-05302-8_11
Metrics:
See at:
doi.org | CNR IRIS | CNR IRIS | link.springer.com
2016
Conference article
Open Access
Nominal cellular automata
Bolognesi T, Ciancia V
The emerging field of Nominal Computation Theory is concerned with the theory of Nominal Sets and its applications to Computer Science. We investigate here the impact of nominal sets on the definition of Cellular Automata and on their computational capabilities, with a special focus on the emergent behavioural properties of this new model and their significance in the context of computation-oriented interpretations of physical phenomena. A preliminary investigation of the relations between Nominal Cellular Automata and Wolfram's Elementary Cellular Automata is also carried out.Source: ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, pp. 24-35. Heraklion, Crete, Greece, 8-9 June 2016
DOI: 10.4204/eptcs.223.2
DOI: 10.48550/arxiv.1608.03320
Project(s): QUANTICOL
Metrics:
Bolognesi T, Ciancia V
The emerging field of Nominal Computation Theory is concerned with the theory of Nominal Sets and its applications to Computer Science. We investigate here the impact of nominal sets on the definition of Cellular Automata and on their computational capabilities, with a special focus on the emergent behavioural properties of this new model and their significance in the context of computation-oriented interpretations of physical phenomena. A preliminary investigation of the relations between Nominal Cellular Automata and Wolfram's Elementary Cellular Automata is also carried out.Source: ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, pp. 24-35. Heraklion, Crete, Greece, 8-9 June 2016
DOI: 10.4204/eptcs.223.2
DOI: 10.48550/arxiv.1608.03320
Project(s): QUANTICOL
Metrics:
See at:
arXiv.org e-Print Archive | Electronic Proceedings in Theoretical Computer Science | Electronic Proceedings in Theoretical Computer Science | Electronic Proceedings in Theoretical Computer Science | eptcs.web.cse.unsw.edu.au | CNR IRIS | ISTI Repository | doi.org | CNR IRIS
2017
Journal article
Restricted
Exploring nominal cellular automata
Bolognesi T, Ciancia V
he emerging field of Nominal Computation Theory is concerned with the theory of Nominal Sets and its applications to Computer Science. We investigate here the impact of nominal sets on the definition of Cellular Automata and on their computational capabilities, with a special focus on the emergent behavioural properties of this new model and their significance in the context of computation-oriented interpretations of physical phenomena. An investigation of the relations between Nominal Cellular Automata and Wolfram's Elementary Cellular Automata is carried out, together with an analysis of interesting particles, exhibiting "nominal" behaviour, in a particular kind of rules, reminiscent of the class of totalistic Cellular Automata, that we call "bagged".Source: THE JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, vol. 93, pp. 23-41
DOI: 10.1016/j.jlamp.2017.08.001
Project(s): QUANTICOL
Metrics:
Bolognesi T, Ciancia V
he emerging field of Nominal Computation Theory is concerned with the theory of Nominal Sets and its applications to Computer Science. We investigate here the impact of nominal sets on the definition of Cellular Automata and on their computational capabilities, with a special focus on the emergent behavioural properties of this new model and their significance in the context of computation-oriented interpretations of physical phenomena. An investigation of the relations between Nominal Cellular Automata and Wolfram's Elementary Cellular Automata is carried out, together with an analysis of interesting particles, exhibiting "nominal" behaviour, in a particular kind of rules, reminiscent of the class of totalistic Cellular Automata, that we call "bagged".Source: THE JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, vol. 93, pp. 23-41
DOI: 10.1016/j.jlamp.2017.08.001
Project(s): QUANTICOL
Metrics:
See at:
Journal of Logical and Algebraic Methods in Programming | CNR IRIS | CNR IRIS | www.sciencedirect.com
2018
Journal article
Open Access
Qualitative and quantitative monitoring of spatio-temporal properties with SSTL
Nenzi L, Bortolussi L, Ciancia V, Loreti M, Massink M
In spatially located, large scale systems, time and space dynamics interact and drives the behaviour. Examples of such systems can be found in many smart city applications and Cyber-Physical Systems. In this paper we present the Signal Spatio-Temporal Logic (SSTL), a modal logic that can be used to specify spatio-temporal properties of linear time and discrete space models. The logic is equipped with a Boolean and a quantitative semantics for which ecient monitoring algorithms have been developed. As such, it is suitable for real-time verication of both white box and black box complex systems. These algorithms can also be combined with stochastic model checking routines. SSTL combines the until temporal modality with two spatial modalities, one expressing that something is true somewhere nearby and the other capturing the notion of being surrounded by a region that satises a given spatio-temporal property. The monitoring algorithms are implemented in an open source Java tool. We illustrate the use of SSTL analysing the formation of patterns in a Turing Reaction-Diusion system and spatio-temporal aspects of a large bike-sharing system.Source: LOGICAL METHODS IN COMPUTER SCIENCE, vol. 14 (issue 4), pp. 1-38
DOI: 10.23638/lmcs-14(4:2)2018
DOI: 10.48550/arxiv.1706.09334
Project(s): QUANTICOL
Metrics:
Nenzi L, Bortolussi L, Ciancia V, Loreti M, Massink M
In spatially located, large scale systems, time and space dynamics interact and drives the behaviour. Examples of such systems can be found in many smart city applications and Cyber-Physical Systems. In this paper we present the Signal Spatio-Temporal Logic (SSTL), a modal logic that can be used to specify spatio-temporal properties of linear time and discrete space models. The logic is equipped with a Boolean and a quantitative semantics for which ecient monitoring algorithms have been developed. As such, it is suitable for real-time verication of both white box and black box complex systems. These algorithms can also be combined with stochastic model checking routines. SSTL combines the until temporal modality with two spatial modalities, one expressing that something is true somewhere nearby and the other capturing the notion of being surrounded by a region that satises a given spatio-temporal property. The monitoring algorithms are implemented in an open source Java tool. We illustrate the use of SSTL analysing the formation of patterns in a Turing Reaction-Diusion system and spatio-temporal aspects of a large bike-sharing system.Source: LOGICAL METHODS IN COMPUTER SCIENCE, vol. 14 (issue 4), pp. 1-38
DOI: 10.23638/lmcs-14(4:2)2018
DOI: 10.48550/arxiv.1706.09334
Project(s): QUANTICOL
Metrics:
See at:
arXiv.org e-Print Archive | Archivio istituzionale della ricerca - Università di Trieste | Archivio istituzionale della ricerca - Università di Camerino | CNR IRIS | Episciences | ISTI Repository | doi.org | doi.org | CNR IRIS
2019
Journal article
Open Access
VoxLogicA: a Spatial-Logic based tool for Declarative Image Analysis
Belmonte G, Ciancia V, Latella D, Massink M
Glioblastomas are among the most common malignant intracranial tumours. Neuroimaging protocols are used before and after treatment to evaluate its effect and to monitor the evolution of the disease. In clinical studies and routine treatment, magnetic resonance images (MRI) are evaluated, largely manually, and based on qualitative criteria such as the presence of hyper-intense tissue in the image. VoxLogicA is an image analysis tool, designed to perform tasks such as identifying brain tumours in 3D magneto-resonance scans. The aim is to have a system that is portable, predictable and reproducible, and requires minimal computing expertise to operate.Source: ERCIM NEWS, vol. 118, pp. 12-13
Project(s): QUANTICOL
Belmonte G, Ciancia V, Latella D, Massink M
Glioblastomas are among the most common malignant intracranial tumours. Neuroimaging protocols are used before and after treatment to evaluate its effect and to monitor the evolution of the disease. In clinical studies and routine treatment, magnetic resonance images (MRI) are evaluated, largely manually, and based on qualitative criteria such as the presence of hyper-intense tissue in the image. VoxLogicA is an image analysis tool, designed to perform tasks such as identifying brain tumours in 3D magneto-resonance scans. The aim is to have a system that is portable, predictable and reproducible, and requires minimal computing expertise to operate.Source: ERCIM NEWS, vol. 118, pp. 12-13
Project(s): QUANTICOL
See at:
ercim-news.ercim.eu | CNR IRIS | ISTI Repository | CNR IRIS
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
2012
Conference article
Open Access
A tool for the synthesis of cryptographic orchestrators
Ciancia V., Martin J. A., Martinelli F., Matteucci I., Petrocchi M., Pimentel E.
Security is one of the main challenges of service oriented computing. Services need to be loosely coupled, easily accessible and yet provide tight security guarantees enforced by cryptographic protocols. In this paper, we address how to automatically synthesize an orchestrator process able to guarantee the secure composition of electronic services, supporting different communication and cryptographic protocols. We present a theoretical model based on process algebra, partial model checking and logical satisfiability, plus an automated tool implementing the proposed theory.DOI: 10.1145/2422498.2422508
Project(s): ANIKETOS
Metrics:
Ciancia V., Martin J. A., Martinelli F., Matteucci I., Petrocchi M., Pimentel E.
Security is one of the main challenges of service oriented computing. Services need to be loosely coupled, easily accessible and yet provide tight security guarantees enforced by cryptographic protocols. In this paper, we address how to automatically synthesize an orchestrator process able to guarantee the secure composition of electronic services, supporting different communication and cryptographic protocols. We present a theoretical model based on process algebra, partial model checking and logical satisfiability, plus an automated tool implementing the proposed theory.DOI: 10.1145/2422498.2422508
Project(s): ANIKETOS
Metrics:
See at:
IRIS Cnr | IRIS Cnr | IRIS Cnr | dblp.uni-trier.de | doi.org | Hal | 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
2013
Other
Open Access
Quantitative evaluation of enforcement strategies
Ciancia V, Martinelli F, Matteucci I, Morisset C
In Security, monitors and enforcement mechanisms run in parallel with programs to check, and modify their run-time behaviour, respectively, in order to guarantee the satisfaction of a security policy. For the same policy, several enforcement strategies are possible. We provide a framework for quantitative monitoring and enforcement. Enforcement strategies are analysed according to user-dened parameters. This is done by extending the notion controller processes, that mimics the well-known edit automata, with weights on transitions, valued in a C-semiring. C-semirings permit one to be exible and general in the quantitative criteria. Furthermore, we provide some examples of orders on controllers that are evaluated under incomparable criteria.
Ciancia V, Martinelli F, Matteucci I, Morisset C
In Security, monitors and enforcement mechanisms run in parallel with programs to check, and modify their run-time behaviour, respectively, in order to guarantee the satisfaction of a security policy. For the same policy, several enforcement strategies are possible. We provide a framework for quantitative monitoring and enforcement. Enforcement strategies are analysed according to user-dened parameters. This is done by extending the notion controller processes, that mimics the well-known edit automata, with weights on transitions, valued in a C-semiring. C-semirings permit one to be exible and general in the quantitative criteria. Furthermore, we provide some examples of orders on controllers that are evaluated under incomparable criteria.
2014
Other
Open Access
Logics of space and time
Ciancia V, Latella D, Massink M
We review some literature in the field of spatial logics. The selection of papers we make is intended as an introductory guide in this broad area. In perspective, this review should be expanded in the future and become tailored to the use of spatial reasoning in the context of population models and their ODE / PDE approximations. The application to keep in mind is the analysis of population models where individuals are scattered over a spatial structure. In this context, typically, space is intended to be multi-dimensional, discrete or continuous; it may be useful to think in terms of Euclidean spaces, but also graph-based relational models may be the subject of spatial reasoning. Furthermore, metrics, measures, probabilities and rates may also be part of the requirements of an analysis methodology.Project(s): QUANTICOL
Ciancia V, Latella D, Massink M
We review some literature in the field of spatial logics. The selection of papers we make is intended as an introductory guide in this broad area. In perspective, this review should be expanded in the future and become tailored to the use of spatial reasoning in the context of population models and their ODE / PDE approximations. The application to keep in mind is the analysis of population models where individuals are scattered over a spatial structure. In this context, typically, space is intended to be multi-dimensional, discrete or continuous; it may be useful to think in terms of Euclidean spaces, but also graph-based relational models may be the subject of spatial reasoning. Furthermore, metrics, measures, probabilities and rates may also be part of the requirements of an analysis methodology.Project(s): QUANTICOL
See at:
CNR IRIS | milner.inf.ed.ac.uk | ISTI Repository | CNR IRIS
2014
Other
Open Access
Specifying and verifying properties of space. Extended Version.
Ciancia V, Latella D, Loreti M, Massink M
The interplay between process behaviour and spatial aspects of computation has become more and more relevant in Computer Science, especially in the field of collective adaptive systems, but also, more generally, when dealing with systems distributed in physical space. Traditional verification techniques are well suited to analyse the temporal evolution of programs; however, properties of space are typically not explicitly taken into account. We propose a methodology to verify properties depending upon physical space. We define an appropriate logic, stemming from the tradition of topological interpretations of modal logics, dating back to earlier logicians such as Tarski, where modalities describe neighbourhood. We lift the topological definitions to the more general setting of closure spaces, also encompassing discrete, graph-based structures. We further extend the framework with a spatial until operator, and define an efficient model checking procedure, implemented in a proof-of-concept tool.Project(s): QUANTICOL
Ciancia V, Latella D, Loreti M, Massink M
The interplay between process behaviour and spatial aspects of computation has become more and more relevant in Computer Science, especially in the field of collective adaptive systems, but also, more generally, when dealing with systems distributed in physical space. Traditional verification techniques are well suited to analyse the temporal evolution of programs; however, properties of space are typically not explicitly taken into account. We propose a methodology to verify properties depending upon physical space. We define an appropriate logic, stemming from the tradition of topological interpretations of modal logics, dating back to earlier logicians such as Tarski, where modalities describe neighbourhood. We lift the topological definitions to the more general setting of closure spaces, also encompassing discrete, graph-based structures. We further extend the framework with a spatial until operator, and define an efficient model checking procedure, implemented in a proof-of-concept tool.Project(s): QUANTICOL
See at:
CNR IRIS | milner.inf.ed.ac.uk | ISTI Repository | CNR IRIS
2014
Conference article
Open Access
Specifying and Verifying Properties of Space
Ciancia V, Latella D, Loreti M, Massink M
The interplay between process behaviour and spatial aspects of computation has become more and more relevant in Computer Science, especially in the field of collective adaptive systems, but also, more generally, when dealing with systems distributed in physical space. Traditional verification techniques are well suited to analyse the temporal evolution of programs; properties of space are typically not explicitly taken into account. We propose a methodology to verify properties depending upon physical space. We define an appropriate logic, stemming from the tradition of topological interpretations of modal logics, dating back to earlier logicians such as Tarski, where modalities describe neighbourhood. We lift the topological definitions to a more general setting, also encompassing discrete, graph-based structures. We further extend the framework with a spatial until operator, and define an efficient model checking procedure, implemented in a proof-of-concept tool.DOI: 10.1007/978-3-662-44602-7_18
Project(s): QUANTICOL, ASCENS
Metrics:
Ciancia V, Latella D, Loreti M, Massink M
The interplay between process behaviour and spatial aspects of computation has become more and more relevant in Computer Science, especially in the field of collective adaptive systems, but also, more generally, when dealing with systems distributed in physical space. Traditional verification techniques are well suited to analyse the temporal evolution of programs; properties of space are typically not explicitly taken into account. We propose a methodology to verify properties depending upon physical space. We define an appropriate logic, stemming from the tradition of topological interpretations of modal logics, dating back to earlier logicians such as Tarski, where modalities describe neighbourhood. We lift the topological definitions to a more general setting, also encompassing discrete, graph-based structures. We further extend the framework with a spatial until operator, and define an efficient model checking procedure, implemented in a proof-of-concept tool.DOI: 10.1007/978-3-662-44602-7_18
Project(s): QUANTICOL
, ASCENS Metrics:
See at:
link.springer.com | doi.org | Hyper Article en Ligne | CNR IRIS | CNR IRIS | www.scopus.com
2014
Conference article
Restricted
Data verification for collective adaptive systems: spatial model-checking of vehicle location data
Ciancia V, Gilmore S, Latella D, Loreti M, Massink M
In this paper we present the use of a novel spa- tial model-checker to detect problems in the data which an adaptive system gathers in order to inform future action. We categorise received data as being plausible, implausible, possible or problematic. Data correctness is essential to ensure correct functionality in systems which adapt in response to data and our categorisation influences the degree of caution which should be used in acting in response to this received data. We illustrate the theory with a concrete example of detecting errors in vehicle location data for buses in the city of Edinburgh. Vehicle location data is visualised symbolically on a street map, and categories of problems identified by the spatial model-checker are rendered by repainting the symbols for vehicles in different colours.DOI: 10.1109/sasow.2014.16
Project(s): QUANTICOL
Metrics:
Ciancia V, Gilmore S, Latella D, Loreti M, Massink M
In this paper we present the use of a novel spa- tial model-checker to detect problems in the data which an adaptive system gathers in order to inform future action. We categorise received data as being plausible, implausible, possible or problematic. Data correctness is essential to ensure correct functionality in systems which adapt in response to data and our categorisation influences the degree of caution which should be used in acting in response to this received data. We illustrate the theory with a concrete example of detecting errors in vehicle location data for buses in the city of Edinburgh. Vehicle location data is visualised symbolically on a street map, and categories of problems identified by the spatial model-checker are rendered by repainting the symbols for vehicles in different colours.DOI: 10.1109/sasow.2014.16
Project(s): QUANTICOL
Metrics:
See at:
doi.org | CNR IRIS | ieeexplore.ieee.org | CNR IRIS
2014
Other
Open Access
QUANTICOL - D6.1 - Dissemination plan for the project
Gilmore S, Ter Beek M H, Bortolussi L, Ciancia V, Galpin V, Hillston J, Massink M, Tribastone M
This document sets out the dissemination plan for the QUANTICOL project. The project has ambitions to see its research outputs and results disseminated widely in academia and beyond. We present here our plan to achieve this goal and review the progress on the plan which has been achieved in the rst year of the project. This gives an insight into how we see the plan being developed and implemented in later years of the project.Project(s): QUANTICOL
Gilmore S, Ter Beek M H, Bortolussi L, Ciancia V, Galpin V, Hillston J, Massink M, Tribastone M
This document sets out the dissemination plan for the QUANTICOL project. The project has ambitions to see its research outputs and results disseminated widely in academia and beyond. We present here our plan to achieve this goal and review the progress on the plan which has been achieved in the rst year of the project. This gives an insight into how we see the plan being developed and implemented in later years of the project.Project(s): QUANTICOL
See at:
blog.inf.ed.ac.uk | CNR IRIS | ISTI Repository | CNR IRIS
2015
Conference article
Open Access
Qualitative and quantitative monitoring of spatio-temporal properties
Nenzi L, Bortolussi L, Ciancia V, Loreti M, Massink M
We address the specification and verification of spatio-temporal behaviours of complex systems, extending Signal Spatio-Temporal Logic (SSTL) with a spatial operator capable of specifying topological properties in a discrete space. The latter is modelled as a weighted graph, and provided with a boolean and a quantitative semantics. Furthermore, we define efficient monitoring algorithms for both the boolean and the quantitative semantics. These are implemented in a Java tool available online. We illustrate the expressiveness of SSTL and the effectiveness of the monitoring procedures on the formation of patterns in a Turing reaction-diffusion system.DOI: 10.1007/978-3-319-23820-3_2
Project(s): QUANTICOL
Metrics:
Nenzi L, Bortolussi L, Ciancia V, Loreti M, Massink M
We address the specification and verification of spatio-temporal behaviours of complex systems, extending Signal Spatio-Temporal Logic (SSTL) with a spatial operator capable of specifying topological properties in a discrete space. The latter is modelled as a weighted graph, and provided with a boolean and a quantitative semantics. Furthermore, we define efficient monitoring algorithms for both the boolean and the quantitative semantics. These are implemented in a Java tool available online. We illustrate the expressiveness of SSTL and the effectiveness of the monitoring procedures on the formation of patterns in a Turing reaction-diffusion system.DOI: 10.1007/978-3-319-23820-3_2
Project(s): QUANTICOL
Metrics:
See at:
arts.units.it | Archivio istituzionale della ricerca - Università di Trieste | CNR IRIS | link.springer.com | ISTI Repository | doi.org | CNR IRIS | CNR IRIS