@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}, note = {Invited talk}, year = 2019, pdf = {https://arxiv.org/abs/1908.01137}, 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, doi = {10.1007/978-3-030-25540-4_3}, pdf = {https://arxiv.org/pdf/1904.08590.pdf}, url = {https://arxiv.org/abs/1904.08590} }

@inproceedings{BBM-mfcs19, address = {Aachen, Germany}, month = aug, volume = {138}, 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}, pages = {76:1-76:15}, year = 2019, doi = {10.4230/LIPIcs.MFCS.2019.76}, pdf = {http://drops.dagstuhl.de/opus/volltexte/2019/11020/pdf/LIPIcs-MFCS-2019-76.pdf}, url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11020} }

@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}, pages = {1-13}, year = 2019, doi = {10.1109/LICS.2019.8785684}, pdf = {https://arxiv.org/pdf/1903.03773.pdf}, url = {https://arxiv.org/abs/1903.03773}, abstract = {In this paper, we analyze timed systems with data structures, using a rich interplay of logic and properties of graphs. We start by describing behaviors of timed systems using graphs with timing constraints. Such a graph is called realizable if we can assign time-stamps to nodes or events so that they are consistent with the timing constraints. The logical definability of several graph properties has been a challenging problem, and we show, using a highly non-trivial argument, that the realizability property for collections of graphs with strict timing constraints is logically definable in a class of propositional dynamic logic (EQ-ICPDL), which is strictly contained in MSO. Using this result, we propose a novel, algorithmically efficient and uniform proof technique for the analysis of timed systems enriched with auxiliary data structures, like stacks and queues. Our technique unravels new results (for emptiness checking as well as model checking) for timed systems with richer features than considered so far, while also recovering existing results.} }

@inproceedings{AGKR-tacas2020, address = {Dublin, Ireland}, month = apr, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Armin Biere and David Parker}, acronym = {{TACAS}'20}, booktitle = {{P}roceedings of the 26th {I}nternational {C}onference on {T}ools and {A}lgorithms for {C}onstruction and {A}nalysis of {S}ystems ({TACAS}'20)}, author = {Akshay, S. and Gastin, Paul and Krishna, Shankara Narayanan and Roychoudhary, Sparsa}, title = {Revisiting Underapproximate Reachability for Multipushdown Systems}, year = 2020, note = {To appear} }

*This file was generated by
bibtex2html 1.98.*