@inproceedings{JB-AC-AP-GVN-stacs91, 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 = {Beauquier, Joffroy and Choquet, Annie and Petit, Antoine and Vidal-Naquet, Guy}, title = {Detection of Deadlocks in an Infinite Family of Nets}, pages = {334-347} }

@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.} }

@article{GP-AP-SCM-92, address = {Bucharest, Romania}, publisher = {Academia Republicii Populare Romine}, journal = {Studii {\b S}i Cercet{\u{a}}ri Matematice}, author = {Paun, Gheorghe and Petit, Antoine}, title = {Generalized Reduced Languages}, volume = {44}, number = {4}, pages = {309-318}, year = {1992}, missingnmonth = {}, missingmonth = {} }

@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.} }

@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{AP-ACTA-93, publisher = {Springer}, journal = {Acta Informatica}, author = {Petit, Antoine}, title = {Recognizable Trace Languages, Distributed Automata and the Distribution Problem}, volume = {30}, number = {1}, pages = {89-101}, year = {1993}, month = jan }

@phdthesis{AP-Hab-93, author = {Petit, Antoine}, title = {M{\'e}moire d'habilitation {\`a} diriger des recherches}, type = {M{\'e}moire d'habilitation}, year = {1993}, missingmonth = {}, missingnmonth = {}, school = {Universit{\'e} Paris-Sud~11, Orsay, France} }

@inproceedings{CC-AP-mfcs93, address = {Gdansk, Poland}, month = aug, year = 1993, volume = 711, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, editor = {Borzyszkowski, Andrzej M. and Sokolowski, Stefan}, acronym = {{MFCS}'93}, booktitle = {{P}roceedings of the 18th {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'93)}, author = {C{\'e}rin, {\relax Ch}ristophe and Petit, Antoine}, title = {Speed-Up of Recognizable Trace Languages}, pages = {332-341} }

@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.} }

@inproceedings{ACF-AP-stacs95, address = {Munich, Germany}, month = mar, year = 1995, volume = 900, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Mayr, Ernst W. and Puech, Claude}, acronym = {{STACS}'95}, booktitle = {{P}roceedings of the 12th {A}nnual {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'95)}, author = {Fabret, Anne-C{\'e}cile and Petit, Antoine}, title = {On the Undecidability of Deadlock Detection in Families of Nets}, pages = {479-490} }

@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} }

@inproceedings{SH-AP-mfcs95, 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 = {Huguet, S{\'e}bastien and Petit, Antoine}, title = {Modular Constructions of Distributing Automata}, pages = {467-478} }

@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.} }

@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.} }

@article{BCB-RC-AP-97, address = {Les Ulis, France}, publisher = {EDP Sciences}, journal = {RAIRO Informatique Th{\'e}orique et Applications}, author = {Charron{-}Bost, Bernadette and Cori, Robert and Petit, Antoine}, title = {Introduction {\`a} l'algorithmique en m{\'e}moire partag{\'e}e}, volume = {31}, number = {2}, pages = {97-148}, year = {1997}, missingmonth = {}, missingnmonth = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CCP-RAIRO97.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CCP-RAIRO97.ps}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CCP-RAIRO97.pdf}, lsv-lang = {FR} }

@book{JCB-HC-CK-DK-MM-JMM-AP-YR-livre96, author = {Bajard, Jean-Claude and Comon, Hubert and Kenyon, Claire and Krob, Daniel and Morvan, Michel and Muller, Jean-Michel and Petit, Antoine and Robert, Yves}, title = {Exercices d'algorithmique (oraux d'{ENS})}, year = {1997}, publisher = {Vuibert}, month = jan, pages = {272}, isbn = {2-84180-105-5}, lsv-lang = {FR} }

@inproceedings{RM-AP-mfcs97, address = {Bratislava, Slovakia}, month = aug, year = 1997, volume = 1295, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Pr{\'i}vara, Igor and Ruzicka, Peter}, acronym = {{MFCS}'97}, booktitle = {{P}roceedings of the 22nd {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'97)}, author = {Meyer, Rapha{\"e}l and Petit, Antoine}, title = {Decomposition of {TrPTL} Formulas}, pages = {418-427}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/MeyPet-mfcs97.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MeyPet-mfcs97.ps}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MeyPet-mfcs97.pdf} }

@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.} }

@techreport{AP-mc98, author = {Petit, Antoine}, title = {Le model-checking, une technique de v{\'e}rification en plein essor. {I}ntroduction}, year = {1998}, month = oct, type = {Contract Report}, institution = {EDF/DER/MOS - LSV}, lsv-lang = {FR} }

@techreport{BB-MB-AP-src98, author = {B{\'e}rard, B{\'e}atrice and Bidoit, Michel and Petit, Antoine}, title = {Recommandations sur le cahier des charges {SRC}}, year = {1998}, missingmonth = {}, missingnmonth = {}, type = {Contract Report}, institution = {EDF/DER/MOS - LSV}, lsv-lang = {FR} }

@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.} }

@inproceedings{CC-AP-mteac98, address = {Las Vegas, Nevada, USA}, month = jan, year = 1998, editor = {B{\"o}hm, A. P. Wim and Najjar, Walid A.}, acronym = {{MTEAC}'98}, booktitle = {{P}roceedings of the {W}orkshop on {M}ultithreaded {E}xecution, {A}rchitecture and {C}ompilation ({MTEAC}'98)}, author = {C{\'e}rin, {\relax Ch}ristophe and Petit, Antoine}, title = {Application of Algebraic Techniques to Compute the Efficiency Measure for Multithreaded Architecture}, missingpages = {??}, howpublished = {Proceedings published as Technical Report CS-98-102, Colorado State University}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CP-mteac98.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CP-mteac98.ps} }

@techreport{DD1-98, author = {Laroussinie, Fran{\c{c}}ois and Petit, Antoine and Schnoebelen, {\relax Ph}ilippe}, title = {Le model-checking, une technique de v{\'e}rification en plein essor. {I}~--- {P}rincipes et techniques}, year = {1998}, month = oct, type = {Contract Report}, institution = {EDF/DER/MOS - LSV}, lsv-lang = {FR} }

@techreport{DD3-98, author = {B{\'e}rard, B{\'e}atrice and C{\'e}c{\'e}, G{\'e}rard and Dufourd, Catherine and Finkel, Alain and Laroussinie, Fran{\c{c}}ois and Petit, Antoine and Schnoebelen, {\relax Ph}ilippe and Sutre, Gr{\'e}goire}, title = {Le model-checking, une technique de v{\'e}rification en plein essor. {II}~--- {Q}uelques outils}, year = {1998}, month = oct, type = {Contract Report}, institution = {EDF/DER/MOS - LSV}, lsv-lang = {FR} }

@article{GG-RM-AP-PW-98, publisher = {Elsevier Science Publishers}, journal = {Information Processing Letters}, author = {Guaiana, Giovana and Meyer, Rapha{\"e}l and Petit, Antoine and Weil, Pascal}, title = {An Extension of the Wreath Product Principle for Finite {M}azurkiewicz Traces}, volume = {67}, number = {6}, pages = {277-282}, year = {1998}, month = sep, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GMPW-IPL98.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GMPW-IPL98.ps} }

@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.} }

@inproceedings{RM-AP-stacs98, address = {Paris, France}, month = feb, year = 1998, volume = 1373, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Morvan, Michel and Meinel, {\relax Ch}ristoph and Krob, Daniel}, acronym = {{STACS}'98}, booktitle = {{P}roceedings of the 15th {A}nnual {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'98)}, author = {Meyer, Rapha{\"e}l and Petit, Antoine}, title = {Expressive Completeness of {LTrL} on Finite Traces: {A}n Algebraic Proof}, pages = {533-543} }

@inproceedings{PB-AP-icalp99, address = {Prague, Czech Republic}, month = jul, year = 1999, volume = 1644, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Wiedermann, Jir{\'i} and van Emde Boas, Peter and Nielsen, Mogens}, acronym = {{ICALP}'99}, booktitle = {{P}roceedings of the 26th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'99)}, author = {Bouyer, Patricia and Petit, Antoine}, title = {Decomposition and Composition of Timed Automata}, pages = {210-219}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BP-icalp99.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BP-icalp99.ps}, abstract = {We propose in this paper a decomposition theorem for the timed automata introduced by Alur and Dill. To this purpose, we define a new simple and natural concatenation operation, indexed by the set of clocks to be reset, on timed automata generalizing the classical untimed concatenation. \par Then we extend the famous Kleene's and B{\"u}chi's theorems on classical untimed automata by simply changing the basic objects to take time into account, keeping the union operation and replacing the concatenation, finite and infinite iterations by the new timed concatenations and their induced iterations.\par Thus, and up to our knowledge, our result provides the simplest known algebraic characterization of recognizable timed languages.} }

@book{docdor99, author = {Schnoebelen, {\relax Ph}ilippe and B{\'e}rard, B{\'e}atrice and Bidoit, Michel and Laroussinie, Fran{\c{c}}ois and Petit, Antoine}, title = {V{\'e}rification de logiciels : techniques et outils du model-checking}, year = {1999}, month = apr, publisher = {Vuibert}, isbn = {2-7117-8646-3}, url = {http://www.vuibert.com/livre593.html}, lsv-lang = {FR} }

@inproceedings{BDFP-mfcs-2000, address = {Bratislava, Slovakia}, month = aug, year = 2000, volume = 1893, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Nielsen, Mogens and Rovan, Branislav}, acronym = {{MFCS} 2000}, booktitle = {{P}roceedings of the 25th {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS} 2000)}, author = {Bouyer, Patricia and Dufourd, Catherine and Fleury, Emmanuel and Petit, Antoine}, title = {Expressiveness of Updatable Timed Automata}, pages = {232-242}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BDFP-mfcs2000.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BDFP-mfcs2000.ps}, abstract = {Since their introduction by Alur and Dill, timed automata have been one of the most widely studied models for real-time systems. The syntactic extension of so-called updatable timed automata allows more powerful updates of clocks than the reset operation proposed in the original model.\par We prove that any language accepted by an updatable timed automaton (from classes where emptiness is decidable) is also accepted by a {"}classical{"} timed automaton. We propose even more precise results on bisimilarity between updatable and classical timed automata.} }

@misc{Calife-1.1, author = {B{\'e}rard, B{\'e}atrice and Cast{\'e}ran, Pierre and Fleury, Emmanuel and Fribourg, Laurent and Monin, Jean-Fran{\c{c}}ois and Paulin, {\relax Ch}ristine and Petit, Antoine and Rouillard, Davy}, title = {Document de sp{\'e}cification du mod{\`e}le commun}, year = {2000}, month = apr, howpublished = {Fourniture~1.1 du projet RNRT Calife}, lsv-lang = {FR} }

@misc{Calife-4.2, author = {Bouyer, Patricia and Fleury, Emmanuel and Petit, Antoine}, title = {Document de synth{\`e}se sur les proc{\'e}dures de v{\'e}rification des syst{\`e}mes temps r{\'e}el : Les automates temporis{\'e}s}, year = {2000}, month = jan, howpublished = {Fourniture~4.2 du projet RNRT Calife}, lsv-lang = {FR} }

@inproceedings{PB-CD-EF-AP-cav2000, address = {Chicago, Illinois, USA}, month = jul, year = 2000, volume = 1855, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Emerson, E. Allen and Sistla, A. Prasad}, acronym = {{CAV} 2000}, booktitle = {{P}roceedings of the 12th {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV} 2000)}, author = {Bouyer, Patricia and Dufourd, Catherine and Fleury, Emmanuel and Petit, Antoine}, title = {Are Timed Automata Updatable?}, pages = {464-479}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BDEP-cav2000.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BDEP-cav2000.ps}, abstract = {In classical timed automata, as defined by Alur and Dill and since widely studied, the only operation allowed to modify the clocks is the reset operation. For instance, a clock can neither be set to a non-null constant value, nor be set to the value of another clock nor, in a non-deterministic way, to some value lower or higher than a given constant. In this paper we study in details such updates.\par We characterize in a thin way the frontier between decidability and undecidability. Our main contributions are the following:\par 1)~We exhibit many classes of updates for which emptiness is undecidable. These classes depend on the clock constraints that are used ---~diagonal-free or not~--- whereas it is well-known that these two kinds of constraints are equivalent for classical timed automata.\par 2)~We propose a generalization of the region automaton proposed by Alur and Dill, allowing to handle larger classes of updates. The complexity of the decision procedure remains PSPACE-complete.} }

@inproceedings{cclps-smc2000, address = {Nashville, Tennessee, USA}, month = oct, year = 2000, publisher = {Argos Press}, acronym = {{SMC} 2000}, booktitle = {{P}roceedings of the {IEEE} {I}nternational {C}onference on {S}ystems, {M}an and {C}ybernetics ({SMC} 2000)}, author = {Canet, G{\'e}raud and Couffin, Sandrine and Lesage, Jean-Jacques and Petit, Antoine and Schnoebelen, {\relax Ph}ilippe}, title = {Towards the Automatic Verification of {PLC} Programs Written in {I}nstruction {L}ist}, pages = {2449-2454}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CCLPS-smc2000.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CCLPS-smc2000.ps}, doi = {10.1109/ICSMC.2000.884359}, abstract = {We propose a framework for the automatic verification of PLC (programmable logic controller) programs written in Instruction List, one of the five languages defined in the IEC 61131-3 standard. We~propose a formal semantics for a significant fragment of the IL language, and a direct coding of this semantics into a model checking tool. We then automatically verify rich behavioral properties written in linear temporal logic. Our~approach is illustrated on the example of the tool-holder of a turning center} }

@inproceedings{cdprs-cifa2000, address = {Lille, France}, month = jul, year = 2000, optaddress = {Villeneuve d'Ascq, France}, publisher = {Union des Chercheurs Ing{\'e}nieurs et {S}cientifiques, Villeneuve d'Ascq, France}, editor = {Borne, Pierre and Richard, Jean-Pierre and Vanheeghe, {\relax Ph}ilippe}, acronym = {{CIFA} 2000}, booktitle = {{A}ctes de la 1{\`e}re {C}onf{\'e}rence {I}nternationale {F}rancophone d'{A}utomatique ({CIFA} 2000)}, author = {Canet, G{\'e}raud and Denis, Bruno and Petit, Antoine and Rossi, Olivier and Schnoebelen, {\relax Ph}ilippe}, title = {Un cadre pour la v{\'e}rification automatique de programmes~{IL}}, pages = {693-698}, noisbn = {2-9512309-1-5}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CDPRS-cifa2000.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CDPRS-cifa2000.ps}, lsv-lang = {FR} }

@inproceedings{BPT-concur-2001, address = {Aalborg, Denmark}, month = aug, year = 2001, volume = 2154, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Larsen, Kim G. and Nielsen, Modens}, acronym = {{CONCUR}'01}, booktitle = {{P}roceedings of the 12th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'01)}, author = {Bouyer, Patricia and Petit, Antoine and Th{\'e}rien, Denis}, title = {An Algebraic Characterization of Data and Timed Languages}, pages = {248-261}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BPT-concur2001.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BPT-concur2001.ps}, abstract = {Algebra offers an elegant and powerful approach to understand regular languages and finite automata. Such framework has been notoriously lacking for timed languages and timed automata. We introduce the notion of monoid recognizability for data languages, which include timed languages as special case, in a way that respects the spirit of the classical situation. We study closure properties and hierarchies in this model, and prove that emptiness is decidable under natural hypotheses. Our class of recognizable languages properly includes many families of deterministic timed languages that have been proposed until now, and the same holds for non-deterministic versions.} }

@techreport{Calife-4.4, author = {B{\'e}rard, B{\'e}atrice and Bouyer, Patricia and Petit, Antoine}, title = {Mod{\'e}lisation du protocole~{PGM} et de certaines de ses propri{\'e}t{\'e}s en {UPPAAL}}, year = {2001}, month = nov, type = {Contract Report}, number = {4.4}, institution = {projet RNRT Calife}, note = {18 pages} }

@misc{ap-express01, author = {Petit, Antoine}, title = {About Extensions of Timed Automata}, howpublished = {Invited talk, 8th {I}nternational {W}orkshop on {E}xpressiveness in {C}oncurrency ({EXPRESS}'01), {A}alborg, {D}enmark}, year = 2001, month = aug }

@book{lsvmcbook01, author = {B{\'e}rard, B{\'e}atrice and Bidoit, Michel and Finkel, Alain and Laroussinie, Fran{\c{c}}ois and Petit, Antoine and Petrucci, Laure and Schnoebelen, {\relax Ph}ilippe}, title = {Systems and Software Verification. {M}odel-Checking Techniques and Tools}, year = {2001}, missingmonth = {}, missingnmonth = {}, publisher = {Springer}, isbn = {3-540-41523-8}, url = {http://www.springer.com/978-3-540-41523-8}, olderurl = {http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-41523-8} }

@book{scopos13-2001, author = {Badouel, {\'E}ric and Boucheron, St{\'e}phane and Dicky, Anne and Petit, Antoine and Santha, Miklos and Weil, Pascal and Zeitoun, Marc}, title = {Probl\`{e}mes d'informatique fondamentale}, publisher = {Springer}, volume = {13}, series = {Scopos}, year = {2001}, missingmonth = {}, missingnmonth = {}, isbn = {3-540-42341-9}, url = {http://www.springer.com/978-3-540-42341-9}, olderurl = {http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-42341-9} }

@article{BP-JALC2002, journal = {Journal of Automata, Languages and Combinatorics}, author = {Bouyer, Patricia and Petit, Antoine}, title = {A {K}leene{\slash}B{\"u}chi-like Theorem for Clock Languages}, volume = {7}, number = {2}, pages = {167-186}, year = {2002}, missingmonth = {}, missingnmonth = {}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BP-JALC2001.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BP-JALC2001.ps}, abstract = {We propose in this paper a generalization of the famous Kleene\slash B{\"u}chi's theorem on formal languages, one of the cornerstones of theoretical computer science, to the timed model of clock languages. These languages extend the now classical timed languages introduced by Alur and Dill as a suitable model of real-time systems. As a corollary of our main result, we get a simple algebraic characterization of timed languages recognized by (updatable) timed automata.} }

@inproceedings{bbp-rttools02, address = {Copenhagen, Denmark}, month = aug, year = 2002, howpublished = {Technical Report 2002-025, Department of Information Technology, Uppsala University, Sweden}, publisher = {Uppsala University}, editor = {Petterson, Paul and Yi, Wang}, acronym = {{RT-TOOLS}'02}, booktitle = {{P}roceedings of the 2nd {W}orkshop on {R}eal-{T}ime {T}ools ({RT-TOOLS}'02)}, author = {B{\'e}rard, B{\'e}atrice and Bouyer, Patricia and Petit, Antoine}, title = {Analysing the {PGM} Protocol with {UPPAAL}}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/pgmfin.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/pgmfin.ps}, abstract = {Pragmatic General Multicast (PGM) is a reliable multicast protocol, designed to minimize both the probability of negative acknowledgements (NAK) implosion and the loading of the network due to retransmissions of lost packets. This protocol was presented to the Internet Engineering Task Force as an open reference specification. \par In this paper, we focus on the main reliability property which PGM intends to guarantee: a receiver either receives all data packets from transmissions and repairs or is able to detect unrecoverable data packet loss.\par To this purpose, we propose a modelization of (a simplified version of) PGM via a network of timed automata. Using Uppaal model-checker, we then study the validity of the reliability property above, which turns out to not be always verified but to depend of the values of several parameters that we underscore.} }

@inproceedings{BBP-msr2003, address = {Metz, France}, month = oct, year = 2003, publisher = {Herm{\`e}s}, editor = {M{\'e}ry, Dominique and Rezg, Nidhal and Xie, Xiaolan}, acronym = {{MSR}'03}, booktitle = {{A}ctes du 4{\`e}me {C}olloque sur la {M}od{\'e}lisation des {S}yst{\`e}mes {R}{\'e}actifs ({MSR}'03)}, author = {B{\'e}rard, B{\'e}atrice and Bouyer, Patricia and Petit, Antoine}, title = {Une analyse du protocole {PGM} avec {UPPAAL}}, pages = {415-430}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBP-msr2003.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBP-msr2003.ps}, abstract = {Pragmatic General Multicast (PGM) is a reliable multicast protocol, designed to minimize both the probability of negative acknowledgements (NAK) implosion and the loading of the network due to retransmissions of lost packets. This protocol was presented to the Internet Engineering Task Force as an open reference specification. In this paper, we focus on the main reliability property which PGM intends to guarantee: a receiver either receives all data packets from transmissions and repairs or is able to detect unrecoverable data packet loss. To this purpose, we propose a modelization of (a simplified version of) PGM via a network of timed automata. Using Uppaal model-checker, we then study the validity of the reliability property above, which turns out to not be always verified but to depend of the values of several parameters that we underscore.} }

@inproceedings{BDMP-cav-2003, address = {Boulder, Colorado, USA}, month = jul, year = 2003, volume = 2725, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Hunt, Jr, Warren A. and Somenzi, Fabio}, acronym = {{CAV}'03}, booktitle = {{P}roceedings of the 15th {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'03)}, author = {Bouyer, Patricia and D'Souza, Deepak and Madhusudan, P. and Petit, Antoine}, title = {Timed Control with Partial Observability}, pages = {180-192}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDMP-CAV03.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDMP-CAV03.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BDMP-CAV03.ps}, abstract = {We consider the problem of synthesizing controllers for timed systems modeled using timed automata. The point of departure from earlier work is that we consider controllers that have only a partial observation of the system that it controls. In discrete event systems (where continuous time is not modeled), it is well known how to handle partial observability, and decidability issues do not differ from the complete information setting. We show however that timed control under partial observability is undecidable even for internal specifications (while the analogous problem under complete observability is decidable) and we identify a decidable subclass.} }

@article{BPT03, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Bouyer, Patricia and Petit, Antoine and Th{\'e}rien, Denis}, title = {An Algebraic Approach to Data Languages and Timed Languages}, volume = {182}, number = {2}, pages = {137-162}, year = {2003}, month = may, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BPT-IetC.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BPT-IetC.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BPT-IetC.ps}, abstract = {Algebra offers an elegant and powerful approach to understand regular languages and finite automata. Such framework has been notoriously lacking for timed languages and timed automata. We introduce the notion of monoid recognizability for data languages, which includes timed languages as special case, in away that respects the spirit of the classical situation. We study closure properties and hierarchies in this model, and prove that emptiness is decidable under natural hypotheses. Our class of recognizable languages properly includes many families of deterministic timed languages that have been proposed until now, and the same holds for non-deterministic versions.} }

@article{BBP-IJPR04, publisher = {Taylor \& Francis}, journal = {International Journal of Production Research}, author = {B{\'e}rard, B{\'e}atrice and Bouyer, Patricia and Antoine Petit}, title = {Analysing the {PGM} Protocol with {U}ppaal}, volume = {42}, number = {14}, pages = {2773-2791}, year = {2004}, month = jul, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBP-IJPR04.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBP-IJPR04.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBP-IJPR04.ps}, abstract = {Pragmatic General Multicast (PGM) is a reliable multicast protocol, designed to minimize both the probability of negative acknowledgements~(NAK) implosion and the load of the network due to retransmissions of lost packets. This protocol was presented to the Internet Engineering Task Force as an open reference specification.\par In this paper, we focus on the main reliability property which PGM intends to guarantee: a receiver either receives all data packets from transmissions and repairs or is able to detect unrecoverable data packet loss. \par We first propose a modelization of (a simplified version of) PGM via a network of timed automata. Using Uppaal model-checker, we then study the validity of the reliability property above, which turns out not to be always verified but to depend on the values of several parameters that we underscore.} }

@article{BDFP04, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Bouyer, Patricia and Dufourd, Catherine and Fleury, Emmanuel and Petit, Antoine}, title = {Updatable Timed Automata}, volume = {321}, number = {2-3}, pages = {291-345}, year = {2004}, month = aug, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/uta-BDFP04.pdf}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/uta-BDFP04.pdf}, ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/uta-BDFP04.ps}, doi = {10.1016/j.tcs.2004.04.003}, abstract = {We investigate extensions of Alur and Dill's timed automata, based on the possibility to update the clocks in a more elaborate way than simply reset them to zero. We call these automata updatable timed automata. They form an undecidable class of models, in the sense that emptiness checking is not decidable. However, using an extension of the region graph construction, we exhibit interesting decidable subclasses. In a surprising way, decidability depends on the nature of the clock constraints which are used, diagonal-free or not, whereas these constraints play identical roles in timed automata. We thus describe in a quite precise way the thin frontier between decidable and undecidable classes of updatable timed automata. \par We also study the expressive power of updatable timed automata. It turns out that any updatable automaton belonging to some decidable subclass can be effectively transformed into an equivalent timed automaton without updates but with silent transitions. The transformation suffers from an enormous combinatorics blow-up which seems unavoidable. Therefore, updatable timed automata appear to be a concise model for representing and analyzing large classes of timed systems. } }

@techreport{LSV:04:10, author = {Baclet, Manuel and Pacalet, Renaud and Petit, Antoine}, title = {Register Transfer Level Simulation}, type = {Research Report}, number = {LSV-04-10}, year = {2004}, month = may, institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, note = {15~pages}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2004-10.rr.ps}, ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/ rr-lsv-2004-10.rr.ps} }

@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.} }

@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.} }

@incollection{BP-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 = {Bouyer, Patricia and Petit, Antoine}, title = {On extensions of timed automata}, pages = {35-63}, abstract = {Since their definition in the early nineties, timed automata have been one of the most used and widely studied models for representing and analyzing real-time systems. In their seminal paper, Alur and Dill proved the probably most important property of timed automata: checking emptiness of the language accepted by a timed automaton, or equivalently checking a reachability property in a timed automaton, is decidable. This result relies on the construction of the so-called region automaton, which abstracts behaviours of a timed automaton into behaviours of a finite automaton. Since then, symbolic algorithms have been developed to solve that problem, several model-checkers have been implemented, and numerous case studies have been verified.\par Lots of works have naturally aimed at proposing extensions of timed automata with new features, while preserving the above-mentioned fundamental decidability result. The motivation for these extensions is basically twofold. First it can increase the expressiveness of timed automata, allowing to model larger classes of systems. Then it can improve the conciseness (and hence the readability) of models by constructing more compact representations for a given system.\par In this paper, we discuss and compare some of the most important extensions of timed automata that have been considered in the literature.} }

@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.", }}

*This file was generated by
bibtex2html 1.98.*