Group consensus in second-order multi-agent systems with nonlinear dynamics

In this paper, group consensus of second-order multi-agent systems with nonlinear dynamics is investigated. First, we design the distributed protocols for achieving group consensus, in which the strengths of the interactions among the agents are enhanced through tuning the coupling strengths. Further, taking the difference of the edges among agents into account, edge-based distributed protocols through tuning coupling weights of a fraction of edges are designed. Remarkably, only the edges of spanning tree in each group are pinned and the coupling strengths or weights of pinned edges are enhanced according to the updated laws. Both the types of distributed protocols are proved analytically and verified by numerical illustrations.

Declarative Parameterized Verification of Distributed Protocols via the Cubicle Model Checker

We show that Cubicle, an SMT-based infinite-state model checker, can be applied as a verification engine for GLog, a logic-based language based on relational updates rules that has been applied to specify topology-sensitive distributed protocols with asynchronous communication. In this setting, the absence of protocol anomalies can be reduced to a coverability problem in which the initial set of configurations is not fixed a priori (Existential Coverability Problem). Existential Coverability in GLog can naturally be expressed into Parameterized Verification judgements in Cubicle. The encoding is based on a translation of relational update rules into transition rules that modify cells of unbounded arrays. To show the effectiveness of the approach, we discuss several verification problems for distributed protocols and distributed objects, a challenging task for traditional verification tools. The experimental results show the flexibility and robustness of Cubicle for the considered class of protocol examples.

Correctness of the Chord protocol

Internet of Things (IoT) can be seen as a cooperation of various devices with limited performances that participate in the same system. IoT devices compose a distributed architecture system. The core of every IoT system is its discovery and control services. To realize such services, some authors used the developed solutions from the different domains. One such solution is the Chord protocol, one of the first, the simplest and the most popular distributed protocols. Unfortunately, the application of the Chord protocol was realized using the correctness of the Chord protocol for granted, or by the very hard assumptions. In this paper we prove the correctness of the Chord protocol using the logic of time and knowledge with the respect to the set of possible executions, called regular runs. We provide the deterministic description of the correctness of the Chord protocol and consider Chord actions that maintain ring topology while the nodes can freely join or leave.