Books | |
| • | . Cours et exercices d'informatique, Classes préparatoires, premier et second cycles universitaires. Vuibert, 1998. ( BibTeX ) |
Chapters in Books | |
| • | . Specification and Verification using Temporal Logics. In Modern applications of automata theory, IISc Research Monographs 2. World Scientific, 2009. To appear. ( PDF | BibTeX + Abstract ) |
| • | . Weighted automata and weighted logics. In Handbook of Weighted Automata, EATCS Monographs in Theoretical Computer Science, chapter 5, pages 175-211. Springer, 2009. ( PDF | BibTeX ) |
| • | . Local safety and local liveness for distributed systems. In Perspectives in Concurrency Theory, IARCS-Universities, pages 86-106. Universities Press, 2009. ( PDF | BibTeX + Abstract ) |
| • | . Reachability and boundedness in time-constrained MSC graphs. In Perspectives in Concurrency Theory, IARCS-Universities, pages 157-183. Universities Press, 2009. ( PDF | BibTeX + Abstract ) |
| • | . First-order definable languages. In Logic and Automata: History and Perspectives, Texts in Logic and Games 2, pages 261-306. Amsterdam University Press, 2008. ( PDF | BibTeX + Abstract ) |
| • | . Safety and Liveness Properties for Real Traces and a Direct Translation from LTL to Monoids. In Formal and Natural Computing, LNCS 2300, pages 26-38. Springer, 2002. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . Infinite traces. In The Book of Traces, chapter 11, pages 393-486. World Scientific, 1995. ( PS | PS.GZ | BibTeX ) |
| • | . Infinite Traces. In Semantics of Systems of Concurrent Processes - Proceedings of the LITP Spring School on Theoretical Computer Science, La Roche Posay, France, April 1990, LNCS 469, pages 277-308. Springer, 1990. ( BibTeX + Abstract ) |
Edited Books | |
| • | S. Anantharaman, P. Gastin, G. Hains, J. Mullins and M. Rusinowitch (eds.). Selected papers of the International Workshop on Security Analysis of Systems: Formalisms and Tools (SASYFT'04), Orléans, France, June 2004. ( BibTeX ) |
| • | M. Droste and P. Gastin (eds.). Selected papers of the workshop on Logic and Algebra in Concurrency, Dresden, Germany, September 2000. Journal of Automata, Languages and Combinatorics 7(2), 2002. ( BibTeX ) |
| • | P. Gastin and J. Rutten (eds.). Selected papers of the workshop on Topology and Completion in Semantics, Chartes, France, November 1993. Theoretical Computer Science 151(1), 1995. ( BibTeX ) |
Journals | |
| • | . Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces. Information and Computation, 2010. To appear. ( BibTeX + Abstract ) |
| • | . Distributed synthesis for well-connected architectures. Formal Methods in System Design 34(3), pages 215-237, 2009. ( PDF | BibTeX + Abstract ) |
| • | . A Survey on Small Fragments of First-Order Logic over Finite Words. International Journal of Foundations of Computer Science 19(3), pages 513-548, 2008. ( PDF | BibTeX + Abstract ) |
| • | . On aperiodic and star-free formal power series in partially commuting variables. Theory of Computing Systems 42(4), pages 608-631, 2008. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . Uniform satisfiability in PSPACE for local temporal logics over Mazurkiewicz traces. Fundamenta Informaticae 80(1-3), pages 169-197, 2007. ( PDF | BibTeX + Abstract ) |
| • | . Timed substitutions for regular signal-event languages. Formal Methods in System Design 31(2), pages 101-134, 2007. ( PDF | BibTeX + Abstract ) |
| • | . Weighted automata and weighted logics. Theoretical Computer Science 380(1-2), pages 69-86, 2007. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . Pure future local temporal logics are expressively complete for Mazurkiewicz traces. Information and Computation 204(11), pages 1597-1619, 2006. ( PDF | BibTeX + Abstract ) |
| • | . From local to global temporal logics over Mazurkiewicz traces. Theoretical Computer Science 356(1-2), pages 126-135, 2006. ( PDF | BibTeX + Abstract ) |
| • | . Local temporal logic is expressively complete for cograph dependence alphabets. Information and Computation 195(1-2), pages 30-52, 2004. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . A simple process algebra based on atomic actions with resources. Mathematical Structures in Computer Science 14(1), pages 1-55, 2004. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . A truly concurrent semantics for a process algebra using resource pomsets. Theoretical Computer Science 281(1-2), pages 369-421, 2002. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . Resource traces: A domain for processes sharing exclusive resources. Theoretical Computer Science 278(1-2), pages 195-221, 2002. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . LTL is expressively complete for Mazurkiewicz traces. Journal of Computer and System Sciences 64(2), pages 396-418, 2002. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . Asynchronous cellular automata for pomsets. Theoretical Computer Science 247(1-2), pages 1-38, 2000. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . The Kleene-Schützenberger theorem for formal power series in partially commuting variables. Information and Computation 153(1), pages 47-80, 1999. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . Approximating traces. Acta Informatica 35(7), pages 567-593, 1998. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . Characterization of the Expressive Power of Silent Transitions in Timed Automata. Fundamenta Informaticae 36(2), pages 145-182, 1998. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . Rational and Recognizable Complex Trace Languages. Information and Computation 116(1), pages 134-153, 1995. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . An Extension of Kleene's and Ochmanski's Theorems to Infinite Traces. Theoretical Computer Science 125(2), pages 167-204, 1994. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . The poset of infinitary traces. Theoretical Computer Science 120(1), pages 101-121, 1993. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . An efficient crash-tolerant sequential traversal. Parallel Processing Letters 3, pages 87-97, 1993. ( BibTeX + Abstract ) |
| • | . Decidability of the star problem in A* × {b}*. Information Processing Letters 44(2), pages 65-71, 1992. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . Un modèle asynchrone pour les systèmes distribués. Theoretical Computer Science 74(1), pages 121-161, 1990. ( BibTeX + Abstract ) |
Conferences | |
| • | . Weighted versus Probabilistic Logics. In DLT'09, LNCS 5583, pages 18-38. Springer, 2009. ( PDF | BibTeX + Abstract ) |
| • | . Natural Specifications Yield Decidability for Distributed Synthesis of Asynchronous Systems. In SOFSEM'09, LNCS 5404, pages 141-152. Springer, 2009. ( PDF | BibTeX + Abstract ) |
| • | . Distributed Timed Automata with Independently Evolving Clocks. In CONCUR'08, LNCS 5201, pages 82-97. Springer, 2008. ( PDF | BibTeX + Abstract ) |
| • | . Automata and Logics for Timed Message Sequence Charts. In FSTTCS'07, LNCS 4855, pages 290-302. Springer, 2007. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . Local testing of message sequence charts is difficult. In FCT'07, LNCS 4639, pages 76-87. Springer, 2007. ( PDF | BibTeX + Abstract ) |
| • | . Minimal counter-example generation for SPIN. In SPIN'07, LNCS 4595, pages 24-38. Springer, 2007. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . Distributed synthesis for well-connected architectures. In FSTTCS'06, LNCS 4337, pages 321-332. Springer, 2006. ( PDF | BibTeX + Abstract ) |
| • | . A fresh look at testing for asynchronous communication. In ATVA'06, LNCS 4218, pages 369-383. Springer, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . Refinements and abstractions of signal-event (timed) languages. In FORMATS'06, LNCS 4202, pages 67-81. Springer, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . Intersection of regular signal-event (timed) languages. In FORMATS'06, LNCS 4202, pages 52-66. Springer, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . Uniform Satisfiability Problem for Local Temporal Logics over Mazurkiewicz Traces. In CONCUR'05, LNCS 3653, pages 533-547. Springer, 2005. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . Weighted Automata and Weighted Logics. In ICALP'05, LNCS 3580, pages 513-525. Springer, 2005. ( PDF | PS | PS.GZ | PDF (long version) | PS (long version) | PS.GZ (long version) | BibTeX + Abstract ) |
| • | . Distributed games with causal memory are decidable for series-parallel systems. In FSTTCS'04, LNCS 3328, pages 275-286. Springer, 2004. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . Pure future local temporal logics are expressively complete for Mazurkiewicz traces. In LATIN'04, LNCS 2976, pages 232-241. Springer, 2004. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . Distributed games and distributed control for asynchronous systems. In LATIN'04, LNCS 2976, pages 455-465. Springer, 2004. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . Minimization of counterexamples in SPIN. In SPIN'04, LNCS 2989, pages 92-108. Springer, 2004. ( PDF | PS | PS.GZ | BibTeX + Abstract ) |
| • | . Satisfiability and Model Checking for MSO-definable Temporal Logics are in PSPACE. In CONCUR'03, LNCS 2761, pages 222-236. Springer, 2003. ( PS | PS.GZ | PS (long version) | PS.GZ (long version) | BibTeX + Abstract ) |
| • | . Local LTL with past constants is expressively complete for Mazurkiewicz traces. In MFCS'03, LNCS 2747, pages 429-438. Springer, 2003. ( PS | PS.GZ | PS (long version) | PS.GZ (long version) | BibTeX + Abstract ) |
| • | . LTL with past and two-way very-weak alternating automata. In MFCS'03, LNCS 2747, pages 439-448. Springer, 2003. ( PS | PS.GZ | PS (long version) | PS.GZ (long version) | BibTeX + Abstract ) |
| • | . An Elementary Expressively Complete Temporal Logic for Mazurkiewicz Traces. In ICALP'02, LNCS 2380, pages 938-949. Springer, 2002. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . Local Temporal Logic is Expressively Complete for Cograph Dependence Alphabets. In LPAR'01, LNAI 2250, pages 55-69. Springer, 2001. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . Fast LTL to Büchi Automata Translation. In CAV'01, LNCS 2102, pages 53-65. Springer, 2001. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . Model Checking Systems of Replicated Processes with SPIN. In SPIN'01, LNCS 2057, pages 235-251. Springer, 2001. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . Avoiding state explosion for distributed systems with timestamps. In FME'01, LNCS 2021, pages 119-134. Springer, 2001. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . LTL is expressively complete for Mazurkiewicz traces. In ICALP 2000, LNCS 1853, pages 211-222. Springer, 2000. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . On aperiodic and star-free formal power series in partially commuting variables. In FPSAC'00, pages 158-169. Springer, 2000. ( PS | PS.GZ | PDF (long version) | PS (long version) | PS.GZ (long version) | BibTeX + Abstract ) |
| • | . An expressively complete temporal logic without past tense operators for Mazurkiewicz traces. In CSL'99, LNCS 1683, pages 188-203. Springer, 1999. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . A truly concurrent semantics for a simple parallel programming language. In CSL'99, LNCS 1683, pages 515-529. Springer, 1999. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . A (non-elementary) modular decision procedure for LTrL. In MFCS'98, LNCS 1450, pages 356-365. Springer, 1998. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . On recognizable and rational formal power series in partially commuting variables. In ICALP'97, LNCS 1256, pages 682-692. Springer, 1997. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . Removing ε-Transitions in Timed Automata. In STACS'97, LNCS 1200, pages 583-594. Springer, 1997. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . Recent Developments in Trace Theory. In DLT'95, pages 373-385. World Scientific, 1996. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . Asynchronous cellular automata for Pomsets without auto-concurrency. In CONCUR'96, LNCS 1119, pages 627-638. Springer, 1996. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . On the Power of Non-Observable Actions in Timed Automata. In STACS'96, LNCS 1046, pages 257-268. Springer, 1996. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . On congruences and partial orders. In MFCS'95, LNCS 969, pages 434-443. Springer, 1995. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . A domain for concurrent termination: A generalization of Mazurkiewicz traces. In ICALP'95, LNCS 944, pages 15-26. Springer-Verlag, 1995. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . A Survey of Recognizable Languages of Infinite Traces. In Advances in Petri Nets 1992: The DEMON Project, LNCS 609, pages 392-409. Springer-Verlag, 1992. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . PoSet properties of complex traces. In MFCS'92, LNCS 629, pages 255-263. Springer-Verlag, 1992. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . Asynchronous Cellular Automata for Infinite Traces. In ICALP'92, LNCS 623, pages 583-594. Springer-Verlag, 1992. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . A linear fault-tolerant naming algorithm. In WDAG'90, LNCS 486, pages 57-70. Springer, 1991. ( BibTeX + Abstract ) |
| • | . Recognizable Complex Trace Languages. In MFCS'91, LNCS 520, pages 131-140. Springer-Verlag, 1991. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . A Kleene Theorem for Infinite Trace Languages. In ICALP'91, LNCS 510, pages 254-266. Springer-Verlag, 1991. ( PS | PS.GZ | BibTeX + Abstract ) |
| • | . Recognizable and rational languages of finite and infinite traces. In STACS'91, LNCS 480, pages 89-104. Springer-Verlag, 1991. ( BibTeX + Abstract ) |
Theses | |
| • | . Mémoire d'habilitation à diriger des recherches. Mémoire d'habilitation, Université Paris 6, Paris, France, 1992. ( BibTeX ) |
| • | . Un modèle distribué. Thèse de doctorat, Laboratoire d'Informatique Théorique et Programmation, Paris, France, 1987. ( BibTeX ) |
Other Publications | |
| • | . Pebble weighted automata and transitive closure logics. Research Report LSV-10-06, Laboratoire Spécification et Vérification, ENS Cachan, France, March 2010. 20 pages. ( PDF | BibTeX + Abstract ) |
| • | . Decidability of well-connectedness for distributed synthesis. Research Report LSV-10-02, Laboratoire Spécification et Vérification, ENS Cachan, France, February 2010. 15 pages. ( PDF | BibTeX + Abstract ) |
| • | . Asynchronous cellular automata and logic for pomsets without auto-concurrency. Technical Report 97.24, Laboratoire d'Informatique Algorithmique, Fondements et Applications, Paris, France, 1997. ( PS | PS.GZ | BibTeX + Abstract ) |