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.Source: CALCO 2013 - 5th Conference on Algebra and Coalgebra in Computer Science, pp. 110–125, Warsaw, Poland, 3-6 Settembre 2013
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 | link.springer.com | CNR ExploRA

2019 Contribution to book Open Access

See at: drops.dagstuhl.de | ISTI Repository | CNR ExploRA

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.Source: History and Philosophy of Computing. HaPoC 2015. IFIP Advances in Information and Communication Technology, edited by Gadducci F.; Tavosanis M., pp. 141–155, 2016
DOI: 10.1007/978-3-319-47286-7_10
Project(s): QUANTICOL , ASCENS
Metrics:

See at: hal.inria.fr | doi.org | link-springer-com-443.webvpn.fjmu.edu.cn | CNR ExploRA

2021 Conference article Open Access

See at: ISTI Repository | link.springer.com | CNR ExploRA

2020 Report Open Access

See at: arxiv.org | ISTI Repository | CNR ExploRA

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: ICE 2016 - 9th Interaction and Concurrency Experience, 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 | ISTI Repository | doi.org | CNR ExploRA

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: Journal of Logical and Algebraic Methods in Programming [online] 93 (2017): 23–41. doi:10.1016/j.jlamp.2017.08.001
DOI: 10.1016/j.jlamp.2017.08.001
Project(s): QUANTICOL
Metrics:

See at: Journal of Logical and Algebraic Methods in Programming | www.sciencedirect.com | CNR ExploRA

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 14 (2018): 1–38. doi:10.23638/LMCS-14(4:2)2018
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 | Episciences | ISTI Repository | doi.org | doi.org | CNR ExploRA

2014 Report 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.Source: ISTI Technical reports, 2014
Project(s): QUANTICOL

See at: milner.inf.ed.ac.uk | ISTI Repository | CNR ExploRA

See at: doi.org | link.springer.com | CNR ExploRA

2014 Report 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.Source: ISTI Technical reports, 2014
Project(s): QUANTICOL

See at: milner.inf.ed.ac.uk | ISTI Repository | CNR ExploRA

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.Source: Theoretical Computer Science, pp. 222–235, Roma, 1-3 Settembre 2014
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 | www.scopus.com | CNR ExploRA

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.Source: FoCAS Workshp @ SASO - 2014 IEEE Eighth International Conference on Self-Adaptive and Self-Organizing Systems Workshops, pp. 32–37, Imperial College, London, UK, 8 September 2014
DOI: 10.1109/sasow.2014.16
Project(s): QUANTICOL
Metrics:

See at: doi.org | ieeexplore.ieee.org | CNR ExploRA

2014 Report 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.Source: Project report, QUANTICOL, Deliverable D6.1, 2014
Project(s): QUANTICOL

See at: blog.inf.ed.ac.uk | ISTI Repository | CNR ExploRA

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.Source: RV 2015 - Runtime Verification 2015. 6th International Conference, pp. 21–37, Vienna, Austria, 22 - 25 September 2015
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 | ISTI Repository | doi.org | link.springer.com | CNR ExploRA

2015 Contribution to book Open Access

An experimental spatio-temporal model checker
Ciancia V., Grilletti G., Latella D., Loreti M., Massink M.
In this work we present a spatial extension of the global model checking algorithm of the temporal logic CTL. This classical veri- fication framework is augmented with ideas coming from the tradition of topological spatial logics. More precisely, we add to CTL the operators of the Spatial Logic of Closure Spaces, including the surrounded operator, with its intended meaning of a point being surrounded by entities sat- isfying a specific property. The interplay of space and time permits one to define complex spatio-temporal properties. The model checking algo- rithm that we propose features no particular efficiency optimisations, as it is meant to be a reference specification of a family of more efficient algorithms that are planned for future work. Its complexity depends on the product of temporal states and points of the space. Nevertheless, a prototype model checker has been implemented, made available, and used for experimentation of the application of spatio-temporal verifica- tion in the field of collective adaptive systems.Source: Software Engineering and Formal Methods, edited by Domenico Bianculli, Radu Calinescu, Bernhard Rumpe, pp. 297–311, 2015
DOI: 10.1007/978-3-662-49224-6_24
Project(s): QUANTICOL
Metrics:

See at: ISTI Repository | doi.org | link.springer.com | CNR ExploRA

2015 Conference article Open Access

Exploring spatio-temporal properties of bike-sharing systems
Ciancia V., Latella D., Massink M., Paskauskas R.
In this paper we explore the combination of novel spatio-temporal model-checking techniques, and of a recently developed model-based approach to the study of bike sharing systems, in order to detect, visualize and investigate potential problems with bike sharing system configurations. In particular the formation and dynamics of clusters of full stations is explored. Such clusters are likely to be related to the difficulties of users to find suitable parking places for their hired bikes and show up as surprisingly long cycling trips in the trip duration statistics of real bike sharing systems of both small and large cities. Spatio- temporal analysis of the pattern formation may help to explain the phenomenon and possibly lead to alternative bike repositioning strategies aiming at the reduction of the size of such clusters and improving the quality of service.Source: IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, pp. 74–79, Cambridge, MA, USA, 21-25/09/2015
DOI: 10.1109/sasow.2015.17
Project(s): QUANTICOL
Metrics:

See at: ISTI Repository | doi.org | ieeexplore.ieee.org | CNR ExploRA

2015 Report Open Access

An attribute-based front-end for FlyFast
Ciancia V., Latella D., Massink M.
TypicalCollectiveAdaptiveSystems(CAS)consistofalarge number of interacting objects that coordinate their activities in a decen- tralised and often implicit way. The design of such systems is challenging. It requires scalable analysis tools and techniques to check properties of proposed system designs before they are put into operation. A promising technique is Fast Mean-Field Approximated Model-checking. In particu- lar, the FlyFast model-checker uses an on-the-fly algorithm for bounded PCTL model-checking of selected individuals in the context of very large populations whose behaviour is approximated using deterministic limit techniques. Recently, specific modelling languages have been proposed for CAS. A key feature of such languages is the attribute-based interac- tion paradigm. In this paper we present an attribute-based coordination language as a front-end for FlyFast. Its formal probabilistic semantics is provided and a translation to the original FlyFast language is presented and proved correct.Source: ISTI Technical reports, 2015
Project(s): QUANTICOL

See at: ISTI Repository | CNR ExploRA

2016 Report Open Access

On-the-fly mean-field model-checking for attribute-based coordination preliminary version. Quanticol technical report TR-QC-01-2016
Ciancia V., Latella D., Massink M.
Typical Collective Adaptive Systems (CAS) consist of a large number of interacting objects that coordinate their activities in a decentralised and often implicit way. The design of such systems is challenging. It requires scalable analysis tools and techniques to check properties of proposed system designs before they are put into operation. A promising technique is Fast Mean- Field Approximated Model-checking. In particular, the FlyFast model-checker uses an on-the-fly algorithm for bounded PCTL model-checking of selected individuals in the context of very large populations whose global behaviour is approximated using deterministic limit techniques. Recently, specific modelling languages have been proposed for CAS. A key feature of such languages is the attribute-based interaction paradigm. In this paper we present a simple non value-passing version of an attribute-based coordination language as a front-end for FlyFast. Its formal probabilistic semantics is provided and a translation to the original FlyFast language is presented and proved correct. Application examples are also provided.Source: ISTI Technical reports, 2016
Project(s): QUANTICOL

See at: ISTI Repository | CNR ExploRA

2016 Conference article Open Access

On-the-fly mean-field model-checking for attribute-based coordination
Ciancia V., Latella D., Massink M.
Typical Collective Adaptive Systems (CAS) consist of a large number of interacting objects that coordinate their activities in a decentralised and often implicit way. The design of such systems is challenging, as it requires scalable analysis tools and methods to check properties of proposed system designs before they are put into operation. A promising technique is Fast Mean-Field Approximated Model-checking. The FlyFast model-checker uses an on-the-fly algorithm for bounded PCTL model-checking of selected individuals in the context of very large populations whose global behaviour is approximated using deterministic limit techniques. Recently, specific modelling languages have been proposed for CAS. A key feature of such languages is the attribute-based interaction paradigm. In this paper we present an attribute-based coordination language as a front-end for FlyFast. Its formal probabilistic semantics is provided and a translation to the original FlyFast language is given and proved correct. Application examples are also provided.Source: COORDINATION 2016 - DisCoTec 2016 - Coordination Models and Languages. 18th IFIP WG 6.1 International Conference, pp. 67–83, Heraklion, Crete, Greece, 6-9 June 2016
DOI: 10.1007/978-3-319-39519-7_5
Project(s): QUANTICOL
Metrics:

See at: hal.inria.fr | ISTI Repository | doi.org | Hyper Article en Ligne | link.springer.com | CNR ExploRA