Parameterized Verification of Asynchronous Shared-Memory Systems

Date: Thursday, January 31, 2013
Speaker: Javier Esparza
Venue: TU Wien

We characterize the complexity of the safety verification problem forparameterized systems consisting of a leader process and arbitrarily manyanonymous and identical contributors. Processes communicate through ashared, bounded-value register. While each operation on the registeris atomic, there is no synchronization primitive to execute a sequenceof operations atomically. The model is inspired by distributedalgorithms implemented on sensor networks.We analyze the complexity of the safety verification problem whenprocesses are modeled by finite-state machines, pushdown machines, andTuring machines. Our proofs use combinatorial characterizations ofcomputations in the model, and in case of pushdown-systems, some novellanguage-theoretic constructions of independent interest.

Posted in RiSE Seminar