Searcharxiv⌕ Search

arXiv subjects

Fabio Gadducci

Publications and source records attributed to Fabio Gadducci.

23 records · Page 2Linked to original sources

A spatial model checker in GPU (extended version)

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.

cs.LO↗

Retracing and assessing the CEP project

The last decade witnessed a renewed interest in the development of the Italian computer industry and in the role of the Fifties pioneers in Rome, Milan, Ivrea, and Pisa. The aim of the paper is to retrace some steps of the CEP project, carried out by the University of Pisa in collaboration with Olivetti, by reassessing the documents preserved in the University archives. The project was a seminal enterprise for Italy, and among its accomplishments it delivered in 1957 the first Italian computer. The mix of public sector funding and industrial foretelling witnessed by the project is one of the leading examples in Italy of best practices, and its success paved the way for the birth of Computer Science in the country as an industry as well as a scientific discipline.

cs.GL↗

Event Structures for Petri nets with Persistence

Event structures are a well-accepted model of concurrency. In a seminal paper by Nielsen, Plotkin and Winskel, they are used to establish a bridge between the theory of domains and the approach to concurrency proposed by Petri. A basic role is played by an unfolding construction that maps (safe) Petri nets into a subclass of event structures, called prime event structures, where each event has a uniquely determined set of causes. Prime event structures, in turn, can be identified with their domain of configurations. At a categorical level, this is nicely formalised by Winskel as a chain of coreflections. Contrary to prime event structures, general event structures allow for the presence of disjunctive causes, i.e., events can be enabled by distinct minimal sets of events. In this paper, we extend the connection between Petri nets and event structures in order to include disjunctive causes. In particular, we show that, at the level of nets, disjunctive causes are well accounted for by persistent places. These are places where tokens, once generated, can be used several times without being consumed and where multiple tokens are interpreted collectively, i.e., their histories are inessential. Generalising the work on ordinary nets, Petri nets with persistence are related to a new subclass of general event structures, called locally connected, by means of a chain of coreflections relying on an unfolding construction.

cs.LO↗

Rewriting modulo symmetric monoidal structure

String diagrams are a powerful and intuitive graphical syntax for terms of symmetric monoidal categories (SMCs). They find many applications in computer science and are becoming increasingly relevant in other fields such as physics and control theory. An important role in many such approaches is played by equational theories of diagrams, typically oriented and applied as rewrite rules. This paper lays a comprehensive foundation of this form of rewriting. We interpret diagrams combinatorially as typed hypergraphs and establish the precise correspondence between diagram rewriting modulo the laws of SMCs on the one hand and double pushout (DPO) rewriting of hypergraphs, subject to a soundness condition called convexity, on the other. This result rests on a more general characterisation theorem in which we show that typed hypergraph DPO rewriting amounts to diagram rewriting modulo the laws of SMCs with a chosen special Frobenius structure. We illustrate our approach with a proof of termination for the theory of non-commutative bimonoids.

math.CT↗

On Barbs and Labels in Reactive Systems

Reactive systems (RSs) represent a meta-framework aimed at deriving behavioral congruences for those computational formalisms whose operational semantics is provided by reduction rules. RSs proved a flexible specification device, yet so far most of the efforts dealing with their behavioural semantics focused on idem pushouts (IPOs) and saturated (also known as dynamic) bisimulations. In this paper we introduce a novel, intermediate behavioural equivalence: L-bisimilarity, which is able to recast both its IPO and saturated counterparts. The equivalence is parametric with respect to a set L of RSs labels, and it is shown that under mild conditions on L it is indeed a congruence. Furthermore, L-bisimilarity can also recast the notion of barbed semantics for RSs, proposed by the same authors in a previous paper. In order to provide a suitable test-bed, we instantiate our proposal by addressing the semantics of (asynchronous) CCS and of the calculus of mobile ambients.

cs.LO↗