Javier Esparza
Parameterized Verification of Asynchronous Shared-Memory Systems
VCLA hosted a talk by Javier Esparza on January 31st, 2013.
| DATE: | Thursday, January 31, 2013 |
| TIME: | 17:00 |
| VENUE: | seminar room Zemanek |
ABSTRACT
We characterize the complexity of the safety verification problem for parameterized systems consisting of a leader process and arbitrarily many anonymous and identical contributors. Processes communicate through a shared, bounded-value register. While each operation on the register is atomic, there is no synchronization primitive to execute a sequence of operations atomically. The model is inspired by distributed algorithms implemented on sensor networks.
We analyze the complexity of the safety verification problem when processes are modeled by finite-state machines, pushdown machines, and Turing machines. Our proofs use combinatorial characterizations of computations in the model, and in case of pushdown-systems, some novel language-theoretic constructions of independent interest.
This is joint work with Pierre Ganty and Rupak Majumdar.
