Author name cluster

Ivano Salvo

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

1 author row

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.

Details DOI

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.

Details DOI

I&C Journal 2001 Journal Article

A Characterization of Weakly Church–Rosser Abstract Reduction Systems That Are Not Church–Rosser

Benedetto Intrigila
Ivano Salvo
Stefano Sorgi

Basic properties of rewriting systems can be stated in the framework of abstract reduction systems (ARS). Properties like confluence (or Church–Rosser, CR) and weak confluence (or weak Church–Rosser, WCR) and their relationships can be studied in this setting: as a matter of fact, well-known counterexamples to the implication WCR ⇒ CR have been formulated as ARS. In this paper, starting from the observation that such counterexamples are structurally similar, we set out a graph-theoretic characterization of WCR ARS that is not CR in terms of a suitable class of reduction graphs, such that in every WCR not CR ARS, we can embed at least one element of this class. Moreover, we give a tighter characterization for a restricted class of ARS enjoying a suitable regularity condition. Finally, as a consequence of our approach, we prove some interesting results about ARS using the mathematical tools developed. In particular, we prove an extension of the Newman's lemma and we find out conditions that, once assumed together with WCR property, ensure the unique normal form property. The Appendix treats two interesting examples, both generated by graph-rewriting rules, with specific combinatorial properties.

Details DOI