Natural Specifications Yield Decidability for Distributed Synthesis of Asynchronous Systems

Paul Gastin 1 Nathalie Sznajder 1 Thomas Chatain 1, 2
1 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
Abstract : We study the synthesis problem in an asynchronous distributed setting: a finite set of processes interact locally with an uncontrollable environment and communicate with each other by sending signals--actions that are immediately received by the target process. The synthesis problem is to come up with a local strategy for each process such that the resulting behaviours of the system meet a given specification. We consider external specifications over partial orders. External means that specifications only relate input and output actions from and to the environment and not signals exchanged by processes. We also ask for some closure properties of the specification. We present this new setting for studying the distributed synthesis problem, and give decidability results: the non-distributed case, and the subclass of networks where communication happens through a strongly connected graph. We believe that this framework for distributed synthesis yields decidability results for many more architectures.
Type de document :
Communication dans un congrès
Nielsen, Mogens and Ku\v cera, Antonín and Bro Miltersen, Peter and Palamidessi, Catuscia and T\ruma, Petr and Valencia, Franck. Proceedings of the 35th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM'09), Jan 2009, Mlýn, Czech Republic. Springer, 5404, pp.141-152, 2009, 〈10.1007/978-3-540-95891-8_16〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00772667
Contributeur : Stefan Haar <>
Soumis le : jeudi 10 janvier 2013 - 22:44:17
Dernière modification le : jeudi 11 janvier 2018 - 06:23:37

Identifiants

Collections

Citation

Paul Gastin, Nathalie Sznajder, Thomas Chatain. Natural Specifications Yield Decidability for Distributed Synthesis of Asynchronous Systems. Nielsen, Mogens and Ku\v cera, Antonín and Bro Miltersen, Peter and Palamidessi, Catuscia and T\ruma, Petr and Valencia, Franck. Proceedings of the 35th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM'09), Jan 2009, Mlýn, Czech Republic. Springer, 5404, pp.141-152, 2009, 〈10.1007/978-3-540-95891-8_16〉. 〈hal-00772667〉

Partager

Métriques

Consultations de la notice

102