UTP Semantics for BigrTiMo

BigrTiMo [1], a process algebra that combines the rTiMo calculus [2] and the Bigraph model [3], is capable of specifying a rich variety of properties for structure-aware mobile systems. Compared with rTiMo, our BigrTiMo calculus can specify not only time, mobility and local communication, but also remote communication. In this paper, we study the semantic foundation of this highly expressive modelling language and propose a denotational semantic model for it based on Hoare and He’s Unifying Theories of Programming (UTP) [4]. Compared to the standard UTP model, in addition to the communication, the novelty of the proposed UTP model in this paper covers time, location and global shared variable. Moreover, we give an example to show the contribution of BigrTiMo and illustrate how to use our semantic model and the trace-merging definition proposed in our paper under this example. We also demonstrate the proofs of some algebraic laws proposed in [1] based on our denotational semantics.