Decidability of Parameterised Model-Checking

Mat Hague (Oxford University Computing Laboratory)

Info

Date	18th February 2009 (week 5, Hilary Term 2009)
Time	12:00
Place	Room 441, Oxford University Computing Laboratory

Abstract

A parameterised system consists of a schemata P, which, given an input n, produces a concrete system P(n). The reachability problem asks whether a given state is reachable in P(n) for some n. This problem can be used to verify concurrent systems consisting of a variable number of threads or network nodes. In general, this problem is known to be undecidable, even for finite-state nodes/threads.

A pushdown system augments a finite state system with a stack, which can be used to model recursive procedure calls. When two threads are allowed recursion and communication, reachability becomes undecidable.

However, in LICS 2008, Kahlon presented a surprising algorithm that showed parameterised reachability is decidable for pushdown threads. I will survey the results in this area and attempt to provide an intuition for the concessions that permit decidability.