Evènement pour le groupe Modélisation et Verification

Date 2009-11-12  11:00-12:15
TitreReachability 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 
LieuSalle 076, LaBRI, Rez-de-chaussée 
OrateurAlexander Heussner 

Aucun document lié à cet événement.

Retour à l'index