Modeling and Reasoning About Wireless Networks: A Graph-based Calculus Approach

TL;DR

This paper introduces a graph-based process calculus for modeling wireless networks, enabling formal reasoning about network behaviors and topologies with local broadcasts, supported by semantics and case studies.

Contribution

It presents a novel graph-based calculus with semantics for wireless networks, connecting bisimulation and barbed congruence, and demonstrating practical applications.

Findings

Weak bisimilarity implies weak barbed congruence

The calculus effectively models network topologies and behaviors

Case studies illustrate practical applicability

Abstract

We propose a graph-based process calculus for modeling and reasoning about wireless networks with local broadcasts. Graphs are used at syntactical level to describe the topological structures of networks. This calculus is equipped with a reduction semantics and a labelled transition semantics. The former is used to define weak barbed congruence. The latter is used to define a parameterized weak bisimulation emphasizing locations and local broadcasts. We prove that weak bisimilarity implies weak barbed congruence. The potential applications are illustrated by some examples and two case studies.