-
Synchronisability in Mailbox Communication
Authors:
Cinzia Di Giusto,
Laetitia Laversa,
Kirstin Peters
Abstract:
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…
▽ More
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.
△ Less
Submitted 21 November, 2024;
originally announced November 2024.
-
Execution-time opacity control for timed automata
Authors:
Étienne André,
Marie Duflot,
Laetitia Laversa,
Engel Lefaucheux
Abstract:
Timing leaks in timed automata (TA) can occur whenever an attacker is able to deduce a secret by observing some timed behavior. In execution-time opacity, the attacker aims at deducing whether a private location was visited, by observing only the execution time. It can be decided whether a TA is opaque in this setting. In this work, we tackle control, and show that we are able to decide whether a…
▽ More
Timing leaks in timed automata (TA) can occur whenever an attacker is able to deduce a secret by observing some timed behavior. In execution-time opacity, the attacker aims at deducing whether a private location was visited, by observing only the execution time. It can be decided whether a TA is opaque in this setting. In this work, we tackle control, and show that we are able to decide whether a TA can be controlled at runtime to ensure opacity. Our method is constructive, in the sense that we can exhibit such a controller. We also address the case when the attacker cannot have an infinite precision in its observations.
△ Less
Submitted 5 December, 2024; v1 submitted 16 September, 2024;
originally announced September 2024.
-
A partial order view of message-passing communication models
Authors:
Cinzia Di Giusto,
Davide Ferré,
Laetitia Laversa,
Etienne Lozes
Abstract:
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…
▽ More
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.
△ Less
Submitted 13 January, 2023; v1 submitted 24 October, 2022;
originally announced October 2022.
-
Guessing the buffer bound for k-synchronizability
Authors:
Cinzia Di Giusto,
Laetitia Laversa,
Etienne Lozes
Abstract:
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…
▽ More
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.
△ Less
Submitted 29 April, 2021;
originally announced April 2021.
-
On the k-synchronizability of systems
Authors:
Cinzia Di Giusto,
Cinzia Giusto,
Laetitia Laversa,
Etienne Lozes
Abstract:
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…
▽ More
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.
△ Less
Submitted 21 January, 2020; v1 submitted 4 September, 2019;
originally announced September 2019.
-
Spiking Neural Networks modelled as Timed Automata with parameter learning
Authors:
Elisabetta De Maria,
Cinzia Di Giusto,
Laetitia Laversa
Abstract:
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…
▽ More
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.
△ Less
Submitted 1 August, 2018;
originally announced August 2018.
