2017/01/10 by Shichao Liu, Ying Jiang, Liu, Shichao +1 · 1 citation
Computer Science · Mathematics · #Algorithm #Bisimulation #Calculus (dental) #Computer science #Congruence (geometry) #Discrete mathematics #FOS: Computer and information sciences #Formal Methods in Verification #Graph #Logic in Computer Science (cs.LO) #Mathematics #Operational semantics #Parameterized complexity #Petri Nets in System Modeling #Pi calculus #Process calculus #Programming language #Semantics (computer science) #Service-Oriented Architecture and Web Services #Theoretical computer science #Wireless #Wireless network #cs.LO
paper · pdf · doi:10.48550/arxiv.1701.02526
published in arXiv (Cornell University) (Cornell University)
openalex publication_date 2017/01/10 · openalex created_date 2017/01/26 · arxiv created 2017/06/16 · arxiv updated 2017/06/19 · openalex updated_date 2026/07/28
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.