MSc THESIS DEFENSE
12 noon - 12:30 pm, Lecture hall 5
Verifying flat FIFO systems through counter systems
Archit Chauhan
Chennai Mathematical Institute.
14-06-18

---

Abstract

Finite state automata augmented with a channel through which messages can be passed are useful for modeling systems such as web services. If the channel satisfies the property that the message that was sent first is received first, then such automata are called FIFO systems. FIFO systems are Turing powerful and most verification problems are undecidable. However, in the restricted case where every control state is part of at most one simple cycle (called flat FIFO systems), some problems are known to be decidable. Given a flat FIFO system, we provide a method to construct a reversal bounded counter system that simulates the given flat FIFO system. Reversal bounded counter systems are another class of automata which have been widely studied and many decidability results are known. We study its implications, in terms of decidability of verification problems for flat FIFO systems.