Abstract

Mobile systems in which the communication topology changes dynamically are prevalent today. Familiar examples are networks of mobile devices and distributed multi-agent systems. This kind of mobility is manifested by exchange of communication channel names between processes and hence is called "name" mobility. Name mobility together with asynchronous communication, which is the fundamental mode of operation in networked systems, can be expressed very naturally in a language known as asynchronous pi-calculus. There exists many theories of asynchronous pi-calculus that study process equivalences such as bisimulation and testing.
Our work extends theories of testing equivalence for variants of asynchronous pi-calculus with different expressive power based on lack or presence of capabilities such as sending or receiving on certain names, or comparing names. Inspired by the success of model-checking in automatic verification of concurrent systems, we are now working on developing modal logics for mobile systems and corresponding model-checking algorithms.
The talk includes an introduction to asynchronous pi-calculus and testing equivalence. Then it presents variants of asynchronous pi-calculus with different capabilities on name usage, and describes examples of equivalence laws that we have established within each variant. The final part of the talk includes motivations and current progress in formulating modal logics and model-checking problems for mobile systems.

Mr. Reza Ziaei is a PhD candidate in computer science at the University of Illinois at Urbana Champaign. His research interests include formal verification and model-checking of distributed systems and design and analysis of algorithms for mobile ad-hoc networks.