Networked cybernetic and physical systems of the Internet of Things (IoT) immerse civilian and industrial infrastructures into an interconnected and dynamic web of hybrid and mobile devices. The key feature of such systems is the hybrid and tight coupling of mobile and pervasive discrete communications in a continuously evolving environment (discrete computations with predominant continuous dynamics). In the aim of ensuring the correctness and reliability of such heterogeneous infrastructures, we introduce the hybrid π -calculus ( H p C ), to formally capture both mobility, pervasiveness and hybridisation in infrastructures where the network topology and its communicating entities evolve continuously in the physical world. The π -calculus proposed by Robin Milner et al. is a process calculus that can model mobile communications and computations in a very elegant manner. The H p C we propose is a conservative extension of the classical π -calculus, i.e., the extension is “minimal”, and yet describes mobility, time and physics of systems, while allowing to lift all theoretical results (e.g. bisimulation) to the context of that extension. We showcase the H p C by considering a realistic handover protocol among mobile devices.

Branching bisimilarity is a well-known equivalence relation for labelled transition systems. Based on this equivalence relation, with an additional simple rootedness condition, a congruence relation for calculus of communication system (CCS) processes can be obtained. However, neither branching bisimilarity nor the corresponding congruence relation preserves divergence, and it is still a question whether, based on a divergence-preserving variant of branching bisimilarity, a divergence-preserving congruence relation for CCS processes can be obtained by introducing the same simple rootedness condition. In this article, we present a partial solution by showing that rooted divergence-preserving branching bisimilarity is preserved under the usual CCS operators, including prefixing, summation, parallel composition, relabelling, restriction, and (weakly) guarded recursion.

We present an equational inference system for finite-state expressions, and prove that the system is sound and complete with respect to divergence preserving branching congruence, closing a problem that has been open since 1993. The inference system refines Rob van Glabbeek's simple and elegant complete axiomatisation for branching bisimulation congruence of finite-state behaviours by joining four simple axioms after dropping one axiom which is unsound under the more refined divergence sensitive semantics.

In this paper we prove completeness of four axiomatisations for finite-state behaviours with respect to behavioural equivalences at various τ-abstract levels: branching congruence, delay congruence, η-congruence, and weak congruence. Instead of merging guarded recursive equations, which was the approach originally used by Robin Milner and has since become the standard strategy for proving completeness results of this kind, in this work we take a new approach by solving guarded recursive equations with canonical solutions which are those with the fewest reachable states. The new strategy allows uniform treatment of the axiomatisations with respect to different behavioural equivalences.

The study of modal logics and various bisimulation equivalences so far shows the following progression: 1. weak bisimilarity is characterized by Hennessy-Milner logic (HML), a simple propositional modal logic with a weak possibility modality, and 2. extending HML by refining the weak possibility modality one obtains a logic which characterizes branching bisimilarity, a refinement of weak bisimilarity, and 3. further extending the logic with a divergence modality one obtains a logic which characterizes branching bisimilarity with explicit divergence, a refinement of branching bisimilarity. In this paper, we explore the development by exchanging the above 2 and 3, i.e. by first extending HML with a divergence modality and then refining the weak possibility modality in the extended logic. We have the following findings: A. extending HML with a new divergence modality one obtains a new logic which characterizes complete weak bisimilarity, an equivalence relation with distinguishing power in between weak bisimilarity and branching bisimilarity with explicit divergence; B. further extending the obtained logic by refining the weak possibility modality in it one obtains another logic which characterizes branching bisimilarity with explicit divergence. As main results of the paper, the logic in A. provides a modal characterization for complete weak bisimilarity, and moreover the two new logics in A. and B. are both sub-logics of the known logic obtained in above 3.

Some bisimulation based abstract equivalence relations may equate divergent systems with non-divergent ones, examples including weak bisimulation equivalence and branching bisimulation equivalence. Thus extra efforts are needed to analyze divergence for the compared systems. In this paper we propose a new method for analyzing divergence in bisimulation semantics, which relies only on simple observations of individual transitions. We show that this method can verify several typical divergence preserving bisimulation equivalences including two well-known ones. As an application case study, we use the proposed method to verify the HSY collision stack to draw the conclusion that the stack implementation is correct in terms of linearizability with lock-free progress condition.