I completed B.Tech in Electrical Engineering from Meghnad Saha Institute of Technology (India) in 2012 and M.Tech in System and Control from Indian Institute of Technology, Roorkee (India) in 2015. During my M.Tech, I was visiting TU-Berlin (Germany) for one semester (winter 2014-15) to work on my master thesis under the supervision of Anne-Kathrin Schmuck and Prof. Jörg Raisch.
I did an internship at MPI-SWS with Prof. Rupak Majumdar for three months in 2015, before joining as a PhD student with him in 2016.
Building G 26
Phone: +49 (0)631 9303 8527 Email: kmallik (at) m p i - s w s.org Skype: kaushik_mallik
My research is primarily focused on automatic synthesis of provably correct controllers for cyber-physical systems.
One of the most promising ideas in this field is to use techniques from formal methods in computer science for controller synthesis.
Although the general principle of how to do this is known by now, practical usage is limited due to scalability issues.
During my PhD, I have explored several scalable extensions to the existing formal methods-based controller synthesis techniques...
Compositional Abstraction-based Controller Synthesis. Oftentimes, physical systems are made up of several interconnected components.
This line of research tries to exploit the underlying component-level decomposition of systems while doing controller synthesis.
We addressed both non-stochastic and stochastic systems in two separate papers.
Lazy Multi-layered Abstraction-based Controller Synthesis.
The use of formal methods in controller synthesis often relies on a finite-state abstraction (a simpler approximation) of the system.
The abstraction is usually constructed by state-space discretization, which suffers heavily from the "curse of dimensionality''.
In this line of research, we use multi-layered abstractions of different granularities, such that during the synthesis process, the coarser abstractions are used as much as possible, while the finer ones are used only when necessary.
Read our ATVA paper which summarises the multi-layered approach for both safety and reach-avoid specifications.
We implemented the algorithms in the tool MASCOT.
Incremental Abstraction (for Controller Synthesis) in a Changing Environment.
We again consider the problem of controller synthesis using abstractions, this time in an environment where the system has limited apriori knowledge of the disturbance.
As the system is deployed with a preliminary controller obtained from an initial abstraction, it starts collecting more data about the actual disturbance levels.
We propose a systematic local adaptation scheme that avoids complete recomputation of the abstraction when new data arrives.
This is an ongoing work with several practical challenges yet to be addressed.
Take a first look in our upcoming CDC paper.
More recently, I have also looked into a problem related to controller synthesis for controlled Markov processes for infinite horizon processes...
Consider a discrete-time continuous state dynamical system with additive stochastic noise, known as Controlled Markov Process (CMP). We showed how to synthesize a controller for CMPs that maximizes the probability of satisfaction of Büchi specification (visit a set of states infinitely often). We decompose computation of the maximal probability of satisfying the Büchi condition into two steps. The first step is to compute the maximal qualitative winning set, from where the Büchi condition can be enforced with probability one. The second step is to find the maximal probability of reaching the already computed qualitative winning set. For the first step, we present a novel abstraction-based approximate computation, and point out that the second step can be handled by the existing methods. We show that our techniques are able to provide tight approximations to the qualitative winning set for the Van der Pol oscillator (picture in the right) and a 3-d Dubin’s vehicle. See our preprint to know more.
I also co-supervised Kyle Hsu with Anne-Kathrin Schmuck in summer 2017, who was working on the Lazy Multi-layered Abstraction Based Control project. Right now, I am co-supervising Merhdad Zareian with Mahmoud Salamati, who is working on an ongoing project of Abstraction Based Control for tracking reference trajectories.
Assume-Guarantee Distributed Synthesis* with Rupak Majumdar, Anne-Kathrin Schmuck, and Damien Zufferey, To appear in EMSOFT 2020. (PDF)
Resilient Abstraction-Based Controller Design with Stanly Samuel, Anne-Kathrin Schmuck, and Daniel Neider, To appear in CDC 2020. (PDF | Poster)
for Controller Synthesis with Non-uniform Disturbances with Yunjun Bai, To appear in ICFEM 2020. (PDF)
Journals and Book Chapters
Abstraction-Based Control Design (Lecture Notes)* with Rupak Majumdar and Anne-Kathrin Schmuck, Engineering Secure and Dependable Software Systems 53 (2019): 117.