|
Evènement pour le groupe Modélisation et Verification
Date | 2009-11-12 11:00-12: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 non-empty 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, Rez-de-chaussée |
Orateur | Alexander Heussner |
Url | LaBRI |
Aucun document lié à cet événement. RetourRetour à l'index
| |