Decidability of Parameterised Model-Checking
- 12:00 18th February 2009 ( week 5, Hilary Term 2009 )Room 441, 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:
