Abstract: 

Distributed Synthesis is concerned with the automated computation of implementations of interacting reactive software components, given specifications for each component in linear temporal logic (LTL). Based on a discrete abstraction of component interactions as a multi-player game over a finite graph and specifications for all controllable system components given as ω-regular properties over this graph, we co-synthesize contract and controller candidates locally for each controllable component and propose a negotiation mechanism that iteratively refines these candidates until a solution to the given distributed synthesis problem is found. Our framework relies on the concept of permissive templates, which collect an infinite number of controller candidates in a concise data structure. We utilize the efficient computability, adaptability, and compositionality of such templates to obtain an efficient, yet sound and complete negotiation framework for contract-based distributed logical control.

Biography:  

Dr.Satya Nayak is a postdoctoral researcher at the Institute of Science and Technology Austria (ISTA), working with Krishnendu Chatterjee. His research mainly focuses on the formal verification and synthesis of cyber-physical systems. He completed his PhD in Computer Science at the Max Planck Institute for Software Systems (MPI-SWS), working in the Control Software Systems group under Anne-Kathrin Schmuck. He completed his Masters in Computer Science and Bachelors in Mathematics and Computer Science at Chennai Mathematical Institute.