• Algorithms and verification of concurrent systems
• Distributed games
• Controller synthesis for concurrent systems
• Specification formalisms for concurrent systems

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 (*)

  (*) Local coordinators

Summary

Parallel and distributed computing is omnipresent. Modern processors execute several tasks in parallel. Most systems, like mobile phones, cars, trains are constructed from modules communicating with each other. The same is true for many programs. Designing and proving the correctness of such systems is a critical and challenging task. It is one of the important goals of theoretical computer science to find adequate methodology and tools for doing it. In our proposal we are concerned with security understood as guaranteeing that a behavior satisfies a specification. We want to develop concepts and tools to design safe systems and to verify that the behavior of systems complies with their specifications -- turning our attention mostly to distributed systems. Our project fits in the general framework known as computer aided verification, and concentrates on the model checking problem and the synthesis problem. In the past few years, these two problems have developed at a rapid pace, both in theory and in applications. The method used relies on the basic concepts of the theory of computation: finite state automata, formal languages of words or trees. The foundation of the method is the equivalence between the algebraic notion of recognizability, logical definability and automata-theoretic recognizability. The first two formalisms are used to specify properties of a system, and the third one is used in the verification algorithms – verification reduces to testing the emptiness of the language accepted by an automaton. While systems with many parallel components can be inherently complex, their modeling by graph or sequences of states is a source of additional complexity. There may be many interleavings of the same system execution due to the necessity of (ad hoc) ordering actions occurring in parallel. Knowing the structure of the system, we can deduce that some interleavings should be considered as equivalent, i.e., representing the same behavior. Ordering actions which are in fact independent can actually lead to an exponential blow-up of the number of behaviors to be studied, which makes the usual algorithms unable to cope with reasonable size distributed systems. The heuristics of discovering equivalent interleavings are called partial order reduction methods. We propose another way to tackle the above described problem of explosion in the number of representations of an execution. There exist so called non-interleaving models of computations with a built-in notion of independence. For them the problem of many models describing the same execution does not exist. The problem that appears is that for these new, less studied, models we lack the wealth of results that we have for more classical models like words or trees. We plan to investigate the possibility of doing verification using non-interleaving models by developing the necessary theoretical results and investigating their applicability. Our plan is to work as long as possible in the non-interleaving word. Hence, to model systems by non-interleaving models, to use logical formalism over these models and to use variants of automata suitable for these models. The hope is that having explicit information about the concurrency may help in the verification process. In some cases this approach is essential because some interesting properties of systems are not expressible in the interleaving framework. Below we shortly summarize different models and formalism which we would like to investigate and use. We also single out several problems on which we plan to work.

Models

Petri nets, asynchronous automata, HMSC (hierarchical message sequence charts) are classical examples of non-interleaving models of systems where the notions of concurrency and causality are explicit. To describe their behavior, it is preferable to use mathematical structures that can express some form of concurrency information. The simplest and best investigated structures are traces. More general models are for example posets (with the interesting subclass of series-parallel posets) and MSC (message sequence charts). There exist also branching time models such as event structures. As opposed to the models mentioned before, one event structure can describe all the possible executions of a system. Such models are necessary when one is interested in branching properties.

Specification formalisms

If one decides to work directly with non-interleaving models it is necessary to use formalisms adapted to them. First and second-order logics extend naturally to all kinds of models and serve as a kind of a yardstick to compare the expressive power of other formalisms. Temporal logic on traces is the subject of many recent papers, but not much is know about temporal logics on other models. The algebraic approach works relatively well in the case of traces and series-parallel posets. Finally, being both basic and versatile, automata can be also used to specify desired behaviors. Asynchronous automata for traces and branching automata for series-parallel posets are interesting extensions of this classical notion.

Distributed games

Games can be seen as a model of interactive computation, as a specification formalism or as a technical tool. In the interleaving setting, the final step of verification is to check emptiness of the language of an automaton. The general method for doing this is to solve an associated two-player game. Similarly the synthesis problem reduces to a problem of solving games. For noninterleaving settings, we propose to consider games where the environment plays against a coalition of players, each of which has only partial knowledge about the global state of the game.

Problems

We briefly summarize some of the problems we want to consider. We want to develop tools for solving interesting classes of distributed games (in general they are not algorithmically solvable). We would like to use the distributed game model to study the distributed synthesis problem. We plan to use this model to study the different notions of bisimulations for concurrent systems. We want to find an efficient method of synthesizing asynchronous automata from a given specification, and to develop and study the notion of alternating asynchronous automaton. Understanding the relations between diagram-based specifications (using HMSCs, LSCs, etc) and communicating automata and other machines is an important objective. For instance, to develop an automatic modification scheme for non-executable specifications. We want to continue to study linear time temporal logics for non-interleaving models. We would also like to develop branching time logics. We plan to use this logic together with the Petri net unwinding technique to obtain new model checking algorithms. Finally we want to study the extensions of the fundamental notions of recognizability, regularity and rationality. Their extension to traces turned out to be very rewarding; now we want to study these notions over pomsets and event structures. This could allow us to find a more manageable subclasses of these models.

• October 17, 2005.
  • 9h. P. Gastin, Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces.
  • 9h40. D. Janin, Reasonning on parity games.
  • 10h50 W. Zielonka, Beyond parity games.
  • 11h30. A. Muscholl, On web services composition [ppt] (joint work with I. Walukiewicz).
  • 13h30. N. Sznajder, Controller synthesis for synchronous distributed systems.
  • 14h10. O. Ly, The MSO theory of Callithamnion Roseum is decidable
• November 8, 2004.
  • 9h. D. Janin. Monadic theory of finite representations of infinite ultimately periodic words.
  • 9h30. B. Lerman. Distributed games.
  • 10h. F. Horn. Some results on Street games.
  • 11h. I. Walukiewicz. Timed alternating automata.
  • 11h30. P. Weil. Tree languages and preclones.
  • 14h. B. Courcelle (LaBRI seminar). Graphs and matroids.
  • 15h30. H. Gimbert. Positional Nash equilibria.
  • 16h. Séverine Fratani. Finite automata with oracles.
• July 5, 2004.
  • 9h W. Zielonka. Some new games to play.
  • 10h Igor Walukiewicz. SubLTL - An NP-complete fragment of LTL.
  • 11h Paulo Tabuada (Working group on verification) Synthesis of correct-by-design embedded control software.
  • 14h Achim Blumensath. A Pumping Lemma for Higher-Order Pushdown Automata.
  • 15h Blaise Genest. The Kleene-Büchi theorem for existentially bounded communicating automata.
  • 16h Hugo Gimbert. When can you play positionally? (paper available here.)
• January 21, 2004.
  • 9h30 W. Zielonka, Stochastic games with partial information.
  • 10h30 Igor Walukiewicz, Unwindings.
  • 11h30 Blaise Genest, Specifying and Verifying Partial Order Properties using Template MSCs.
  • 14h30 David Janin, Logical complexity of tree languages.
  • 15h30 Benjamin Lerman, Distributed games.

Talks

1. VERSYDIS presentation at Rennes, by Paul Gastin, 12/11/03. Slides. Printable version.

Visits and related presentations

1. Marc Zeitoun, LaBRI, 03/11/2003. Asynchronous distributed games.
2. Julien Bernet, LIAFA, from 05/01/2004 to 08/01/2004, Solving linear distributed games.
3. Igor Walukiewicz, LIAFA, from 25/02/2004 to 27/02/2004.
4. Anca Muscholl, LaBRI, from 17/05/2004 to 19/05/2004.
5. Blaise Genest and Anca Muscholl, LaBRI, from 20/10/2004 to 23/10/2004.

Publications

List, BibTeX format (oct. 2006).

Doctoral and habilitation theses

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.

Journal papers

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.

International conferences

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.

Research reports

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.