On Correct CPS Systems

Kaushik Mallik is a postdoctoral researcher at the Institute of Science and Technology (ISTA) in Austria. His research focuses on the correct design of safety-critical cyber-physical systems, specifically through scalable abstractions and formally verified synthesis algorithms. His other research interests include the development of tools for detecting and preventing algorithmic biases in machine-learned decision makers. He holds a B. Tech degree (2012) in Electrical Engineering from Meghnad Saha Institute of Technology, India, an M. Tech degree (2015) in Systems and Control from IIT Roorkee, India, and a PhD degree (2022) in Computer Science from the Max Planck Institute of Software Systems (MPI-SWS), Germany. His PhD dissertation received the 2023 ETAPS Doctoral Dissertation Award. He won the Late Smt. Uma Goyal W/O Sri Uday Shankar Goyal Memorial cash prize for securing the first rank in the Electrical Engineering department during his master’s at IIT Roorkee. He received the IIT Master-Sandwich-Programme scholarship from DAAD (2014) to pursue his master’s dissertation at TU Berlin, Germany.

Can you tell us a little bit about your research during your PhD?

My primary area of research was centered on the automated design of verified control software for Cyber-Physical Systems (CPS). CPS are automated systems where networks of dynamical system components interact with networks of software components through feedback loops. From a technical perspective, CPS are hybrid systems that are modelled through a mixture of continuous and discrete dynamic equations. These systems pervade numerous facets of our daily lives, ranging from vacuum cleaning robots and modern automobiles, to aircraft and surgical robots, among others. Given that numerous CPS applications are safety-critical, providing rigorous correctness guarantees is a critical undertaking.

Over the past five years, I have been actively engaged in the development of algorithmic solutions addressing important open questions within the domain of verified CPS design. During my doctoral studies, our research was bifurcated into two major directions.

First, we developed new design heuristics for mitigating the scalability bottleneck prevalent in existing CPS design approaches. Many of our ideas were inspired by established techniques from the classical software verification literature, such as lazy abstraction, assume-guarantee reasoning, etc.

Second, we developed novel algorithms for specific categories of design problems for which solutions were hitherto non-existent. In particular, we showed how we can design verified controllers for stochastic dynamical systems and for omega-regular control objectives.

Is there a particular paper that heavily influenced your work?

Yes, one of the papers that had a lasting influence on our work is “Feedback Refinement Relations for the Synthesis of Symbolic Controllers” by Reissig et al. (2016). This paper provides a clean solution for the design of symbolic controller for nonlinear dynamical systems, employing discrete abstractions. In fact, our latest tool Mascot-SDS, which is able to synthesize controllers for stochastic dynamical systems, still uses components from the tool SCOTS, the tool presented in Reissig et al. (2016).

Aside from research, what aspect of pursuing a PhD did you find most rewarding?

Travelling to new destinations for professional purposes and meeting interesting people. While working remotely has many benefits, I still feel a greater sense of connection and easier communicability when meeting someone in person.

Do you have any advice or insights of how to pursue a successful PhD that you would like to share?

My advice is threefold.

First, do not dismiss any learning opportunities, even if they seem to be unrelated to your field. You will often discover intriguing connections and familiar patterns in unrelated domains.

Second, invest a great deal of time and effort in strengthening your communication skills, encompassing both written and verbal forms. The impact of your research contributions is inextricably linked to your ability to communicate them lucidly to others. Try to perfect every talk you deliver, every informal explanation you give, and every paragraph you write. At the same time, be welcoming to feedback from colleagues: they will help you address your shortcomings over time.

Third, do not shy away from networking opportunities and social activities. If you are unsure about what to talk to a person whom you just met at a conference, then just start to explain your work; it will naturally take off from there. More often than not, the other person will like to hear about your work, even if you may feel otherwise. Social events are equally great for networking. In my experience, long-lasting collaborations often begin at dinner tables after the conference hours!

Is there a habit that you had during your PhD that would like to change if you had the opportunity to travel back in time?

In the early days of my PhD, I was more of an individualist when it came to solving research problems. I would rather spend days getting stuck on a difficult problem than discussing them with peers. Perhaps, I was too embarrassed to acknowledge defeat to others. That changed over time. I began to recognize the importance of collaborations in research and understood that, by exchanging ideas with peers, we can contribute to higher quality work in shorter amount of time compared to solitary effort. In hindsight, I wish I had known this simple fact from the beginning.

Tell us about your current research.

Right now, I am mainly working on two different projects. The first one is a brand-new topic where we are extending runtime verification to monitor if a machine-learned decision maker has been fair or unbiased in its decisions affecting humans. Eliminating biases in algorithmic decision-making is an active field of research in AI and machine-learning. Most works try to minimize biases through static measures, which requires knowledge of the system model and are susceptible to dynamic uncertainties. We are working on new complementary methods to monitor biases at runtime, without explicit knowledge of the system. Our monitors are statistical estimators, which observe one long execution sequence of the system, and after each observation outputs how fair or biased the system was until the current time step. We believe that our works will introduce new toolkits for mitigating decision biases in AI.

The second project involves bidding games. Bidding games are two-player sequential graph games modelling auctions. At each step, the players bid for the privilege to make the next move in the game. We are looking into some of the important theoretical open problems on richer classes of bidding game arenas. Alongside, we are developing novel algorithms for using bidding games in controller synthesis. This is an ongoing work and is in a premature stage; stay tuned for more updates soon!

What excites you about the research fields of formal methods?

We are currently witnessing a major paradigm shift in how we design software for CPS and software for automated systems in general. Manually written software code is being replaced by machine-learned components. While machine learning has achieved what was previously unthinkable, it also made any kind of formal analysis of systems more difficult. Our community has made remarkable progress in how we can formally verify systems even in the presence of machine-learned components in the loop. For example, verification of feedback control loops involving neural network controllers, use of safety shields to guarantee safety for systems with machine-learned components, controller synthesis with formal PAC guarantees for black-box machine-learned systems, etc., are all exciting topics. As I mentioned earlier, I am currently engaged in a project whose aim is to monitor biases in automated decision-making software. It feels great to experience this whole new branch of formal methods being born first-hand, with so many opportunities being created for us to make new contributions.