PhD Defence: Amrita Suresh

Dec 12 14:00 ₂₀₂₂

Abstract: Distributed systems involve processes that run independently and communicate asynchronously. While they capture a wide range of use cases and are hence, ubiquitous in our world, it is also particularly difficult to ensure their correctness.

In this thesis, we model such systems using mathematical and logical formulation, and try to verify them algorithmically. In particular, we focus on FIFO (First-In First-Out) machines, with one or more finite-state machines communicating via unbounded reliable FIFO buffers.

As most verification problems are known to be undecidable for FIFO machines, we focus on various subclasses and approximations of the model. The first model we consider is branch-well structured transition systems (branch-WSTS), a class which strictly includes the well-known class of WSTS. We study the problems of boundedness and termination for such systems, and demonstrate some examples of them. We also define another class of systems where the monotony condition is relaxed and show that a variant of the coverability problem is decidable under effectivity conditions.

We then study the restriction of input-boundedness on FIFO machines, and show that rational reachability and various other properties are decidable for FIFO machines under the input-bounded restriction. In doing so, we answer a long-standing open question regarding the reachability of input-bounded FIFO machines. We also derive some complexity bounds by considering the simplest case, a FIFO machine with a single channel.

Another restriction that we study is synchronizability in communicating systems. In particular, we explore this notion for MSCs (Message Sequence Charts), which is a model to represent executions of a communicating system. We show that if any set of MSCs can satisfy two properties, namely MSO (Monadic Second-order Logic) definability and bounded (special-)tree width, then synchronizability is decidable. Moreover, reachability and model-checking are also decidable within this framework. We also unify some classes from the literature using this framework, and for some other classes, show their undecidability.

Jury:

• Ahmed BOUAJJANI, Professor, Paris Diderot University (Univ. Paris 7) - Reviewer
• Rupak MAJUMDAR, Director, Max Planck Institute for Software System - Reviewer
• Mihaela SIGHIREANU, Professor, ENS Paris-Saclay - President
• Thierry JERON, Research Director, IRISA/INRIA Rennes - Examiner
• Nobuko YOSHIDA, Professor, University of Oxford - Examiner
• Benedikt BOLLIG, Research Director, CNRS, ENS Paris-Saclay - PhD supervisor
• Alain FINKEL, Professor, ENS Paris-Saclay - PhD supervisor