
Evènement pour le groupe Modélisation et Verification
Date  20091112 11:0012:15 
Titre  Reachability Analysis of Communicating Pushdown Systems 
Résumé  The reachability analysis of recursive programs that communicate
over asynchronous and reliable fifo channels calls for restrictions
to ensure decidability. We extend here a model proposed by La Torre,
Madhusudan and Parlato [TACAS08], based on communicating pushdown
systems that can dequeue with empty stack only. Our extension adds
the dual modality, which allows to dequeue with nonempty stack, thus
modelling interrupts for working threads. We study (possibly cyclic)
network architectures under a semantic assumption (mutex
communication) that ensures the decidability of reachability for
finite state systems. Subsequently, we determine precisely how
pushdowns can be added to this setting while preserving the
decidability; in the positive case we obtain exponential time as the
exact complexity bound of reachability. A second result is a
generalization of the doubly exponential time algorithm of [LaTorre
et al: TACAS08] for bounded context analysis to our symmetric
queueing policy. We provide here a direct (and simpler) proof.
Joint work with Jérôme Leroux, Anca Muscholl, Grégoire Sutre 
Lieu  Salle 076, LaBRI, Rezdechaussée 
Orateur  Alexander Heussner 
Url  LaBRI 
Aucun document lié à cet événement. RetourRetour à l'index
 