Daniele Gorla

TCS Journal 2024 Journal Article

Preface

• Ugo Dal Lago
• Daniele Gorla

TCS Journal 2022 Journal Article

Behavioural logics for configuration structures

• Paolo Baldan
• Daniele Gorla
• Tommaso Padoan
• Ivano Salvo

We provide a behavioural logic for configuration structures, a model due to van Glabbeek and Plotkin which generalises the families of (finite) configurations of event structures. The logic is a conservative extension of a logic provided by Baldan and Crafa for prime event structures. We show that logical equivalence can be characterized as a form of hereditary history preserving bisimilarity. We compare such a notion of bisimilarity with an equivalence proposed by van Glabbeek in the setting of higher-dimensional automata, showing that, in general, it is finer, while the two notions coincide in the framework of general event structures. Finally, we explore how to restrict the general logic to capture a notion of history preserving bisimilarity.

I&C Journal 2022 Journal Article

Characterising spectra of equivalences for event structures, logically

• Paolo Baldan
• Daniele Gorla
• Tommaso Padoan
• Ivano Salvo

We present a logical characterisation of the equivalences in the spectrum for labelled Prime Event Structures (PESs) and use it for also studying how such spectrum changes when restricting to subclasses of event structures. We first show that a minor modification of the logic characterising hereditary history preserving bisimilarity induces PES isomorphism as logical equivalence. Then, we distill fragments of the logic that characterise all the equivalences in the aforementioned spectrum. In particular, we single out logics for interleaving/step/pomset trace equivalences and weak (pomset) history preserving bisimilarity, which were missing. Finally, we apply our logical characterisation to investigate how the spectrum simplifies when we restrict to subclasses of event structures: Coherence Spaces, where causality is absent, and Elementary Event Structures, where instead conflicts are not allowed. Inclusions between behavioural equivalences are proved by providing encodings between the corresponding sublogics, whereas the non-inclusion between equivalences is witnessed by using distinguishing formulae, i. e. , by providing structures which are identified by an equivalence and distinguished by a formula in the logics of the other equivalence.

NeurIPS Conference 2021 Conference Paper

DOCTOR: A Simple Method for Detecting Misclassification Errors

• Federica Granese
• Marco Romanelli
• Daniele Gorla
• Catuscia Palamidessi
• Pablo Piantanida

Deep neural networks (DNNs) have shown to perform very well on large scale object recognition problems and lead to widespread use for real-world applications, including situations where DNN are implemented as “black boxes”. A promising approach to secure their use is to accept decisions that are likely to be correct while discarding the others. In this work, we propose DOCTOR, a simple method that aims to identify whether the prediction of a DNN classifier should (or should not) be trusted so that, consequently, it would be possible to accept it or to reject it. Two scenarios are investigated: Totally Black Box (TBB) where only the soft-predictions are available and Partially Black Box (PBB) where gradient-propagation to perform input pre-processing is allowed. Empirically, we show that DOCTOR outperforms all state-of-the-art methods on various well-known images and sentiment analysis datasets. In particular, we observe a reduction of up to 4% of the false rejection rate (FRR) in the PBB scenario. DOCTOR can be applied to any pre-trained model, it does not require prior information about the underlying dataset and is as simple as the simplest available methods in the literature.

I&C Journal 2010 Journal Article

Towards a unified approach to encodability and separation results for process calculi

• Daniele Gorla

We present a unified approach to evaluate the relative expressive power of process calculi. In particular, we identify a small set of criteria (that have already been somehow presented in the literature) that an encoding should satisfy to be considered a valid means for language comparison. We argue that the combination of such criteria is a valid proposal by noting that: (i) several well-known encodings appeared in the literature satisfy them; (ii) this notion is not trivial, because some known encodings do not satisfy all the criteria we have proposed; (iii) several well-known separation results can be formulated in terms of our criteria; and (iv) some widely believed (but never formally proved) separation results can be proved by using the criteria we propose. Moreover, the criteria defined induce general proof-techniques for separation results that can be easily instantiated to cover known case-studies.

I&C Journal 2008 Journal Article

Comparing communication primitives via their relative expressive power

• Daniele Gorla

In this paper, we study sixteen communication primitives, arising from the combination of four useful programming features: synchronism (synchronous vs asynchronous primitives), arity (monadic vs polyadic data), communication medium (message passing vs shared dataspaces) and pattern-matching. Some of these primitives have already been used in at least one language which has appeared in the literature; however, to reason uniformly on such primitives, we plug them into a common framework based on the π. By means of possibility/impossibility of ‘reasonable’ encodings, we compare every pair of primitives to obtain a hierarchy of languages based on their relative expressive power.

I&C Journal 2007 Journal Article

Basic observables for a calculus for global computing

• Rocco De Nicola
• Daniele Gorla
• Rosario Pugliese

We develop the semantic theory of a foundational language for modelling applications over global computers whose interconnection structure can be explicitly manipulated. Together with process distribution, process mobility and remote asynchronous communication through distributed data repositories, the language has primitives for explicitly modelling inter-node connections and for dynamically activating and deactivating them. For the proposed language, we define natural notions of extensional observations and study their closure under operational reductions and/or language contexts to obtain barbed congruence and may testing equivalence. We then focus on barbed congruence and provide an alternative characterisation in terms of a labelled bisimulation. To test practical usability of the semantic theory, we model a system of communicating mobile devices and use the introduced proof techniques to verify one of its key properties.

TCS Journal 2006 Journal Article

On the expressive power of KLAIM-based calculi

• Rocco De Nicola
• Daniele Gorla
• Rosario Pugliese

We study the expressive power of variants of KLAIM, an experimental language with programming primitives for network-aware programming that combines the process algebra approach with the coordination-oriented one. KLAIM has proved to be suitable for programming a wide range of distributed applications with agents and code mobility, and has been implemented on the top of a runtime system written in Java. In this paper, the expressivity of its constructs is tested by distilling from it a few, more and more foundational, languages and by studying the encoding of each of them into a simpler one. The expressive power of the considered calculi is finally tested by comparing one of them with asynchronous π -calculus.