Selected publications by Paul Gastin

Books

• L. Albert, P. Gastin, B. Petazzoni, A. Petit, N. Puech and P. Weil.  Cours et exercices d'informatique, Classes préparatoires, premier et second cycles universitaires. Vuibert, 1998. ( BibTeX )

Chapters in Books

• S. Demri and P. Gastin.  Specification and Verification using Temporal Logics.  In Modern applications of automata theory, IISc Research Monographs 2. World Scientific, 2010. To appear. ( PDF | BibTeX + Abstract )
• M. Droste and P. Gastin.  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 )
• V. Diekert and P. Gastin.  Local safety and local liveness for distributed systems.  In Perspectives in Concurrency Theory, IARCS-Universities, pages 86-106. Universities Press, 2009. ( PDF | BibTeX + Abstract )
• P. Gastin, M. Mukund and K. Narayan Kumar.  Reachability and boundedness in time-constrained MSC graphs.  In Perspectives in Concurrency Theory, IARCS-Universities, pages 157-183. Universities Press, 2009. ( PDF | BibTeX + Abstract )
• V. Diekert and P. Gastin.  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 )
• V. Diekert and P. Gastin.  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 )
  doi: 10.1007/3-540-45711-9_2
• P. Gastin and A. Petit.  Infinite traces.  In The Book of Traces, chapter 11, pages 393-486. World Scientific, 1995. ( PS | PS.GZ | BibTeX )
• P. Gastin.  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

• P. Gastin and D. Kuske.  Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces.  Information and Computation 208(7), pages 797-816, 2010. ( PDF | BibTeX + Abstract )
  doi: 10.1016/j.ic.2009.12.003
• P. Gastin, N. Sznajder and M. Zeitoun.  Distributed synthesis for well-connected architectures.  Formal Methods in System Design 34(3), pages 215-237, 2009. ( PDF | BibTeX + Abstract )
  doi: 10.1007/s10703-008-0064-7
• V. Diekert, P. Gastin and M. Kufleitner.  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 )
  doi: 10.1142/S0129054108005802
• M. Droste and P. Gastin.  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 )
  doi: 10.1007/s00224-007-9064-z
• P. Gastin and D. Kuske.  Uniform satisfiability in PSPACE for local temporal logics over Mazurkiewicz traces.  Fundamenta Informaticae 80(1-3), pages 169-197, 2007. ( PDF | BibTeX + Abstract )
• B. Bérard, P. Gastin and A. Petit.  Timed substitutions for regular signal-event languages.  Formal Methods in System Design 31(2), pages 101-134, 2007. ( PDF | BibTeX + Abstract )
  doi: 10.1007/s10703-007-0034-5
• M. Droste and P. Gastin.  Weighted automata and weighted logics.  Theoretical Computer Science 380(1-2), pages 69-86, 2007. ( PDF | PS | PS.GZ | BibTeX + Abstract )
  doi: 10.1016/j.tcs.2007.02.055
• V. Diekert and P. Gastin.  Pure future local temporal logics are expressively complete for Mazurkiewicz traces.  Information and Computation 204(11), pages 1597-1619, 2006. ( PDF | BibTeX + Abstract )
  doi: 10.1016/j.ic.2006.07.002
• V. Diekert and P. Gastin.  From local to global temporal logics over Mazurkiewicz traces.  Theoretical Computer Science 356(1-2), pages 126-135, 2006. ( PDF | BibTeX + Abstract )
  doi: 10.1016/j.tcs.2006.01.035
• V. Diekert and P. Gastin.  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 )
  doi: 10.1016/j.ic.2004.08.001
• P. Gastin and M. W. Mislove.  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 )
  doi: 10.1017/S0960129503003943
• P. Gastin and M. W. Mislove.  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 )
• P. Gastin and D. Teodosiu.  Resource traces: A domain for processes sharing exclusive resources.  Theoretical Computer Science 278(1-2), pages 195-221, 2002. ( PS | PS.GZ | BibTeX + Abstract )
• V. Diekert and P. Gastin.  LTL is expressively complete for Mazurkiewicz traces.  Journal of Computer and System Sciences 64(2), pages 396-418, 2002. ( PS | PS.GZ | BibTeX + Abstract )
• M. Droste, P. Gastin and D. Kuske.  Asynchronous cellular automata for pomsets.  Theoretical Computer Science 247(1-2), pages 1-38, 2000. ( PDF | PS | PS.GZ | BibTeX + Abstract )
• M. Droste and P. Gastin.  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 )
• V. Diekert and P. Gastin.  Approximating traces.  Acta Informatica 35(7), pages 567-593, 1998. ( PS | PS.GZ | BibTeX + Abstract )
• B. Bérard, V. Diekert, P. Gastin and A. Petit.  Characterization of the Expressive Power of Silent Transitions in Timed Automata.  Fundamenta Informaticae 36(2), pages 145-182, 1998. ( PS | PS.GZ | BibTeX + Abstract )
• V. Diekert, P. Gastin and A. Petit.  Rational and Recognizable Complex Trace Languages.  Information and Computation 116(1), pages 134-153, 1995. ( PS | PS.GZ | BibTeX + Abstract )
• P. Gastin, A. Petit and W. Zielonka.  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 )
• P. Gastin and B. Rozoy.  The poset of infinitary traces.  Theoretical Computer Science 120(1), pages 101-121, 1993. ( PS | PS.GZ | BibTeX + Abstract )
• P. Gastin and V. Villain.  An efficient crash-tolerant sequential traversal.  Parallel Processing Letters 3, pages 87-97, 1993. ( BibTeX + Abstract )
• P. Gastin, E. Ochmanski, A. Petit and B. Rozoy.  Decidability of the star problem in A^* × {b}^*.  Information Processing Letters 44(2), pages 65-71, 1992. ( PS | PS.GZ | BibTeX + Abstract )
• P. Gastin.  Un modèle asynchrone pour les systèmes distribués.  Theoretical Computer Science 74(1), pages 121-161, 1990. ( BibTeX + Abstract )

Conferences

• B. Bollig, P. Gastin, B. Monmege and M. Zeitoun.  Pebble weighted automata and transitive closure logics.  In ICALP'10, LNCS 6199, pages 587-598. Springer, 2010. ( PDF | PDF (long version) | BibTeX + Abstract )
  doi: 10.1007/978-3-642-14162-1_49
• B. Bollig and P. Gastin.  Weighted versus Probabilistic Logics.  In DLT'09, LNCS 5583, pages 18-38. Springer, 2009. ( PDF | BibTeX + Abstract )
  doi: 10.1007/978-3-642-02737-6_2
• Th. Chatain, P. Gastin and N. Sznajder.  Natural Specifications Yield Decidability for Distributed Synthesis of Asynchronous Systems.  In SOFSEM'09, LNCS 5404, pages 141-152. Springer, 2009. ( PDF | BibTeX + Abstract )
  doi: 10.1007/978-3-540-95891-8_16
• S. Akshay, B. Bollig, P. Gastin, M. Mukund and K. Narayan Kumar.  Distributed Timed Automata with Independently Evolving Clocks.  In CONCUR'08, LNCS 5201, pages 82-97. Springer, 2008. ( PDF | BibTeX + Abstract )
  doi: 10.1007/978-3-540-85361-9_10
• S. Akshay, B. Bollig and P. Gastin.  Automata and Logics for Timed Message Sequence Charts.  In FSTTCS'07, LNCS 4855, pages 290-302. Springer, 2007. ( PDF | PS | PS.GZ | BibTeX + Abstract )
  doi: 10.1007/978-3-540-77050-3_24
• P. Bhateja, P. Gastin, M. Mukund and K. Narayan Kumar.  Local testing of message sequence charts is difficult.  In FCT'07, LNCS 4639, pages 76-87. Springer, 2007. ( PDF | BibTeX + Abstract )
  doi: 10.1007/978-3-540-74240-1_8
• P. Gastin and P. Moro.  Minimal counter-example generation for SPIN.  In SPIN'07, LNCS 4595, pages 24-38. Springer, 2007. ( PDF | PS | PS.GZ | BibTeX + Abstract )
  doi: 10.1007/978-3-540-73370-6_4
• P. Gastin, N. Sznajder and M. Zeitoun.  Distributed synthesis for well-connected architectures.  In FSTTCS'06, LNCS 4337, pages 321-332. Springer, 2006. ( PDF | BibTeX + Abstract )
  doi: 10.1007/11944836_30
• P. Bhateja, P. Gastin and M. Mukund.  A fresh look at testing for asynchronous communication.  In ATVA'06, LNCS 4218, pages 369-383. Springer, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract )
  doi: 10.1007/11901914_28
• B. Bérard, P. Gastin and A. Petit.  Refinements and abstractions of signal-event (timed) languages.  In FORMATS'06, LNCS 4202, pages 67-81. Springer, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract )
  doi: 10.1007/11867340_6
• B. Bérard, P. Gastin and A. Petit.  Intersection of regular signal-event (timed) languages.  In FORMATS'06, LNCS 4202, pages 52-66. Springer, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract )
  doi: 10.1007/11867340_5
• P. Gastin and D. Kuske.  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 )
  doi: 10.1007/11539452_40
• M. Droste and P. Gastin.  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 )
  doi: 10.1007/11523468_42
• P. Gastin, B. Lerman and M. Zeitoun.  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 )
• V. Diekert and P. Gastin.  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 )
• P. Gastin, B. Lerman and M. Zeitoun.  Distributed games and distributed control for asynchronous systems.  In LATIN'04, LNCS 2976, pages 455-465. Springer, 2004. ( PDF | PS | PS.GZ | BibTeX + Abstract )
• P. Gastin, P. Moro and M. Zeitoun.  Minimization of counterexamples in SPIN.  In SPIN'04, LNCS 2989, pages 92-108. Springer, 2004. ( PDF | PS | PS.GZ | BibTeX + Abstract )
• P. Gastin and D. Kuske.  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 )
• P. Gastin, M. Mukund and K. Narayan Kumar.  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 )
• P. Gastin and D. Oddoux.  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 )
• P. Gastin and M. Mukund.  An Elementary Expressively Complete Temporal Logic for Mazurkiewicz Traces.  In ICALP'02, LNCS 2380, pages 938-949. Springer, 2002. ( PS | PS.GZ | BibTeX + Abstract )
• V. Diekert and P. Gastin.  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 )
• P. Gastin and D. Oddoux.  Fast LTL to Büchi Automata Translation.  In CAV'01, LNCS 2102, pages 53-65. Springer, 2001. ( PS | PS.GZ | BibTeX + Abstract )
• F. Derepas and P. Gastin.  Model Checking Systems of Replicated Processes with SPIN.  In SPIN'01, LNCS 2057, pages 235-251. Springer, 2001. ( PS | PS.GZ | BibTeX + Abstract )
• F. Derepas, P. Gastin and D. Plainfossé.  Avoiding state explosion for distributed systems with timestamps.  In FME'01, LNCS 2021, pages 119-134. Springer, 2001. ( PS | PS.GZ | BibTeX + Abstract )
• V. Diekert and P. Gastin.  LTL is expressively complete for Mazurkiewicz traces.  In ICALP 2000, LNCS 1853, pages 211-222. Springer, 2000. ( PS | PS.GZ | BibTeX + Abstract )
• M. Droste and P. Gastin.  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 )
• V. Diekert and P. Gastin.  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 )
• P. Gastin and M. W. Mislove.  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 )
• P. Gastin, R. Meyer and A. Petit.  A (non-elementary) modular decision procedure for LTrL.  In MFCS'98, LNCS 1450, pages 356-365. Springer, 1998. ( PS | PS.GZ | BibTeX + Abstract )
• M. Droste and P. Gastin.  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 )
• V. Diekert, P. Gastin and A. Petit.  Removing ε-Transitions in Timed Automata.  In STACS'97, LNCS 1200, pages 583-594. Springer, 1997. ( PS | PS.GZ | BibTeX + Abstract )
• V. Diekert, P. Gastin and A. Petit.  Recent Developments in Trace Theory.  In DLT'95, pages 373-385. World Scientific, 1996. ( PS | PS.GZ | BibTeX + Abstract )
• M. Droste and P. Gastin.  Asynchronous cellular automata for Pomsets without auto-concurrency.  In CONCUR'96, LNCS 1119, pages 627-638. Springer, 1996. ( PS | PS.GZ | BibTeX + Abstract )
• B. Bérard, P. Gastin and A. Petit.  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 )
• S. Bauget and P. Gastin.  On congruences and partial orders.  In MFCS'95, LNCS 969, pages 434-443. Springer, 1995. ( PS | PS.GZ | BibTeX + Abstract )
• V. Diekert and P. Gastin.  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 )
• P. Gastin and A. Petit.  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 )
• P. Gastin and A. Petit.  PoSet properties of complex traces.  In MFCS'92, LNCS 629, pages 255-263. Springer-Verlag, 1992. ( PS | PS.GZ | BibTeX + Abstract )
• P. Gastin and A. Petit.  Asynchronous Cellular Automata for Infinite Traces.  In ICALP'92, LNCS 623, pages 583-594. Springer-Verlag, 1992. ( PS | PS.GZ | BibTeX + Abstract )
• J. Beauquier, P. Gastin and V. Villain.  A linear fault-tolerant naming algorithm.  In WDAG'90, LNCS 486, pages 57-70. Springer, 1991. ( BibTeX + Abstract )
  doi: 10.1007/3-540-54099-7_5
• V. Diekert, P. Gastin and A. Petit.  Recognizable Complex Trace Languages.  In MFCS'91, LNCS 520, pages 131-140. Springer-Verlag, 1991. ( PS | PS.GZ | BibTeX + Abstract )
• P. Gastin, A. Petit and W. Zielonka.  A Kleene Theorem for Infinite Trace Languages.  In ICALP'91, LNCS 510, pages 254-266. Springer-Verlag, 1991. ( PS | PS.GZ | BibTeX + Abstract )
• P. Gastin.  Recognizable and rational languages of finite and infinite traces.  In STACS'91, LNCS 480, pages 89-104. Springer-Verlag, 1991. ( BibTeX + Abstract )

Theses

• P. Gastin.  Mémoire d'habilitation à diriger des recherches.  Mémoire d'habilitation, Université Paris 6, Paris, France, 1992. ( BibTeX )
• P. Gastin.  Un modèle distribué.  Thèse de doctorat, Laboratoire d'Informatique Théorique et Programmation, Paris, France, 1987. ( BibTeX )

Other Publications

• P. Gastin and N. Sznajder.  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 )
• M. Droste and P. Gastin.  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 )

About LSV

• News
• People
• Research
• Seminars
• Teaching
• Contact

• École Normale Supérieure de Cachan
• Centre National de la Recherche Scientifique