The MSO Theory of Connectedly Communicating Processes

Title:The MSO Theory of Connectedly Communicating Processes
Speaker: Dr. Shaofa Yang (SIAT, Chinese Academy of Sciences, Shenzhen)
Time: 3:00pm, December 5th (Monday), 2011
Venue: Lecture Room, Level 3, Building No. 5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences

Abstract: We identify a network of sequential processes that communicate by synchronizing frequently on common actions. More precisely, we demand that there is a bound k such that if the process p executes k steps without hearing from process q—directly or indirectly—then it will never hear from q again. The non‐interleaved branching time behavior of a system of connectedly communicating processes (CCP) is given by its event structure unfolding. We show that the monadic second order (MSO) theory of the event structure unfolding of every CCP is decidable. Using this result, we also show that an associated distributed controller synthesis problem is decidable for linear time specifications that do not discriminate between two different linearizations of the same partially ordered execution.

This is joint work with P. Madhusudan, P.S. Thiagarajan. It appeared in Proc. of FSTTCS 2005.

Biography: Shaofa Yang is an associate professor at Shenzhen Institute of Advanced Technology (SIAT), Chinese Academy of Sciences, since late 2010. In 1996, Yang was awarded the Scholarship for Undergraduate Studies in Singapore from the Ministry of Education, Singapore. The scholarship covered full tuition fees and living allowance for his undergraduate study at Department of Computer Science, National University of Singapore, and carried a bond of working in Singapore for six years upon graduation. Yang graduated with a first class bachelor (honours) degree in 2000, and subsequently worked as a full‐time teaching assistant in the same department for six years, while concurrently pursuing part‐time graduate studies. He obtained masters and Ph.D. degree in 2003 and 2006, respectively. Prior to joining SIAT, he held post‐doctoral positions at INRIA‐Rennes, France (2006‐2008) and IIST, United Nations University, located at Macau, China (2008‐2010). Yang’s research interests include design, analysis, verification and synthesis of discrete‐continuous control systems, verification and synthesis of concurrent systems, model checking, and logics in computer science. His research results appeared in journals such as Theoretical Computer Science, Information and Computation, and conferences such as CONCUR, Hybrid Systems: Computation and Control.