We present a timed process calculus for modelling wireless networks in which individual stations broadcast and receive messages; moreover the broadcasts are subject to collisions. Based on a reduction semantics for the calculus we define a contextual
equivalence to compare the external behaviour of such wireless networks. Further, we construct an extensional LTS (labelled transition system) which models the activities of stations that can be directly observed by the external environment. Standard bisimulations in this LTS provide a sound proof method for proving systems contextually equivalence. We illustrate the usefulness of the proof methodology by a series of examples. Finally we show that this proof method is also complete, for a large class of systems.
We propose a process calculus to model high level wireless systems, where the topology of a network is described by a digraph. The calculus enjoys features which are proper of wireless networks, namely broadcast communication and probabilistic behavi
our. We first focus on the problem of composing wireless networks, then we present a compositional theory based on a probabilistic generalisation of the well known may-testing and must-testing pre- orders. Also, we define an extensional semantics for our calculus, which will be used to define both simulation and deadlock simulation preorders for wireless networks. We prove that our simulation preorder is sound with respect to the may-testing preorder; similarly, the deadlock simulation pre- order is sound with respect to the must-testing preorder, for a large class of networks. We also provide a counterexample showing that completeness of the simulation preorder, with respect to the may testing one, does not hold. We conclude the paper with an application of our theory to probabilistic routing protocols.
Process behaviour is often defined either in terms of the tests they satisfy, or in terms of the logical properties they enjoy. Here we compare these two approaches, using extensional testing in the style of DeNicola, Hennessy, and a recursive versio
n of the property logic HML. We first characterise subsets of this property logic which can be captured by tests. Then we show that those subsets of the property logic capture precisely the power of tests.
