Paving the way for verification of distributed systems
From our undergraduate courses, we are familiar with the notion finite-state automata (also known as finite-state machines or, simply, state machines), which are abstract models of computation systems. During a computation, the automaton processes the various actions that constitute the computation, and moves from one state to another. A computation is accepted if, at the end of it, the finite-state automaton finally acquires an accepting state.
However, for many practical cases, it is not enough to analyse what happens at the end of the computation, and becomes important to consider what happens during a computation. In this sense, the analysis concerns itself with conditions such as “the system always remains safe” (safety condition) or “the system does something good repeatedly” (liveness condition). In this setting, it turns out naturally to assume that these computation systems have non-terminating behaviours. Therefore, infinite computations are considered. The finite-state automata to study such systems evaluate computations by observing whether or not the automaton “always remains in the set of good states,” or that it “visits good states repeatedly”.
While finite-state automata provide an abstract representation of non-terminating, sequential (or single threaded) computation systems — and the corresponding safety and liveness automata have been studied extensively — the study of non-terminating distributed systems has not seen much progress since the 1990’s. In particular, “distributed automata” analysing the safety and liveness properties of distributed systems have been elusive.
In this talk, I will present the word that I did as a part of my PhD thesis, which introduces classes of finite-state automata as well as distributed automata that help in analysing these important properties of non-terminating distributed systems.
- Finite state automata
- Connection between code, logic, and automata
- Verification using automata
- Distributed automata and verification of distributed systems
Some appetite for Computer Science theory.
Namit Chaturvedi is a computer science researcher, currently working at LinkedIn. He obtained his PhD in logic and automata theory in 2015 and transitioned to the world of machine learning and AI. He has previously worked on diverse projects, from load balancing on distributed systems to applying automata theory for physical access control. He has 10 publications in peer-reviewed conferences and journals; and jointly holds 2 technology patents.
His interests include outdoor sports, history of science, effect of science and technology on societies, and beer.