Related papers: Formally Proving and Enhancing a Self-Stabilising …
Topological self-stabilization describes the ability of a distributed system to let the nodes themselves establish a meaningful overlay network. Independent from the initial network topology, the system converges to the desired topology via…
Maintaining an acceptable level of quality of service in modern complex systems is challenging, particularly in the presence of various forms of uncertainty caused by changing execution context, unpredicted events, etc. Although…
In the context of large-scale networks, the consideration of faults is an evident necessity. This document is focussing on the self-stabilizing approach which aims at conceiving algorithms "repairing themselves" in case of transient faults,…
In this paper, we formalize design patterns, commonly used in the self-stabilizing area, to obtain general statements regarding both correctness and time complexity guarantees. Precisely, we study a general class of algorithms designed for…
This paper presents a new formal method for verification of quantum communication protocols. By extending the symbolic system of Petri nets, we can define quantum pure states in Petri-net settings. Therefore, it is possible to emerge a…
We introduce an automata-theoretic method for the verification of distributed algorithms running on ring networks. In a distributed algorithm, an arbitrary number of processes cooperate to achieve a common goal (e.g., elect a leader).…
Self-stabilization is a versatile technique to withstand any transient fault in a distributed system. Mobile robots (or agents) are one of the emerging trends in distributed computing as they mimic autonomous biologic entities. The…
We present algorithms for distributed verification and silent-stabilization of a DFS(Depth First Search) spanning tree of a connected network. Computing and maintaining such a DFS tree is an important task, e.g., for constructing efficient…
We propose a general framework to build certified proofs of distributed self-stabilizing algorithms with the proof assistant Coq. We first define in Coq the locally shared memory model with composite atomicity, the most commonly used model…
Self-stabilization is a versatile fault-tolerance approach that characterizes the ability of a system to eventually resume a correct behavior after any finite number of transient faults. In this paper, we propose a self-stabilizing reset…
The formalism of the models with Petri networks provides a sound theoretical base, supported by powerful mathematical methods able to extract information necessary for the formalism and simulation of the real system that provides features…
Self-stabilization is a general paradigm to provide forward recovery capabilities to distributed systems and networks. Intuitively, a protocol is self-stabilizing if it is able to recover without external intervention from any catastrophic…
Containment-based trees encompass various handy structures such as B+-trees, R-trees and M-trees. They are widely used to build data indexes, range-queryable overlays, publish/subscribe systems both in centralized and distributed contexts.…
This paper deals with the trade-off between time, workload, and versatility in self-stabilization, a general and lightweight fault-tolerant concept in distributed computing.In this context, we propose a transformer that provides an…
A distributed algorithm is self-stabilizing if after faults and attacks hit the system and place it in some arbitrary global state, the systems recovers from this catastrophic situation without external intervention in finite time.…
Being able to find small Petri nets with the same behaviour as formal specifications of concurrent systems benefits both effective verification and practical implementation of such systems. This paper considers specifications given in the…
Autonomous systems -- such as self-driving cars, autonomous drones, and automated trains -- must come with strong safety guarantees. Over the past decade, techniques based on formal methods have enjoyed some success in providing strong…
We prove several new tight distributed lower bounds for classic symmetry breaking graph problems. As a basic tool, we first provide a new insightful proof that any deterministic distributed algorithm that computes a $\Delta$-coloring on…
In this thesis a comprehensive verification framework is proposed to contend with some important issues in composability verification and a verification process is suggested to verify composability of different kinds of systems models, such…
In this essay I aim to investigate and discuss the process through which bundles of things "self-organize" into other things. In particular, I engage in such investigation by trying to apply a framework of analysis of structural stability…