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