Parameterized Communicating Automata: Complementation and Model CheckingReportar como inadecuado

Parameterized Communicating Automata: Complementation and Model Checking - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 LSV - Laboratoire Spécification et Vérification Cachan 2 MEXICO - Modeling and Exploitation of Interaction and Concurrency LSV - Laboratoire Spécification et Vérification Cachan, ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643 3 CSE - Department of Computer Science and Engineering Kanpur

Abstract : We study the language-theoretical aspects of parameterized communicating automata PCAs, in which processes communicate via rendez-vous. A given PCA can be run on any topology of bounded degree such as pipelines, rings, ranked trees, bus topologies, and grids. We show that, under a context bound, which restricts the local behavior of each process, PCAs are effectively complementable. Complementability is considered a key aspect of robust automata models and can, in particular, be exploited for verification. In this paper, we use it to obtain a characterization of context-bounded PCAs in terms of monadic second-order MSO logic. As the emptiness problem for context-bounded PCAs is decidable for the classes of pipelines, rings, and trees, their model-checking problem wrt. MSO properties also becomes decidable. While previous work on model checking parameterized systems typically uses temporal logics without next operator, our MSO logic allows one to express several natural next modalities.

Autor: Benedikt Bollig - Paul Gastin - Akshay Kumar -



Documentos relacionados