• Algorithmes et vérification des systèmes concurrents
• Jeux distribués
• Synthèse de contrôleurs pour les systèmes concurrents
• Formalismes de spécification pour les systèmes concurrents

LIAFA Université Paris 7  CNRS (UMR 7089)	LaBRI Université Bordeaux 1  CNRS (UMR 5800)	LSV ENS Cachan CNRS (UMR 8643)
Blaise Genest	Julien Bernet	Paul Gastin
Hugo Gimbert	David Janin	Nathalie Sznajder
Florian Horn	Olivier Ly
Benjamin Lerman	Anca Muscholl
Wieslaw Zielonka (*)	Igor Walukiewicz (*)
	Pascal Weil
	Marc Zeitoun (*)

(*) Coordinateurs locaux

Le calcul concurrent et distribué est omniprésent : les processeurs modernes exécutent plusieurs tâches en parallèle, la plupart des systèmes (téléphones mobiles, automobiles, trains, etc) sont construits à partir de modules qui communiquent entre eux, et on peut en dire autant de très nombreux programmes et systèmes informatiques. La conception de tels systèmes, et la preuve de leur correction (les problèmes de synthèse et de vérification) sont des tâches difficiles mais indispensables, qui sont au coeur de ce projet. Ces deux problèmes ont connu un développement spectaculaire ces dernières années. Cependant les méthodes courantes rencontrent leurs limites (le phénomène dit d'explosion combinatoire) dès que l'on tente de les appliquer à des systèmes distribués, et ce malgré l'apparition d'heuristiques astucieuses. En effet, ces méthodes reposent pour l'essentiel sur une représentation séquentielle des comportements, mal adaptée aux systèmes distribués. Au contraire, ce projet se propose d'aborder les problèmes de vérification et de synthèse à l'aide de formalismes non séquentiels (modèles, langages de spécification et algorithmique). Les modèles de calcul sans entrelacement intègrent dans leur définition une notion de dépendance causale (réseaux de Petri, diagrammes du type MSC ou HMSC, automates  à contrôle distribué, traces, posets, structures d'événements). Pour ces modèles, le problème de l'existence d'un grand nombre d'exécutions équivalentes ne se pose pas. En revanche, nous ne disposons pas, pour ces modèles plus complexes, de l'accumulation de résultats connus pour les modèles plus classiques mais moins puissants des arbres ou des mots. Notre projet vise à développer les fondements nécessaires à l'application des formalismes non séquentiels à la verification et à la synthèse des systèmes distribués. Nous souhaitons ainsi éprouver la thèse selon laquelle disposer d'une information explicite sur le parallélisme et la distribution peut aider dans les tâches de vérification et de synthèse. Nous donnerons une importance particulière à l'usage des jeux distribués : il s'agit d'un modèle récemment introduit dans ce domaine, dont la version séquentielle a fait ses preuves dans l'étude des systèmes non distribués, et sur lequel les participants du projet ont acquis une expertise particulière.

• 17 octobre 2005.
  • 9h. P. Gastin, Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces.
  • 9h40. D. Janin, Raisonner sur les jeux de parité.
  • 10h50. W. Zielonka, Au delà des jeux de parité.
  • 11h30. A. Muscholl, On web services composition [ppt] (travail commun avec I. Walukiewicz).
  • 13h30. N. Sznajder, Synthèse de contrôleur pour les systèmes distribués synchrones.
  • 14h10. O. Ly, La théorie MSO de la Callithamnion Roseum est décidable
• 8 novembre 2004.
  • 9h. D. Janin. Théorie monadique des représentations finies de mots infinis ultimement périodiques.
  • 9h30. B. Lerman. Jeux distribués.
  • 10h. F. Horn. Quelques résultats sur les jeux de Street.
  • 11h. I. Walukiewicz. Automates temporisés et alternants.
  • 11h30. P. Weil. Langages d'arbres et préclones.
  • 14h. B. Courcelle (séminaire LaBRI). Graphes et matroides.
  • 15h30. H. Gimbert. Équilibres de Nash positionnels.
  • 16h. Séverine Fratani. Automates finis à oracles.
• 5 juillet 2004.
  • 9h W. Zielonka. Quelques nouveaux jeux à jouer.
  • 10h Igor Walukiewicz. SubLTL - Un fragment NP-complet de LTL.
  • 11h Paulo Tabuada (Groupe de travail vérification) Synthesis of correct-by-design embedded control software.
  • 14h Achim Blumensath. Lemme de pompage pour les automates à pile d'ordre supérieur.
  • 15h Blaise Genest. Extention du théorème de Kleene-Büchi pour les automates communicants existentiellement bornés.
  • 16h Hugo Gimbert. Quand peut-on jouer positionnellement? (article également disponible).
• 21 Janvier 2004.
  • 9h30 W. Zielonka, Jeux stochastiques à information complète.
  • 10h30 Igor Walukiewicz, Dépliages.
  • 11h30 Blaise Genest, Spécification et vérification de propriétés d'ordre partiels via les template MSCs.
  • 14h30 David Janin, Complexité logique de langages d'arbres.
  • 15h30 Benjamin Lerman, Jeux distribués.

Présentations de l'ACI

1. Présentation de VERSYDIS à Rennes, 11/12/03, par Paul Gastin. Transparents. Version imprimable.

Visites et présentations

1. Marc Zeitoun, LaBRI, 03/11/2003. Jeux distribués asynchrones.
2. Julien Bernet, LIAFA, du 05/01/2004 au 08/01/2004, Résolution des jeux distribués linéaires.
3. Igor Walukiewicz, LIAFA, du 25/02/2004 au 27/02/2004.
4. Anca Muscholl, LaBRI, du 17/05/2004 au 19/05/2004.
5. Blaise Genest et Anca Muscholl, LaBRI, du 20/10/2004 au 23/10/2004.

Publications

Liste au format BibTeX (maj. oct. 2006).

Thèses et habilitations

1. J. Bernet. Jeux distribués. Doctoral thesis, LaBRI, Université Bordeaux 1, Soutenance le 8 novembre 2006.
2. B. Genest. The odyssey of MSC-graphs. Doctoral thesis, LIAFA, University Paris 7, 2005.
3. H. Gimbert. Jeux positionnels. Doctoral thesis, LIAFA, University Paris 7, En cours d'évaluation.
4. D. Janin. Contribution aux fondements des méthodes formelles: jeux, logique et automates. Habilitation thesis, LaBRI, University Bordeaux 1, Nov. 2005.
5. B. Lerman. Vérification et spécification des systèmes distribués. Doctoral thesis, LIAFA, University Paris 7, Nov. 2005.
6. M. Zeitoun. Concurrence et automates. Habilitation thesis, LIAFA, University Paris 7, Dec. 2005.

Publications en journal (d'audience internationale, avec comité de sélection)

7. B. Courcelle and P. Weil. The recognizability of sets of graphs is a robust property. Theoretical Comput. Sci., 342:173–228, 2005.
8. V. Diekert and P. Gastin. Local temporal logic is expressively complete for cograph dependence alphabets. Inform. Comput., 195:30–52, 2004. PDF.
9. V. Diekert and P. Gastin. From local to global temporal logics over Mazurkiewicz traces. Theoretical Comput. Sci., 356(1-2):126–135, 2006. In honour of Professor Christian Choffrut on the occasion of his 60th birthday.
10. V. Diekert and P. Gastin. Pure future local temporal logics are expressively complete for Mazurkiewicz traces. Inform. Comput., 204:1597–1619, 2006.
11. M. Droste and P. Gastin. On aperiodic and star-free formal power series in partially commuting variables. ACM Trans. Comput. Syst., 2006. to appear. Also available as Research Report LSV-05-12, Laboratoire Spécification et Vérification, ENS Cachan, France, July 2005.
12. M. Droste and P. Gastin. Weighted automata and weighted logics. Theoretical Comput. Sci., 2007. Special issue of ICALP'05. To appear. Also available as Research Report LSV-05-13, Laboratoire Spécification et Vérification, ENS Cachan, France, July 2005.
13. Z. Ésik and P. Weil. Algebraic recognizability of regular tree languages. Theoretical Comput. Sci., 340:291–321, 2005.
14. B. Genest, D. Kuske, and A. Muscholl. A Kleene theorem and model checking for a class of communicating automata. Inform. Comput., 204(6):920–956, 2006.
15. B. Genest, A. Muscholl, H. Seidl, and M. Zeitoun. Infinite-state High level MSCs: realizability and model-checking. J. Comput. System Sci., 72(4):617–647, 2006 2006. PDF.
16. E. Graedel and I. Walukiewicz. Positional determinacy of games with infinitely many priorities. Methods of Logic in Computer Science, 2006. to appear.
17. D. Janin and G. Lenzi. On the relationship between monadic and weak monadic second order logic on arbitrary trees, with applications to the mu-calculus. Fundamenta Informaticae, 61(3,4):247–265, 2004.
18. A. Muscholl and I. Walukiewicz. An NP-complete fragment of LTL. International Journal of Foundations of Computer Science, 16(4):743–455, 2005.
19. D. Niwinski and I. Walukiewicz. Deciding nondeterministic hierarchy of deterministic tree automata. Elec. Notes Theor. Comp. Sci., 123:195–208, 2005.
20. P. Weil. On the logical definability of certain graph poset languages. J. Automata, Languages and Comput., 2005. To appear. PDF.

Conférences (d'audience internationale, avec comité de sélection)

21. B. Bérard, P. Gastin, and A. Petit. Intersection of regular signal-event (timed) languages. In E. Asarin and P. Bouyer, editors, Proc. of 4th Int. Conf. on Formal Modelling and Analysis of Timed Systems (FORMATS'06), volume 4202 of Lect. Notes Comp. Sci., pages 52–66. Springer, 2006.
22. B. Bérard, P. Gastin, and A. Petit. Refinements and abstractions of signal-event (timed) languages. In E. Asarin and P. Bouyer, editors, Proc. of 4th Int. Conf. on Formal Modelling and Analysis of Timed Systems (FORMATS'06), volume 4202 of Lect. Notes Comp. Sci., pages 67–81. Springer, 2006.
23. J. Bernet and D. Janin. Tree automata and discrete distributed games. In M. Liskiewicz and R. Reischuk, editors, Fundamentals of Computation Theory, volume 3623 of Lect. Notes Comp. Sci., pages 540–551. Springer, 2005.
24. J. Bernet and D. Janin. On distributed program specification and synthesis in architectures with cycles. In E. Najm, J.-F. Pradat-Peyre, and V. Viguié Donzeau-Gouge, editors, 26th IFIP WG 6.1 International Conference on Formal Methods for Networked and Distributed Systems (FORTE 2006), volume 4229 of Lect. Notes Comp. Sci., pages 175–190. Springer, 2006.
25. D. Berwanger and D. Janin. Automata on directed graphs: Edge versus vertex marking. In Third Int. Conf. on Graph Transformations (ICGT), volume 4128 of Lect. Notes Comp. Sci., pages 46–60. Springer, 2006.
26. P. Bhateja, P. Gastin, and M. Mukund. A fresh look at testing for asynchronous communication. In S. Graf and W. Zhang, editors, Proc. of 4th Int. Symp. on Automated Tech. for Verification and Analysis (ATVA'06), volume 4218 of Lect. Notes Comp. Sci. Springer, 2006. To appear.
27. M. Bojanczyk and I. Walukiewicz. Characterizing EF and EX tree logics. In Proc. of 15th Int. Conf. on Concurrency Theory, CONCUR '04, volume 3170 of Lect. Notes Comp. Sci., pages 131–145. Springer, 2004. PS.
28. A. Bouquet, O. Serre, and I. Walukiewicz. Pushdown games with the unboundedness and regular conditions. In Proc. of 23rd Foundations of Software Technology and Theoret. Comp. Sci., FSTTCS '03, volume 2914 of Lect. Notes Comp. Sci., pages 88–99, 2003. PDF.
29. A. Dawar and D. Janin. On the bisimulation invariant fragment of monadic Σ₁ in the finite. In Proc. of 24th Foundations of Software Technology and Theoret. Comp. Sci., FSTTCS '04, volume 3328, pages 224–236, 2004.
30. V. Diekert and P. Gastin. Pure future local temporal logics are expressively complete for Mazurkiewicz traces. In Proc. of 6th Symp. Latin American Theoret. INform., LATIN '04, volume 2976 of Lect. Notes Comp. Sci., pages 232–241. Springer, 2004. PDF.
31. M. Droste and P. Gastin. Weighted automata and weighted logics. In G. F. Italiano, editor, Proc. of 32nd Int. Coll. on Automata, Languages and Programming, ICALP '05, number 3580 in Lect. Notes Comp. Sci., pages 513–525. Springer, 2005.
32. P. Gastin and D. Kuske. Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces. In L. de Alfaro, editor, Proc. of 16th Int. Conf. on Concurrency Theory, CONCUR '05, number 3653 in Lect. Notes Comp. Sci., pages 533–547. Springer, 2005.
33. P. Gastin, B. Lerman, and M. Zeitoun. Distributed games and distributed control for asynchronous systems. In M. Farach-Colton, editor, Proc. of 6th Symp. Latin American Theoret. INform., LATIN '04, volume 2976 of Lect. Notes Comp. Sci., pages 455–465. Springer, 2004. PDF.
34. P. Gastin, B. Lerman, and M. Zeitoun. Distributed games with causal memory are decidable for series-parallel systems. In Proc. of 24th Foundations of Software Technology and Theoret. Comp. Sci., FSTTCS '04, volume 3328 of Lect. Notes Comp. Sci., pages 275–286. Springer, 2004. PDF.
35. P. Gastin, P. Moro, and M. Zeitoun. Minimization of counterexamples in SPIN. In Model Checking Software: Proc. of 11th SPIN '04, volume 2989 of Lect. Notes Comp. Sci., pages 92–108. Springer, 2004. PDF.
36. P. Gastin, N. Sznajder, and M. Zeitoun. Distributed synthesis for well-connected architectures. In N. Garg and S. Arun-Kumar, editors, Proc. of 26th Foundations of Software Technology and Theoret. Comp. Sci., FSTTCS '06, Lect. Notes Comp. Sci. Springer, 2006. To appear.
37. B. Genest. Compositional message sequence charts (CMSCs) are better to implement than MSCs. In Proc. of Tools and Algorithms for the construction and analysis of systems, TACAS '05, volume 3440 of Lect. Notes Comp. Sci., pages 510–525. Springer, 2005.
38. B. Genest. On implementation of global concurrent systems with local asynchronous controllers. In Proc. of 16th Int. Conf. on Concurrency Theory, CONCUR '05, volume 3653 of Lect. Notes Comp. Sci., pages 443–457, 2005.
39. B. Genest, D. Kuske, and A. Muscholl. A Kleene theorem and model checking for a class of communicating automata. In Proc. of Developments in Language Theory, DLT '04, volume 3340 of Lect. Notes Comp. Sci., pages 30–48. Springer, 2004.
40. B. Genest, D. Kuske, A. Muscholl, and D. Peled. Snapshot verification. In Proc. of Tools and Algorithms for the construction and analysis of systems, TACAS '05, volume 3440 of Lect. Notes Comp. Sci. Springer, 2005.
41. B. Genest, M. Minea, A. Muscholl, and D. Peled. Specifying and verifying partial order properties using template MSCs. In Proc. of Foundations of Software Science and Computation Structures, FOSSACS '04, volume 2987 of Lect. Notes Comp. Sci., pages 195–210. Springer, 2004.
42. B. Genest and A. Muscholl. Message sequence charts: A survey. In 5th Int. Conf. on Application of Concurrency to System Design, ACSD'05, pages 2–4, 2005. Invited talk.
43. B. Genest and A. Muscholl. Constructing exponential-size deterministic Zielonka automata. In Proc. of 33rd Int. Coll. on Automata, Languages and Programming, ICALP '06, volume 4052 of Lect. Notes Comp. Sci., pages 565–576, 2006.
44. H. Gimbert. Parity and exploration games on infinite graphs. In Proc. of Computer Science Logic, CSL '04, volume 3210 of Lect. Notes Comp. Sci., pages 56–70. Springer, 2004. PS.
45. H. Gimbert and W. Zielonka. Discounting infinite games but how and why? In L. de Alfaro, editor, Proc. of Games in Design and Verification '04, volume 119 of Elec. Notes Theor. Comp. Sci., pages 3–9. Elsevier, 2004.
46. H. Gimbert and W. Zielonka. When can you play positionally? In Proc. of Symp. on Math. Foundations of Comput. Sci., MFCS '04, volume 3153 of Lect. Notes Comp. Sci., pages 686–697. Springer, 2004. PS.
47. H. Gimbert and W. Zielonka. Games where you can play optimally without any memory. In Proc. of 16th Int. Conf. on Concurrency Theory, CONCUR '05, volume 3653 of Lect. Notes Comp. Sci., pages 428–442. Springer, 2005.
48. H. Gimbert and W. Zielonka. Deterministic priority mean-payoff games as limits of discounted games. In Proc. of 33rd Int. Coll. on Automata, Languages and Programming, ICALP '06, volume 4052, part II of Lect. Notes Comp. Sci., pages 312–323. Springer, 2006.
49. L. Hélouët, M. Zeitoun, and A. Degorre. Scenarios and covert channels: another game... In L. de Alfaro, editor, Proc. of Games in Design and Verification '04, volume 119 of Elec. Notes Theor. Comp. Sci., pages 93–116. Elsevier, 2004. PDF.
50. T. Knapik, D. Niwinski, P. Urzyczyn, and I. Walukiewicz. Unsafe grammars and panic automata. In Proc. of 32nd Int. Coll. on Automata, Languages and Programming, ICALP '05, volume 3580 of Lect. Notes Comp. Sci., pages 1450–1461, 2005.
51. S. Lasota and I. Walukiewicz. Alternating timed automata. In Proc. of Foundations of Software Science and Computation Structures, FOSSACS '05, number 3441 in Lect. Notes Comp. Sci., pages 250–265, 2005. Journal version available from WWW.
52. O. Ly. Compositional verification: Decidability issues using graph substitutions. In Proc. of Symp. on Math. Foundations of Comput. Sci., MFCS '04, volume 3153 of Lect. Notes Comp. Sci., pages 537–549. Springer, 2004.
53. S. Mohalik and I. Walukiewicz. Distributed games. In Proc. of 23rd Foundations of Software Technology and Theoret. Comp. Sci., FSTTCS '03, volume 2914 of Lect. Notes Comp. Sci., pages 338–351, 2003. PS (long version).
54. A. Murawski, L. Ong, and I. Walukiewicz. Idealized Algol with ground recursion, and DPDA equivalence. In Proc. of 32nd Int. Coll. on Automata, Languages and Programming, ICALP '05, volume 3580 of Lect. Notes Comp. Sci., pages 917–929, 2005.
55. A. Murawski and I. Walukiewicz. Third-order idealized Algol with iteration is decidable. In Proc. of Foundations of Software Science and Computation Structures, FOSSACS '05, volume 3441 of Lect. Notes Comp. Sci., pages 202–218, 2005.
56. A. Muscholl and I. Walukiewicz. An NP-complete fragment of LTL. In Proc. of Developments in Language Theory, DLT '04, volume 3340 of Lect. Notes Comp. Sci., pages 334–344. Springer, 2004. PS.
57. D. Niwinski and I. Walukiewicz. Deciding nondeterministic hierarchy of deterministic tree automata. In R. de Queiroz and P. Cégielski, editors, Proceedings of WoLLIC'04, volume 123 of Elec. Notes Theor. Comp. Sci., pages 195–208. Elsevier, 2005.
58. I. Walukiewicz. A landscape with games in the background. In Proc. of IEEE LICS '04, pages 356–366, 2004. PS.
59. I. Walukiewicz. From logic to games. In Proc. of 25th Foundations of Software Technology and Theoret. Comp. Sci., FSTTCS '05, volume 3821 of Lect. Notes Comp. Sci., pages 78–91, 2005.
60. P. Weil. Algebraic recognizability of languages. In Proc. of Symp. on Math. Foundations of Comput. Sci., MFCS '04, volume 3153 of Lect. Notes Comp. Sci., pages 149–175. Springer, 2004.
61. W. Zielonka. Perfect-information stochastic parity games. In Proc. of Foundations of Software Science and Computation Structures, FOSSACS '04, volume 2987 of Lect. Notes Comp. Sci., pages 499–513. Springer, 2004.
62. W. Zielonka. An invitation to play. In Proc. of Symp. on Math. Foundations of Comput. Sci., MFCS '05, volume 3618 of Lect. Notes Comp. Sci., pages 58–70. Springer, 2005.

Rapports de recherche

63. J. Bernet and D. Janin. Automata theory for distributed games. Technical report, LaBRI, 2004.
64. J.-M. Couvreur, D. Poitrenaud, and P. Weil. Unfoldings for general Petri nets. Submitted.