Skip to main content

Decidability of Parameterised Model-Checking

Mat Hague ( Oxford University Computing Laboratory )

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.

Share this: