arXiv subjects

Cinzia Di Giusto

Publications and source records attributed to Cinzia Di Giusto.

At least 19 recordsLinked to original sources

arXiv2025

On the Impact of the Communication Model on Realisability

Multiparty Session Types (MPST) provide a type-theoretic foundation for specifying and verifying communication protocols in distributed systems. MPST rely on the notion of global type which specifies the global behaviour and local types, which are the projections of the global behaviour onto each local participant. A central notion in MPST is realisability - whether local implementations derived from a global specification correctly realise the intended protocol under a given communication model. While realisability has been extensively studied under peer-to-peer semantics, it remains poorly understood in alternative communication models such as bag-based, causally ordered, or synchronous communications. In this paper, we develop a unified framework for reasoning about realisability and subtyping across a spectrum of communication models. We show that the communication model does not impact the notion of subtyping, but that it impacts the notion of realisability. We introduce several decision procedures for subtyping checking and realisability checking with complexities ranging from NLOGSPACE to EXPSPACE depending on the assumptions made on the global types, in particular depending on their complementability and the size of a given complement.

cs.FL↗

arXiv2025

Proceedings of the Combined 32nd International Workshop on Expressiveness in Concurrency and 22nd Workshop on Structural Operational Semantics

This volume contains the proceedings of EXPRESS/SOS 2025: the Combined 32nd International Workshop on Expressiveness in Concurrency and the 22nd Workshop on Structural Operational Semantics, which was held in Aarhus, Denmark, as an affiliated workshop of CONFEST 2025. The EXPRESS/SOS workshop series aims at bringing together researchers interested in the formal semantics of systems and programming concepts, and in the expressiveness of computational models.

cs.LO↗

arXiv2025

Proceedings 18th Interaction and Concurrency Experience

This volume contains the proceedings of ICE'25, the 18th Interaction and Concurrency Experience, which was held on Friday 20th June 2025 at the École National Supérieure des Arts et Métiers in Lille, France, as a satellite workshop of DisCoTec 2025. The ICE workshop series features a distinguishing review and selection procedure: PC members are encouraged to interact, anonymously, with authors. The 2025 edition of ICE received 7 submissions, each reviewed by three PC members, and about 75 comments were exchanged during the review process, witnessing very lively discussions. Four papers were accepted for publication plus 1 oral communication, which was accepted for presentation at the workshop. We were proud to host one invited talk, by Kirstin Peters. The abstract of her talk is included in this volume, together with the final versions of the research papers, which take into account the discussion at the workshop and during the review process.

cs.DC↗

arXiv2025

Realisability and Complementability of Multiparty Session Types

Multiparty session types (MPST) are a type-based approach for specifying message-passing distributed systems. They rely on the notion of global type specifying the global behaviour and local types, which are the projections of the global behaviour onto each local participant. An essential property of global types is realisability, i.e., whether the composition of the local behaviours conforms to those specified by the global type. We explore how realisability of MPST relates to their complementability, i.e., whether there exists a global type that describes the complementary behaviour of the original global type. First, we show that if a global type is realisable with p2p communications, then it is realisable with synchronous communications. Second, we show that if a global type is realisable in the synchronous model, then it is complementable, in the sense that there exists a global type that describes the complementary behaviour of the original global type. Third, we give an algorithm to decide whether a complementable global type, given with an explicit complement, is realisable in p2p. As a side contribution, we propose a complementation construction for global types with sender-driven choice, and more generally commutation-deterministic, with a linear blowup in the size of the global type.

cs.FL↗

arXiv2024

Proceedings 17th Interaction and Concurrency Experience

This volume contains the proceedings of ICE'24, the 17th Interaction and Concurrency Experience, which was held on Friday 21th June 2024 at the University of Groningen in Groningen, The Netherlands, as a satellite workshop of DisCoTec 2024. The ICE workshop series features a distinguishing review and selection procedure: PC members are encouraged to interact, anonymously, with authors. The 2024 edition of ICE included double blind reviewing of original research papers, in order to increase fairness and avoid bias in reviewing. Each paper was reviewed by three PC members, and altogether 3 papers were accepted for publication plus 1 oral communication, which was accepted for presentation at the workshop. We were proud to host one invited talk, by Jorge A. Pérez. The abstract of his talk is included in this volume, together with the final versions of the research papers, which take into account the discussion at the workshop and during the review process.

cs.DC↗

arXiv2024

Synchronisability in Mailbox Communication

We revisit the problem of synchronisability for communicating automata, i.e., whether the language of send messages for an asynchronous system is the same as the language of send messages with a synchronous communication. The un/decidability of the problem depends on the specific asynchronous semantics considered as well as the topology (the communication flow) of the system. Synchronisability is known to be undecidable under the peer-to-peer semantics, while it is still an open problem for mailbox communication. The problem was shown to be decidable for ring topologies. In this paper, we show that when generalising to automata with accepting states, synchronisability is undecidable under the mailbox semantics, this result is obtained by resorting to the Post Correspondence problem. In an attempt to solve the specific problem where all states are accepting, we also show that synchronisability is decidable for tree topologies (where, as well as for rings, peer-to-peer coincides with mailbox semantics). We also discuss synchronisability for multitrees in the mailbox setting.

cs.FL↗

arXiv2024

Proceedings Combined 31st International Workshop on Expressiveness in Concurrency and 21st Workshop on Structural Operational Semantics

This volume contains the proceedings of EXPRESS/SOS 2024: the Combined 31st International Workshop on Expressiveness in Concurrency and the 21st Workshop on Structural Operational Semantics, which was held in Calgary, Canada, as an affiliated workshop of CONFEST 2024. The EXPRESS/SOS workshop series aims at bringing together researchers interested in the formal semantics of systems and programming concepts, and in the expressiveness of computational models.

cs.FL↗

arXiv2023

Weakly synchronous systems with three machines are Turing powerful

Communicating finite-state machines (CFMs) are a Turing powerful model of asynchronous message-passing distributed systems. In weakly synchronous systems, processes communicate through phases in which messages are first sent and then received, for each process. Such systems enjoy a limited form of synchronization, and for some communication models, this restriction is enough to make the reachability problem decidable. In particular, we explore the intriguing case of p2p (FIFO) communication, for which the reachability problem is known to be undecidable for four processes, but decidable for two. We show that the configuration reachability problem for weakly synchronous systems of three processes is undecidable. This result is heavily inspired by our study on the treewidth of the Message Sequence Charts (MSCs) that might be generated by such systems. In this sense, the main contribution of this work is a weakly synchronous system with three processes that generates MSCs of arbitrarily large treewidth.

cs.CL↗

arXiv2023

Proceedings 16th Interaction and Concurrency Experience

This volume contains the proceedings of ICE'23, the 16th Interaction and Concurrency Experience, which was held at the NOVA University in Lisbon, Portugal, as a satellite event of DisCoTec'22. The ICE workshop series features a distinguishing review and selection procedure: PC members are encouraged to interact, anonymously, with authors. The 2023 edition of ICE included double blind reviewing of original research papers, in order to increase fairness and avoid bias in reviewing. Each paper was reviewed by three PC members, and altogether 5 papers were accepted for publication plus 4 oral presentations which are not part of this volume. We were proud to host 2 invited talks, by Carla Ferreira and Adrian Francalanza. The abstracts of these talks are included in this volume, together with the final versions of the research papers, which take into account the discussion at the workshop and during the review process.

cs.DC↗

arXiv2023

Complexity of Membership and Non-Emptiness Problems in Unbounded Memory Automata

We study the complexity relationship between three models of unbounded memory automata: nu-automata ($ν$-A), Layered Memory Automata (LaMA)and History-Register Automata (HRA). These are all extensions of finite state automata with unbounded memory over infinite alphabets. We prove that the membership problem is NP-complete for all of them, while they fall into different classes for what concerns non-emptiness. The problem of non-emptiness is known to be Ackermann-complete for HRA, we prove that it is PSPACE-complete for $ν$-A.

cs.FL↗

arXiv2023

A partial order view of message-passing communication models

There is a wide variety of message-passing communication models, ranging from synchronous ''rendez-vous'' communications to fully asynchronous/out-of-order communications. For large-scale distributed systems, the communication model is determined by the transport layer of the network, and a few classes of orders of message delivery (FIFO, causally ordered) have been identified in the early days of distributed computing. For local-scale message-passing applications, e.g., running on a single machine, the communication model may be determined by the actual implementation of message buffers and by how FIFO queues are used. While large-scale communication models, such as causal ordering, are defined by logical axioms, local-scale models are often defined by an operational semantics. In this work, we connect these two approaches, and we present a unified hierarchy of communication models encompassing both large-scale and local-scale models, based on their concurrent behaviors. We also show that all the communication models we consider can be axiomatized in the monadic second order logic, and may therefore benefit from several bounded verification techniques based on bounded special treewidth.

cs.CL↗

arXiv2022

Proceedings 15th Interaction and Concurrency Experience

This volume contains the proceedings of ICE'22, the 15th Interaction and Concurrency Experience, which was held as an hybrid event in Lucca, Italy, and as a satellite event of DisCoTec'22. The ICE workshop series features a distinguishing review and selection procedure: PC members are encouraged to interact, anonymously, with authors. The 2022 edition of ICE included double blind reviewing of original research papers, in order to increase fairness and avoid bias in reviewing. Each paper was reviewed by between two and four PC members (with an average of 3.33333333333), and altogether 5 papers were accepted for publication -- plus 3 oral presentations which are not part of this volume. We were proud to host 2 invited talks, by Ilaria Castellani and Matthew Parkinson. The abstracts of these talks are included in this volume, together with the final versions of the research papers, which take into account the discussion at the workshop.

cs.DC↗

arXiv2021

Towards Generalised Half-Duplex Systems

FIFO automata are finite state machines communicating through FIFO queues. They can be used for instance to model distributed protocols. Due to the unboundedness of the FIFO queues, several verification problems are undecidable for these systems. In order to model-check such systems, one may look for decidable subclasses of FIFO systems. Binary half-duplex systems are systems of two FIFO automata exchanging over a half-duplex channel. They were studied by Cece and Finkel who established the decidability in polynomial time of several properties. These authors also identified some problems in generalising half-duplex systems to multi-party communications. We introduce greedy systems, as a candidate to generalise binary half-duplex systems. We show that greedy systems retain the same good properties as binary half-duplex systems, and that, in the setting of mailbox communications, greedy systems are quite closely related to a multiparty generalisation of half-duplex systems.

cs.DC↗

arXiv2021

Guessing the buffer bound for k-synchronizability

A communicating system is $k$-synchronizable if all of the message sequence charts representing the executions can be divided into slices of $k$ sends followed by $k$ receptions. It was previously shown that, for a fixed given $k$, one could decide whether a communicating system is $k$-synchronizable. This result is interesting because the reachability problem can be solved for $k$-synchronizable systems. However, the decision procedure assumes that the bound $k$ is fixed. In this paper we improve this result and show that it is possible to decide if such a bound $k$ exists.

cs.FL↗

arXiv2020

On the k-synchronizability of systems

In this paper, we work on the notion of k-synchronizability: a system is k-synchronizable if any of its executions, up to reordering causally independent actions, can be divided into a succession of k-bounded interaction phases. We show two results (both for mailbox and peer-to-peer automata): first, the reachability problem is decidable for k-synchronizable systems; second, the membership problem (whether a given system is k-synchronizable) is decidable as well. Our proofs fix several important issues in previous attempts to prove these two results for mailbox automata.

cs.FL↗

arXiv2018

Spiking Neural Networks modelled as Timed Automata with parameter learning

In this paper we present a novel approach to automatically infer parameters of spiking neural networks. Neurons are modelled as timed automata waiting for inputs on a number of different channels (synapses), for a given amount of time (the accumulation period). When this period is over, the current potential value is computed considering current and past inputs. If this potential overcomes a given threshold, the automaton emits a broadcast signal over its output channel , otherwise it restarts another accumulation period. After each emission, the automaton remains inactive for a fixed refractory period. Spiking neural networks are formalised as sets of automata, one for each neuron, running in parallel and sharing channels according to the network structure. Such a model is formally validated against some crucial properties defined via proper temporal logic formulae. The model is then exploited to find an assignment for the synaptical weights of neural networks such that they can reproduce a given behaviour. The core of this approach consists in identifying some correcting actions adjusting synaptical weights and back-propagating them until the expected behaviour is displayed. A concrete case study is discussed.

q-bio.NC↗

arXiv2016

Activity Networks with Delays An application to toxicity analysis

ANDy , Activity Networks with Delays, is a discrete time framework aimed at the qualitative modelling of time-dependent activities. The modular and concise syntax makes ANDy suitable for an easy and natural modelling of time-dependent biological systems (i.e., regulatory pathways). Activities involve entities playing the role of activators, inhibitors or products of biochemical network operation. Activities may have given duration, i.e., the time required to obtain results. An entity may represent an object (e.g., an agent, a biochemical species or a family of thereof) with a local attribute, a state denoting its level (e.g., concentration, strength). Entities levels may change as a result of an activity or may decay gradually as time passes by. The semantics of ANDy is formally given via high-level Petri nets ensuring this way some modularity. As main results we show that ANDy systems have finite state representations even for potentially infinite processes and it well adapts to the modelling of toxic behaviours. As an illustration, we present a classification of toxicity properties and give some hints on how they can be verified with existing tools on ANDy systems. A small case study on blood glucose regulation is provided to exemplify the ANDy framework and the toxicity properties.

q-bio.QM↗

arXiv2013

Session Types with Runtime Adaptation: Overview and Examples

In recent work, we have developed a session types discipline for a calculus that features the usual constructs for session establishment and communication, but also two novel constructs that enable communicating processes to be stopped, duplicated, or discarded at runtime. The aim is to understand whether known techniques for the static analysis of structured communications scale up to the challenging context of context-aware, adaptable distributed systems, in which disciplined interaction and runtime adaptation are intertwined concerns. In this short note, we summarize the main features of our session-typed framework with runtime adaptation, and recall its basic correctness properties. We illustrate our framework by means of examples. In particular, we present a session representation of supervision trees, a mechanism for enforcing fault-tolerant applications in the Erlang language.

cs.PL↗