@phdthesis{Gas87,
  author = {Gastin, Paul},
  title = {Un mod{\`e}le distribu{\'e}},
  school = {Laboratoire d'Informatique Th{\'e}orique et 
		Programmation, Paris, France},
  type = {Th{\`e}se de doctorat},
  year = 1987
}
@article{Gas90tcs,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Gastin, Paul},
  title = {Un mod{\`e}le asynchrone pour les syst{\`e}mes distribu{\'e}s},
  volume = 74,
  number = 1,
  year = 1990,
  pages = {121-161},
  abstract = { Many researches are engaged in the field of distributed systems
                  modelization. We present a new model inspired by the
                  language theory. Its particularity within this theory is the
                  rejection of interleaving for the representation of
                  concurrency. Here, the main ideas are born from languages as
                  CSP or~ESTELLE. The point is mainly the real lack of
                  dependency between processes apart from synchronisations,
                  which are rendez-vous. Once the model defined, we introduce,
                  as in the infinitary free monoid, notions such as length,
                  concatenation, prefix order, upper bound and infinite
                  product. So the distributed model is provided with all
                  operations one needs to develop semantics. Then, we prove
                  that the finitary part of the distributed model is
                  isomorphic to the free partially commutative monoid~(fpcm).
                  Finally, we settle the bases of an infinitary extension of
                  the fpcm.}
}
@inproceedings{BGV90,
  address = {Bari, Italy},
  year = 1991,
  volume = 486,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {van Leeuwen, Jan and Santoro, Nicola},
  acronym = {{WDAG}'90},
  booktitle = {{P}roceedings of the 4th {I}nternational {W}orkshop
               on {D}istributed {A}lgorithms ({WDAG}'90)},
  author = {Beauquier, Joffroy and Gastin, Paul and Villain, Vincent},
  title = {A linear fault-tolerant naming algorithm},
  pages = {57-70},
  doi = {10.1007/3-540-54099-7_5},
  abstract = {We solve the naming problem (how to give a unique identifier to
                  each site of an unknown network), when some sites are
                  supposed to have a faulty behaviour of fail-stop type. The
                  solution uses several tokens, in order to ensure that,
                  despite crash failure of some sites, at least one token will
                  perform a complete traversal of the network. The
                  complexities in time and in number of messages of this
                  algorithm are linear with respect to the size of the network
                  (number of communication lines), which improves the
                  exponential solution already known in the Byzantine case
                  with some special assumptions.}
}
@inproceedings{Gas90epit,
  address = {La Roche Posay, France},
  month = apr,
  year = 1990,
  volume = 469,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Guessarian, Ir{\`e}ne},
  booktitle = {Semantics of Systems of Concurrent Processes~--- 
          {P}roceedings of the {LITP} {S}pring {S}chool on 
          {T}heoretical {C}omputer {S}cience},
  author = {Gastin, Paul},
  title = {Infinite Traces},
  pages = {277-308},
  abstract = {Trace languages are used in computer science to provide a
                  description of the behaviours of concurrent systems. If we
                  are interested in systems which never stop then we have to
                  consider languages of infinite traces. In this paper, we
                  generalize to infinite traces three well known points of
                  view about finite traces: equivalence class of words,
                  projections on the dependence cliques and dependence graphs.
                  These approaches are complementary and, depending on the
                  problem we deal with, each of them can prove to be more
                  appropriate than the others. In this way, we obtain an
                  infinitary trace monoid and extend Levi's lemma and the
                  Foata normal form. Next, we prove that the infinitary trace
                  monoid is a completely coherent PoSet. We also define an
                  ultrametric distance and prove that it is a complete metric
                  space. Therefore, either the PoSet or the topological
                  framework can be used to solve fix-point equations and then
                  to provide semantics of recursive constructs. Finally, we
                  introduce recognizable languages of finite and infinite
                  traces. We prove that they are characterized by a syntactic
                  congruence and that the family of recognizable languages is
                  closed by concatenation and by the Boolean operations:
                  union, intersection and complement.}
}
@inproceedings{PG-AP-WZ-icalp91,
  address = {Madrid, Spain},
  month = jul,
  year = 1991,
  volume = 510,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  editor = {Leach Albert, Javier and Monien, Burkhard and
            Rodriguez-Artalejo, Mario},
  acronym = {{ICALP}'91},
  booktitle = {{P}roceedings of the 18th {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming
               ({ICALP}'91)},
  author = {Gastin, Paul and Petit, Antoine and 
                  Zielonka, Wieslaw},
  title = {A {K}leene Theorem for Infinite Trace Languages},
  pages = {254-266},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/TCS94gpz.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/TCS94gpz.ps},
  abstract = {Kleene's theorem is considered as one of the cornerstones of
                  theoretical computer science. It ensures that, for languages
                  of finite words, the family of recognizable languages is
                  equal to the family of rational languages. It has been
                  generalized in various ways, for instance, to formal power
                  series by Sch{\"u}tzenberger, to infinite words by B{\"u}chi and to
                  finite traces by Ochma{\'n}ski. Finite traces have been
                  introduced by Mazurkiewicz in order to modelize the
                  behaviours of distributed systems. The family of
                  recognizable trace languages is not closed by Kleene's star
                  but by a concurrent version of this iteration. This leads to
                  the natural definition of co-rational languages obtained as
                  the rational one by simply replacing the Kleene's iteration
                  by the concurrent iteration. Cori, Perrin and M{\'e}tivier
                  proved, in substance, that any co-rational trace language is
                  recognizable. Independently, Ochma{\'n}ski generalized Kleene's
                  theorem showing that the recognizable trace languages are
                  exactly the co-rational languages. Besides, infinite traces
                  have been recently introduced as a natural extension of both
                  finite traces and infinite words. In this paper we
                  generalize Kleene's theorem to languages of infinite traces
                  proving that the recognizable languages of finite or
                  infinite traces are exactly the co-rational languages.}
}
@inproceedings{VD-PG-AP-mfcs91,
  address = {Kazimierz Dolny, Poland},
  month = sep,
  year = 1991,
  volume = 520,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  editor = {Tarlecki, Andrzej},
  acronym = {{MFCS}'91},
  booktitle = {{P}roceedings of the 16th
               {I}nternational {S}ymposium on
               {M}athematical {F}oundations of 
               {C}omputer {S}cience
               ({MFCS}'91)},
  author = {Diekert, Volker and Gastin, Paul and 
                  Petit, Antoine},
  title = {Recognizable Complex Trace Languages},
  pages = {131-140},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/IC95dgp.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/IC95dgp.ps},
  abstract = {A.~Mazurkiewicz defined traces in order to modelize
                  non-sequential processes. Complex traces have been recently
                  introduced as a generalization of both traces and infinite
                  words. This paper studies the family of recognizable complex
                  trace languages. It is proved that this family is closed
                  under boolean operations, concatenation, left and right
                  quotients. Then sufficient conditions ensuring the
                  recognizability of the finite and infinite iterations of a
                  recognizable complex trace language are given. The notion of
                  co-iteration is defined and the Kleene-Ochma{\'n}ski theorem is
                  generalized to complex traces.}
}
@inproceedings{Gas91,
  address = {Hamburg, Germany},
  month = feb,
  year = 1991,
  volume = 480,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  editor = {Choffrut, {\relax Ch}ristian and Jantzen, Matthias},
  acronym = {{STACS}'91},
  booktitle = {{P}roceedings of the 8th {A}nnual
               {S}ymposium on {T}heoretical {A}spects of
               {C}omputer {S}cience
               ({STACS}'91)},
  author = {Gastin, Paul},
  title = {Recognizable and rational languages of finite and
		      infinite traces},
  pages = {89-104},
  abstract = {Trace languages are used in computer science to provide a
                  description of the behaviours of concurrent systems. If we
                  are interested in systems which never stop then we have to
                  consider languages of infinite traces. In this paper, we
                  introduce and study recognizable and rational languages of
                  finite and infinite traces. We characterize recognizable
                  languages by means of a syntactic congruence. We prove that
                  the family of recognizable languages is strictly included in
                  the family of rational languages. Next, we study the closure
                  properties of the family of recognizable languages. We prove
                  that this family is closed under the Boolean operations and
                  under concatenation. Contrary to the (finite) iteration, the
                  infinite iteration of a finite trace is proved to be
                  recognizable. We conclude this paper with some open
                  problems.}
}
@inproceedings{PG-AP-APN-92,
  year = 1992,
  volume = 609,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  editor = {Rozenberg, Grzegorz},
  booktitle = {{A}dvances in {P}etri {N}ets 1992: 
               {T}he {DEMON} {P}roject},
  author = {Gastin, Paul and Petit, Antoine},
  title = {A Survey of Recognizable Languages of Infinite
                 Traces},
  pages = {392-409},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/APN92gp.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/APN92gp.ps},
  abstract = {A.~Mazurkiewicz defined traces in order to represent
                  non-sequential processes. In order to describe
                  non-sequential processes which never terminate, \emph{e.g.}
                  distributed operating systems, the notion of infinite traces
                  is needed. The aim of this survey is to present in a uniform
                  way the known results on recognizable infinite trace
                  languages. The proofs of the presented results are not
                  proposed here but can be found in the original papers.}
}
@inproceedings{PG-AP-icalp92,
  address = {Vienna, Austria},
  month = jul,
  year = 1992,
  volume = 623,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  editor = {Kuich, Werner},
  acronym = {{ICALP}'92},
  booktitle = {{P}roceedings of the 19th {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming
               ({ICALP}'92)},
  author = {Gastin, Paul and Petit, Antoine},
  title = {Asynchronous Cellular Automata for Infinite 
                 Traces},
  pages = {583-594},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Icalp92gp.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Icalp92gp.ps},
  abstract = {A.~Mazurkiewicz introduced the monoid of traces to provide a
                  very natural semantics for concurrent processes. In a
                  general monoid, the behaviours of finite state systems are
                  described by recognizable languages, which form hence a
                  basic family. For finite traces and finite or infinite
                  words, there exist several equivalent characterizations of
                  this family as for instance, saturating morphisms or
                  (co-)rational expressions. For infinite traces, this family
                  has been introduced by means of saturating morphisms and
                  characterized by co-rational expressions but it suffers from
                  lack of finite state system characterizations. In this
                  paper, we remedy this deficiency providing a
                  characterization of the family of recognizable infinite
                  trace languages by means of asynchronous (cellular) automata
                  (which carry the most intuitive idea of finite state
                  concurrent machines). To this purpose, we give effective
                  constructions for co-rational operations on these automata
                  which are of independent interest.}
}
@inproceedings{PG-AP-mfcs92,
  address = {Prague, Czechoslovakia},
  month = aug,
  year = 1992,
  volume = 629,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  editor = {Havel, Ivan M. and Koubek, V{\'a}clav},
  acronym = {{MFCS}'92},
  booktitle = {{P}roceedings of the 17th
               {I}nternational {S}ymposium on
               {M}athematical {F}oundations of 
               {C}omputer {S}cience
               ({MFCS}'92)},
  author = {Gastin, Paul and Petit, Antoine},
  title = {{P}o{S}et properties of complex traces},
  pages = {255-263},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Mfcs92gp.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Mfcs92gp.ps},
  abstract = {This paper investigates PoSet properties of the monoid~\(\mathbb{G}\) of
                  infinite dependence graphs and of the monoid~\(\mathbb{C}\) of complex
                  traces. We show that a subset of~\(\mathbb{G}\) admits a least upper
                  bound if and only if this set is coherent and countable.
                  Hence, \(\mathbb{G}\)~is bounded complete. The compact and the prime
                  dependence graphs are characterized and we prove that each
                  dependence graph is the least upper bound of its compact
                  (resp. its prime) lower bounds. Therefore, up to the
                  restriction to countable sets, \(\mathbb{G}\)~is a coherently complete
                  Scott-Domain and is Prime Algebraic. We define very
                  naturally two orders on~\(\mathbb{C}\) : the product order and the prefix
                  order. We show that \(\mathbb{C}\) with each order is a coherently
                  complete CPO and we characterize the least upper bound (the
                  greatest lower bound resp.) of a subset of~\(\mathbb{C}\) when it exists.
                  But contrary to the case of~\(\mathbb{G}\), we prove that 
                  \(\mathbb{C}\)~is not a 
                  Scott-Domain in general.}
}
@phdthesis{Gas92,
  author = {Gastin, Paul},
  title = {M{\'e}moire d'habilitation {\`a} diriger des 
		  recherches},
  howpublished = {Technical Report LITP-92.97},
  year = {1992},
  type = {M{\'e}moire d'habilitation},
  school = {Universit{\'e} Paris~6, Paris, France}
}
@article{GOPR92,
  publisher = {Elsevier Science Publishers},
  journal = {Information Processing Letters},
  author = {Gastin, Paul and Ochma{\'n}ski, Edward and Petit, Antoine and Rozoy, Brigitte},
  title = {Decidability of the star problem 
                in {{\(A^*\)}}{\(\times\{b\}^*\)}},
  volume = 44,
  number = {2},
  year = 1992,
  month = nov,
  pages = {65-71},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/IPL92gopr.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/IPL92gopr.ps},
  abstract = {We adress in this paper the decidability of the Star Problem in
                  trace monoids: Let~{\(L\)} be a recognizable trace language, 
                  is~{\(L^*\)}
                  recognizable? We prove that this problem is decidable when
                  the trace monoid is a direct product of free monoids 
                  {\(A^*\times
                  \{b\}^*\)}. This result shows, for the first time and contrary to
                  a possible intuition, that the Star Problem is of distinct
                  nature than the Recognizability Problem: Let~{\(L\)} be a rational
                  trace language, is~{\(L\)} recognizable?}
}
@article{GV93,
  publisher = {World Scientific},
  journal = {Parallel Processing Letters},
  author = {Gastin, Paul and Villain, Vincent},
  title = {An efficient crash-tolerant sequential traversal},
  volume = 3,
  year = 1993,
  pages = {87-97},
  abstract = {Fault-tolerance is an increasingly
                  important requirement for most
                  of the todays distributed
                  systems. However, the cost and
                  complexity of the design of such
                  systems are considerably higher
                  than those of non fault-tolerant
                  ones.\par
                  An interesting approach to simplify the
                  design of 
                  fault-tolerant systems appears in~[TN88] :
                  some methods are developed, that
                  automatically convert benign failures
                  tolerant systems into systems overcoming
                  more severe failures. With these methods,
                  one can first solve the simpler problem of
                  designing a program which only tolerates
                  benign failures, and then convert it
                  automatically into one with a higher
                  degree of fault-tolerance. Therefore, the
                  design of benign failures tolerant systems
                  is a basic concern in this framework.  \par
                  The aim of this paper is to make easier,
                  by means of a modular methodology, the
                  conception of algorithms overcoming the
                  most benign type of failures :
                  crash-failures.}
}
@article{GR93,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Gastin, Paul and Rozoy, Brigitte},
  title = {The poset of infinitary traces},
  volume = 120,
  number = 1,
  year = 1993,
  pages = {101-121},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/TCS93-gr.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/TCS93-gr.ps},
  abstract = {\emph{Partially Commutative Monoids}, also called
                  \emph{Trace Monoids}, are among the most studied
                  formalisms which describe the behaviour of
                  distributed systems. In order to modelize
                  systems which never stop, we have to
                  consider an extension of traces, namely
                  \emph{Infinite traces}. Finite trace monoids are
                  strongly related to \emph{Partial Order Sets
                  (PoSets), Domains and Event Structures},
                  which are other models to describe the
                  behaviour of distributed systems. The aim
                  of this paper is to establish similar
                  connexions between infinite trace monoids,
                  PoSets and event structures. We prove that
                  the set of finite and infinite traces with
                  the prefix order is a \emph{Scott-domain} and a
                  \emph{coherently complete prime algebraic PoSet}.
                  Moreover, we establish a representation
                  theorem between the class of finite and
                  infinite trace PoSets and a subclass of
                  labelled prime event structures.}
}
@article{PG-AP-WZ-TCS-94,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Gastin, Paul and Petit, Antoine and 
                  Zielonka, Wieslaw},
  title = {An Extension of {K}leene's and {O}chma{\'n}ski's
                 Theorems to Infinite Traces},
  volume = {125},
  number = {2},
  pages = {167-204},
  year = {1994},
  month = mar,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/TCS94gpz.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/TCS94gpz.ps},
  abstract = {As was noted by 
	Mazurkiewicz, traces constitute a 
	convenient tool for describing finite 
	behaviour of concurrent systems. 
	Extending in a natural way 
	Mazurkiewicz's original definition, 
	infinite traces have been recently 
	introduced enabling to deal with 
	infinite behaviour of non-terminating 
	concurrent systems. In this paper we 
	examine the basic families of 
	recognizable sets and of rational sets 
	of infinite traces. The seminal Kleene 
	characterization of recognizable 
	subsets of the free monoid and its 
	subsequent extensions to infinite words 
	due to B{\"u}chi and to finite traces due 
	to Ochma{\'n}ski are the cornestones of the 
	corresponding theories. The main result 
	of our paper is an extension of these 
	characterizations to the domain of 
	infinite traces. Using recognizing and 
	weakly recognizing morphisms, as well 
	as a generalization of the 
	Sch{\"u}tzenberger product of monoids, we 
	prove various closure properties of 
	recognizable trace languages. Moreover, 
	we establish normal form 
	representations for recognizable and 
	rational sets of infinite traces.}
}
@incollection{PG-AP-TB-95,
  author = {Gastin, Paul and Petit, Antoine},
  title = {Infinite traces},
  editor = {Diekert, Volker and Rozenberg, Grzegorz},
  booktitle = {The Book of Traces},
  chapter = {11},
  type = {chapter},
  pages = {393-486},
  year = {1995},
  publisher = {World Scientific},
  nopsgz = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PSGZ/InfiniteTraces.ps.gz},
  nops = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/InfiniteTraces.ps}
}
@article{VD-PG-AP-IC-95,
  publisher = {Elsevier Science Publishers},
  journal = {Information and Computation},
  author = {Diekert, Volker and Gastin, Paul and 
                  Petit, Antoine},
  title = {Rational and Recognizable Complex Trace Languages},
  volume = {116},
  number = {1},
  pages = {134-153},
  year = {1995},
  month = jan,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/IC95dgp.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/IC95dgp.ps},
  abstract = {Mazurkiewicz defined traces 
	as an algebraic model of finite concurrent 
	processes. In order to modelize 
	non-terminating processes a good notion of 
	infinite trace was needed, which finally 
	led to the notion of complex trace. For 
	complex traces an associative 
	concatenation and omega-iteration are 
	defined. This paper defines and 
	investigates rational and recognizable 
	complex trace languages. We prove various 
	closure results such as the closure under 
	boolean operations (for recognizable 
	languages), concatenation, and left and 
	right quotients by recognizable sets. Then 
	we study sufficient conditions ensuring 
	the recognizability of the finite and 
	infinite iterations of complex trace 
	languages. We introduce a generalization 
	of the notion of concurrent iteration 
	which leads to the main result of the 
	paper: the generalization of Kleene's and 
	Ochma{\'n}ski's theorems to complex trace 
	languages.}
}
@article{GR95,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Gastin, Paul and Rutten, Jan},
  editor = {Gastin, Paul and Rutten, Jan},
  title = {Selected papers of the workshop on \emph{Topology and 
	   Completion in 
	   Semantics}, Chartes, France, November 1993},
  year = 1995,
  volume = 151,
  number = 1,
  month = nov
}
@inproceedings{BG95,
  address = {Prague, Czech Republic},
  month = aug,
  year = 1995,
  volume = 969,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Wiedermann, Jir{\'i} and H{\'a}jek, Petr},
  acronym = {{MFCS}'95},
  booktitle = {{P}roceedings of the 20th
               {I}nternational {S}ymposium on
               {M}athematical {F}oundations of 
               {C}omputer {S}cience
               ({MFCS}'95)},
  author = {Bauget, Serge and Gastin, Paul},
  title = {On congruences and partial orders},
  pages = {434-443},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Mfcs95bg.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Mfcs95bg.ps},
  abstract = {Mazurkiewicz trace theory is not powerful enough to describe
                  concurrency paradigms as, for instance, the {"}Producer\slash
                  Consumer{"}. We propose in this paper a generalization of
                  Mazurkiewicz trace monoids which allows to model such
                  problems. We consider quotients of the free monoids by
                  congruences which preserve the commutative images of words.
                  An equivalence class in the quotient monoid consists of all
                  the sequential observations of a distributed computation. In
                  order to characterize congruences which do model
                  concurrency, we study the relationship of this approach and
                  the classical representation of distributed computations
                  with partial orders. We show that the only congruences for
                  which the classes can be represented by partial orders and
                  for which the concatenation transfers modularly to partial
                  orders are congruences generated by commutations, that is
                  trace congruences. We prove necessary conditions and
                  sufficient conditions on congruences so that their classes
                  can be represented by partial orders. In particular, an
                  important sufficient condition covers both trace congruences
                  and the {"}Producer\slash Consumer{"} congruence.}
}
@inproceedings{DG95,
  address = {Szeged, Hungary},
  month = jul,
  year = 1995,
  volume = 944,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  editor = {F{\"u}l{\"o}p, Zolt{\'a}n and G{\'e}cseg, Ferenc},
  acronym = {{ICALP}'95},
  booktitle = {{P}roceedings of the 22th {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming
               ({ICALP}'95)},
  author = {Diekert, Volker and Gastin, Paul},
  title = {A domain for concurrent termination:
              A generalization of {M}azurkiewicz traces},
  pages = {15-26},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Icalp95dg.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Icalp95dg.ps},
  abstract = {This paper generalizes the concept of Mazurkiewicz traces to a
                  fuzzy description of a concurrent process, where a known
                  prefix is given in a first component and a second alphabetic
                  component yields necessary information about future actions.
                  This allows to define a good semantic domain where the
                  concatenation is continuous with respect to the Scott- and
                  to the Lawson topology. For this, we define the notion of
                  alpha-trace and of delta-trace. We show various mathematical
                  results proving thereby the soundness of our approach. Our
                  theory is a proper generalization of the theory of finite
                  and infinite words (with explicit termination) and of the
                  theory of finite and infinite (real and complex) traces. We
                  make use of trace theory, domain theory, and topology.}
}
@inproceedings{BB-PG-AP-stacs96,
  address = {Grenoble, France},
  month = feb,
  year = 1996,
  volume = 1046,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Puech, Claude and Reischuk, R{\"u}diger},
  acronym = {{STACS}'96},
  booktitle = {{P}roceedings of the 13th {A}nnual
               {S}ymposium on {T}heoretical {A}spects of
               {C}omputer {S}cience
               ({STACS}'96)},
  author = {B{\'e}rard, B{\'e}atrice and Gastin, Paul and 
                  Petit, Antoine},
  title = {On the Power of Non-Observable Actions in Timed
                 Automata},
  pages = {257-268},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BGP-stacs96.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BGP-stacs96.ps},
  abstract = {Timed finite automata, introduced by Alur and Dill, are one of
                  the most widely studied models for real-time systems. We
                  focus in this paper on the power of silent transitions, \emph{i.e.}
                  \(\epsilon\)-transitions, in such automata. We show that
                  \(\epsilon\)-transitions strictly increase the power of timed
                  automata and that the class of timed languages recognized by
                  automata with \(\epsilon\)-transitions is much more robust than
                  the corresponding class without \(\epsilon\)-transition. Our main
                  result shows that \(\epsilon\)-transitions increase the power of
                  these automata only if they reset clocks.}
}
@inproceedings{VD-PG-AP-dlt96,
  address = {Magdeburg, Germany},
  year = 1996,
  publisher = {World Scientific},
  editor = {Dassow, J{\"u}rgen and Rozenberg, Grzegorz and
            Salomaa, Arto},
  acronym = {{DLT}'95},
  booktitle = {{P}roceedings of the 2nd {I}nternational
               {C}onference on {D}evelopments in {L}anguage {T}heory
               ({DLT}'95)},
  author = {Diekert, Volker and Gastin, Paul and 
                  Petit, Antoine},
  title = {Recent Developments in Trace Theory},
  pages = {373-385},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DGP-dlt95.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DGP-dlt95.ps},
  abstract = {In this paper we give a survey on some active research in the
                  theory of Mazurkiewicz traces. We restrict our attention to
                  some few topics: recognizable languages, asynchronous
                  automata including infinite traces, trace codings, and trace
                  rewriting.}
}
@inproceedings{DrGa96,
  address = {Pisa, Italy},
  month = aug,
  year = 1996,
  volume = 1119,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Montanari, Ugo and Sassone, Vladimiro},
  acronym = {{CONCUR}'96},
  booktitle = {{P}roceedings of the 7th 
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'96)},
  author = {Droste, Manfred and Gastin, Paul},
  title = {Asynchronous cellular automata for Pomsets without
                  auto-concurrency},
  pages = {627-638},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Concur96dg.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Concur96dg.ps},
  abstract = {This paper extends to pomsets without auto-concurrency the
                  fundamental notion of asynchronous cellular automata (ACA)
                  which was originally introduced for traces by~Zielonka. We
                  generalize to pomsets the notion of asynchronous mapping
                  introduced by~Zielonka and we show how to construct a
                  deterministic ACA from an asynchronous mapping. Our main
                  result generalizes B{\"u}chi's theorem for a class of pomsets
                  without auto-concurrency which satisfy a natural axiom. This
                  axiom ensures that an asynchronous cellular automaton works
                  on the pomset as a concurrent read owner write machine. More
                  precisely, we prove the equivalence between
                  non-deterministic~ACA, deterministic~ACA and monadic second 
                  order logic for this class of pomsets.}
}
@inproceedings{VD-PG-AP-stacs97,
  address = {L{\"u}beck, Germany},
  month = feb,
  year = 1997,
  volume = 1200,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Reischuk, R{\"u}diger and Morvan, Michel},
  acronym = {{STACS}'97},
  booktitle = {{P}roceedings of the 14th {A}nnual
               {S}ymposium on {T}heoretical {A}spects of
               {C}omputer {S}cience
               ({STACS}'97)},
  author = {Diekert, Volker and Gastin, Paul and Petit, Antoine},
  title = {Removing {{\(\epsilon\)}}-Transitions in Timed Automata},
  pages = {583-594},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DGP-stacs97.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DGP-stacs97.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DGP-stacs97.pdf},
  abstract = {Timed automata are among the most widely studied models for
                  real-time systems. Silent transitions, \emph{i.e.},
                  \(\epsilon\)-transitions, have already been proposed in the
                  original paper on timed automata by Alur and Dill. B{\'e}rard,
                  Gastin and Petit have shown that \(\epsilon\)-transitions
                  can be removed, if they do not reset clocks; moreover
                  \(\epsilon\)-transitions strictly increase the power of timed
                  automata, if there is a self-loop containing
                  \(\epsilon\)-transitions which reset some clocks. This paper left
                  open the problem about the power of the \(\epsilon\)-transitions
                  which reset clocks, if they do not lie on any cycle.\par
                  The present paper settles this open question. Precisely, we
                  prove that a timed automaton such that no \(\epsilon\)-transition
                  with nonempty reset set lies on any directed cycle can be
                  effectively transformed into a timed automaton without
                  \(\epsilon\)-transitions. Interestingly, this main result holds
                  under the assumption of non-Zenoness and it is false
                  otherwise.\par 
                  Besides, we develop a promising new technique based on a
                  notion of precise 
                  time which allows to show that some timed languages are not
                  recognizable by any \(\epsilon\)-free timed automaton.}
}
@inproceedings{DrGa97,
  address = {Bologna, Italy},
  month = jul,
  year = 1997,
  volume = 1256,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Degano, Pierpaolo and Gorrieri, Roberto and Marchetti-Spaccamela, Alberto},
  acronym = {{ICALP}'97},
  booktitle = {{P}roceedings of the 24th {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming
               ({ICALP}'97)},
  author = {Droste, Manfred and Gastin, Paul},
  title = {On recognizable and rational formal power series
              in partially commuting variables},
  pages = {682-692},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/Icalp97dg.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Icalp97dg.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Icalp97dg.pdf},
  abstract = {Kleene's theorem on the coincidence of regular and rational
                  languages in free monoids has been generalized by
                  Sch{\"u}tzenberger to a description of the recognizable formal
                  power series in non-commuting variables over arbitrary
                  semi-rings, and by Ochma\'nski to a characterization of the
                  recognizable languages in trace monoids. Here we will
                  describe the recognizable formal power series over arbitrary
                  semi-rings and in partially commuting variables, \emph{i.e.} over
                  trace monoids. We prove that the recognizable series are
                  certain rational power series, which can be constructed from
                  the polynomials by using the operations sum, product and a
                  restricted star which is applied only to series for which
                  the elements in the support all have the same connected
                  alphabet. The converse is true if the underlying semi-ring
                  is commutative. It is shown that these assumptions are
                  necessary. This provides a joint generalization of both
                  Sch{\"u}tzenberger's and Ochma\'nski's theorems. }
}
@techreport{DG97j,
  author = {Droste, Manfred and Gastin, Paul},
  title = {Asynchronous cellular automata and 
            logic for pomsets without auto-concurrency},
  institution = {Laboratoire d'Informatique Algorithmique, Fondements et
                 Applications, Paris, France},
  type = {Technical Report},
  number = {97.24},
  year = 1997,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/ACAj97dg.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ACAj97dg.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACAj97dg.pdf},
  abstract = {This paper extends to pomsets without auto-concurrency the
                  fundamental notion of asynchronous cellular automata~(ACA)
                  which was originally introduced for traces by Zielonka. We
                  generalize to pomsets the notion of asynchronous mapping
                  introduced by Zielonka and we show how to construct a
                  deterministic ACA from an asynchronous mapping. Our main
                  result generalizes B{\"u}chi's theorem for finite words to a
                  class of pomsets without auto-concurrency which satisfy a
                  natural axiom. This axiom ensures that an asynchronous
                  cellular automaton works on the pomset as a concurrent read
                  and exclusive owner write machine. More precisely, we prove
                  the equivalence between non deterministic ACA, deterministic
                  ACA and monadic second order logic for this class of
                  pomsets.}
}
@article{BB-VD-PG-AP-98,
  publisher = {{IOS} Press},
  journal = {Fundamenta Informaticae},
  author = {B{\'e}rard, B{\'e}atrice and Diekert, Volker and 
                 Gastin, Paul and Petit, Antoine},
  title = {Characterization of the Expressive Power of Silent
                 Transitions in Timed Automata},
  volume = {36},
  number = {2},
  pages = {145-182},
  year = {1998},
  month = nov,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BDGP-FUNDI98.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BDGP-FUNDI98.ps},
  abstract = {Timed automata are among the 
	most widely studied models for real-time 
	systems. Silent transitions (or 
	\(\epsilon\)-transitions) have already been 
	proposed in the original paper on timed 
	automata by Alur and~Dill. We show that the 
	class of timed languages recognized by 
	automata with \(\epsilon\)-transitions, is more 
	robust and more expressive than the 
	corresponding class without 
	\(\epsilon\)-transitions. \par
	We then focus on \(\epsilon\)-transitions which do 
	not reset clocks. We propose an algorithm to 
	construct, given a timed automaton, an 
	equivalent one without such transitions. This 
	algorithm is in two steps, it first suppresses 
	the cycles of \(\epsilon\)-transitions without 
	reset and then the remaining ones.\par
	Then, we prove that a timed automaton such 
	that no \(\epsilon\)-transition which resets clocks 
	lies on any directed cycle, can be effectively 
	transformed into a timed automaton without 
	\(\epsilon\)-transitions. Interestingly, this main 
	result holds under the assumption of 
	non-Zenoness and it is false otherwise.\par
	To complete the picture, we exhibit a simple 
	timed automaton with an \(\epsilon\)-transition, 
	which resets some clock, on a cycle and which 
	is not equivalent to any \(\epsilon\)-free timed 
	automaton. To show this, we develop a 
	promising new technique based on the notion of 
	precise action.}
}
@book{LA-PG-BP-AP-NP-PW-livre98,
  author = {Albert, Luc and Gastin, Paul and 
                 Petazzoni, Bruno and Petit, Antoine
                 and Puech, Nicolas and Weil, Pascal},
  title = {Cours et exercices d'informatique, Classes
                 pr{\'e}paratoires, premier et second cycles
                 universitaires},
  year = {1998},
  month = jun,
  publisher = {Vuibert},
  isbn = {2-7117-8621-8},
  lsv-lang = {FR}
}
@inproceedings{PG-RM-AP-mfcs98,
  address = {Brno, Czech Republic},
  month = aug,
  year = 1998,
  volume = 1450,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Brim, Lubos and Gruska, Jozef and Zlatuska, Jir{\'i}},
  acronym = {{MFCS}'98},
  booktitle = {{P}roceedings of the 23rd
               {I}nternational {S}ymposium on
               {M}athematical {F}oundations of 
               {C}omputer {S}cience
               ({MFCS}'98)},
  author = {Gastin, Paul and Meyer, Rapha{\"e}l and 
                  Petit, Antoine},
  title = {A (non-elementary) modular decision procedure for
                 {LTrL}},
  pages = {356-365},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GMP-mfcs98.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GMP-mfcs98.ps},
  abstract = {Thiagarajan and Walukiewicz have defined a
                  temporal logic~LTrL on Mazurkiewicz
                  traces, patterned on the famous
                  propositional temporal logic of linear
                  time~LTL defined by Pnueli. They have
                  shown that this logic is equal in
                  expressive power to the first order theory
                  of finite and infinite traces.\par 
                  The hopes to get an {"}easy{"} decision
                  procedure for~LTrL, as it is the case 
                  for~LTL, vanished very recently due to a
                  result of Walukiewicz who showed that the
                  decision procedure for~LTrL is
                  non-elementary. However, tools like Mona
                  or Mosel show that it is possible to
                  handle non-elementary logics on
                  significant examples. Therefore, it
                  appears worthwhile to have a direct
                  decision procedure for LTrL.\par 
                  In this paper we propose such a decision
                  procedure, in a modular way. Since the
                  logic~LTrL is not pure future, our
                  algorithm constructs by induction a finite
                  family of B{\"u}chi automata for each
                  LTrL-formula. As expected by the results
                  of Walukiewicz, the main difficulty comes
                  from the {"}Until{"} operator.}
}
@article{DiGa98,
  publisher = {Springer},
  journal = {Acta Informatica},
  author = {Diekert, Volker and Gastin, Paul},
  title = {Approximating traces},
  volume = 35,
  number = 7,
  year = 1998,
  pages = {567-593},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Alphatracesdg.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Alphatracesdg.ps},
  abstract = {In order to give a semantics to 
	concurrent processes, one needs a powerful 
	model which enjoys many important mathematical 
	properties. We generalize Mazurkiewicz 
	(infinite) traces by adding an information 
	concerning the possible continuations of a 
	process. This allows to define an 
	approximation order and a composition. We 
	obtain a prime algebraic coherently complete 
	domain where the compacts are exactly the 
	finite approximations of actual processes. The 
	composition is shown to be monotone and 
	\(\sqcup\)-continuous. We define a suitable 
	metric which induces the Lawson topology and 
	yields a complete and compact metric space. 
	The finite approximations of processes form a 
	dense subset and the composition is uniformly 
	continuous.}
}
@article{DrGa99j,
  author = {Droste, Manfred and Gastin, Paul},
  title = {The {K}leene-{S}ch{\"u}tzenberger theorem for formal power series
             in partially commuting variables},
  volume = 153,
  number = 1,
  year = 1999,
  month = aug,
  pages = {47-80},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/IC99dg.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/IC99dg.ps},
  abstract = {Kleene's theorem on the 
	coincidence of regular and rational 
	languages in free monoids has been 
	generalized by Sch{\"u}tzenberger to a 
	description of the recognizable formal power 
	series in non-commuting variables over 
	arbitrary semi-rings, and by Ochma{\'n}ski to a 
	characterization of the recognizable 
	languages in trace monoids.\par
	We will describe the recognizable formal 
	power series over arbitrary semirings and in 
	partially commuting variables, \emph{i.e.} over 
	trace monoids. We prove that the 
	recognizable series are certain rational 
	power series, which can be constructed from 
	the polynomials by using the operations sum, 
	product and a restricted star which is 
	applied only to series for which the 
	elements in the support all have the same 
	connected alphabet. The converse is true if 
	the underlying semiring is commutative.\par
	Moreover, if in addition the semiring is 
	idempotent then the same result holds with a 
	star restricted to series for which the 
	elements in the support have connected 
	(possibly different) alphabets. It is shown 
	that these assumptions over the semiring are 
	necessary. This provides a joint 
	generalization of Kleene's, Sch{\"u}tzenberger's 
	and Ochma{\'n}ski's theorems.}
}
@inproceedings{GaMi99,
  address = {Madrid, Spain},
  month = sep,
  year = 1999,
  volume = 1683,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Flum, J{\"o}rg and Rodr{\'\i}guez-Artalejo, Mario},
  acronym = {{CSL}'99},
  booktitle = {{S}elected {P}apers from the 13th {I}nternational
               {W}orkshop on {C}omputer {S}cience {L}ogic
               ({CSL}'99)},
  author = {Gastin, Paul and Mislove, Michael W.},
  title = {A truly concurrent semantics for a
              simple parallel programming language},
  pages = {515-529},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Csl99gm.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Csl99gm.ps},
  abstract = {This paper represents the 
	beginning of a study aimed at devising 
	semantic models for true concurrency that 
	provide clear distinctions between 
	concurrency, parallelism and choice. We 
	present a simple programming language which 
	includes (weakly) sequential composition, 
	asynchronous and synchronous parallel 
	composition, a restriction operator, and 
	that supports recursion. We develop an 
	operational and a denotational semantics for 
	this language, and we obtain a congruence 
	theorem relating the behavior of a process 
	as described by the transition system to the 
	meaning of the process in the denotational 
	model. This implies that the denotational 
	model is adequate with respect to the 
	operational model. Our denotational model is 
	based on the resource traces of Gastin and 
	Teodesiu, and since a single resource trace 
	represents all possible executions of a 
	concurrent process, we are able to model 
	each term of our concurrent language by a 
	single trace. Therefore we obtain a 
	deterministic semantics for our language and 
	we are able to model parallelism without 
	introducing nondeterminism.}
}
@inproceedings{DiGa99,
  address = {Madrid, Spain},
  month = sep,
  year = 1999,
  volume = 1683,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Flum, J{\"o}rg and Rodr{\'\i}guez-Artalejo, Mario},
  acronym = {{CSL}'99},
  booktitle = {{S}elected {P}apers from the 13th {I}nternational
               {W}orkshop on {C}omputer {S}cience {L}ogic
               ({CSL}'99)},
  author = {Diekert, Volker and Gastin, Paul},
  title = {An expressively complete temporal logic without past tense
              operators for {M}azurkiewicz traces},
  pages = {188-203},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Csl99dg.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Csl99dg.ps},
  abstract = {Mazurkiewicz traces are a widely 
	accepted model of concurrent systems. We 
	introduce a linear time temporal logic which has 
	the same expressive power as the first order 
	theory of finite (infinite resp.) traces. The 
	main contribution of the paper is that we only 
	use future tense modalities in order to obtain 
	expressive completeness. Our proof is direct and 
	uses no reduction to words. As a formal 
	consequence Kamp's theorem for both finite and 
	infinite words becomes a corollary. This direct 
	approach became possible due to a new proof 
	technique of Wilke developed for the case of 
	finite words.}
}
@article{DrGaKu00,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Droste, Manfred and Gastin, Paul and Kuske, Dietrich},
  title = {Asynchronous cellular automata for pomsets},
  volume = 247,
  number = {1-2},
  year = 2000,
  month = sep,
  pages = {1-38},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DGK-TCS00.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DGK-TCS00.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DGK-TCS00.ps},
  abstract = {This paper extends to pomsets without 
	auto-concurrency the fundamental notion of 
	asynchronous cellular automata (ACA) which was 
	originally introduced for traces by Zielonka. We 
	generalize to pomsets the notion of asynchronous 
	mapping introduced by Cori, M{\'e}tivier and Zielonka 
	and we show how to construct a deterministic ACA from 
	an asynchronous mapping. \par

	Then we investigate the relation between the 
	expressiveness of monadic second order logic, 
	nondeterministic ACAs and deterministic ACAs. We can 
	generalize B{\"u}chi's theorem for finite words to a class 
	of pomsets without auto-concurrency which satisfy a 
	natural axiom. This axiom ensures that an asynchronous 
	cellular automaton works on the pomset as a concurrent 
	read and exclusive owner write machine. More 
	precisely, in this class non-deterministic ACAs, 
	deterministic ACAs and monadic second order logic have 
	the same expressive power. \par

	Then we consider a class where deterministic ACAs are 
	strictly weaker than nondeterministic ones. But in 
	this class nondeterministic ACAs still capture monadic 
	second order logic. Finally it is shown that even this 
	equivalence does not hold in the class of all pomsets 
	since there the class of recognizable pomset languages 
	is not closed under complementation.}
}
@inproceedings{DiGa00,
  address = {Geneva, Switzerland},
  month = jul,
  year = 2000,
  volume = 1853,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Montanari, Ugo and Rolim, Jos{\'e} D. P. and
            Welzl, Emo},
  acronym = {{ICALP} 2000},
  booktitle = {{P}roceedings of the 27th {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming
               ({ICALP} 2000)},
  author = {Diekert, Volker and Gastin, Paul},
  title = {{LTL} is expressively complete for {M}azurkiewicz traces},
  pages = {211-222},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Icalp00dg.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Icalp00dg.ps},
  abstract = {A long standing open problem in the 
	theory of (Mazurkiewicz) traces has been the 
	question whether LTL (Linear Time Logic) is 
	expressively complete with respect to the first 
	order theory. We solve this problem positively for 
	finite and infinite traces and for the simplest 
	temporal logic, which is based only on next and 
	until modalities. Similar results were established 
	previously, but they were all weaker, since they 
	used additional past or future modalities. Another 
	feature of our work is that our proof is direct and 
	does not use any reduction to the word case. It is 
	based on an algebraic characterization of first 
	order trace languages, following a proof technique 
	introduced recently by Thomas Wilke in order to 
	prove the expressive completeness of LTL for 
	finite words.}
}
@inproceedings{DrGa00,
  address = {Moscow, Russia},
  month = jun,
  year = 2000,
  publisher = {Springer},
  editor = {Krob, Daniel and Mikhalev, Alexander A. and Mikhalev, Alexander V.},
  acronym = {{FPSAC}'00},
  booktitle = {{P}roceedings of the 12th {I}nternational {C}onference on 
	   {F}ormal {P}ower {S}eries and {A}lgebraic
	   {C}ombinatorics ({FPSAC}'00)},
  author = {Droste, Manfred and Gastin, Paul},
  title = {On aperiodic and star-free formal power series
              in partially commuting variables},
  pages = {158-169},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Fpsac00dg.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Fpsac00dg.ps},
  abstract = {Formal power series over 
	non-commuting variables have been 
	investigated as representations of the 
	behaviour of automata with multiplicities. 
	Here we introduce and investigate the 
	concepts of aperiodic and of star-free 
	formal power series over semirings and 
	partially commuting variables. We prove that 
	if the semiring~\(K\) is idempotent and 
	commutative, or if \(K\) is idempotent and the 
	variables are non-commuting, then the 
	product of any two aperiodic series is again 
	aperiodic. We also show that if \(K\) is 
	idempotent and the matrix monoids over \(K\) 
	have a Burnside property (satisfied, \emph{e.g.} by 
	the tropical semiring), then the aperiodic 
	and the star-free series coincide. This 
	generalizes a classical result of 
	Sch{\"u}tzenberger~(1961) for aperiodic regular 
	languages and contains a result of Guaiana, 
	Restivo and Salemi~(1992) on aperiodic trace 
	languages.}
}
@inproceedings{DiGa01lpar,
  address = {Havana, Cuba},
  month = dec,
  year = 2001,
  volume = 2250,
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  editor = {Nieuwenhuis, Robert and Voronkov, Andrei},
  acronym = {{LPAR}'01},
  booktitle = {{P}roceedings of the 8th {I}nternational
               {C}onference on {L}ogic for {P}rogramming,
               {A}rtificial {I}ntelligence, and {R}easoning
               ({LPAR}'01)},
  author = {Diekert, Volker and Gastin, Paul},
  title = {Local Temporal Logic is Expressively Complete
              for Cograph Dependence Alphabets},
  pages = {55-69},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Lpar01dg.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Lpar01dg.ps},
  abstract = {Recently, local logics for 
	Mazurkiewicz traces are of increasing 
	interest. This is mainly due to the fact 
	that the satisfiability problem has the 
	same complexity as in the word case. If we 
	focus on a purely local interpretation of 
	formulae at vertices (or events) of a 
	trace, then the satisfiability problem of 
	linear temporal logics over traces turns 
	out to be PSPACE-complete. But now the 
	difficult problem is to obtain expressive 
	completeness results with respect to first 
	order logic. \par

	The main result of the paper shows such an 
	expressive completeness result, if the 
	underlying dependence alphabet is a 
	cograph, \emph{i.e.}, if all traces are series 
	parallel graphs. Moreover, we show that 
	this is the best we can expect in our 
	setting: If the dependence alphabet is not 
	a cograph, then we cannot express all 
	first order properties.}
}
@inproceedings{GaOd01,
  address = {Paris, France},
  month = jul,
  year = 2001,
  volume = 2102,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Berry, G{\'e}rard and Comon, Hubert and Finkel, Alain},
  acronym = {{CAV}'01},
  booktitle = {{P}roceedings of the 13th
               {I}nternational {C}onference on 
               {C}omputer {A}ided {V}erification
               ({CAV}'01)},
  author = {Gastin, Paul and Oddoux, Denis},
  title = {Fast {LTL} to {B}{\"u}chi Automata Translation},
  pages = {53-65},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Cav01go.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Cav01go.ps},
  abstract = {We present an algorithm to generate 
	B{\"u}chi automata from LTL formulae. This algorithm 
	generates a very weak alternating automaton and 
	then transforms it into a B{\"u}chi automaton, using a 
	generalized B{\"u}chi automaton as an intermediate 
	step. Each automaton is simplified on-the-fly in 
	order to save memory and time. As usual we 
	simplify the LTL formula before any treatment. We 
	implemented this algorithm and compared it with 
	Spin: the experiments show that our algorithm is 
	much more efficient than Spin. The criteria of 
	comparison are the size of the resulting 
	automaton, the time of the computation and the 
	memory used. Our implementation is available on 
	the web at the following address: 
	\url{http://verif.liafa.jussieu.fr/ltl2ba}}
}
@inproceedings{DeGa01,
  address = {Toronto, Canada},
  month = may,
  year = 2001,
  volume = 2057,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Dwyer, Matthew B.},
  acronym = {{SPIN}'01},
  booktitle = {{P}roceedings of the 8th {I}nternational
               {SPIN} {W}orkshop on {M}odel {C}hecking {S}oftware
               ({SPIN}'01)},
  author = {Derepas, Fabrice and Gastin, Paul},
  title = {Model Checking Systems of Replicated Processes with {SPIN}},
  pages = {235-251},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Spin01dg.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Spin01dg.ps},
  abstract = {This paper describes a 
	reduction technique which is very useful 
	against the state explosion problem 
	which occurs when model checking 
	distributed systems with several 
	instances of the same process. Our 
	technique uses symmetry which appears in 
	the system. Exchanging those instances 
	is not as simple as it seems, because 
	there can be a lot of references to 
	process locations in the system. We 
	implemented a solution using the Spin 
	model checker, and added two keywords to 
	the Promela language to handle these new 
	concepts.}
}
@inproceedings{DeGaPl01,
  address = {Berlin, Germany},
  month = mar,
  year = 2001,
  volume = 2021,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Oliveira, Jos{\'e} Nuno and Zave, Pamela},
  acronym = {{FME}'01},
  booktitle = {{F}ormal {M}ethods for {I}ncreasing {S}oftware 
	   {P}roductivity~--- 
	   {P}roceedings of the {I}nternational {S}ymposium of {F}ormal 
	   {M}ethods {E}urope ({FME}'01)},
  author = {Derepas, Fabrice and Gastin, Paul and 
	      Plainfoss{\'e}, David},
  title = {Avoiding state explosion for distributed systems
              with timestamps},
  pages = {119-134},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Fme01dgp.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Fme01dgp.ps},
  abstract = {This paper describes a 
	reduction technique which is very useful 
	against the state explosion problem which 
	occurs when model checking many distributed 
	systems. Timestamps are often used to keep 
	track of the relative order of events. They 
	are usually implemented with very large 
	counters and therefore they generate state 
	explosion. The aim of this paper is to 
	present a very efficient reduction of the 
	state space generated by a model checker when 
	using timestamps. The basic idea is to map 
	the timestamps values to the smallest 
	possible range. This is done dynamically and 
	on-the-fly by adding to the model checker a 
	call to a reduction function after each newly 
	generated state. Our reduction works for 
	model checkers using explicit state 
	enumeration and does not require any change 
	in the model. Our method has been applied to 
	an industrial example and the reduction 
	obtained was spectacular.}
}
@article{DG02JALC,
  journal = {Journal of Automata, Languages and Combinatorics},
  author = {Droste, Manfred and Gastin, Paul},
  editor = {Droste, Manfred and Gastin, Paul},
  title = {Selected papers of the workshop on \emph{Logic and Algebra in 
	   Concurrency}, Dresden, Germany, September 2000},
  volume = 7,
  number = 2,
  year = 2002
}
@incollection{DiGa02Roz,
  missingmonth = mar,
  missingnmonth = 3,
  year = 2002,
  volume = 2300,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Brauer, Wilfried and
            Ehrig, Hartmut and
            Karhum{\"a}ki, Juhani and
            Salomaa, Arto},
  acronym = {{F}ormal and {N}atural {C}omputing},
  booktitle = {{F}ormal and {N}atural {C}omputing~---
           {E}ssays {D}edicated to {G}rzegorz {R}ozenberg},
  author = {Diekert, Volker and Gastin, Paul},
  title = {Safety and Liveness Properties for Real Traces and
              a Direct Translation from {LTL} to Monoids},
  pages = {26-38},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/diegas01-3.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/diegas01-3.ps},
  doi = {10.1007/3-540-45711-9_2},
  abstract = { For infinite words there are 
	well-known characterizations of safety and liveness 
	properties. We extend these results to real 
	Mazurkiewicz traces. This is possible due to a 
	result, which has been established recently: Every 
	first-order definable real trace language is 
	definable in linear temporal logic using future 
	tense operators, only. We show that the canonical 
	choice for a topological characterization of safety 
	and liveness properties is given by the Scott 
	topology. In this paper we use an algebraic approach 
	where we work with aperiodic monoids. Therefore we 
	also give a direct translation from temporal logic 
	to aperiodic monoids which is of independent 
	interest.}
}
@article{DiGa02jcss,
  publisher = {Elsevier Science Publishers},
  journal = {Journal of Computer and System Sciences},
  author = {Diekert, Volker and Gastin, Paul},
  title = {{LTL} is expressively complete for {M}azurkiewicz traces},
  volume = 64,
  number = 2,
  year = 2002,
  month = mar,
  pages = {396-418},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/JCSS02dg.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/JCSS02dg.ps},
  abstract = {A long standing open problem in the 
	theory of (Mazurkiewicz) traces has been the 
	question whether LTL (Linear Temporal Logic) is 
	expressively complete with respect to the first 
	order theory. We solve this problem positively for 
	finite and infinite traces and for the simplest 
	temporal logic, which is based only on next and 
	until modalities. Similar results were established 
	previously, but they were all weaker, since they 
	used additional past or future modalities. Another 
	feature of our work is that our proof is direct and 
	does not use any reduction to the word case.}
}
@article{GaMi02tcs,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Gastin, Paul and Mislove, Michael W.},
  title = {A truly concurrent semantics for a
            process algebra using resource pomsets},
  volume = 281,
  number = {1-2},
  year = 2002,
  month = jun,
  pages = {369-421},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GM-TCS02.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GM-TCS02.ps},
  abstract = {In this paper we study a process 
	algebra whose semantics is based on true 
	concurrency. In our model, actions are defined in 
	terms of the resources they need to execute, which 
	allows a simple definition of a weak sequential 
	composition operator. This operator allows actions 
	which do not share any resources to execute 
	concurrently, while dependent actions have to occur 
	sequentially. This weak sequential composition 
	operation may be used to automatically parallelize a 
	sequential process. We add to this operator the 
	customary (strict) sequential composition and a 
	parallel composition allowing synchronization on 
	specified actions. Our language also supports a 
	hiding operator that allows the hiding of actions 
	and even of individual resources used by actions. 
	Strict sequential composition and hiding require 
	that we generalize from the realm of Mazurkiewicz 
	traces to that of pomsets, since these operations 
	introduce {"}over-synchronized{"} traces~--- ones for 
	which a pair of independent actions may occur 
	sequentially. Our language also supports recursion 
	and our semantics makes the unwinding of recursion 
	visible by the use of special resources used to 
	label unwindings. This was done on purpose in order 
	to enable the observation of divergence, but the 
	usual semantics that does not observe unwindings can 
	be obtained by using the hiding operator to abstract 
	away from these special resources. We give both an 
	SOS-style operational semantics for our language, as 
	well as a denotational semantics based on resource 
	pomsets. Generalizing results from our earlier work 
	in this area, we derive a congruence theorem for our 
	language which shows that the SOS-style operational 
	rules induce the same equivalence relation on the 
	language as the semantic map does. A corollary is 
	that our denotational model is both adequate and 
	fully abstract relative to the behavior function 
	defined from our operational semantics. This 
	behavior consists naturally of the strings of 
	actions the process can perform. This work continues 
	our study into modelling concurrency in the absence 
	of nondeterminism. In particular, our language is 
	deterministic.}
}
@article{GaTe02,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Gastin, Paul and Teodosiu, Dan},
  title = {Resource traces: A domain for processes sharing exclusive
            resources},
  volume = 278,
  number = {1-2},
  year = 2002,
  month = may,
  pages = {195-221},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GT-TCS02.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GT-TCS02.ps},
  abstract = {The theory of finite and infinite words 
	with explicit termination is commonly used to give 
	denotational semantics for algebras of sequential 
	processes. In this paper we generalize this theory 
	to the case of partially terminated concurrent 
	processes synchronizing on a fixed set of shared 
	exclusive resources. \par

	We start with an alphabet of actions, a set of 
	resources, and a resource map assigning to each 
	action the non-empty subset of resources it uses. 
	Actions that do not share common resources are 
	declared independent. The specification we use for 
	partially terminated processes (resource traces) is 
	similar to failure semantics. It consists of two 
	components: an already observed part represented as 
	an action-labeled event structure (Mazurkiewicz 
	trace), and a guard set containing the resources 
	granted to the process for its further development. 
	A process concatenation is then defined such that 
	independent actions can be dispatched concurrently. 
	Specification refinement leads to the definition of 
	a natural approximation ordering between processes 
	which generates a coherently complete prime 
	algebraic Scott domain, where process concatenation 
	is continuous in both arguments. Furthermore, we 
	define a natural ultrametric on processes based on 
	prefix information. The induced topology is shown to 
	be equivalent to the compact Lawson topology 
	generated by the approximation ordering. Moreover, 
	process concatenation is shown to be uniformly 
	continuous with respect to the defined ultrametric. 
	\par

	We develop a mathematical theory which perfectly 
	extends the central properties of the domain of 
	finite and infinte words with explicit termination 
	and the domain of finite and infinite Mazurkiewicz 
	traces. Its natural semantics is well suited to the 
	design of modular denotational semantics for 
	algebras of processes sharing exclusive resources 
	such as programs using some set of shared registers 
	(PRAM) or concurrent sequential processes 
	synchronizing over exclusive communication channels 
	(CSP).}
}
@inproceedings{GaMu02icalp,
  address = {M{\'a}laga, Spain},
  month = jul,
  year = 2002,
  volume = 2380,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Widmayer, Peter and
	Triguero Ruiz, Francisco and Morales Bueno, Rafael and
	Hennessy, Matthew and Eidenbenz, Stephan and Conejo, Ricardo},
  acronym = {{ICALP}'02},
  booktitle = {{P}roceedings of the 29th {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming
               ({ICALP}'02)},
  author = {Gastin, Paul and Mukund, Madhavan},
  title = {An Elementary Expressively Complete Temporal Logic
              for {M}azurkiewicz Traces},
  pages = {938-949},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/gasmuk02long2.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/gasmuk02long2.ps},
  abstract = {In contrast to the 
	classical setting of sequences, no 
	temporal logic has yet been identified 
	over Mazurkiewicz traces that is 
	equivalent to the first-order theory of 
	traces and yet admits an elementary 
	decision procedure. In this paper, we 
	describe a local temporal logic over 
	traces that is expressively complete 
	and whose satisfiability problem is in 
	PSPACE. Contrary to the situation for 
	sequences, past modalities are 
	essential for such a logic. A somewhat 
	unexpected corollary is that 
	first-order logic with three variables 
	is expressively complete for traces.}
}
@inproceedings{GaKu03concur,
  address = {Marseilles, France},
  month = aug,
  year = 2003,
  volume = 2761,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Amadio, Roberto M. and Lugiez, Denis},
  acronym = {{CONCUR}'03},
  booktitle = {{P}roceedings of the 14th 
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'03)},
  author = {Gastin, Paul and Kuske, Dietrich},
  title = {Satisfiability and Model Checking for {MSO}-definable
              Temporal Logics are in {PSPACE}},
  pages = {222-236},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/concur03gk-final.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/concur03gk-final.ps},
  abstract = {Temporal logics over Mazurkiewicz 
	traces have been extensively studied over the past 
	fifteen years. In order to be usable for the 
	verification of concurrent systems they need to have 
	reasonable complexity for the satisfiability and the 
	model checking problems. Whenever a new temporal 
	logic was introduced, a new proof (usually non 
	trivial) was needed to establish the complexity of 
	these problems. In this paper, we introduce a 
	unified framework to define local temporal logics 
	over traces. We prove that the satisfiability 
	problem and the model checking problem for 
	asynchronous Kripke structures for local temporal 
	logics over traces are decidable in PSPACE. This 
	subsumes and sometimes improves all complexity 
	results previously obtained on local temporal logics 
	for traces.}
}
@inproceedings{GaMuNa03mfcs,
  address = {Bratislava, Slovakia},
  month = aug,
  year = 2003,
  volume = 2747,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Rovan, Branislav and Vojt{\'a}{\v{s}}, Peter},
  acronym = {{MFCS}'03},
  booktitle = {{P}roceedings of the 28th
               {I}nternational {S}ymposium on
               {M}athematical {F}oundations of 
               {C}omputer {S}cience
               ({MFCS}'03)},
  author = {Gastin, Paul and Mukund, Madhavan and Narayan Kumar, K.},
  title = {Local {LTL} with past constants is  expressively complete for
              {M}azurkiewicz traces},
  pages = {429-438},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/mfcs03gmn-final.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/mfcs03gmn-final.ps},
  abstract = {To obtain an expressively complete 
	linear-time temporal logic (LTL) over 
	Mazurkiewicz traces that is computationally 
	tractable, we need to interpret formulas locally, 
	at individual events in a trace, rather than 
	globally, at configurations. Such local logics 
	necessarily require past modalities, in contrast 
	to the classical setting of LTL over sequences. 
	Earlier attempts at defining expressively 
	complete local logics have used very general past 
	modalities as well as filters (side-conditions) 
	that {"}look sideways{"} and talk of concurrent 
	events. In this paper, we show that it is 
	possible to use unfiltered future modalities in 
	conjunction with past constants and still obtain 
	a logic that is expressively complete over 
	traces.}
}
@inproceedings{GaOd03mfcs,
  address = {Bratislava, Slovakia},
  month = aug,
  year = 2003,
  volume = 2747,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Rovan, Branislav and Vojt{\'a}{\v{s}}, Peter},
  acronym = {{MFCS}'03},
  booktitle = {{P}roceedings of the 28th
               {I}nternational {S}ymposium on
               {M}athematical {F}oundations of 
               {C}omputer {S}cience
               ({MFCS}'03)},
  author = {Gastin, Paul and Oddoux, Denis},
  title = {{LTL} with past and two-way very-weak alternating automata},
  pages = {439-448},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/mfcs03go-final.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/mfcs03go-final.ps},
  abstract = {It is crucial for a model 
	checker using LTL as a specification 
	language to have very efficient translation 
	of LTL formulas to B{\"u}chi automata. Most such 
	algorithms are based on a tableau 
	construction. Recently, an implementation 
	using very-weak alternating automata as an 
	intermediary step proved to be dramatically 
	faster than previous implementations based 
	on the tableau construction. In this paper, 
	we want to generalize this method to PLTL 
	(LTL with past modalities). For this, we 
	study two-way very-weak alternating automata 
	(\(2\)VWAA). Our main result is an efficient 
	translation of \(2\)VWAA to generalized B{\"u}chi 
	automata (GBA). Since we can easily 
	transform a PLTL formula to an equivalent 
	\(2\)VWAA, this algorithm allows to use PLTL 
	specifications with classical model checkers 
	such as SPIN.}
}
@misc{gastin-movep2004,
  author = {Gastin, Paul},
  title = {Basics of model checking},
  year = 2004,
  month = dec,
  nonote = {-- pages},
  howpublished = {Invited tutorial, 6th {W}inter {S}chool on
		{M}odelling and {V}erifying {P}arallel {P}rocesses
		({MOVEP}'04), Brussels, Belgium}
}
@misc{gastin-epit32,
  author = {Gastin, Paul},
  title = {Specifications for distributed systems},
  year = 2004,
  month = apr,
  howpublished = {Invited lecture, 32nd {S}pring {S}chool on 
		{T}heoretical {C}omputer {S}cience ({C}oncurrency {T}heory), 
		Luminy, France}
}
@article{icomp-DG2004,
  publisher = {Elsevier Science Publishers},
  journal = {Information and Computation},
  author = {Diekert, Volker and Gastin, Paul},
  title = {Local temporal logic is expressively complete for 
		 cograph dependence alphabets},
  volume = {195},
  number = {1-2},
  pages = {30-52},
  year = 2004,
  month = nov,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG04-icomp.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DG04-icomp.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG04-icomp.pdf},
  doi = {10.1016/j.ic.2004.08.001},
  abstract = {Recently, local logics for Mazurkiewicz 
	traces are of increasing interest. This is mainly 
	due to the fact that the satisfiability problem has 
	the same complexity as in the word case. If we focus 
	on a purely local interpretation of formulae at 
	vertices (or events) of a trace, then the 
	satisfiability problem of linear temporal logics 
	over traces turns out to be PSPACE-complete. But 
	now the difficult problem is to obtain expressive 
	completeness results with respect to first order 
	logic. \par

	The main result of the paper shows such an 
	expressive completeness result, if the underlying 
	dependence alphabet is a cograph, \emph{i.e.} 
	if all 
	traces are series parallel posets. Moreover, we show 
	that this is the best we can expect in our setting: 
	If the dependence alphabet is not a cograph, then we 
	cannot express all first order properties.}
}
@inproceedings{GaLeZe04fsttcs,
  address = {Chennai, India},
  month = dec,
  year = 2004,
  volume = 3328,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Lodaya, Kamal and Mahajan, Meena},
  acronym = {{FSTTCS}'04},
  booktitle = {{P}roceedings of the 24th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'04)},
  author = {Gastin, Paul and Lerman, Benjamin and Zeitoun, Marc},
  title = {Distributed games with causal memory are decidable for
            series-parallel systems},
  pages = {275-286},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GLZ-fsttcs04.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GLZ-fsttcs04.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GLZ-fsttcs04.ps},
  abstract = {This paper deals with distributed 
	control problems by means of distributed games 
	played on Mazurkiewicz traces. The main difference 
	with other notions of distributed games recently 
	introduced is that, instead of having a \emph{local} view, 
	strategies and controllers are able to use a more 
	accurate memory, based on their \emph{causal} view. Our 
	main result states that using the causal view makes 
	the control synthesis problem decidable for 
	series-parallel systems for \emph{all} recognizable winning 
	conditions on finite behaviors, while this problem 
	with local view was proved undecidable even for 
	reachability conditions.}
}
@article{GaMi04mscs,
  publisher = {Cambridge University Press},
  journal = {Mathematical Structures in Computer Science},
  author = {Gastin, Paul and Mislove, Michael W.},
  title = {A simple process algebra based on atomic actions with 
	      resources},
  year = 2004,
  month = feb,
  volume = 14,
  number = 1,
  pages = {1-55},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GM-mscs04.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GM-mscs04.ps},
  doi = {10.1017/S0960129503003943},
  abstract = {This paper gives the first truly 
	concurrent denotational, \emph{i.e.} 
	compositional 
	semantics for a simple, deterministic parallel 
	language. By truly concurrent we mean the 
	denotational model does not rely on an interleaving 
	of concurrent actions for its definition. Thus, our 
	semantics does not reduce parallelism to 
	nondeterminism, as is done in the more established 
	approaches to concurrency. We also present a natural 
	SOS-style operational semantics for our language, 
	and we prove a congruence theorem relating the two 
	semantics. This implies the operational model itself 
	is compositional. The congruence theorem also 
	implies the denotational model is adequate with 
	respect to the operational semantics, and we 
	characterize the relatively mild conditions under 
	which the denotational semantics is fully abstract 
	with respect to the operational semantics. \par

	Our simple language includes a (weak) sequential 
	composition operator which takes advantage of the 
	truly concurrent nature of the semantics, as well as 
	a parallel composition operator which allows local 
	events to execute asynchronously, while requiring 
	synchronizing events to execute simultaneously. In 
	addition, the language supports a restriction 
	operator and includes recursion. \par

	The denotational semantics also is novel for its 
	treatment of recursion. The meaning of a recursive 
	process is defined using a least fixed point on a 
	subdomain that is determined by the body of the 
	recursion, and that varies from one process to 
	another. Nonetheless, the recursion operators in the 
	language have continuous interpretations in the 
	denotational model. 

	Our denotational model is based on a 
	domain-theoretic generalization of Mazurkiewicz 
	traces in which the concatenation operator, as well 
	as the other operators from our language can be 
	given continuous interpretations.}
}
@inproceedings{GaMoZe04spin,
  address = {Barcelona, Spain},
  month = apr,
  year = 2004,
  volume = 2989,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Graf, Susanne and Mounier, Laurent},
  acronym = {{SPIN}'04},
  booktitle = {{P}roceedings of the 11th {I}nternational
               {SPIN} {W}orkshop on {M}odel {C}hecking {S}oftware
               ({SPIN}'04)},
  author = {Gastin, Paul and Moro, Pierre and 
	Zeitoun, Marc},
  title = {Minimization of counterexamples in 
		{SPIN}},
  pages = {92-108},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GMZ-spin04.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GMZ-spin04.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GMZ-spin04.ps},
  abstract = {We propose an algorithm to find a 
	counterexample to some property in a finite state 
	program. This algorithm is derived from SPIN's 
	one, but it finds a counterexample faster than 
	SPIN does. In particular it still works in linear 
	time. Compared with SPIN's algorithm, it requires 
	only one additional bit per state stored. We 
	further propose another algorithm to compute a 
	counterexample of minimal size. Again, this 
	algorithm does not use more memory than SPIN does 
	to approximate a minimal counterexample. The cost 
	to find a counterexample of minimal size is that 
	one has to revisit more states than SPIN. We 
	provide an implementation and discuss 
	experimental results.}
}
@inproceedings{GaLeZe04latin,
  address = {Buenos Aires, Argentina},
  month = apr,
  year = 2004,
  volume = 2976,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Farach-Colton, Martin},
  acronym = {{LATIN}'04},
  booktitle = {{P}roceedings of the 6th {L}atin {A}merican
               {S}ymposium on {T}heoretical {I}nformatics
               ({LATIN}'04)},
  author = {Gastin, Paul and Lerman, Benjamin and Zeitoun, Marc},
  title = {Distributed games and distributed control for asynchronous 
	    systems},
  pages = {455-465},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GLZ-latin04.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GLZ-latin04.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GLZ-latin04.pdf},
  abstract = {We introduce distributed games over 
	asynchronous transition systems to model a 
	distributed controller synthesis problem. A game 
	involves two teams and is not turn-based: several 
	players of both teams may simultaneously be enabled. 
	We define distributed strategies based on the causal 
	view that players have of the system. We reduce the 
	problem of finding a winning distributed strategy 
	with a given memory to finding a memoryless winning 
	distributed strategy in a larger distributed game. 
	We reduce the latter problem to finding a strategy 
	in a classical \(2\)-player game. This allows to 
	transfer results from the sequential case to this 
	distributed setting.}
}
@inproceedings{DiGa04latin,
  address = {Buenos Aires, Argentina},
  month = apr,
  year = 2004,
  volume = 2976,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Farach-Colton, Martin},
  acronym = {{LATIN}'04},
  booktitle = {{P}roceedings of the 6th {L}atin {A}merican
               {S}ymposium on {T}heoretical {I}nformatics
               ({LATIN}'04)},
  author = {Diekert, Volker and Gastin, Paul},
  title = {Pure future local temporal logics are expressively complete
              for {M}azurkiewicz traces},
  pages = {232-241},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-latin04.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DG-latin04.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-latin04.pdf},
  abstract = {The paper settles a long standing 
	problem for Mazurkiewicz traces: the pure future 
	local temporal logic defined with the basic 
	modalities exists-next and until is expressively 
	complete. The analogous result with a global 
	interpretation was solved some years ago by 
	Thiagarajan and Walukiewicz (1997) and in its 
	final form without any reference to past tense 
	constants by Diekert and Gastin (2000). Each, the 
	(previously known) global or the (new) local 
	result generalizes Kamp's Theorem for words, 
	because for sequences local and global viewpoints 
	coincide. But traces are labelled partial orders 
	and then the difference between an interpretation 
	globally over cuts (configurations) or locally at 
	points (events) is significant. For global 
	temporal logics the satisfiability problem is 
	non-elementary (Walukiewicz, 1998), whereas for 
	local temporal logics both the satisfiability 
	problem and the model checking problem are sovable 
	in PSPACE (Gastin and Kuske, 2003) as in the case 
	of words. This makes local temporal logics much 
	more attractive.}
}
@misc{gastin-wpv05,
  author = {Gastin, Paul},
  title = {On the synthesis of distributed controllers},
  year = 2005,
  month = nov,
  howpublished = {Invited talk, Workshop Perspectives in  
		Verification, in honor of Wolfgang Thomas on the occasion of his
                Doctorate Honoris Causa, Cachan, France}
}
@inproceedings{Gastin-ICALP2005,
  address = {Lisboa, Portugal},
  month = jul,
  year = 2005,
  volume = {3580},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Caires, Lu{\'\i}s and Italiano, Giuseppe F. and
	    Monteiro, Lu{\'\i}s and Palamidessi, Catuscia and Yung, Moti},
  acronym = {{ICALP}'05},
  booktitle = {{P}roceedings of the 32nd {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming
               ({ICALP}'05)},
  author = {Droste, Manfred and Gastin, Paul},
  title = {Weighted Automata and Weighted Logics},
  pages = {513-525},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/icalp05dg-final.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/icalp05dg-final.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/icalp05dg-final.pdf},
  doi = {10.1007/11523468_42},
  abstract = {Weighted automata are used to 
	describe quantitative properties in various 
	areas such as probabilistic systems, image 
	compression, speech-to-text processing. The 
	behaviour of such an automaton is a mapping, 
	called a formal power series, assigning to 
	each word a weight in some semiring. We 
	generalize B{\"{u}}chi's and Elgot's 
	fundamental theorems to this quantitative 
	setting. We introduce a weighted version of 
	MSO~logic and prove that, for commutative 
	semirings, the behaviours of weighted 
	automata are precisely the formal power 
	series definable with our weighted logic. We 
	also consider weighted first-order logic and 
	show that aperiodic series coincide with the 
	first-order definable ones, if the semiring 
	is locally finite, commutative and has some 
	aperiodicity property.}
}
@inproceedings{GK-concur05,
  address = {San Francisco, California, USA},
  month = aug,
  year = 2005,
  volume = 3653,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Abadi, Mart{\'\i}n and de Alfaro, Luca},
  acronym = {{CONCUR}'05},
  booktitle = {{P}roceedings of the 16th 
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'05)},
  author = {Gastin, Paul and Kuske, Dietrich},
  title = {Uniform Satisfiability Problem for Local Temporal Logics
		 over {M}azurkiewicz Traces},
  pages = {533-547},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/concur05gk-final.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/concur05gk-final.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/concur05gk-final.ps},
  doi = {10.1007/11539452_40},
  abstract = {We continue our study of the complexity 
	of temporal logics over concurrent systems that can be 
	described by Mazurkiewicz traces. In a previous paper 
	(CONCUR~2003), we investigated the class of local and 
	MSO definable temporal logics that capture all known 
	temporal logics and we showed that the satisfiability 
	problem for any such logic is in PSPACE (provided the 
	dependence alphabet is fixed). In this paper, we 
	concentrate on the uniform satisfiability problem: we 
	consider the dependence alphabet (\emph{i.e.}, the 
	architecture of the distributed system) as part of the 
	input. We prove lower and upper bounds for the uniform 
	satisfiability problem that depend on the number of 
	monadic quantifier alternations present in the chosen 
	MSO-modalities.}
}
@misc{gastin-prefsttcs06,
  author = {Gastin, Paul},
  title = {Refinements and Abstractions of Signal-Event (Timed) Languages},
  year = 2006,
  month = dec,
  howpublished = {Invited talk, Advances and Issues in Timed Systems,
                  Kolkata, India}
}
@misc{gastin-wata06,
  author = {Gastin, Paul},
  title = {Weigthed logics and weighted automata},
  year = 2006,
  month = mar,
  howpublished = {Invited talk, Workshop Weighted Automata: Theory and Applications,
		Leipzig, Germany}
}
@misc{gastin-epit06,
  author = {Gastin, Paul},
  title = {Distributed synthesis: synchronous and asynchronous semantics},
  year = 2006,
  month = may,
  howpublished = {Invited talk, 34{\`e}me {\'E}cole de Printemps en 
		Informatique Th{\'e}orique, Ile de R{\'e}, France}
}
@misc{gastin-mfps22,
  author = {Gastin, Paul},
  title = {Refinements and Abstractions of Signal-Event (Timed) Languages},
  year = 2006,
  month = may,
  howpublished = {Invited talk, 22nd {C}onference on 
        {M}athematical {F}oundations of {P}rogramming 
        {S}emantics ({MFPS}'06)}
}
@inproceedings{GSZ-fsttcs2006,
  address = {Kolkata, India},
  month = dec,
  year = 2006,
  volume = 4337,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Garg, Naveen and Arun-Kumar, S.},
  acronym = {{FSTTCS}'06},
  booktitle = {{P}roceedings of the 26th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'06)},
  author = {Gastin, Paul and Sznajder, Nathalie and Zeitoun, Marc},
  title = {Distributed synthesis for well-connected architectures},
  pages = {321-332},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GSZ-fsttcs2006.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GSZ-fsttcs2006.pdf},
  doi = {10.1007/11944836_30},
  abstract = {We study the synthesis problem for external linear or branching
specifications and distributed, synchronous architectures with arbitrary
delays on processes. External means that the specification only relates input
and output variables. We~introduce the subclass of uniformly
well-connected~(UWC) architectures for which there exists a routing allowing
each output process to get the values of all inputs it is connected to, as
soon as possible. We~prove that the distributed synthesis problem is decidable
on UWC architectures if and only if the set of all sets of input variables
visible by output variables is totally ordered, under set inclusion. We~also
show that if we extend this class by letting the routing depend on the output
process, then the previous decidability result fails. Finally, we provide a
natural restriction on specifications under which the whole class of~UWC
architectures is decidable.}
}
@inproceedings{BGP1-formats06,
  address = {Paris, France},
  month = sep,
  year = 2006,
  volume = 4202,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Asarin, Eug{\`e}ne and Bouyer, Patricia},
  acronym = {{FORMATS}'06},
  booktitle = {{P}roceedings of the 4th {I}nternational {C}onference
           on {F}ormal {M}odelling and {A}nalysis of {T}imed
           {S}ystems ({FORMATS}'06)},
  author = {B{\'e}rard, B{\'e}atrice and Gastin, Paul and Petit, Antoine},
  title = {Refinements and abstractions of signal-event (timed) languages},
  pages = {67-81},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP1-formats06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP1-formats06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BGP1-formats06.ps},
  doi = {10.1007/11867340_6},
  abstract = {In the classical framework of formal languages, a refinement
operation is modeled by a substitution and an abstraction by an inverse
substitution. These mechanisms have been widely studied, because they describe
a change in the specification level, from an abstract view to a more concrete
one, or conversely. For~timed systems, there is up to now no uniform notion of
substitutions. In~this paper, we study the timed substitutions in the general
framework of signal-event languages, where both signals and events are taken
into account. We~prove that regular signal-event languages are closed under
substitutions and inverse substitutions. }
}
@inproceedings{BGP2-formats06,
  address = {Paris, France},
  month = sep,
  year = 2006,
  volume = 4202,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Asarin, Eug{\`e}ne and Bouyer, Patricia},
  acronym = {{FORMATS}'06},
  booktitle = {{P}roceedings of the 4th {I}nternational {C}onference
           on {F}ormal {M}odelling and {A}nalysis of {T}imed
           {S}ystems ({FORMATS}'06)},
  author = {B{\'e}rard, B{\'e}atrice and Gastin, Paul and Petit, Antoine},
  title = {Intersection of regular signal-event (timed) languages},
  pages = {52-66},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP2-formats06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP2-formats06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BGP2-formats06.ps},
  doi = {10.1007/11867340_5},
  abstract = {We propose in this paper a construction for a {"}well known{"}
result: regular signal-event languages are closed by intersection. In~fact,
while this result is indeed trivial for languages defined by Alur and Dill's
timed automata (the proof is an immediate extension of the one in the untimed
case), it turns out that the construction is much more tricky when considering
the most involved model of signal-event automata. While several constructions
have been proposed in particular cases, it is the first time, up to our
knowledge, that a construction working on finite and infinite signal-event
words and taking into account signal stuttering, unobservability of
zero-duration \(\tau\)-signals and Zeno runs is proposed.}
}
@inproceedings{BGM-atva2006,
  address = {Beijing, China},
  month = oct,
  year = {2006},
  volume = 4218,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Graf, Susanne and Zhang, Wenhui},
  acronym = {{ATVA}'06},
  booktitle = {{P}roceedings of the 4th {I}nternational
               {S}ymposium on {A}utomated {T}echnology
               for {V}erification and {A}nalysis
               ({ATVA}'06)},
  author = {Bhateja, Puneet and Gastin, Paul and Mukund, Madhavan},
  title = {A fresh look at testing for asynchronous communication},
  pages = {369-383},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGM-atva06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGM-atva06.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BGM-atva06.ps},
  doi = {10.1007/11901914_28},
  abstract = {Testing is one of the fundamental techniques for verifying if a
computing system conforms to its specification. We~take a fresh look at the
theory of testing for message-passing systems based on a natural notion of
observability in terms of input-output relations. We~propose two notions of
test equivalence: one which corresponds to presenting all test inputs up front
and the other which corresponds to interactively feeding inputs to the system
under test. We compare our notions with those studied earlier, notably the
equivalence proposed by Tretmans. In~Tretmans' framework, asynchrony is
modelled using synchronous communication by augmenting the state space of the
system with queues. We~show that the first equivalence we consider is strictly
weaker than Tretmans' equivalence and undecidable, whereas the second notion
is incomparable. We~also establish (un)decidability results for these
equivalences.}
}
@article{DG-icomp2006,
  publisher = {Elsevier Science Publishers},
  journal = {Information and Computation},
  author = {Diekert, Volker and Gastin, Paul},
  title = {Pure future local temporal logics are expressively complete for 
                   {M}azurkiewicz traces},
  pages = {1597-1619},
  year = 2006,
  month = nov,
  volume = 204,
  number = 11,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-icomp06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-icomp06.pdf},
  doi = {10.1016/j.ic.2006.07.002},
  abstract = {The paper settles a long standing problem for Mazurkiewicz
traces: the pure future local temporal logic defined with the basic modalities
exists-next and until is expressively complete. This means every first-order
definable language of Mazurkiewicz traces can be defined in a pure future
local temporal logic. The~analogous result with a global interpretation has
been known, but the treatment of a local interpretation turned out to be much
more involved. Local logics are interesting because both the satisfiability
problem and the model checking problem are solvable in PSPACE for these logics
whereas they are non-elementary for global logics. Both, the (previously
known) global and the (new) local results generalize Kamp's Theorem for words,
because for sequences local and global viewpoints coincide. }
}
@article{DG06-TCS,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Diekert, Volker and Gastin, Paul},
  title = {From local to global temporal logics over {M}azurkiewicz traces},
  year = 2006,
  month = may,
  volume = 356,
  number = {1-2},
  pages = {126-135},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG06-TCS.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG06-TCS.pdf},
  doi = {10.1016/j.tcs.2006.01.035},
  abstract = {We review some results on global and local temporal logic on
Mazurkiewicz traces. Our~main contribution is to show how to derive the
expressive completeness of global temporal logic with respect to first-order
logic [V.~Diekert, P.~Gastin, LTL~is expressively complete for Mazurkiewicz
traces, J.~Comput. System Sci.~64 (2002) 396-418] from the similar result on
local temporal logic [V.~Diekert, P.~Gastin, Pure future local temporal logics
are expressively complete for Mazurkiewicz traces, in: M.~Farach-Colton~(Ed.),
Proc.~LATIN'04, Lecture Notes in Computer Science, Vol.~2976, Springer,
Berlin, 2004, pp.~232-241, Full version available as Research Report
LSV-05-22, Laboratoire Sp\'ecification et V\'erification, ENS Cachan, France].}
}
@inproceedings{ABG-fsttcs07,
  address = {New~Delhi, India},
  month = dec,
  year = 2007,
  volume = 4855,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Arvind, V. and Prasad, Sanjiva},
  acronym = {{FSTTCS}'07},
  booktitle = {{P}roceedings of the 27th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'07)},
  author = {Akshay, S. and Bollig, Benedikt and Gastin, Paul},
  title = {Automata and Logics for Timed Message Sequence Charts},
  pages = {290-302},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABG-fsttcs07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABG-fsttcs07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ABG-fsttcs07.ps},
  doi = {10.1007/978-3-540-77050-3_24},
  abstract = {We provide a framework for distributed systems that impose timing constraints 
    on their executions. We~propose a timed model of communicating finite-state machines, 
    which communicate by exchanging messages through channels and use event clocks to 
    generate collections of timed message sequence charts~(T-MSCs). As~a specification 
    language, we~propose a monadic second-order logic equipped with timing predicates and 
    interpreted over~T-MSCs. We establish expressive equivalence of our automata and logic. 
    Moreover, we prove that, for (existentially) bounded channels, emptiness and 
    satisfiability are decidable for our automata and logic.}
}
@inproceedings{BGMN-fct07,
  address = {Budapest, Hungary},
  month = aug,
  year = 2007,
  volume = 4639,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Csuhaj-Varj{\'u}, Erzs{\'e}bet and {\'E}sik, Zolt{\'a}n},
  acronym = {{FCT}'07},
  booktitle = {{P}roceedings of the 16th {I}nternational {S}ymposium
	  on {F}undamentals of {C}omputation {T}heory
	  ({FCT}'07)},
  author = {Bhateja, Puneet and Gastin, Paul and Mukund, Madhavan and Narayan
                  Kumar, K.},
  title = {Local testing of message sequence charts is difficult},
  pages = {76-87},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGMN-fct07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGMN-fct07.pdf},
  doi = {10.1007/978-3-540-74240-1_8},
  abstract = {Message sequence charts are an attractive visual formalism used
    to specify distributed communicating systems. One~way to test such a
    system is to substitute a component by a test process and observe its
    interaction with the rest of the system. We~study the question of whether
    we can characterize the distributed behaviour of the system based on such
    local observations. The~main difficulty is that local observations can
    combine in unexpected ways to define implied scenarios not present in the
    original specification. It~is known that checking whether a scenario
    specification is closed with respect to implied scenarios is undecidable
    when observations are made one process at a time, even for regular
    specifications. We~show that this undecidability holds even if we have
    only two processes in the system. We then strengthen the observer to be
    able to observe multiple processes simultaneously. Even in this stronger
    framework, the problem remains undecidable. In~fact, undecidability
    continues to hold even without message labels, provided we observe two or
    more processes simultaneously. On~the other hand, if we do not have
    message labels and we restrict observations to one process at a time, the
    problem of checking for implied scenarios is decidable.}
}
@inproceedings{GM-spin07,
  address = {Berlin, Germany},
  month = jul,
  year = 2007,
  volume = 4595,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Bo{\v{s}}nacki, Dragan and Edelkamp, Stefan},
  acronym = {{SPIN}'07},
  booktitle = {{P}roceedings of the 14th {I}nternational
               {SPIN} {W}orkshop on {M}odel {C}hecking {S}oftware
               ({SPIN}'07)},
  author = {Gastin, Paul and Moro, Pierre},
  title = {Minimal counter-example generation for {SPIN}},
  pages = {24-38},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GM-spin07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GM-spin07.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GM-spin07.ps},
  doi = {10.1007/978-3-540-73370-6_4},
  abstract = {In this paper, we propose an algorithm to compute a counter-example of
  minimal size to some property in a finite state program, using the same
  programmation constraints than~SPIN. This algorithm uses nested
  Breadth-first searches guided by priority queues.
  This algorithm works in quadratic time and is linear in memory.}
}
@misc{versydis-final,
  author = {Gastin, Paul and others},
  title = {{ACI} {S}{\'e}curit{\'e} {I}nformatique {VERSYDIS}~--- 
            Rapport final},
  year = 2006,
  month = oct,
  type = {Contract Report},
  note = {10~pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Versydis-final.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Versydis-final.pdf}
}
@article{GK-fi07,
  publisher = {{IOS} Press},
  journal = {Fundamenta Informaticae},
  author = {Gastin, Paul and Kuske, Dietrich},
  title = {Uniform satisfiability in {PSPACE} for local temporal logics
	  over {M}azurkiewicz traces},
  volume = 80,
  number = {1-3},
  pages = {169-197},
  year = 2007,
  month = nov,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GK-fi07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GK-fi07.pdf},
  abstract = {We study the complexity of temporal logics over
  concurrent systems that can be described by Mazurkiewicz traces. We
  develop a general method to prove that the uniform satisfiability
  problem of local temporal logics is in~PSPACE. We~also
  demonstrate that this method applies to all known local temporal
  logics.}
}
@article{BGP-fmsd07,
  publisher = {Springer},
  journal = {Formal Methods in System Design},
  author = {B{\'e}rard, B{\'e}atrice and Gastin, Paul and Petit,
                  Antoine},
  title = {Timed substitutions for regular signal-event languages},
  volume = 31,
  number = 2,
  pages = {101-134},
  year = 2007,
  month = oct,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP-fmsd07.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP-fmsd07.pdf},
  doi = {10.1007/s10703-007-0034-5},
  abstract = {In the classical framework of formal languages, a refinement
   operation is modeled by a substitution and an abstraction by an inverse
   substitution. These mechanisms have been widely studied, because they
   describe a change in the specification level, from an abstract view to a
   more concrete one, or conversely. For timed systems, there is up to now no
   uniform notion of substitution. In~this paper, we~study timed substitutions
   in the general framework of signal-event languages, where both signals and
   events are taken into account. We prove that regular signal-event languages
   are closed under substitution and inverse substitution.\par
   To obtain these results, we use in a crucial way a {"}well known{"} result:
   regular signal-event languages are closed under intersection. In fact,
   while this result is indeed easy for languages defined by Alur and Dill's
   timed automata, it turns out that the construction is much more tricky when
   considering the most involved model of signal-event automata. We give here
   a construction working on finite and infinite signal-event words and taking
   into account signal stuttering, unobservability of zero-duration \(\tau\)-signals
   and Zeno runs. Note that if several constructions have been proposed in
   particular cases, it is the first time that a general construction is
   provided.}
}
@article{DrGa06tocsys,
  publisher = {Springer},
  journal = {Theory of Computing Systems},
  author = {Droste, Manfred and Gastin, Paul},
  title = {On aperiodic and star-free formal power series in
              partially commuting variables},
  year = 2008,
  month = may,
  volume = 42,
  number = 4,
  pages = {608-631},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/
		rr-lsv-2005-12.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/
		rr-lsv-2005-12.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
		rr-lsv-2005-12.ps},
  doi = {10.1007/s00224-007-9064-z},
  abstract = {Formal power series over non-commuting variables have been
    investigated as representations of the behavior of automata with
    multiplicities. Here we introduce and investigate the concepts of
    aperiodic and of star-free formal power series over semirings and
    partially commuting variables. We prove that if the semiring~\(K\) is
    idempotent and commutative, or if \(K\) is idempotent and the variables
    are non-commuting, then the product of any two aperiodic series is again
    aperiodic. We also show that if \(K\) is idempotent and the matrix monoids
    over~\(K\) have a Burnside property (satisfied, \textit{e.g.}~by the
    tropical semiring), then the aperiodic and the star-free series coincide.
    This generalizes a classical result of Sch{\"u}tzenberger~(1961) for
    aperiodic regular languages and subsumes a result of Guaiana, Restivo and
    Salemi~(1992) on aperiodic trace languages. }
}
@article{DrGa07tcs,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Droste, Manfred and Gastin, Paul},
  title = {Weighted automata and weighted logics},
  year = 2007,
  month = jun,
  volume = 380,
  number = {1-2},
  pages = {69-86},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/
		rr-lsv-2005-13.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/
		rr-lsv-2005-13.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
		rr-lsv-2005-13.ps},
  doi = {10.1016/j.tcs.2007.02.055},
  abstract = {Weighted automata are used to describe quantitative properties
                  in various areas such as probabilistic systems, image
                  compression, speech-to-text processing. The~behaviour of
                  such an automaton is a mapping, called a formal power
                  series, assigning to each word a weight in some semiring. 
		  We~generalize B{\"u}chi's and Elgot's fundamental theorems to this
                  quantitative setting. We~introduce a weighted version of MSO
                  logic and prove that, for commutative semirings, the
                  behaviours of weighted automata are precisely the formal
                  power series definable with particular sentences of our
                  weighted logic. We~also consider weighted first-order logic
                  and show that aperiodic series coincide with the first-order
                  definable ones, if the semiring is locally finite,
                  commutative and has some aperiodicity property.},
  oldnote = {Special issue of ICALP'05. To appear. 
               Also available as Research Report LSV-05-13, 
               Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, 
               France, July 2005.}
}
@misc{dots-3.1,
  author = {Bollig, Benedikt and Bouyer, Patricia and Cassez, Franck and
                  Chatain, {\relax Th}omas and Gastin, Paul and Haddad, Serge
                  and Jard, Claude},
  title = {Model for distributed timed systems},
  howpublished = {Deliverable DOTS~3.1 (ANR-06-SETI-003)},
  year = 2008,
  month = sep
}
@incollection{DG-hwa08,
  year = 2009,
  series = {EATCS Monographs in Theoretical Computer Science},
  publisher = {Springer},
  editor = {Kuich, Werner and Vogler, Heiko and Droste, Manfred},
  booktitle = {Handbook of Weighted Automata},
  author = {Droste, Manfred and Gastin, Paul},
  title = {Weighted automata and weighted logics},
  pages = {175-211},
  chapter = 5,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-hwa08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-hwa08.pdf}
}
@incollection{DG-pct08,
  futureaddress = {},
  month = jan,
  year = 2009,
  series = {IARCS-Universities},
  publisher = {Universities Press},
  booktitle = {Perspectives in Concurrency Theory},
  editor = {Lodaya, Kamal and Mukund, Madhavan and
		 Ramanujam, R.},
  author = {Diekert, Volker and Gastin, Paul},
  title = {Local safety and local liveness for distributed systems},
  pages = {86-106},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-pct08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-pct08.pdf},
  abstract = {We introduce local safety and local liveness for distributed
    systems whose executions are modeled by Mazurkiewicz traces. We
    characterize local safety by local closure and local liveness by local
    density. Restricting to first-order definable properties, we prove a
    decomposition theorem in the spirit of the separation theorem for linear
    temporal logic. We then characterize local safety and local liveness by
    means of canonical local temporal logic formulae.}
}
@inproceedings{ABGMN-concur08,
  address = {Toronto, Canada},
  month = aug,
  year = 2008,
  volume = 5201,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {van Breugel, Franck and Chechik, Marsha},
  acronym = {{CONCUR}'08},
  booktitle = {{P}roceedings of the 19th 
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'08)},
  author = {Akshay, S. and Bollig, Benedikt and Gastin, Paul and Mukund,
                  Madhavan and Narayan Kumar, K.},
  title = {Distributed Timed Automata with Independently Evolving
                  Clocks},
  pages = {82-97},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABGMN-concur08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABGMN-concur08.pdf},
  doi = {10.1007/978-3-540-85361-9_10},
  abstract = { We propose a model of distributed timed systems where each 
component is a timed automaton with a set of local clocks that evolve at a 
rate independent of the clocks of the other components. A clock can be 
read by any component in the system, but it can only be reset by the 
automaton it belongs to.\par
There are two natural semantics for such systems. The \emph{universal} 
semantics captures behaviors that hold under any choice of clock rates for 
the individual components. This is a natural choice when checking that a 
system always satisfies a positive specification. However, to check if a 
system avoids a negative specification, it is better to use the 
\emph{existential} semantics---the set of behaviors that the system can 
possibly exhibit under some choice of clock rates.\par
We show that the existential semantics always describes a regular set of 
behaviors. However, in the case of universal semantics, checking emptiness 
turns out to be undecidable. As an alternative to the universal semantics, 
we propose a \emph{reactive} semantics that allows us to check positive 
specifications and yet describes a regular set of behaviors. }
}
@article{DGK-ijfcs08,
  publisher = {World Scientific},
  journal = {International Journal of Foundations of Computer Science},
  author = {Diekert, Volker and Gastin, Paul and Kufleitner, 
		 Manfred},
  title = {A Survey on Small Fragments of First-Order Logic over 
		 Finite Words},
  volume = 19,
  number = 3,
  pages = {513-548},
  year = 2008,
  month = jun,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DGK-ijfcs08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DGK-ijfcs08.pdf},
  doi = {10.1142/S0129054108005802},
  abstract = {We consider fragments of first-order logic over finite
	words. In~particular, we~deal with 
	first-order logic with a restricted number of 
	variables and with the lower levels of the 
	alternation hierarchy. We~use the algebraic 
	approach to show decidability of 
	expressibility within these fragments. As~a 
	byproduct, we~survey several characterizations 
	of the respective fragments.  We~give complete 
	proofs for all characterizations and we 
	provide all necessary background.  Some of the 
	proofs seem to be new and simpler than those 
	which can be found elsewhere. We also give a 
	proof of Simon's theorem on factorization 
	forests restricted to aperiodic monoids 
	because this is simpler and sufficient for our 
	purpose.}
}
@unpublished{PG-algo,
  author = {Gastin, Paul},
  title = {Algorithmique},
  year = {2007},
  month = nov,
  note = {Course notes, {M}agist{\`e}re STIC, ENS Cachan, France}
}
@unpublished{PG-languages,
  author = {Gastin, Paul},
  title = {Langages formels},
  year = {2007},
  month = may,
  note = {Course notes, {M}agist{\`e}re STIC, ENS Cachan, France}
}
@misc{ltl2ba-v1.1,
  author = {Gastin, Paul and Oddoux, Denis},
  title = {LTL2BA~v1.1},
  year = {2007},
  month = aug,
  nohowpublished = {Available at http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/},
  note = {Written in~C++ (about 4000 lines)},
  note-fr = {\'Ecrit en~C++ (environ 4000 lignes)},
  url = {http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/}
}
@misc{gastex-v2.8,
  author = {Gastin, Paul},
  title = {Gas{{\TeX}}: Graphs and Automata Simplified in~{{\TeX}} (v2.8)},
  year = {2006},
  month = nov,
  nohowpublished = {Available at http://www.lsv.ens-cachan.fr/~gastin/gastex/gastex.html},
  note = {Written in~\TeX (about 2000 lines)},
  note-fr = {\'Ecrit en~\TeX (environ 2000 lignes)},
  url = {http://www.lsv.ens-cachan.fr/~gastin/gastex/gastex.html}
}
@incollection{DiGa08Thomas,
  author = {Diekert, Volker and Gastin, Paul},
  title = {First-order definable languages},
  booktitle = {Logic and Automata: History and Perspectives},
  editor = {Flum, J{\"o}rg and Gr{\"a}del, Erich and Wilke, Thomas},
  publisher = {Amsterdam University Press},
  series = {Texts in Logic and Games},
  volume = 2,
  year = 2008,
  pages = {261-306},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-WT08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-WT08.pdf},
  abstract = {We give an essentially self-contained presentation of some principal
    results for first-order definable languages over finite and infinite
    words.  We~introduce the notion of a \emph{counter-free} B{\"u}chi
    automaton; and we relate counter-freeness to \emph{aperiodicity}
    and to the notion of \emph{very weak alternation}.
    We also show that aperiodicity of a regular
    \(\infty\)-language can be decided in polynomial
    space, if the language is specified by some B{\"u}chi automaton.}
}
@misc{dots-2.2,
  author = {Chatain, {\relax Th}omas and Gastin, Paul and Muscholl, Anca
                  and Sznajder, Nathalie and Walukiewicz, Igor and
		  Zeitoun, Marc},
  title = {Distributed control for restricted specifications},
  howpublished = {Deliverable DOTS~2.2 (ANR-06-SETI-003)},
  year = 2009,
  month = mar
}
@inproceedings{BG-dlt09,
  address = {Stuttgart, Germany},
  month = jun # {-} # jul,
  year = 2009,
  volume = {5583},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Diekert, Volker and Nowotka, Dirk},
  acronym = {{DLT}'09},
  booktitle = {{P}roceedings of the 13th {I}nternational
               {C}onference on {D}evelopments in {L}anguage {T}heory
               ({DLT}'09)},
  author = {Bollig, Benedikt and Gastin, Paul},
  title = {Weighted versus Probabilistic Logics},
  pages = {18-38},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BG-dlt09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BG-dlt09.pdf},
  doi = {10.1007/978-3-642-02737-6_2},
  abstract = {While a mature theory around logics such as MSO, LTL, and CTL
    has been developed in the pure boolean setting of finite automata,
    weighted automata lack such a natural connection with (temporal) logic and
    related verification algorithms. In this paper, we will identify weighted
    versions of MSO and CTL that generalize the classical logics and even
    other quantitative extensions such as probabilistic CTL. We establish
    expressiveness results on our logics giving translations from weighted and
    probabilistic CTL into weighted MSO.}
}
@incollection{GMN-pct08,
  futureaddress = {},
  month = jan,
  year = 2009,
  series = {IARCS-Universities},
  publisher = {Universities Press},
  booktitle = {Perspectives in Concurrency Theory},
  editor = {Lodaya, Kamal and Mukund, Madhavan and
		 Ramanujam, R.},
  author = {Gastin, Paul and Mukund, Madhavan and Narayan Kumar, K.},
  title = {Reachability and boundedness in time-constrained {MSC} graphs},
  pages = {157-183},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GMN-pct08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GMN-pct08.pdf},
  abstract = {Channel boundedness is a necessary condition for a
    message-passing system to exhibit regular, finite-state behaviour at the
    global level. For Message Sequence Graphs~(MSGs), the most basic form of
    High-level Message Sequence Charts~(HMSCs), channel boundedness can be
    characterized in terms of structural conditions on the underlying graph.
    We consider MSGs enriched with timing constraints between events. These
    constraints restrict the global behaviour and can impose channel
    boundedness even when it is not guaranteed by the graph structure of the
    MSG. We~show that we can use MSGs with timing constraints to simulate
    computations of a two-counter machine. As~a consequence, even the more
    fundamental problem of reachability, which is trivial for untimed MSGs,
    becomes undecidable when we add timing constraints. Different forms of
    channel boundedness also then turn out to be undecidable, using reductions
    from the reachability problem.}
}
@article{GSZ-fmsd09,
  publisher = {Springer},
  journal = {Formal Methods in System Design},
  author = {Gastin, Paul and Sznajder, Nathalie and Zeitoun, Marc},
  title = {Distributed synthesis for well-connected
		 architectures},
  volume = 34,
  number = 3,
  pages = {215-237},
  month = jun,
  year = 2009,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GSZ-fmsd09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GSZ-fmsd09.pdf},
  doi = {10.1007/s10703-008-0064-7},
  abstract = {We study the synthesis problem for external linear or branching
    specifications and distributed, synchronous architectures with arbitrary
    delays on processes. External means that the specification only relates
    input and output variables. We introduce the subclass of uniformly
    well-connected (UWC) architectures for which there exists a routing
    allowing each output process to get the values of all inputs it is
    connected to, as soon as possible. We prove that the distributed synthesis
    problem is decidable on UWC architectures if and only if the output
    variables are totally ordered by their knowledge of input variables. We
    also show that if we extend this class by letting the routing depend on
    the output process, then the previous decidability result fails. Finally,
    we provide a natural restriction on specifications under which the whole
    class of UWC architectures is decidable.}
}
@inproceedings{CGS-sofsem09,
  address = {\v{S}pindler\r{u}v Ml\'{y}n, Czech Republic},
  month = jan,
  year = 2009,
  volume = 5404,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Nielsen, Mogens and Ku{\v c}era, Anton{\'\i}n and Bro
                  Miltersen, Peter and Palamidessi, Catuscia and T{\r{u}}ma,
                  Petr and Valencia, Franck},
  acronym = {{SOFSEM}'09},
  booktitle = {{P}roceedings of the 35th International Conference on 
		Current Trends in Theory and Practice of 
		Computer Science ({SOFSEM}'09)},
  author = {Chatain, {\relax Th}omas and Gastin, Paul and Sznajder, Nathalie},
  title = {Natural Specifications Yield Decidability for Distributed
		Synthesis of Asynchronous Systems},
  pages = {141-152},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CGS-sofsem09.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CGS-sofsem09.pdf},
  doi = {10.1007/978-3-540-95891-8_16},
  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.}
}
@inproceedings{AGMN-fsttcs10,
  address = {Chennai, India},
  month = dec,
  year = 2010,
  volume = 8,
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Lodaya, Kamal and Mahajan, Meena},
  acronym = {{FSTTCS}'10},
  booktitle = {{P}roceedings of the 30th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'10)},
  author = {Akshay, S. and Gastin, Paul and Mukund, Madhavan and Narayan Kumar, K.},
  title = {Model checking  time-constrained scenario-based specifications},
  pages = {204-215},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGMN-fsttcs10.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGMN-fsttcs10.pdf},
  doi = {10.4230/LIPIcs.FSTTCS.2010.204},
  abstract = {We consider the problem of model checking message-passing
    systems with real-time requirements. As behavioural specifications, we use
    message sequence charts (MSCs) annotated with timing constraints. Our
    system model is a network of communicating finite state machines with
    local clocks, whose global behaviour can be regarded as a timed automaton.
    Our goal is to verify that all timed behaviours exhibited by the system
    conform to the timing constraints imposed by the specification. In
    general, this corresponds to checking inclusion for timed languages, which
    is an undecidable problem even for timed regular languages. However, we
    show that we can translate regular collections of time-constrained MSCs
    into a special class of event-clock automata that can be determinized and
    complemented, thus permitting an algorithmic solution to the model
    checking problem.}
}
@proceedings{GL-concur10,
  author = {Gastin, Paul and Laroussinie, Fran{\c{c}}ois},
  editor = {Gastin, Paul and Laroussinie, Fran{\c{c}}ois},
  title = {{P}roceedings of the 21st
           {I}nternational {C}onference on
           {C}oncurrency {T}heory
           ({CONCUR}'10)},
  booktitle = {{P}roceedings of the 21st
           {I}nternational {C}onference on
           {C}oncurrency {T}heory
           ({CONCUR}'10)},
  year = 2010,
  month = aug # {-} # sep,
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {6269},
  url = {http://www.springerlink.com/content/978-3-642-15374-7},
  doi = {10.1007/978-3-642-15375-4}
}
@inproceedings{BGMZ-icalp10,
  address = {Bordeaux, France},
  month = jul,
  year = 2010,
  volume = 6199,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Abramsky, Samson and Meyer{ }auf{ }der{ }Heide, Friedhelm
  	    and Spirakis, Paul},
  acronym = {{ICALP}'10},
  booktitle = {{P}roceedings of the 37th {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming ({ICALP}'10)~-- {P}art~{II}},
  author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin 
  	 	 and Zeitoun, Marc},
  title = {Pebble weighted automata and transitive closure logics},
  pages = {587-598},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-icalp10.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-icalp10.pdf},
  doi = {10.1007/978-3-642-14162-1_49},
  abstract = {We introduce new classes of weighted automata on words. Equipped
    with pebbles and a two-way mechanism, they go beyond the class of
    recognizable formal power series, but capture a weighted version of
    first-order logic with bounded transitive closure. In contrast to previous
    work, this logic allows for unrestricted use of universal quantification.
    Our main result states that pebble weighted automata, nested weighted
    automata, and this weighted logic are expressively equivalent. We also
    give new logical characterizations of the recognizable series.}
}
@article{GK-icomp10,
  publisher = {Elsevier Science Publishers},
  journal = {Information and Computation},
  author = {Gastin, Paul and Kuske, Dietrich},
  title = {Uniform satisfiability problem for local temporal logics over
                  {M}azurkiewicz traces},
  volume = 208,
  number = 7,
  month = jul,
  year = 2010,
  pages = {797-816},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/GK-icomp10.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GK-icomp10.pdf},
  doi = {10.1016/j.ic.2009.12.003},
  abstract = {We continue our study of the complexity of MSO-definable local
    temporal logics over concurrent systems that can be described by
    Mazurkiewicz traces. In previous papers, we showed that the satisfiability
    problem for any such logic is in PSPACE (provided the dependence alphabet
    is fixed) and remains in PSPACE for all classical local temporal logics
    even if the dependence alphabet is part of the input. In~this paper, we
    consider the uniform satisfiability problem for arbitrary MSO-definable
    local temporal logics. For this problem, we prove multi-exponential lower
    and upper bounds that depend on the number of alternations of set
    quantifiers present in the chosen MSO-modalities.}
}
@inproceedings{BCGK-fossacs12,
  address = {Tallinn, Estonia},
  month = mar,
  year = 2012,
  volume = 7213,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Birkedal, Lars},
  acronym = {{FoSSaCS}'12},
  booktitle = {{P}roceedings of the 15th {I}nternational
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'12)},
  author = {Bollig, Benedikt and Cyriac, Aiswarya and Gastin, Paul and
                  Narayan Kumar, K.},
  title = {Model Checking Languages of Data Words},
  pages = {391-405},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGK-fossacs12.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGK-fossacs12.pdf},
  doi = {10.1007/978-3-642-28729-9_26},
  abstract = {We consider the model-checking problem for data multi-pushdown
    automata (DMPA). DMPA generate data words, i.e, strings enriched with
    values from an infinite domain. The latter can be used to represent an
    unbounded number of process identifiers so that DMPA are suitable to model
    concurrent programs with dynamic process creation. To specify properties
    of data words, we use monadic second-order (MSO) logic, which comes with a
    predicate to test two word positions for data equality. While
    satisfiability for MSO logic is undecidable (even for weaker fragments
    such as first-order logic), our main result states that one can decide if
    all words generated by a DMPA satisfy a given formula from the full MSO
    logic.}
}
@inproceedings{BCGZ-mfcs11,
  address = {Warsaw, Poland},
  month = aug,
  year = 2011,
  volume = 6907,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Murlak, Filip and Sankowski, Piotr},
  acronym = {{MFCS}'11},
  booktitle = {{P}roceedings of the 36th
               {I}nternational {S}ymposium on
               {M}athematical {F}oundations of 
               {C}omputer {S}cience
               ({MFCS}'11)},
  author = {Bollig, Benedikt and Cyriac, Aiswarya and Gastin, Paul and Zeitoun, Marc},
  title = {Temporal Logics for Concurrent Recursive Programs: Satisfiability
   	    	 and Model Checking},
  pages = {132-144},
  url = {http://hal.archives-ouvertes.fr/hal-00591139/en/},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGZ-mfcs11.pdf},
  doi = {10.1007/978-3-642-22993-0_15},
  abstract = {We develop a general framework for the design of temporal logics
    for concurrent recursive programs. A program execution is modeled as a
    partial order with multiple nesting relations. To specify properties of
    executions, we consider any temporal logic whose modalities are definable
    in monadic second-order logic and that, in addition, allows PDL-like path
    expressions. This captures, in a unifying framework, a wide range of
    logics defined for trees, nested words, and Mazurkiewicz traces that have
    been studied separately. We show that satisfiability and model checking
    are decidable in EXPTIME and 2EXPTIME, depending on the precise path
    modalities.}
}
@techreport{rr-lsv-11-08,
  author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin and
                  Zeitoun, Marc},
  title = {Weighted Expressions and {DFS} Tree Automata},
  institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  year = {2011},
  month = apr,
  type = {Research Report},
  number = {LSV-11-08},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/
        rr-lsv-2011-08.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/
        rr-lsv-2011-08.pdf},
  note = {32~pages},
  abstract = {We introduce weighted expressions, a~calculus to express
    quantitative properties over unranked trees. They involve products and
    sums from a semiring as well as classical boolean formulas. We~show that
    weighted expressions are expressively equivalent to a new class of
    weighted tree-walking automata. This new automata model is equipped with
    pebbles, and follows a depth-first-search policy in the tree.}
}
@incollection{DG-iis09,
  author = {Demri, St{\'e}phane and Gastin, Paul},
  title = {Specification and Verification using Temporal Logics},
  booktitle = {Modern applications of automata theory},
  editor = {D'Souza, Deepak and Shankar, Priti},
  series = {IISc Research Monographs},
  volume = 2,
  publisher = {World Scientific},
  chapter = 15,
  pages = {457-494},
  year = 2012,
  month = jul,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/DG-iis09.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DG-iis09.pdf},
  abstract = {This chapter illustrates two aspects of automata theory related
    to linear-time temporal logic LTL used for the verification of computer
    systems. First, we present a translation from LTL formulae to B{\"u}chi
    automata. The aim is to design an elementary translation which is
    reasonably efficient and produces small automata so that it can be easily
    taught and used by hand on real examples. Our translation is in the spirit
    of the classical tableau constructions but is optimized in several ways.
    Secondly, we recall how temporal operators can be defined from regular
    languages and we explain why adding even a single operator definable by a
    context-free language can lead to undecidability.}
}
@article{ABG-fmsd12,
  publisher = {Springer},
  journal = {Formal Methods in System Design},
  author = {Akshay, S. and Bollig, Benedikt and Gastin, Paul},
  title = {Event-clock Message Passing Automata: A~Logical
           Characterization and an Emptiness-Checking Algorithm},
  year = 2013,
  month = jun,
  volume = 42,
  number = {3},
  pages = {262-300},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABG-fmsd12.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABG-fmsd12.pdf},
  doi = {10.1007/s10703-012-0179-8},
  abstract = {We are interested in modeling behaviors and verifying
    properties of systems in which time and concurrency play a crucial
    role. We introduce a model of distributed automata which are
    equipped with event clocks as in [Alur, Fix,
    Henzinger. Event-clock automata: A~determinizable class of timed
    automata. TCS 211(1-2):253-273, 1999.], which we call Event Clock
    Message Passing Automata (ECMPA). To describe the behaviors of
    such systems we use timed partial orders (modeled as message
    sequence charts with timing).\par
    Our first goal is to extend the classical
    B{\"u}chi-Elgot-Trakhtenbrot equivalence to the timed and
    distributed setting, by showing an equivalence between ECMPA and a
    timed extension of monadic second-order (MSO) logic. We obtain
    such a constructive equivalence in two different ways:
    (1)~by~restricting the semantics by bounding the set of timed
    partial orders (2)~by~restricting the timed MSO logic to its
    existential fragment. We next consider the emptiness problem for
    ECMPA, which asks if a given ECMPA has some valid timed
    execution. In general this problem is undecidable and we show that
    by considering only bounded timed executions, we can obtain
    decidability. We do this by constructing a timed automaton which
    accepts all bounded timed executions of the ECMPA and checking
    emptiness of this timed automaton.}
}
@article{GS-tocl12,
  publisher = {ACM Press},
  journal = {ACM Transactions on Computational Logic},
  author = {Gastin, Paul and Sznajder, Nathalie},
  title = {Fair Synthesis for Asynchronous Distributed Systems},
  nopages = {},
  volume = 14,
  number = {2:9},
  month = jun,
  year = 2013,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/GS-tocl12.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GS-tocl12.pdf},
  doi = {10.1145/2480759.2480761},
  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
    controlled by a sender process and that are immediately received by the
    target process. The fair synthesis problem is to come up with a local
    strategy for each process such that the resulting fair behaviors of the
    system meet a given specification. We consider external specifications
    satisfying some natural closure properties related to the architecture. We
    present this new setting for studying the fair synthesis problem for
    distributed systems, and give decidability results for the subclass of
    networks where communications happen through a strongly connected graph.
    We claim that this framework for distributed synthesis is natural,
    convenient and avoids most of the usual sources of undecidability for the
    synthesis problem. Hence, it may open the way to a decidable theory of
    distributed synthesis.}
}
@article{GS-ipl12,
  publisher = {Elsevier Science Publishers},
  journal = {Information Processing Letters},
  author = {Gastin, Paul and Sznajder, Nathalie},
  title = {Decidability of well-connectedness for distributed synthesis},
  pages = {963-968},
  volume = {112},
  number = {24},
  month = dec,
  year = 2012,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/GS-ipl12.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GS-ipl12.pdf},
  doi = {10.1016/j.ipl.2012.08.018},
  abstract = {Although the synthesis problem is often undecidable for
    distributed, synchronous systems, it becomes decidable for the subclass of
    uniformly well-connected (UWC) architectures, provided that only robust
    specifications are considered. It is then an important issue to be able to
    decide whether a given architecture falls in this class. This is the
    problem addressed in this paper: we establish the decidability and precise
    complexity of checking this property. This problem is in EXPSPACE and
    NP-hard in the general case, but falls into PSPACE when restricted to a
    natural subclass of architectures.}
}
@inproceedings{GM-ciaa12,
  address = {Porto, Portugal},
  month = jul,
  year = 2012,
  volume = {7381},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  editor = {Moreira, Nelma and Reis, Rog{\'e}rio},
  acronym = {{CIAA}'12},
  booktitle = {{P}roceedings of the 17th {I}nternational 
           {C}onference on {I}mplementation and
           {A}pplication of {A}utomata
           ({CIAA}'12)},
  author = {Gastin, Paul and Monmege, Benjamin},
  title = {Adding Pebbles to Weighted Automata},
  pages = {28-51},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/GM-ciaa12.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GM-ciaa12.pdf},
  doi = {10.1007/978-3-642-31606-7_4},
  abstract = {We extend weighted automata and weighted rational expressions
    with 2-way moves and (reusable) pebbles. We show with examples from
    natural language modeling and quantitative model-checking that weighted
    expressions and automata with pebbles are more expressive and allow much
    more natural and intuitive specifications than classical ones.\par
    We extend Kleene-Sch{\"u}tzenberger theorem showing that weighted
    expressions and automata with pebbles have the same expressive power. We
    focus on an efficient translation from expressions to automata.\par
    We also prove that the evaluation problem for weighted automata can be
    done very efficiently if the number of (reusable) pebbles is low.}
}
@inproceedings{BGMZ-atva12,
  address = {Thiruvananthapuram, India},
  month = oct,
  year = {2012},
  volume = {7561},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Mukund, Madhavan and Chakraborty, Supratik},
  acronym = {{ATVA}'12},
  booktitle = {{P}roceedings of the 10th {I}nternational
               {S}ymposium on {A}utomated {T}echnology
               for {V}erification and {A}nalysis
               ({ATVA}'12)},
  author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin and
 	   	    Zeitoun, Marc},
  title = {A Probabilistic {K}leene Theorem},
  pages = {400-415},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-atva12.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-atva12.pdf},
  doi = {10.1007/978-3-642-33386-6_31},
  abstract = {We provide a Kleene Theorem for (Rabin) probabilistic automata
    over finite words. Probabilistic automata generalize deterministic finite
    automata and assign to a word an acceptance probability. We provide
    probabilistic expressions with probabilistic choice, guarded choice,
    concatenation, and a star operator. We prove that probabilistic
    expressions and probabilistic automata are expressively equivalent. Our
    result actually extends to two-way probabilistic automata with pebbles and
    corresponding expressions.}
}
@inproceedings{CGN-concur12,
  address = {Newcastle, UK},
  month = sep,
  year = 2012,
  volume = 7454,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Koutny, Maciej and Ulidowski, Irek},
  acronym = {{CONCUR}'12},
  booktitle = {{P}roceedings of the 23rd
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'12)},
  author = {Cyriac, Aiswarya and Gastin, Paul and Narayan Kumar, K.},
  title = {{MSO} Decidability of Multi-Pushdown Systems via Split-Width},
  pages = {547-561},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/CGN-concur12.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CGN-concur12.pdf},
  doi = {10.1007/978-3-642-32940-1_38},
  abstract = {Multi-threaded programs with recursion are naturally modeled as
    multi-pushdown systems. The behaviors are represented as multiply nested
    words (MNWs), which are words enriched with additional binary relations
    for each stack matching a push operation with the corresponding pop
    operation. Any MNW can be decomposed by two basic and natural operations:
    shuffle of two sequences of factors and merge of consecutive factors of a
    sequence. We say that the split-width of a MNW is~\(k\) if it admits a
    decomposition where the number of factors in each sequence is at most~\(k\).
    The MSO theory of MNWs with split-width~\(k\) is decidable. We introduce two
    very general classes of MNWs that strictly generalize known decidable
    classes and prove their MSO decidability via their split-width and obtain
    comparable or better bounds of tree-width of known classes.}
}
@inproceedings{BGM-fossacs13,
  address = {Rome, Italy},
  month = mar,
  year = 2013,
  volume = {7794},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Pfenning, Frank},
  acronym = {{FoSSaCS}'13},
  booktitle = {{P}roceedings of the 16th {I}nternational
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'13)},
  author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin},
  title = {Weighted Specifications over Nested Words},
  pages = {385-400},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-fossacs13.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-fossacs13.pdf},
  doi = {10.1007/978-3-642-37075-5_25},
  abstract = {This paper studies several formalisms to specify quantitative
    properties of finite nested words (or~equivalently finite unranked trees).
    These can be used for XML documents or recursive programs: for~instance,
    counting how often a given entry occurs in an XML document, or~computing
    the memory required for a recursive program execution. Our main interest
    is to translate these properties, as efficiently as possible, into an
    automaton, and to use this computational device to decide problems related
    to the properties (e.g.,~emptiness, model checking, simulation) or to
    compute the value of a quantitative specification over a given nested
    word. The specification formalisms are weighted regular expressions (with
    forward and backward moves following linear edges or call-return edges),
    weighted first-order logic, and weighted temporal logics. We~introduce
    weighted automata walking in nested words, possibly dropping\slash lifting
    (reusable) pebbles during the traversal. We prove that the evaluation
    problem for such automata can be done very efficiently if the number of
    pebble names is small, and we also consider the emptiness problem.}
}
@inproceedings{AG-fsttcs14,
  address = {New~Dehli, India},
  month = dec,
  year = 2014,
  volume = {29},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Raman, Venkatesh and Suresh, S.~P.},
  acronym = {{FSTTCS}'14},
  booktitle = {{P}roceedings of the 34th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'14)},
  author = {Aiswarya, C. and Gastin, Paul},
  title = {Reasoning about distributed systems: {WYSIWYG}},
  pages = {11-30},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/AG-fsttcs14.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AG-fsttcs14.pdf},
  doi = {10.4230/LIPIcs.FSTTCS.2014.11},
  abstract = {There are two schools of thought on reasoning about distributed
    systems: one~following interleaving based semantics, and one following
    partial-order{{\slash}}graph based semantics. This paper compares these two
    approaches and argues in favour of the latter. An~introductory treatment
    of the split-width technique is also provided.}
}
@inproceedings{BGK-fsttcs14,
  address = {New~Dehli, India},
  month = dec,
  year = 2014,
  volume = {29},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Raman, Venkatesh and Suresh, S.~P.},
  acronym = {{FSTTCS}'14},
  booktitle = {{P}roceedings of the 34th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'14)},
  author = {Bollig, Benedikt and Gastin, Paul and Kumar, Akshay},
  title = {Parameterized Communicating Automata: Complementation and
                  Model Checking},
  pages = {625-637},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGK-fsttcs14.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGK-fsttcs14.pdf},
  doi = {10.4230/LIPIcs.FSTTCS.2014.625},
  abstract = {We study the language-theoretical aspects of parameterized
    communicating automata (PCAs), in which processes communicate via
    rendez-vous. A given PCA can be run on any topology of bounded degree such
    as pipelines, rings, ranked trees, and grids. We show that, under a
    context bound, which restricts the local behavior of each process, PCAs
    are effectively complementable. Complementability is considered a key
    aspect of robust automata models and can, in particular, be exploited for
    verification. In this paper, we use it to obtain a characterization of
    context-bounded PCAs in terms of monadic second-order (MSO) logic. As the
    emptiness problem for context-bounded PCAs is decidable for the classes of
    pipelines, rings, and trees, their model-checking problem wrt. MSO
    properties also becomes decidable. While previous work on model checking
    parameterized systems typically uses temporal logics without next
    operator, our MSO logic allows one to express several natural next
    modalities.}
}
@article{BCGZ-jal14,
  publisher = {Elsevier Science Publishers},
  journal = {Journal of Applied Logic},
  author = {Bollig, Benedikt and Cyriac, Aiswarya and Gastin, Paul and
                  Zeitoun, Marc},
  title = {Temporal logics for concurrent recursive programs:
                  Satisfiability and model checking},
  volume = 12,
  number = 4,
  pages = {395-416},
  month = dec,
  year = 2014,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGZ-jal14.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGZ-jal14.pdf},
  doi = {10.1016/j.jal.2014.05.001},
  abstract = {We develop a general framework for the design of temporal logics
    for concurrent recursive programs. A program execution is modeled as a
    partial order with multiple nesting relations. To specify properties of
    executions, we consider any temporal logic whose modalities are definable
    in monadic second-order logic and which, in addition, allows PDL-like path
    expressions. This captures, in a unifying framework, a wide range of
    logics defined for ranked and unranked trees, nested words, and
    Mazurkiewicz traces that have been studied separately. We show that
    satisfiability and model checking are decidable in EXPTIME and 2EXPTIME,
    depending on the precise path modalities.}
}
@inproceedings{BGS-rp14,
  address = {Oxford, UK},
  month = sep,
  year = 2014,
  volume = {8762},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Ouaknine, Jo{\"e}l and Potapov, Igor and Worrell, James},
  acronym = {{RP}'14},
  booktitle = {{P}roceedings of the 8th {W}orkshop
           on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'14)},
  author = {Bollig, Benedikt and Gastin, Paul and Schubert, Jana},
  title = {Parameterized Verification of Communicating Automata under Context Bounds},
  pages = {45-57},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGS-rp14.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGS-rp14.pdf},
  doi = {10.1007/978-3-319-11439-2_4},
  abstract = {We study the verification problem for parameterized
    communicating automata~(PCA), in which processes synchronize via message
    passing. A~given PCA can be run on any topology of bounded degree (such as
    pipelines, rings, or ranked trees), and communication may take place
    between any two processes that are adjacent in the topology. Parameterized
    verification asks if there is a topology from a given topology class that
    allows for an accepting run of the given PCA. In general, this problem is
    undecidable even for synchronous communication and simple pipeline
    topologies. We therefore consider context-bounded verification, which
    restricts the behavior of each single process. For several variants of
    context bounds, we show that parameterized verification over pipelines,
    rings, and ranked trees is decidable. Our approach is automata-theoretic
    and uniform. We introduce a notion of graph acceptor that identifies those
    topologies allowing for an accepting run. Depending on the given topology
    class, the topology acceptor can then be restricted, or adjusted, so that
    the verification problem reduces to checking emptiness of finite automata
    or tree automata.}
}
@inproceedings{AGN-atva14,
  address = {Sydney, Australia},
  month = nov,
  year = {2014},
  volume = 8837,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Cassez, Franck and Raskin, Jean-Fran{\c{c}}ois},
  acronym = {{ATVA}'14},
  booktitle = {{P}roceedings of the 12th {I}nternational
               {S}ymposium on {A}utomated {T}echnology
               for {V}erification and {A}nalysis
               ({ATVA}'14)},
  author = {Aiswarya, C. and Gastin, Paul and Narayan Kumar, K.},
  title = {Verifying Communicating Multi-pushdown Systems via Split-width},
  pages = {1-17},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGN-atva14.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGN-atva14.pdf},
  doi = {10.1007/978-3-319-11936-6_1},
  abstract = {Communicating multi-pushdown systems model networks of
    multi-threaded recursive programs communicating via reliable FIFO
    channels. We extend the notion of split-width to this setting, improving
    and simplifying the earlier definition. Split-width, while having the same
    power of clique-{{\slash}}tree-width, gives a divide-and-conquer technique
    to prove the bound of a class, thanks to the two basic operations, shuffle
    and merge, of the split-width algebra. We illustrate this technique on
    examples. We also obtain simple, uniform and optimal decision procedures
    for various verification problems parametrised by split-width.}
}
@inproceedings{CGK-concur14,
  address = {Rome, Italy},
  month = sep,
  year = 2014,
  volume = 8704,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Baldan, Paolo and Gorla, Daniele},
  acronym = {{CONCUR}'14},
  booktitle = {{P}roceedings of the 25th
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'14)},
  author = {Cyriac, Aiswarya and Gastin, Paul and Narayan Kumar, K.},
  title = {Controllers for the Verification of Communicating Multi-Pushdown Systems},
  pages = {297-311},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/CGK-concur14.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CGK-concur14.pdf},
  doi = {10.1007/978-3-662-44584-6_21},
  abstract = {Multi-pushdowns communicating via queues are formal models of
    multi-threaded programs communicating via channels. They are turing
    powerful and much of the work on their verification has focussed on
    under-approximation techniques. Any error detected in the
    under-approximation implies an error in the system. However the successful
    verification of the under-approximation is not as useful if the system
    exhibits unverified behaviours. Our aim is to design controllers that
    observe/restrict the system so that it stays within the verified
    under-approximation. We identify some important properties that a good
    controller should satisfy. We consider an extensive under-approximation
    class, construct a distributed controller with the desired properties and
    also establish the decidability of verification problems for this class.}
}
@inproceedings{BGMZ-csllics14,
  address = {Vienna, Austria},
  month = jul,
  year = 2014,
  publisher = {ACM Press},
  acronym = {{CSL\slash LICS}'14},
  booktitle = {{P}roceedings of the Joint Meeting of the 23rd {EACSL} {A}nnual {C}onference on
  	    {C}omputer {S}cience {L}ogic and the 29th {A}nnual {ACM\slash
            IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({CSL\slash LICS}'14)},
  author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin and
                  Zeitoun, Marc},
  title = {Logical Characterization of Weighted Pebble Walking Automata},
  nopages = {},
  chapter = 19,
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-csllics14.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-csllics14.pdf},
  doi = {10.1145/2603088.2603118},
  abstract = {Weighted automata are a conservative quantitative extension of
    finite automata that enjoys applications, e.g., in language processing and
    speech recognition. Their expressive power, however, appears to be
    limited, especially when they are applied to more general structures than
    words, such as graphs. To address this drawback, weighted automata have
    recently been generalized to weighted pebble walking automata, which
    proved useful as a tool for the specification and evaluation of
    quantitative properties over words and nested words. In this paper, we
    establish the expressive power of weighted pebble walking automata in
    terms of transitive closure logic, lifting a similar result by Engelfriet
    and Hoogeboom from the Boolean case to a quantitative setting. This result
    applies to general classes of graphs, including all the aforementioned
    classes.}
}
@article{ABGMN-fi13,
  publisher = {{IOS} Press},
  journal = {Fundamenta Informaticae},
  author = {Akshay, S. and Bollig, Benedikt and Gastin, Paul and 
  	   	    Mukund, Madhavan and Narayan Kumar, K.},
  title = {Distributed Timed Automata with Independently Evolving Clocks},
  volume = {130},
  number = {4},
  month = apr,
  year = 2014,
  pages = {377-407},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGMN-fi13.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGMN-fi13.pdf},
  doi = {10.3233/FI-2014-996},
  abstract = {We propose a model of distributed timed systems where each
    component is a timed automaton with a set of local clocks that evolve at a
    rate independent of the clocks of the other components. A~clock can be
    read by any component in the system, but it can only be reset by the
    automaton it belongs~to.\par
    There are two natural semantics for such systems. The \emph{universal}
    semantics captures behaviors that hold under any choice of clock rates for
    the individual components. This is a natural choice when checking that a
    system always satisfies a positive specification. To check if a system
    avoids a negative specification, it is better to use the
    \emph{existential} semantics—the set of behaviors that the system
    can possibly exhibit under some choice of clock rates.\par
    We show that the existential semantics always describes a regular set of
    behaviors. However, in the case of universal semantics, checking emptiness
    or universality turns out to be undecidable. As an alternative to the
    universal semantics, we propose a \emph{reactive} semantics that allows us
    to check positive specifications and yet describes a regular set of
    behaviors.}
}
@article{BGMZ-tocl13,
  publisher = {ACM Press},
  journal = {ACM Transactions on Computational Logic},
  author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin and Zeitoun, Marc},
  title = {Pebble Weighted Automata and Weighted Logics},
  volume = 15,
  number = {2:15},
  month = apr,
  year = 2014,
  nopages = {},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-tocl13.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-tocl13.pdf},
  doi = {10.1145/2579819},
  abstract = {We introduce new classes of weighted automata on words. Equipped
    with pebbles, they go beyond the class of recognizable formal power
    series: they capture weighted first-order logic enriched with a
    quantitative version of transitive closure. In contrast to previous work,
    this calculus allows for unrestricted use of existential and universal
    quantifications over positions of the input word. We actually consider
    both two-way and one-way pebble weighted automata. The latter class
    constrains the head of the automaton to walk left-to-right, resetting it
    each time a pebble is dropped. Such automata have already been considered
    in the Boolean setting, in the context of data words. Our main result
    states that two-way pebble weighted automata, one-way pebble weighted
    automata, and our weighted logic are expressively equivalent. We also give
    new logical characterizations of standard recognizable series.}
}
@article{GM-tcs14,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Gastin, Paul and Monmege, Benjamin},
  title = {Adding Pebbles to Weighted Automata~-- Easy Specification
                  {\&} Efficient Evaluation},
  volume = {534},
  month = may,
  year = 2014,
  pages = {24-44},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/GM-tcs14.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GM-tcs14.pdf},
  doi = {10.1016/j.tcs.2014.02.034},
  abstract = {We extend weighted automata and weighted rational expressions
    with 2-way moves and reusable pebbles. We show with examples from natural
    language modeling and quantitative model-checking that weighted
    expressions and automata with pebbles are more expressive and allow much
    more natural and intuitive specifications than classical ones. We extend
    Kleene-Sch{\"u}tzenberger theorem showing that weighted expressions and
    automata with pebbles have the same expressive power. We focus on an
    efficient translation from expressions to automata. We also prove that the
    evaluation problem for weighted automata can be done very efficiently if
    the number of reusable pebbles is low.}
}
@article{AGMN-tcs15,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Akshay, S. and Gastin, Paul and Mukund, 
                 Madhavan and Kumar, K. Narayan},
  title = {Checking conformance for time-constrained scenario-based specifications},
  volume = {594},
  pages = {24-43},
  month = aug,
  year = {2015},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGMN-tcs15.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGMN-tcs15.pdf},
  doi = {10.1016/j.tcs.2015.03.030},
  abstract = {We consider the problem of model checking message-passing
    systems with real-time requirements. As behavioral specifications, we use
    message sequence charts (MSCs) annotated with timing constraints. Our
    system model is a network of communicating finite state machines with
    local clocks, whose global behavior can be regarded as a timed automaton.
    Our goal is to verify that all timed behaviors exhibited by the system
    conform to the timing constraints imposed by the specification. In
    general, this corresponds to checking inclusion for timed languages, which
    is an undecidable problem even for timed regular languages. However, we
    show that we can translate regular collections of time-constrained MSCs
    into a special class of event-clock automata that can be determinized and
    complemented, thus permitting an algorithmic solution to the model
    checking/conformance problem.}
}
@inproceedings{ABG-concur15,
  address = {Madrid, Spain},
  month = sep,
  year = 2015,
  volume = {42},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Aceto, Luca and de Frutos-Escrig, David},
  acronym = {{CONCUR}'15},
  booktitle = {{P}roceedings of the 26th
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'15)},
  author = {Aiswarya, C. and Bollig, Benedikt and Gastin, Paul},
  title = {An Automata-Theoretic Approach to the Verification of Distributed Algorithms},
  pages = {340-353},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABG-concur15.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABG-concur15.pdf},
  doi = {10.4230/LIPIcs.CONCUR.2015.340},
  abstract = {We introduce an automata-theoretic method for the verification
    of distributed algorithms running on ring networks. In a distributed
    algorithm, an arbitrary number of processes cooperate to achieve a common
    goal (e.g., elect a leader). Processes have unique identifiers (pids) from
    an infinite, totally ordered domain. An algorithm proceeds in synchronous
    rounds, each round allowing a process to perform a bounded sequence of
    actions such as send or receive a pid, store it in some register, and
    compare register contents wrt. the associated total order. An algorithm is
    supposed to be correct independently of the number of processes. To
    specify correctness properties, we introduce a logic that can reason about
    processes and pids. Referring to leader election, it may say that, at the
    end of an execution, each process stores the maximum pid in some dedicated
    register. Since the verification of distributed algorithms is undecidable,
    we propose an underapproximation technique, which bounds the number of
    rounds. This is an appealing approach, as the number of rounds needed by a
    distributed algorithm to conclude is often exponentially smaller than the
    number of processes. We provide an automata-theoretic solution, reducing
    model checking to emptiness for alternating two-way automata on words.
    Overall, we show that round-bounded verification of distributed algorithms
    over rings is PSPACE-complete.}
}
@inproceedings{AGS-concur16,
  address = {Qu{\'e}bec City, Canada},
  month = aug,
  year = 2016,
  volume = {59},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Desharnais, Jos{\'e}e and Jagadeesan, Radha},
  acronym = {{CONCUR}'16},
  booktitle = {{P}roceedings of the 27th
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'16)},
  author = {Akshay, S. and Paul Gastin and Krishna, Shankara Narayanan},
  title = {Analyzing Timed Systems Using Tree Automata},
  pages = {27:1-27:14},
  url = {http://arxiv.org/abs/1604.08443},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGS-concur16.pdf},
  doi = {10.4230/LIPIcs.CONCUR.2016.27},
  abstract = {Timed systems, such as timed automata, are usually analyzed
    using their operational semantics on timed words. The classical region
    abstraction for timed automata reduces them to (untimed) finite state
    automata with the same time-abstract properties, such as state
    reachability. We propose a new technique to analyze such timed systems
    using finite tree automata instead of finite word automata. The main idea
    is to consider timed behaviors as graphs with matching edges capturing
    timing constraints. Such graphs can be interpreted in trees opening the
    way to tree automata based techniques which are more powerful than
    analysis based on word automata. The technique is quite general and
    applies to many timed systems. In this paper, as an example, we develop
    the technique on timed pushdown systems, which have recently received
    considerable attention. Further, we also demonstrate how we can use it on
    timed automata and timed multi-stack pushdown systems (with boundedness
    restrictions).}
}
@comment{{B-arxiv16,
  author =		Bollig, Benedikt, 
  affiliation = 	aff-LSVmexico,
  title =    		One-Counter Automata with Counter Visibility, 
  institution = 	Computing Research Repository, 
  number =    		1602.05940, 
  month = 		feb, 
  nmonth =     		2,
  year = 		2016, 
  type = 		RR, 
  axeLSV = 		mexico,
  NOcontrat = 		"",
  
  url =			http://arxiv.org/abs/1602.05940, 
  PDF =			"http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf",
  lsvdate-new =  	20160222,
  lsvdate-upd =  	20160222,
  lsvdate-pub =  	20160222,
  lsv-category = 	"rapl",
  wwwpublic =    	"public and ccsb",
  note = 		18~pages, 

  abstract = "In a one-counter automaton (OCA), one can read a letter
    from some finite alphabet, increment and decrement the counter by
    one, or test it for zero. It is well-known that universality and
    language inclusion for OCAs are undecidable. We consider here OCAs
    with counter visibility: Whenever the automaton produces a letter,
    it outputs the current counter value along with~it. Hence, its
    language is now a set of words over an infinite alphabet. We show
    that universality and inclusion for that model are in PSPACE, thus
    no harder than the corresponding problems for finite automata, which
    can actually be considered as a special case. In fact, we show that
    OCAs with counter visibility are effectively determinizable and
    closed under all boolean operations. As~a~strict generalization, we
    subsequently extend our model by registers. The general nonemptiness
    problem being undecidable, we impose a bound on the number of
    register comparisons and show that the corresponding nonemptiness
    problem is NP-complete.",
}}
@inproceedings{FG-fossacs16,
  address = {Eindhoven, The~Netherlands},
  month = apr,
  year = 2016,
  volume = {9634},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Jacobs, Bart and L{\"o}ding, Christof},
  acronym = {{FoSSaCS}'16},
  booktitle = {{P}roceedings of the 19th {I}nternational
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'16)},
  author = {Fortin, Marie and Gastin, Paul},
  title = {Verification of parameterized communicating automata via split-width},
  pages = {197-213},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/FG-fossacs16.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FG-fossacs16.pdf},
  doi = {10.1007/978-3-662-49630-5_12},
  abstract = {We~study verification problems for distributed systems
    communicating via unbounded FIFO channels. The number of processes
    of the system as well as the communication topology are not fixed
    a~priori. Systems are given by parameterized communicating automata
    (PCAs) which can be run on any communication topology of bounded
    degree, with arbitrarily many processes. Such systems are Turing
    powerful so we concentrate on under-approximate verification. We
    extend the notion of split-width to behaviors of PCAs. We show that
    emptiness, reachability and model-checking problems of PCAs are
    decidable when restricted to behaviors of bounded split-width.
    Reachability and emptiness are EXPTIME-complete, but only polynomial
    in the size of the PCA. We also describe several concrete classes of
    bounded split-width, for which we prove similar results.}
}
@inproceedings{BFG-stacs18,
  address = {Caen, France},
  month = feb,
  volume = {96},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Niedermeier, Rolf and Vall{\'e}e, Brigitte},
  acronym = {{STACS}'18},
  booktitle = {{P}roceedings of the 35th {A}nnual
               {S}ymposium on {T}heoretical {A}spects of
               {C}omputer {S}cience
               ({STACS}'18)},
  author = {Bollig, Benedikt and Fortin, Marie and Gastin, Paul},
  title = {Communicating Finite-State Machines and Two-Variable Logic},
  pages = {17:1-17:14},
  year = {2018},
  doi = {10.4230/LIPIcs.STACS.2018.17},
  pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/8529/pdf/LIPIcs-STACS-2018-17.pdf},
  url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=8529},
  abstract = {Communicating finite-state machines are a fundamental, well-studied model of finite-state processes that communicate via unbounded first-in first-out channels. We show that they are expressively equivalent to existential MSO logic with two first-order variables and the order relation.}
}
@inproceedings{AGKS-concur17,
  address = {Berlin, Germany},
  month = sep,
  year = 2017,
  volume = {85},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Meyer, Roland and Nestmann, Uwe},
  acronym = {{CONCUR}'17},
  booktitle = {{P}roceedings of the 28th
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'17)},
  author = {Akshay, S. and Gastin, Paul and Krishna, Shankara Narayanan and Sarkar, Ilias},
  title = {Towards an Efficient Tree Automata based technique for Timed Systems},
  pages = {39:1--39:15},
  url = {http://drops.dagstuhl.de/opus/volltexte/2017/7801},
  pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/7801/pdf/LIPIcs-CONCUR-2017-39.pdf},
  doi = {10.4230/LIPIcs.CONCUR.2017.39},
  abstract = {The focus of this paper is the analysis of real-time systems with recursion, through the development of good theoretical techniques which are implementable. Time is modeled using clock variables, and recursion using stacks. Our technique consists of modeling the behaviours of the timed system as graphs, and interpreting these graphs on tree terms by showing a bound on their tree-width. We then build a tree automaton that accepts exactly those tree terms that describe realizable runs of the timed system. The emptiness of the timed system thus boils down to emptiness of a finite tree automaton that accepts these tree terms. This approach helps us in obtaining an optimal complexity, not just in theory (as done in earlier work e.g.[concur16]), but also in going towards an efficient implementation of our technique. To do this, we make several improvements in the theory and exploit these to build a first prototype tool that can analyze timed systems with recursion.}
}
@article{ABG-ic17,
  publisher = {Elsevier Science Publishers},
  journal = {Information and Computation},
  author = {Aiswarya, C. and Bollig, Benedikt and Gastin, Paul},
  title = {An Automata-Theoretic Approach to the Verification of Distributed Algorithms},
  volume = {259},
  month = apr,
  year = {2018},
  pages = {305-327},
  doi = {10.1016/j.ic.2017.05.006},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABG-ic17.pdf},
  abstract = {We introduce an automata-theoretic method for the verification of distributed algorithms running on ring networks. In a distributed algorithm, an arbitrary number of processes cooperate to achieve a common goal (e.g., elect a leader). Processes have unique identifiers (pids) from an infinite, totally ordered domain. An algorithm proceeds in synchronous rounds, each round allowing a process to perform a bounded sequence of actions such as send or receive a pid, store it in some register, and compare register contents wrt. the associated total order. An algorithm is supposed to be correct independently of the number of processes. To specify correctness properties, we introduce a logic that can reason about processes and pids. Referring to leader election, it may say that, at the end of an execution, each process stores the maximum pid in some dedicated register.
 
We show that the verification problem of distributed algorithms can be reduced to satisfiability of a formula from propositional dynamic logic with loop and converse (LCPDL), interpreted over grids over a finite alphabet. This translation is independent of any restriction imposed on the algorithm. However, since the verification problem (and satisfiability for LCPDL) is undecidable, we propose an underapproximation technique, which bounds the number of rounds. This is an appealing approach, as the number of rounds needed by a distributed algorithm to conclude is often exponentially smaller than the number of processes. Using our reduction to LCPDL, we provide an automata-theoretic solution, reducing model checking to emptiness for alternating two-way automata on words. Overall, we show that round-bounded verification of distributed algorithms over rings is PSPACE-complete, provided the number of rounds is given in unary.}
}
@inproceedings{GMS-concur18,
  address = {Beijing, China},
  month = sep,
  year = 2018,
  volume = {118},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Schewe, Sven and Zhang, Lijun},
  acronym = {{CONCUR}'18},
  booktitle = {{P}roceedings of the 29th
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'18)},
  author = {Paul Gastin and Sayan Mukherjee and B. Srivathsan},
  title = {Reachability in timed automata with diagonal constraints},
  pages = {28:1-28:17},
  url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9566},
  pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/9566/pdf/LIPIcs-CONCUR-2018-28.pdf},
  doi = {10.4230/LIPIcs.CONCUR.2018.28},
  abstract = {We consider the reachability problem for timed automata having diagonal constraints (like x - y < 5) as guards in transitions. The best algorithms for timed automata proceed by enumerating reachable sets of its configurations, stored in a data structure called ''zones''. Simulation relations between zones are essential to ensure termination and efficiency. The algorithm employs a simulation test Z <= Z' which ascertains that zone Z does not reach more states than zone Z', and hence further enumeration from Z is not necessary. No effective simulations are known for timed automata containing diagonal constraints as guards. We propose a simulation relation <=_{LU}^d for timed automata with diagonal constraints. On the negative side, we show that deciding Z not <=_{LU}^d Z' is NP-complete. On the positive side, we identify a witness for Z not <=_{LU}^d Z' and propose an algorithm to decide the existence of such a witness using an SMT solver. The shape of the witness reveals that the simulation test is likely to be efficient in practice.}
}
@inproceedings{BFG-concur18,
  address = {Beijing, China},
  month = sep,
  year = 2018,
  volume = {118},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Schewe, Sven and Zhang, Lijun},
  acronym = {{CONCUR}'18},
  booktitle = {{P}roceedings of the 29th
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'18)},
  author = {Bollig, Benedikt and Fortin, Marie and Gastin, Paul},
  title = {It Is Easy to Be Wise After the Event: Communicating Finite-State
               Machines Capture First-Order Logic with ''Happened Before''},
  pages = {7:1-7:17},
  url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9545},
  pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/9545/pdf/LIPIcs-CONCUR-2018-7.pdf},
  doi = {10.4230/LIPIcs.CONCUR.2018.7},
  abstract = {Message sequence charts (MSCs) naturally arise as executions of communicating finite-state machines (CFMs), in which finite-state processes exchange messages through unbounded FIFO channels. We study the first-order logic of MSCs, featuring Lamport's happened-before relation. We introduce a star-free version of propositional dynamic logic (PDL) with loop and converse. Our main results state that (i) every first-order sentence can be transformed into an equivalent star-free PDL sentence (and conversely), and (ii) every star-free PDL sentence can be translated into an equivalent CFM. This answers an open question and settles the exact relation between CFMs and fragments of monadic second-order logic. As a byproduct, we show that first-order logic over MSCs has the three-variable property.}
}
@article{AGK-lmcs18,
  journal = {Logical Methods in Computer Science},
  author = {Akshay, S. and Gastin, Paul and Krishna, Shankara Narayanan},
  title = {Analyzing Timed Systems Using Tree Automata},
  volume = {14},
  number = {2},
  pages = {1-35},
  year = {2018},
  month = may,
  doi = {10.23638/LMCS-14(2:8)2018},
  pdf = {https://lmcs.episciences.org/4489/pdf},
  url = {https://lmcs.episciences.org/4489},
  abstract = {Timed systems, such as timed automata, are usually analyzed using their operational semantics on timed words. The classical region abstraction for timed automata reduces them to (untimed) finite state automata with the same time-abstract properties, such as state reachability. We propose a new technique to analyze such timed systems using finite tree automata instead of finite word automata. The main idea is to consider timed behaviors as graphs with matching edges capturing timing constraints. When a family of graphs has bounded tree-width, they can be interpreted in trees and MSO-definable properties of such graphs can be checked using tree automata. The technique is quite general and applies to many timed systems. In this paper, as an example, we develop the technique on timed pushdown systems, which have recently received considerable attention. Further, we also demonstrate how we can use it on timed automata and timed multi-stack pushdown systems (with boundedness restrictions).}
}
@inproceedings{DGK-lics18,
  address = {Oxford, UK},
  publisher = {ACM Press},
  editor = {Hofmann, Martin and Dawar, Anuj and Gr{\"a}del, Erich},
  acronym = {{LICS}'18},
  booktitle = {{P}roceedings of the 33rd {A}nnual {ACM\slash
            IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'18)},
  author = {Dave, Vrunda and Gastin, Paul and Krishna, Shankara Narayanan},
  month = jul,
  title = {{Regular Transducer Expressions for Regular Transformations}},
  year = {2018},
  url = {https://arxiv.org/abs/1802.02094},
  pdf = {https://arxiv.org/pdf/1802.02094.pdf},
  pages = {315-324},
  doi = {10.1145/3209108.3209182},
  abstract = {Functional MSO transductions, deterministic two-way transducers, as well as streaming string transducers are all equivalent models for regular functions. In this paper, we show that every regular function, either on finite words or on infinite words, captured by a deterministic two-way transducer, can be described with a regular transducer expression (RTE). For infinite words, the transducer uses Muller acceptance and \(\omega\)-regular look-ahead. RTEs are constructed from constant functions using the combinators if-then-else (deterministic choice), Hadamard product, and unambiguous versions of the Cauchy product, the 2-chained Kleene-iteration and the 2-chained omega-iteration. Our proof works for transformations of both finite and infinite words, extending the result on finite words of Alur et al. in LICS'14. In order to construct an RTE associated with a deterministic two-way Muller transducer with look-ahead, we introduce the notion of transition monoid for such two-way transducers where the look-ahead is captured by some backward deterministic B├╝chi automaton. Then, we use an unambiguous version of Imre Simon's famous forest factorization theorem in order to derive a ''good'' (\(\omega\)-)regular expression for the domain of the two-way transducer. ''Good'' expressions are unambiguous and Kleene-plus as well as \(\omega\)-iterations are only used on subexpressions corresponding to idempotent elements of the transition monoid. The combinator expressions are finally constructed by structural induction on the ''Good'' (\(\omega\)-)regular expression describing the domain of the transducer.}
}
@article{GM-softc18,
  publisher = {Springer},
  journal = {Soft Computing},
  author = {Gastin, Paul and Monmege, Benjamin},
  title = {{A unifying survey on weighted logics and weighted automata}},
  volume = {22},
  number = {4},
  year = {2018},
  month = feb,
  pages = {1047-1065},
  doi = {10.1007/s00500-015-1952-6},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/softc2016-GM.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/softc2016-GM.pdf},
  abstract = {Logical formalisms equivalent to weighted automata have been the topic of numerous research papers in the recent years. It started with the seminal result by Droste and Gastin on weighted logics over semirings for words. It has been extended in two dimensions by many authors. First, the weight domain has been extended to valuation monoids, valuation structures, etc. to capture more quantitative properties. Along another dimension, different structures such as ranked or unranked trees, nested words, Mazurkiewicz traces, etc. have been considered. The long and involved proofs of equivalences in all these papers are implicitly based on the same core arguments. This article provides a meta-theorem which unifies these different approaches. Towards this, we first revisit weighted automata by defining a new semantics for them in two phases---an abstract semantics based on multisets of weight structures (independent of particular weight domains) followed by a concrete semantics. Then, we introduce a core weighted logic with a minimal number of features and a simplified syntax, and lift the new semantics to this logic. We show at the level of the abstract semantics that weighted automata and core weighted logic have the same expressive power. Finally, we show how previous results can be recovered from our result by logical reasoning. In this paper, we prove the meta-theorem for words, ranked and unranked trees, showing the robustness of our approach.}
}
@inproceedings{GMG-dlt19,
  address = {Warsaw, Poland},
  month = aug,
  volume = {11647},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Piotrek Hofman and Micha\l Skrzypczak},
  acronym = {{DLT}'19},
  booktitle = {{P}roceedings of the 23th {I}nternational
               {C}onference on {D}evelopments in {L}anguage {T}heory
               ({DLT}'19)},
  author = {Paul Gastin and Amaldev Manuel and R. Govind},
  title = {Logics for Reversible Regular Languages and Semigroups with Involution},
  pages = {182-191},
  doi = {10.1007/978-3-030-24886-4\_13},
  year = 2019,
  pdf = {https://arxiv.org/pdf/1907.01214.pdf},
  url = {https://arxiv.org/abs/1907.01214},
  abstract = {We present MSO and FO logics with predicates ``between'' and
  ``neighbour'' that characterise various fragments of the class of regular
  languages that are closed under the reverse operation. The standard
  connections that exist between MSO and FO logics and varieties of finite
  semigroups extend to this setting with semigroups extended with an
  involution. The case is different for FO with neighbour relation where
  we show that one needs additional equations to characterise the class.}
}
@inproceedings{Gastin-cai19,
  address = {Ni{\u s}, Serbia},
  month = jun,
  volume = 11545,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Miroslav {\'C}iri{\'c} and Manfred Droste and Jean-{\'E}ric Pin},
  acronym = {{CAI}'19},
  booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on
                  {A}lgebraic {I}nformatics ({CAI}'19)},
  author = {Gastin, Paul},
  title = {Modular Descriptions of Regular Functions},
  pages = {3-9},
  doi = {},
  note = {Invited talk},
  year = 2019,
  doi = {10.1007/978-3-030-21363-3\_1},
  abstract = {We discuss various formalisms to describe string-to-string
  transformations. Many are based on automata and can be seen as operational
  descriptions, allowing direct implementations when the input scanner is
  deterministic. Alternatively, one may use more human friendly descriptions
  based on some simple basic transformations (e.g., copy, duplicate, erase,
  reverse) and various combinators such as function com- position or extensions
  of regular operations.}
}
@inproceedings{GMS-cav19,
  address = {New York, USA},
  month = jul,
  volume = {11561},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Isil Dillig and Serdar Tasiran},
  acronym = {{CAV}'19},
  booktitle = {{P}roceedings of the 31st
               {I}nternational {C}onference on 
               {C}omputer {A}ided {V}erification
               ({CAV}'19)},
  author = {Paul Gastin and Sayan Mukherjee and B. Srivathsan},
  title = {Fast algorithms for handling diagonal constraints in timed automata},
  pages = {41-59},
  year = 2019,
  url = {https://arxiv.org/abs/1904.08590}
}
@inproceedings{BBM-mfcs19,
  address = {Aachen, Germany},
  month = aug,
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Pinar Heggernes and Joost-Pieter Katoen and Peter Rossmanith},
  acronym = {{MFCS}'19},
  booktitle = {{P}roceedings of the 42nd
               {I}nternational {S}ymposium on
               {M}athematical {F}oundations of 
               {C}omputer {S}cience
               ({MFCS}'19)},
  author = {Manfred Droste and Paul Gastin},
  title = {Aperiodic Weighted Automata and Weighted First-Order Logic},
  note = {To appear},
  year = 2019,
  url = {https://arxiv.org/abs/1902.08149}
}
@inproceedings{AGJK-lics19,
  address = {Vancouver, Canada},
  month = jun,
  publisher = {{IEEE} Press},
  editor = {Bouyer, Patricia},
  acronym = {{LICS}'19},
  booktitle = {{P}roceedings of the 34th {A}nnual {ACM\slash
            IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'19)},
  author = {Akshay, S. and  Gastin, Paul and Jug{\'e}, Vincent and Krishna, Shankara Narayanan},
  title = {Timed systems through the lens of logic},
  note = {To appear},
  year = 2019
}

This file was generated by bibtex2html 1.98.