@phdthesis{Gas87,
author = {Gastin, Paul},
title = {Un mod{\`e}le distribu{\'e}},
school = {Laboratoire d'Informatique Th{\'e}orique et
Programmation, Paris, France},
type = {Th{\`e}se de doctorat},
year = 1987
}
@article{Gas90tcs,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Gastin, Paul},
title = {Un mod{\`e}le asynchrone pour les syst{\`e}mes distribu{\'e}s},
volume = 74,
number = 1,
year = 1990,
pages = {121-161},
abstract = { Many researches are engaged in the field of distributed systems
modelization. We present a new model inspired by the
language theory. Its particularity within this theory is the
rejection of interleaving for the representation of
concurrency. Here, the main ideas are born from languages as
CSP or~ESTELLE. The point is mainly the real lack of
dependency between processes apart from synchronisations,
which are rendez-vous. Once the model defined, we introduce,
as in the infinitary free monoid, notions such as length,
concatenation, prefix order, upper bound and infinite
product. So the distributed model is provided with all
operations one needs to develop semantics. Then, we prove
that the finitary part of the distributed model is
isomorphic to the free partially commutative monoid~(fpcm).
Finally, we settle the bases of an infinitary extension of
the fpcm.}
}
@inproceedings{BGV90,
address = {Bari, Italy},
year = 1991,
volume = 486,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {van Leeuwen, Jan and Santoro, Nicola},
acronym = {{WDAG}'90},
booktitle = {{P}roceedings of the 4th {I}nternational {W}orkshop
on {D}istributed {A}lgorithms ({WDAG}'90)},
author = {Beauquier, Joffroy and Gastin, Paul and Villain, Vincent},
title = {A linear fault-tolerant naming algorithm},
pages = {57-70},
doi = {10.1007/3-540-54099-7_5},
abstract = {We solve the naming problem (how to give a unique identifier to
each site of an unknown network), when some sites are
supposed to have a faulty behaviour of fail-stop type. The
solution uses several tokens, in order to ensure that,
despite crash failure of some sites, at least one token will
perform a complete traversal of the network. The
complexities in time and in number of messages of this
algorithm are linear with respect to the size of the network
(number of communication lines), which improves the
exponential solution already known in the Byzantine case
with some special assumptions.}
}
@inproceedings{Gas90epit,
address = {La Roche Posay, France},
month = apr,
year = 1990,
volume = 469,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Guessarian, Ir{\`e}ne},
booktitle = {Semantics of Systems of Concurrent Processes~---
{P}roceedings of the {LITP} {S}pring {S}chool on
{T}heoretical {C}omputer {S}cience},
author = {Gastin, Paul},
title = {Infinite Traces},
pages = {277-308},
abstract = {Trace languages are used in computer science to provide a
description of the behaviours of concurrent systems. If we
are interested in systems which never stop then we have to
consider languages of infinite traces. In this paper, we
generalize to infinite traces three well known points of
view about finite traces: equivalence class of words,
projections on the dependence cliques and dependence graphs.
These approaches are complementary and, depending on the
problem we deal with, each of them can prove to be more
appropriate than the others. In this way, we obtain an
infinitary trace monoid and extend Levi's lemma and the
Foata normal form. Next, we prove that the infinitary trace
monoid is a completely coherent PoSet. We also define an
ultrametric distance and prove that it is a complete metric
space. Therefore, either the PoSet or the topological
framework can be used to solve fix-point equations and then
to provide semantics of recursive constructs. Finally, we
introduce recognizable languages of finite and infinite
traces. We prove that they are characterized by a syntactic
congruence and that the family of recognizable languages is
closed by concatenation and by the Boolean operations:
union, intersection and complement.}
}
@inproceedings{PG-AP-WZ-icalp91,
address = {Madrid, Spain},
month = jul,
year = 1991,
volume = 510,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Leach Albert, Javier and Monien, Burkhard and
Rodriguez-Artalejo, Mario},
acronym = {{ICALP}'91},
booktitle = {{P}roceedings of the 18th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming
({ICALP}'91)},
author = {Gastin, Paul and Petit, Antoine and
Zielonka, Wieslaw},
title = {A {K}leene Theorem for Infinite Trace Languages},
pages = {254-266},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/TCS94gpz.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/TCS94gpz.ps},
abstract = {Kleene's theorem is considered as one of the cornerstones of
theoretical computer science. It ensures that, for languages
of finite words, the family of recognizable languages is
equal to the family of rational languages. It has been
generalized in various ways, for instance, to formal power
series by Sch{\"u}tzenberger, to infinite words by B{\"u}chi and to
finite traces by Ochma{\'n}ski. Finite traces have been
introduced by Mazurkiewicz in order to modelize the
behaviours of distributed systems. The family of
recognizable trace languages is not closed by Kleene's star
but by a concurrent version of this iteration. This leads to
the natural definition of co-rational languages obtained as
the rational one by simply replacing the Kleene's iteration
by the concurrent iteration. Cori, Perrin and M{\'e}tivier
proved, in substance, that any co-rational trace language is
recognizable. Independently, Ochma{\'n}ski generalized Kleene's
theorem showing that the recognizable trace languages are
exactly the co-rational languages. Besides, infinite traces
have been recently introduced as a natural extension of both
finite traces and infinite words. In this paper we
generalize Kleene's theorem to languages of infinite traces
proving that the recognizable languages of finite or
infinite traces are exactly the co-rational languages.}
}
@inproceedings{VD-PG-AP-mfcs91,
address = {Kazimierz Dolny, Poland},
month = sep,
year = 1991,
volume = 520,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Tarlecki, Andrzej},
acronym = {{MFCS}'91},
booktitle = {{P}roceedings of the 16th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'91)},
author = {Diekert, Volker and Gastin, Paul and
Petit, Antoine},
title = {Recognizable Complex Trace Languages},
pages = {131-140},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/IC95dgp.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/IC95dgp.ps},
abstract = {A.~Mazurkiewicz defined traces in order to modelize
non-sequential processes. Complex traces have been recently
introduced as a generalization of both traces and infinite
words. This paper studies the family of recognizable complex
trace languages. It is proved that this family is closed
under boolean operations, concatenation, left and right
quotients. Then sufficient conditions ensuring the
recognizability of the finite and infinite iterations of a
recognizable complex trace language are given. The notion of
co-iteration is defined and the Kleene-Ochma{\'n}ski theorem is
generalized to complex traces.}
}
@inproceedings{Gas91,
address = {Hamburg, Germany},
month = feb,
year = 1991,
volume = 480,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Choffrut, {\relax Ch}ristian and Jantzen, Matthias},
acronym = {{STACS}'91},
booktitle = {{P}roceedings of the 8th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'91)},
author = {Gastin, Paul},
title = {Recognizable and rational languages of finite and
infinite traces},
pages = {89-104},
abstract = {Trace languages are used in computer science to provide a
description of the behaviours of concurrent systems. If we
are interested in systems which never stop then we have to
consider languages of infinite traces. In this paper, we
introduce and study recognizable and rational languages of
finite and infinite traces. We characterize recognizable
languages by means of a syntactic congruence. We prove that
the family of recognizable languages is strictly included in
the family of rational languages. Next, we study the closure
properties of the family of recognizable languages. We prove
that this family is closed under the Boolean operations and
under concatenation. Contrary to the (finite) iteration, the
infinite iteration of a finite trace is proved to be
recognizable. We conclude this paper with some open
problems.}
}
@inproceedings{PG-AP-APN-92,
year = 1992,
volume = 609,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Rozenberg, Grzegorz},
booktitle = {{A}dvances in {P}etri {N}ets 1992:
{T}he {DEMON} {P}roject},
author = {Gastin, Paul and Petit, Antoine},
title = {A Survey of Recognizable Languages of Infinite
Traces},
pages = {392-409},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/APN92gp.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/APN92gp.ps},
abstract = {A.~Mazurkiewicz defined traces in order to represent
non-sequential processes. In order to describe
non-sequential processes which never terminate, \emph{e.g.}
distributed operating systems, the notion of infinite traces
is needed. The aim of this survey is to present in a uniform
way the known results on recognizable infinite trace
languages. The proofs of the presented results are not
proposed here but can be found in the original papers.}
}
@inproceedings{PG-AP-icalp92,
address = {Vienna, Austria},
month = jul,
year = 1992,
volume = 623,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Kuich, Werner},
acronym = {{ICALP}'92},
booktitle = {{P}roceedings of the 19th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming
({ICALP}'92)},
author = {Gastin, Paul and Petit, Antoine},
title = {Asynchronous Cellular Automata for Infinite
Traces},
pages = {583-594},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Icalp92gp.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Icalp92gp.ps},
abstract = {A.~Mazurkiewicz introduced the monoid of traces to provide a
very natural semantics for concurrent processes. In a
general monoid, the behaviours of finite state systems are
described by recognizable languages, which form hence a
basic family. For finite traces and finite or infinite
words, there exist several equivalent characterizations of
this family as for instance, saturating morphisms or
(co-)rational expressions. For infinite traces, this family
has been introduced by means of saturating morphisms and
characterized by co-rational expressions but it suffers from
lack of finite state system characterizations. In this
paper, we remedy this deficiency providing a
characterization of the family of recognizable infinite
trace languages by means of asynchronous (cellular) automata
(which carry the most intuitive idea of finite state
concurrent machines). To this purpose, we give effective
constructions for co-rational operations on these automata
which are of independent interest.}
}
@inproceedings{PG-AP-mfcs92,
address = {Prague, Czechoslovakia},
month = aug,
year = 1992,
volume = 629,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Havel, Ivan M. and Koubek, V{\'a}clav},
acronym = {{MFCS}'92},
booktitle = {{P}roceedings of the 17th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'92)},
author = {Gastin, Paul and Petit, Antoine},
title = {{P}o{S}et properties of complex traces},
pages = {255-263},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Mfcs92gp.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Mfcs92gp.ps},
abstract = {This paper investigates PoSet properties of the monoid~\(\mathbb{G}\) of
infinite dependence graphs and of the monoid~\(\mathbb{C}\) of complex
traces. We show that a subset of~\(\mathbb{G}\) admits a least upper
bound if and only if this set is coherent and countable.
Hence, \(\mathbb{G}\)~is bounded complete. The compact and the prime
dependence graphs are characterized and we prove that each
dependence graph is the least upper bound of its compact
(resp. its prime) lower bounds. Therefore, up to the
restriction to countable sets, \(\mathbb{G}\)~is a coherently complete
Scott-Domain and is Prime Algebraic. We define very
naturally two orders on~\(\mathbb{C}\) : the product order and the prefix
order. We show that \(\mathbb{C}\) with each order is a coherently
complete CPO and we characterize the least upper bound (the
greatest lower bound resp.) of a subset of~\(\mathbb{C}\) when it exists.
But contrary to the case of~\(\mathbb{G}\), we prove that
\(\mathbb{C}\)~is not a
Scott-Domain in general.}
}
@phdthesis{Gas92,
author = {Gastin, Paul},
title = {M{\'e}moire d'habilitation {\`a} diriger des
recherches},
howpublished = {Technical Report LITP-92.97},
year = {1992},
type = {M{\'e}moire d'habilitation},
school = {Universit{\'e} Paris~6, Paris, France}
}
@article{GOPR92,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Gastin, Paul and Ochma{\'n}ski, Edward and Petit, Antoine and Rozoy, Brigitte},
title = {Decidability of the star problem
in {{\(A^*\)}}{\(\times\{b\}^*\)}},
volume = 44,
number = {2},
year = 1992,
month = nov,
pages = {65-71},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/IPL92gopr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/IPL92gopr.ps},
abstract = {We adress in this paper the decidability of the Star Problem in
trace monoids: Let~{\(L\)} be a recognizable trace language,
is~{\(L^*\)}
recognizable? We prove that this problem is decidable when
the trace monoid is a direct product of free monoids
{\(A^*\times
\{b\}^*\)}. This result shows, for the first time and contrary to
a possible intuition, that the Star Problem is of distinct
nature than the Recognizability Problem: Let~{\(L\)} be a rational
trace language, is~{\(L\)} recognizable?}
}
@article{GV93,
publisher = {World Scientific},
journal = {Parallel Processing Letters},
author = {Gastin, Paul and Villain, Vincent},
title = {An efficient crash-tolerant sequential traversal},
volume = 3,
year = 1993,
pages = {87-97},
abstract = {Fault-tolerance is an increasingly
important requirement for most
of the todays distributed
systems. However, the cost and
complexity of the design of such
systems are considerably higher
than those of non fault-tolerant
ones.\par
An interesting approach to simplify the
design of
fault-tolerant systems appears in~[TN88] :
some methods are developed, that
automatically convert benign failures
tolerant systems into systems overcoming
more severe failures. With these methods,
one can first solve the simpler problem of
designing a program which only tolerates
benign failures, and then convert it
automatically into one with a higher
degree of fault-tolerance. Therefore, the
design of benign failures tolerant systems
is a basic concern in this framework. \par
The aim of this paper is to make easier,
by means of a modular methodology, the
conception of algorithms overcoming the
most benign type of failures :
crash-failures.}
}
@article{GR93,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Gastin, Paul and Rozoy, Brigitte},
title = {The poset of infinitary traces},
volume = 120,
number = 1,
year = 1993,
pages = {101-121},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/TCS93-gr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/TCS93-gr.ps},
abstract = {\emph{Partially Commutative Monoids}, also called
\emph{Trace Monoids}, are among the most studied
formalisms which describe the behaviour of
distributed systems. In order to modelize
systems which never stop, we have to
consider an extension of traces, namely
\emph{Infinite traces}. Finite trace monoids are
strongly related to \emph{Partial Order Sets
(PoSets), Domains and Event Structures},
which are other models to describe the
behaviour of distributed systems. The aim
of this paper is to establish similar
connexions between infinite trace monoids,
PoSets and event structures. We prove that
the set of finite and infinite traces with
the prefix order is a \emph{Scott-domain} and a
\emph{coherently complete prime algebraic PoSet}.
Moreover, we establish a representation
theorem between the class of finite and
infinite trace PoSets and a subclass of
labelled prime event structures.}
}
@article{PG-AP-WZ-TCS-94,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Gastin, Paul and Petit, Antoine and
Zielonka, Wieslaw},
title = {An Extension of {K}leene's and {O}chma{\'n}ski's
Theorems to Infinite Traces},
volume = {125},
number = {2},
pages = {167-204},
year = {1994},
month = mar,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/TCS94gpz.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/TCS94gpz.ps},
abstract = {As was noted by
Mazurkiewicz, traces constitute a
convenient tool for describing finite
behaviour of concurrent systems.
Extending in a natural way
Mazurkiewicz's original definition,
infinite traces have been recently
introduced enabling to deal with
infinite behaviour of non-terminating
concurrent systems. In this paper we
examine the basic families of
recognizable sets and of rational sets
of infinite traces. The seminal Kleene
characterization of recognizable
subsets of the free monoid and its
subsequent extensions to infinite words
due to B{\"u}chi and to finite traces due
to Ochma{\'n}ski are the cornestones of the
corresponding theories. The main result
of our paper is an extension of these
characterizations to the domain of
infinite traces. Using recognizing and
weakly recognizing morphisms, as well
as a generalization of the
Sch{\"u}tzenberger product of monoids, we
prove various closure properties of
recognizable trace languages. Moreover,
we establish normal form
representations for recognizable and
rational sets of infinite traces.}
}
@incollection{PG-AP-TB-95,
author = {Gastin, Paul and Petit, Antoine},
title = {Infinite traces},
editor = {Diekert, Volker and Rozenberg, Grzegorz},
booktitle = {The Book of Traces},
chapter = {11},
type = {chapter},
pages = {393-486},
year = {1995},
publisher = {World Scientific},
nopsgz = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PSGZ/InfiniteTraces.ps.gz},
nops = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/InfiniteTraces.ps}
}
@article{VD-PG-AP-IC-95,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Diekert, Volker and Gastin, Paul and
Petit, Antoine},
title = {Rational and Recognizable Complex Trace Languages},
volume = {116},
number = {1},
pages = {134-153},
year = {1995},
month = jan,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/IC95dgp.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/IC95dgp.ps},
abstract = {Mazurkiewicz defined traces
as an algebraic model of finite concurrent
processes. In order to modelize
non-terminating processes a good notion of
infinite trace was needed, which finally
led to the notion of complex trace. For
complex traces an associative
concatenation and omega-iteration are
defined. This paper defines and
investigates rational and recognizable
complex trace languages. We prove various
closure results such as the closure under
boolean operations (for recognizable
languages), concatenation, and left and
right quotients by recognizable sets. Then
we study sufficient conditions ensuring
the recognizability of the finite and
infinite iterations of complex trace
languages. We introduce a generalization
of the notion of concurrent iteration
which leads to the main result of the
paper: the generalization of Kleene's and
Ochma{\'n}ski's theorems to complex trace
languages.}
}
@article{GR95,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Gastin, Paul and Rutten, Jan},
editor = {Gastin, Paul and Rutten, Jan},
title = {Selected papers of the workshop on \emph{Topology and
Completion in
Semantics}, Chartes, France, November 1993},
year = 1995,
volume = 151,
number = 1,
month = nov
}
@inproceedings{BG95,
address = {Prague, Czech Republic},
month = aug,
year = 1995,
volume = 969,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Wiedermann, Jir{\'i} and H{\'a}jek, Petr},
acronym = {{MFCS}'95},
booktitle = {{P}roceedings of the 20th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'95)},
author = {Bauget, Serge and Gastin, Paul},
title = {On congruences and partial orders},
pages = {434-443},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Mfcs95bg.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Mfcs95bg.ps},
abstract = {Mazurkiewicz trace theory is not powerful enough to describe
concurrency paradigms as, for instance, the {"}Producer\slash
Consumer{"}. We propose in this paper a generalization of
Mazurkiewicz trace monoids which allows to model such
problems. We consider quotients of the free monoids by
congruences which preserve the commutative images of words.
An equivalence class in the quotient monoid consists of all
the sequential observations of a distributed computation. In
order to characterize congruences which do model
concurrency, we study the relationship of this approach and
the classical representation of distributed computations
with partial orders. We show that the only congruences for
which the classes can be represented by partial orders and
for which the concatenation transfers modularly to partial
orders are congruences generated by commutations, that is
trace congruences. We prove necessary conditions and
sufficient conditions on congruences so that their classes
can be represented by partial orders. In particular, an
important sufficient condition covers both trace congruences
and the {"}Producer\slash Consumer{"} congruence.}
}
@inproceedings{DG95,
address = {Szeged, Hungary},
month = jul,
year = 1995,
volume = 944,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {F{\"u}l{\"o}p, Zolt{\'a}n and G{\'e}cseg, Ferenc},
acronym = {{ICALP}'95},
booktitle = {{P}roceedings of the 22th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming
({ICALP}'95)},
author = {Diekert, Volker and Gastin, Paul},
title = {A domain for concurrent termination:
A generalization of {M}azurkiewicz traces},
pages = {15-26},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Icalp95dg.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Icalp95dg.ps},
abstract = {This paper generalizes the concept of Mazurkiewicz traces to a
fuzzy description of a concurrent process, where a known
prefix is given in a first component and a second alphabetic
component yields necessary information about future actions.
This allows to define a good semantic domain where the
concatenation is continuous with respect to the Scott- and
to the Lawson topology. For this, we define the notion of
alpha-trace and of delta-trace. We show various mathematical
results proving thereby the soundness of our approach. Our
theory is a proper generalization of the theory of finite
and infinite words (with explicit termination) and of the
theory of finite and infinite (real and complex) traces. We
make use of trace theory, domain theory, and topology.}
}
@inproceedings{BB-PG-AP-stacs96,
address = {Grenoble, France},
month = feb,
year = 1996,
volume = 1046,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Puech, Claude and Reischuk, R{\"u}diger},
acronym = {{STACS}'96},
booktitle = {{P}roceedings of the 13th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'96)},
author = {B{\'e}rard, B{\'e}atrice and Gastin, Paul and
Petit, Antoine},
title = {On the Power of Non-Observable Actions in Timed
Automata},
pages = {257-268},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BGP-stacs96.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BGP-stacs96.ps},
abstract = {Timed finite automata, introduced by Alur and Dill, are one of
the most widely studied models for real-time systems. We
focus in this paper on the power of silent transitions, \emph{i.e.}
\(\epsilon\)-transitions, in such automata. We show that
\(\epsilon\)-transitions strictly increase the power of timed
automata and that the class of timed languages recognized by
automata with \(\epsilon\)-transitions is much more robust than
the corresponding class without \(\epsilon\)-transition. Our main
result shows that \(\epsilon\)-transitions increase the power of
these automata only if they reset clocks.}
}
@inproceedings{VD-PG-AP-dlt96,
address = {Magdeburg, Germany},
year = 1996,
publisher = {World Scientific},
editor = {Dassow, J{\"u}rgen and Rozenberg, Grzegorz and
Salomaa, Arto},
acronym = {{DLT}'95},
booktitle = {{P}roceedings of the 2nd {I}nternational
{C}onference on {D}evelopments in {L}anguage {T}heory
({DLT}'95)},
author = {Diekert, Volker and Gastin, Paul and
Petit, Antoine},
title = {Recent Developments in Trace Theory},
pages = {373-385},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DGP-dlt95.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DGP-dlt95.ps},
abstract = {In this paper we give a survey on some active research in the
theory of Mazurkiewicz traces. We restrict our attention to
some few topics: recognizable languages, asynchronous
automata including infinite traces, trace codings, and trace
rewriting.}
}
@inproceedings{DrGa96,
address = {Pisa, Italy},
month = aug,
year = 1996,
volume = 1119,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Montanari, Ugo and Sassone, Vladimiro},
acronym = {{CONCUR}'96},
booktitle = {{P}roceedings of the 7th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'96)},
author = {Droste, Manfred and Gastin, Paul},
title = {Asynchronous cellular automata for Pomsets without
auto-concurrency},
pages = {627-638},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Concur96dg.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Concur96dg.ps},
abstract = {This paper extends to pomsets without auto-concurrency the
fundamental notion of asynchronous cellular automata (ACA)
which was originally introduced for traces by~Zielonka. We
generalize to pomsets the notion of asynchronous mapping
introduced by~Zielonka and we show how to construct a
deterministic ACA from an asynchronous mapping. Our main
result generalizes B{\"u}chi's theorem for a class of pomsets
without auto-concurrency which satisfy a natural axiom. This
axiom ensures that an asynchronous cellular automaton works
on the pomset as a concurrent read owner write machine. More
precisely, we prove the equivalence between
non-deterministic~ACA, deterministic~ACA and monadic second
order logic for this class of pomsets.}
}
@inproceedings{VD-PG-AP-stacs97,
address = {L{\"u}beck, Germany},
month = feb,
year = 1997,
volume = 1200,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Reischuk, R{\"u}diger and Morvan, Michel},
acronym = {{STACS}'97},
booktitle = {{P}roceedings of the 14th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'97)},
author = {Diekert, Volker and Gastin, Paul and Petit, Antoine},
title = {Removing {{\(\epsilon\)}}-Transitions in Timed Automata},
pages = {583-594},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DGP-stacs97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DGP-stacs97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DGP-stacs97.pdf},
abstract = {Timed automata are among the most widely studied models for
real-time systems. Silent transitions, \emph{i.e.},
\(\epsilon\)-transitions, have already been proposed in the
original paper on timed automata by Alur and Dill. B{\'e}rard,
Gastin and Petit have shown that \(\epsilon\)-transitions
can be removed, if they do not reset clocks; moreover
\(\epsilon\)-transitions strictly increase the power of timed
automata, if there is a self-loop containing
\(\epsilon\)-transitions which reset some clocks. This paper left
open the problem about the power of the \(\epsilon\)-transitions
which reset clocks, if they do not lie on any cycle.\par
The present paper settles this open question. Precisely, we
prove that a timed automaton such that no \(\epsilon\)-transition
with nonempty reset set lies on any directed cycle can be
effectively transformed into a timed automaton without
\(\epsilon\)-transitions. Interestingly, this main result holds
under the assumption of non-Zenoness and it is false
otherwise.\par
Besides, we develop a promising new technique based on a
notion of precise
time which allows to show that some timed languages are not
recognizable by any \(\epsilon\)-free timed automaton.}
}
@inproceedings{DrGa97,
address = {Bologna, Italy},
month = jul,
year = 1997,
volume = 1256,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Degano, Pierpaolo and Gorrieri, Roberto and Marchetti-Spaccamela, Alberto},
acronym = {{ICALP}'97},
booktitle = {{P}roceedings of the 24th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming
({ICALP}'97)},
author = {Droste, Manfred and Gastin, Paul},
title = {On recognizable and rational formal power series
in partially commuting variables},
pages = {682-692},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/Icalp97dg.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Icalp97dg.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Icalp97dg.pdf},
abstract = {Kleene's theorem on the coincidence of regular and rational
languages in free monoids has been generalized by
Sch{\"u}tzenberger to a description of the recognizable formal
power series in non-commuting variables over arbitrary
semi-rings, and by Ochma\'nski to a characterization of the
recognizable languages in trace monoids. Here we will
describe the recognizable formal power series over arbitrary
semi-rings and in partially commuting variables, \emph{i.e.} over
trace monoids. We prove that the recognizable series are
certain rational power series, which can be constructed from
the polynomials by using the operations sum, product and a
restricted star which is applied only to series for which
the elements in the support all have the same connected
alphabet. The converse is true if the underlying semi-ring
is commutative. It is shown that these assumptions are
necessary. This provides a joint generalization of both
Sch{\"u}tzenberger's and Ochma\'nski's theorems. }
}
@techreport{DG97j,
author = {Droste, Manfred and Gastin, Paul},
title = {Asynchronous cellular automata and
logic for pomsets without auto-concurrency},
institution = {Laboratoire d'Informatique Algorithmique, Fondements et
Applications, Paris, France},
type = {Technical Report},
number = {97.24},
year = 1997,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ACAj97dg.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ACAj97dg.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ACAj97dg.pdf},
abstract = {This paper extends to pomsets without auto-concurrency the
fundamental notion of asynchronous cellular automata~(ACA)
which was originally introduced for traces by Zielonka. We
generalize to pomsets the notion of asynchronous mapping
introduced by Zielonka and we show how to construct a
deterministic ACA from an asynchronous mapping. Our main
result generalizes B{\"u}chi's theorem for finite words to a
class of pomsets without auto-concurrency which satisfy a
natural axiom. This axiom ensures that an asynchronous
cellular automaton works on the pomset as a concurrent read
and exclusive owner write machine. More precisely, we prove
the equivalence between non deterministic ACA, deterministic
ACA and monadic second order logic for this class of
pomsets.}
}
@article{BB-VD-PG-AP-98,
publisher = {{IOS} Press},
journal = {Fundamenta Informaticae},
author = {B{\'e}rard, B{\'e}atrice and Diekert, Volker and
Gastin, Paul and Petit, Antoine},
title = {Characterization of the Expressive Power of Silent
Transitions in Timed Automata},
volume = {36},
number = {2},
pages = {145-182},
year = {1998},
month = nov,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BDGP-FUNDI98.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BDGP-FUNDI98.ps},
abstract = {Timed automata are among the
most widely studied models for real-time
systems. Silent transitions (or
\(\epsilon\)-transitions) have already been
proposed in the original paper on timed
automata by Alur and~Dill. We show that the
class of timed languages recognized by
automata with \(\epsilon\)-transitions, is more
robust and more expressive than the
corresponding class without
\(\epsilon\)-transitions. \par
We then focus on \(\epsilon\)-transitions which do
not reset clocks. We propose an algorithm to
construct, given a timed automaton, an
equivalent one without such transitions. This
algorithm is in two steps, it first suppresses
the cycles of \(\epsilon\)-transitions without
reset and then the remaining ones.\par
Then, we prove that a timed automaton such
that no \(\epsilon\)-transition which resets clocks
lies on any directed cycle, can be effectively
transformed into a timed automaton without
\(\epsilon\)-transitions. Interestingly, this main
result holds under the assumption of
non-Zenoness and it is false otherwise.\par
To complete the picture, we exhibit a simple
timed automaton with an \(\epsilon\)-transition,
which resets some clock, on a cycle and which
is not equivalent to any \(\epsilon\)-free timed
automaton. To show this, we develop a
promising new technique based on the notion of
precise action.}
}
@book{LA-PG-BP-AP-NP-PW-livre98,
author = {Albert, Luc and Gastin, Paul and
Petazzoni, Bruno and Petit, Antoine
and Puech, Nicolas and Weil, Pascal},
title = {Cours et exercices d'informatique, Classes
pr{\'e}paratoires, premier et second cycles
universitaires},
year = {1998},
month = jun,
publisher = {Vuibert},
isbn = {2-7117-8621-8},
lsv-lang = {FR}
}
@inproceedings{PG-RM-AP-mfcs98,
address = {Brno, Czech Republic},
month = aug,
year = 1998,
volume = 1450,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Brim, Lubos and Gruska, Jozef and Zlatuska, Jir{\'i}},
acronym = {{MFCS}'98},
booktitle = {{P}roceedings of the 23rd
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'98)},
author = {Gastin, Paul and Meyer, Rapha{\"e}l and
Petit, Antoine},
title = {A (non-elementary) modular decision procedure for
{LTrL}},
pages = {356-365},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GMP-mfcs98.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GMP-mfcs98.ps},
abstract = {Thiagarajan and Walukiewicz have defined a
temporal logic~LTrL on Mazurkiewicz
traces, patterned on the famous
propositional temporal logic of linear
time~LTL defined by Pnueli. They have
shown that this logic is equal in
expressive power to the first order theory
of finite and infinite traces.\par
The hopes to get an {"}easy{"} decision
procedure for~LTrL, as it is the case
for~LTL, vanished very recently due to a
result of Walukiewicz who showed that the
decision procedure for~LTrL is
non-elementary. However, tools like Mona
or Mosel show that it is possible to
handle non-elementary logics on
significant examples. Therefore, it
appears worthwhile to have a direct
decision procedure for LTrL.\par
In this paper we propose such a decision
procedure, in a modular way. Since the
logic~LTrL is not pure future, our
algorithm constructs by induction a finite
family of B{\"u}chi automata for each
LTrL-formula. As expected by the results
of Walukiewicz, the main difficulty comes
from the {"}Until{"} operator.}
}
@article{DiGa98,
publisher = {Springer},
journal = {Acta Informatica},
author = {Diekert, Volker and Gastin, Paul},
title = {Approximating traces},
volume = 35,
number = 7,
year = 1998,
pages = {567-593},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Alphatracesdg.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Alphatracesdg.ps},
abstract = {In order to give a semantics to
concurrent processes, one needs a powerful
model which enjoys many important mathematical
properties. We generalize Mazurkiewicz
(infinite) traces by adding an information
concerning the possible continuations of a
process. This allows to define an
approximation order and a composition. We
obtain a prime algebraic coherently complete
domain where the compacts are exactly the
finite approximations of actual processes. The
composition is shown to be monotone and
\(\sqcup\)-continuous. We define a suitable
metric which induces the Lawson topology and
yields a complete and compact metric space.
The finite approximations of processes form a
dense subset and the composition is uniformly
continuous.}
}
@article{DrGa99j,
author = {Droste, Manfred and Gastin, Paul},
title = {The {K}leene-{S}ch{\"u}tzenberger theorem for formal power series
in partially commuting variables},
volume = 153,
number = 1,
year = 1999,
month = aug,
pages = {47-80},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/IC99dg.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/IC99dg.ps},
abstract = {Kleene's theorem on the
coincidence of regular and rational
languages in free monoids has been
generalized by Sch{\"u}tzenberger to a
description of the recognizable formal power
series in non-commuting variables over
arbitrary semi-rings, and by Ochma{\'n}ski to a
characterization of the recognizable
languages in trace monoids.\par
We will describe the recognizable formal
power series over arbitrary semirings and in
partially commuting variables, \emph{i.e.} over
trace monoids. We prove that the
recognizable series are certain rational
power series, which can be constructed from
the polynomials by using the operations sum,
product and a restricted star which is
applied only to series for which the
elements in the support all have the same
connected alphabet. The converse is true if
the underlying semiring is commutative.\par
Moreover, if in addition the semiring is
idempotent then the same result holds with a
star restricted to series for which the
elements in the support have connected
(possibly different) alphabets. It is shown
that these assumptions over the semiring are
necessary. This provides a joint
generalization of Kleene's, Sch{\"u}tzenberger's
and Ochma{\'n}ski's theorems.}
}
@inproceedings{GaMi99,
address = {Madrid, Spain},
month = sep,
year = 1999,
volume = 1683,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Flum, J{\"o}rg and Rodr{\'\i}guez-Artalejo, Mario},
acronym = {{CSL}'99},
booktitle = {{S}elected {P}apers from the 13th {I}nternational
{W}orkshop on {C}omputer {S}cience {L}ogic
({CSL}'99)},
author = {Gastin, Paul and Mislove, Michael W.},
title = {A truly concurrent semantics for a
simple parallel programming language},
pages = {515-529},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Csl99gm.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Csl99gm.ps},
abstract = {This paper represents the
beginning of a study aimed at devising
semantic models for true concurrency that
provide clear distinctions between
concurrency, parallelism and choice. We
present a simple programming language which
includes (weakly) sequential composition,
asynchronous and synchronous parallel
composition, a restriction operator, and
that supports recursion. We develop an
operational and a denotational semantics for
this language, and we obtain a congruence
theorem relating the behavior of a process
as described by the transition system to the
meaning of the process in the denotational
model. This implies that the denotational
model is adequate with respect to the
operational model. Our denotational model is
based on the resource traces of Gastin and
Teodesiu, and since a single resource trace
represents all possible executions of a
concurrent process, we are able to model
each term of our concurrent language by a
single trace. Therefore we obtain a
deterministic semantics for our language and
we are able to model parallelism without
introducing nondeterminism.}
}
@inproceedings{DiGa99,
address = {Madrid, Spain},
month = sep,
year = 1999,
volume = 1683,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Flum, J{\"o}rg and Rodr{\'\i}guez-Artalejo, Mario},
acronym = {{CSL}'99},
booktitle = {{S}elected {P}apers from the 13th {I}nternational
{W}orkshop on {C}omputer {S}cience {L}ogic
({CSL}'99)},
author = {Diekert, Volker and Gastin, Paul},
title = {An expressively complete temporal logic without past tense
operators for {M}azurkiewicz traces},
pages = {188-203},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Csl99dg.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Csl99dg.ps},
abstract = {Mazurkiewicz traces are a widely
accepted model of concurrent systems. We
introduce a linear time temporal logic which has
the same expressive power as the first order
theory of finite (infinite resp.) traces. The
main contribution of the paper is that we only
use future tense modalities in order to obtain
expressive completeness. Our proof is direct and
uses no reduction to words. As a formal
consequence Kamp's theorem for both finite and
infinite words becomes a corollary. This direct
approach became possible due to a new proof
technique of Wilke developed for the case of
finite words.}
}
@article{DrGaKu00,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Droste, Manfred and Gastin, Paul and Kuske, Dietrich},
title = {Asynchronous cellular automata for pomsets},
volume = 247,
number = {1-2},
year = 2000,
month = sep,
pages = {1-38},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DGK-TCS00.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DGK-TCS00.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DGK-TCS00.ps},
abstract = {This paper extends to pomsets without
auto-concurrency the fundamental notion of
asynchronous cellular automata (ACA) which was
originally introduced for traces by Zielonka. We
generalize to pomsets the notion of asynchronous
mapping introduced by Cori, M{\'e}tivier and Zielonka
and we show how to construct a deterministic ACA from
an asynchronous mapping. \par
Then we investigate the relation between the
expressiveness of monadic second order logic,
nondeterministic ACAs and deterministic ACAs. We can
generalize B{\"u}chi's theorem for finite words to a class
of pomsets without auto-concurrency which satisfy a
natural axiom. This axiom ensures that an asynchronous
cellular automaton works on the pomset as a concurrent
read and exclusive owner write machine. More
precisely, in this class non-deterministic ACAs,
deterministic ACAs and monadic second order logic have
the same expressive power. \par
Then we consider a class where deterministic ACAs are
strictly weaker than nondeterministic ones. But in
this class nondeterministic ACAs still capture monadic
second order logic. Finally it is shown that even this
equivalence does not hold in the class of all pomsets
since there the class of recognizable pomset languages
is not closed under complementation.}
}
@inproceedings{DiGa00,
address = {Geneva, Switzerland},
month = jul,
year = 2000,
volume = 1853,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Montanari, Ugo and Rolim, Jos{\'e} D. P. and
Welzl, Emo},
acronym = {{ICALP} 2000},
booktitle = {{P}roceedings of the 27th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming
({ICALP} 2000)},
author = {Diekert, Volker and Gastin, Paul},
title = {{LTL} is expressively complete for {M}azurkiewicz traces},
pages = {211-222},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Icalp00dg.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Icalp00dg.ps},
abstract = {A long standing open problem in the
theory of (Mazurkiewicz) traces has been the
question whether LTL (Linear Time Logic) is
expressively complete with respect to the first
order theory. We solve this problem positively for
finite and infinite traces and for the simplest
temporal logic, which is based only on next and
until modalities. Similar results were established
previously, but they were all weaker, since they
used additional past or future modalities. Another
feature of our work is that our proof is direct and
does not use any reduction to the word case. It is
based on an algebraic characterization of first
order trace languages, following a proof technique
introduced recently by Thomas Wilke in order to
prove the expressive completeness of LTL for
finite words.}
}
@inproceedings{DrGa00,
address = {Moscow, Russia},
month = jun,
year = 2000,
publisher = {Springer},
editor = {Krob, Daniel and Mikhalev, Alexander A. and Mikhalev, Alexander V.},
acronym = {{FPSAC}'00},
booktitle = {{P}roceedings of the 12th {I}nternational {C}onference on
{F}ormal {P}ower {S}eries and {A}lgebraic
{C}ombinatorics ({FPSAC}'00)},
author = {Droste, Manfred and Gastin, Paul},
title = {On aperiodic and star-free formal power series
in partially commuting variables},
pages = {158-169},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Fpsac00dg.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Fpsac00dg.ps},
abstract = {Formal power series over
non-commuting variables have been
investigated as representations of the
behaviour of automata with multiplicities.
Here we introduce and investigate the
concepts of aperiodic and of star-free
formal power series over semirings and
partially commuting variables. We prove that
if the semiring~\(K\) is idempotent and
commutative, or if \(K\) is idempotent and the
variables are non-commuting, then the
product of any two aperiodic series is again
aperiodic. We also show that if \(K\) is
idempotent and the matrix monoids over \(K\)
have a Burnside property (satisfied, \emph{e.g.} by
the tropical semiring), then the aperiodic
and the star-free series coincide. This
generalizes a classical result of
Sch{\"u}tzenberger~(1961) for aperiodic regular
languages and contains a result of Guaiana,
Restivo and Salemi~(1992) on aperiodic trace
languages.}
}
@inproceedings{DiGa01lpar,
address = {Havana, Cuba},
month = dec,
year = 2001,
volume = 2250,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
editor = {Nieuwenhuis, Robert and Voronkov, Andrei},
acronym = {{LPAR}'01},
booktitle = {{P}roceedings of the 8th {I}nternational
{C}onference on {L}ogic for {P}rogramming,
{A}rtificial {I}ntelligence, and {R}easoning
({LPAR}'01)},
author = {Diekert, Volker and Gastin, Paul},
title = {Local Temporal Logic is Expressively Complete
for Cograph Dependence Alphabets},
pages = {55-69},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Lpar01dg.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Lpar01dg.ps},
abstract = {Recently, local logics for
Mazurkiewicz traces are of increasing
interest. This is mainly due to the fact
that the satisfiability problem has the
same complexity as in the word case. If we
focus on a purely local interpretation of
formulae at vertices (or events) of a
trace, then the satisfiability problem of
linear temporal logics over traces turns
out to be PSPACE-complete. But now the
difficult problem is to obtain expressive
completeness results with respect to first
order logic. \par
The main result of the paper shows such an
expressive completeness result, if the
underlying dependence alphabet is a
cograph, \emph{i.e.}, if all traces are series
parallel graphs. Moreover, we show that
this is the best we can expect in our
setting: If the dependence alphabet is not
a cograph, then we cannot express all
first order properties.}
}
@inproceedings{GaOd01,
address = {Paris, France},
month = jul,
year = 2001,
volume = 2102,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Berry, G{\'e}rard and Comon, Hubert and Finkel, Alain},
acronym = {{CAV}'01},
booktitle = {{P}roceedings of the 13th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'01)},
author = {Gastin, Paul and Oddoux, Denis},
title = {Fast {LTL} to {B}{\"u}chi Automata Translation},
pages = {53-65},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Cav01go.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Cav01go.ps},
abstract = {We present an algorithm to generate
B{\"u}chi automata from LTL formulae. This algorithm
generates a very weak alternating automaton and
then transforms it into a B{\"u}chi automaton, using a
generalized B{\"u}chi automaton as an intermediate
step. Each automaton is simplified on-the-fly in
order to save memory and time. As usual we
simplify the LTL formula before any treatment. We
implemented this algorithm and compared it with
Spin: the experiments show that our algorithm is
much more efficient than Spin. The criteria of
comparison are the size of the resulting
automaton, the time of the computation and the
memory used. Our implementation is available on
the web at the following address:
\url{http://verif.liafa.jussieu.fr/ltl2ba}}
}
@inproceedings{DeGa01,
address = {Toronto, Canada},
month = may,
year = 2001,
volume = 2057,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Dwyer, Matthew B.},
acronym = {{SPIN}'01},
booktitle = {{P}roceedings of the 8th {I}nternational
{SPIN} {W}orkshop on {M}odel {C}hecking {S}oftware
({SPIN}'01)},
author = {Derepas, Fabrice and Gastin, Paul},
title = {Model Checking Systems of Replicated Processes with {SPIN}},
pages = {235-251},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Spin01dg.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Spin01dg.ps},
abstract = {This paper describes a
reduction technique which is very useful
against the state explosion problem
which occurs when model checking
distributed systems with several
instances of the same process. Our
technique uses symmetry which appears in
the system. Exchanging those instances
is not as simple as it seems, because
there can be a lot of references to
process locations in the system. We
implemented a solution using the Spin
model checker, and added two keywords to
the Promela language to handle these new
concepts.}
}
@inproceedings{DeGaPl01,
address = {Berlin, Germany},
month = mar,
year = 2001,
volume = 2021,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Oliveira, Jos{\'e} Nuno and Zave, Pamela},
acronym = {{FME}'01},
booktitle = {{F}ormal {M}ethods for {I}ncreasing {S}oftware
{P}roductivity~---
{P}roceedings of the {I}nternational {S}ymposium of {F}ormal
{M}ethods {E}urope ({FME}'01)},
author = {Derepas, Fabrice and Gastin, Paul and
Plainfoss{\'e}, David},
title = {Avoiding state explosion for distributed systems
with timestamps},
pages = {119-134},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Fme01dgp.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Fme01dgp.ps},
abstract = {This paper describes a
reduction technique which is very useful
against the state explosion problem which
occurs when model checking many distributed
systems. Timestamps are often used to keep
track of the relative order of events. They
are usually implemented with very large
counters and therefore they generate state
explosion. The aim of this paper is to
present a very efficient reduction of the
state space generated by a model checker when
using timestamps. The basic idea is to map
the timestamps values to the smallest
possible range. This is done dynamically and
on-the-fly by adding to the model checker a
call to a reduction function after each newly
generated state. Our reduction works for
model checkers using explicit state
enumeration and does not require any change
in the model. Our method has been applied to
an industrial example and the reduction
obtained was spectacular.}
}
@article{DG02JALC,
journal = {Journal of Automata, Languages and Combinatorics},
author = {Droste, Manfred and Gastin, Paul},
editor = {Droste, Manfred and Gastin, Paul},
title = {Selected papers of the workshop on \emph{Logic and Algebra in
Concurrency}, Dresden, Germany, September 2000},
volume = 7,
number = 2,
year = 2002
}
@incollection{DiGa02Roz,
missingmonth = mar,
missingnmonth = 3,
year = 2002,
volume = 2300,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Brauer, Wilfried and
Ehrig, Hartmut and
Karhum{\"a}ki, Juhani and
Salomaa, Arto},
acronym = {{F}ormal and {N}atural {C}omputing},
booktitle = {{F}ormal and {N}atural {C}omputing~---
{E}ssays {D}edicated to {G}rzegorz {R}ozenberg},
author = {Diekert, Volker and Gastin, Paul},
title = {Safety and Liveness Properties for Real Traces and
a Direct Translation from {LTL} to Monoids},
pages = {26-38},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/diegas01-3.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/diegas01-3.ps},
doi = {10.1007/3-540-45711-9_2},
abstract = { For infinite words there are
well-known characterizations of safety and liveness
properties. We extend these results to real
Mazurkiewicz traces. This is possible due to a
result, which has been established recently: Every
first-order definable real trace language is
definable in linear temporal logic using future
tense operators, only. We show that the canonical
choice for a topological characterization of safety
and liveness properties is given by the Scott
topology. In this paper we use an algebraic approach
where we work with aperiodic monoids. Therefore we
also give a direct translation from temporal logic
to aperiodic monoids which is of independent
interest.}
}
@article{DiGa02jcss,
publisher = {Elsevier Science Publishers},
journal = {Journal of Computer and System Sciences},
author = {Diekert, Volker and Gastin, Paul},
title = {{LTL} is expressively complete for {M}azurkiewicz traces},
volume = 64,
number = 2,
year = 2002,
month = mar,
pages = {396-418},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/JCSS02dg.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/JCSS02dg.ps},
abstract = {A long standing open problem in the
theory of (Mazurkiewicz) traces has been the
question whether LTL (Linear Temporal Logic) is
expressively complete with respect to the first
order theory. We solve this problem positively for
finite and infinite traces and for the simplest
temporal logic, which is based only on next and
until modalities. Similar results were established
previously, but they were all weaker, since they
used additional past or future modalities. Another
feature of our work is that our proof is direct and
does not use any reduction to the word case.}
}
@article{GaMi02tcs,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Gastin, Paul and Mislove, Michael W.},
title = {A truly concurrent semantics for a
process algebra using resource pomsets},
volume = 281,
number = {1-2},
year = 2002,
month = jun,
pages = {369-421},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GM-TCS02.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GM-TCS02.ps},
abstract = {In this paper we study a process
algebra whose semantics is based on true
concurrency. In our model, actions are defined in
terms of the resources they need to execute, which
allows a simple definition of a weak sequential
composition operator. This operator allows actions
which do not share any resources to execute
concurrently, while dependent actions have to occur
sequentially. This weak sequential composition
operation may be used to automatically parallelize a
sequential process. We add to this operator the
customary (strict) sequential composition and a
parallel composition allowing synchronization on
specified actions. Our language also supports a
hiding operator that allows the hiding of actions
and even of individual resources used by actions.
Strict sequential composition and hiding require
that we generalize from the realm of Mazurkiewicz
traces to that of pomsets, since these operations
introduce {"}over-synchronized{"} traces~--- ones for
which a pair of independent actions may occur
sequentially. Our language also supports recursion
and our semantics makes the unwinding of recursion
visible by the use of special resources used to
label unwindings. This was done on purpose in order
to enable the observation of divergence, but the
usual semantics that does not observe unwindings can
be obtained by using the hiding operator to abstract
away from these special resources. We give both an
SOS-style operational semantics for our language, as
well as a denotational semantics based on resource
pomsets. Generalizing results from our earlier work
in this area, we derive a congruence theorem for our
language which shows that the SOS-style operational
rules induce the same equivalence relation on the
language as the semantic map does. A corollary is
that our denotational model is both adequate and
fully abstract relative to the behavior function
defined from our operational semantics. This
behavior consists naturally of the strings of
actions the process can perform. This work continues
our study into modelling concurrency in the absence
of nondeterminism. In particular, our language is
deterministic.}
}
@article{GaTe02,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Gastin, Paul and Teodosiu, Dan},
title = {Resource traces: A domain for processes sharing exclusive
resources},
volume = 278,
number = {1-2},
year = 2002,
month = may,
pages = {195-221},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GT-TCS02.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GT-TCS02.ps},
abstract = {The theory of finite and infinite words
with explicit termination is commonly used to give
denotational semantics for algebras of sequential
processes. In this paper we generalize this theory
to the case of partially terminated concurrent
processes synchronizing on a fixed set of shared
exclusive resources. \par
We start with an alphabet of actions, a set of
resources, and a resource map assigning to each
action the non-empty subset of resources it uses.
Actions that do not share common resources are
declared independent. The specification we use for
partially terminated processes (resource traces) is
similar to failure semantics. It consists of two
components: an already observed part represented as
an action-labeled event structure (Mazurkiewicz
trace), and a guard set containing the resources
granted to the process for its further development.
A process concatenation is then defined such that
independent actions can be dispatched concurrently.
Specification refinement leads to the definition of
a natural approximation ordering between processes
which generates a coherently complete prime
algebraic Scott domain, where process concatenation
is continuous in both arguments. Furthermore, we
define a natural ultrametric on processes based on
prefix information. The induced topology is shown to
be equivalent to the compact Lawson topology
generated by the approximation ordering. Moreover,
process concatenation is shown to be uniformly
continuous with respect to the defined ultrametric.
\par
We develop a mathematical theory which perfectly
extends the central properties of the domain of
finite and infinte words with explicit termination
and the domain of finite and infinite Mazurkiewicz
traces. Its natural semantics is well suited to the
design of modular denotational semantics for
algebras of processes sharing exclusive resources
such as programs using some set of shared registers
(PRAM) or concurrent sequential processes
synchronizing over exclusive communication channels
(CSP).}
}
@inproceedings{GaMu02icalp,
address = {M{\'a}laga, Spain},
month = jul,
year = 2002,
volume = 2380,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Widmayer, Peter and
Triguero Ruiz, Francisco and Morales Bueno, Rafael and
Hennessy, Matthew and Eidenbenz, Stephan and Conejo, Ricardo},
acronym = {{ICALP}'02},
booktitle = {{P}roceedings of the 29th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming
({ICALP}'02)},
author = {Gastin, Paul and Mukund, Madhavan},
title = {An Elementary Expressively Complete Temporal Logic
for {M}azurkiewicz Traces},
pages = {938-949},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/gasmuk02long2.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/gasmuk02long2.ps},
abstract = {In contrast to the
classical setting of sequences, no
temporal logic has yet been identified
over Mazurkiewicz traces that is
equivalent to the first-order theory of
traces and yet admits an elementary
decision procedure. In this paper, we
describe a local temporal logic over
traces that is expressively complete
and whose satisfiability problem is in
PSPACE. Contrary to the situation for
sequences, past modalities are
essential for such a logic. A somewhat
unexpected corollary is that
first-order logic with three variables
is expressively complete for traces.}
}
@inproceedings{GaKu03concur,
address = {Marseilles, France},
month = aug,
year = 2003,
volume = 2761,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Amadio, Roberto M. and Lugiez, Denis},
acronym = {{CONCUR}'03},
booktitle = {{P}roceedings of the 14th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'03)},
author = {Gastin, Paul and Kuske, Dietrich},
title = {Satisfiability and Model Checking for {MSO}-definable
Temporal Logics are in {PSPACE}},
pages = {222-236},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/concur03gk-final.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/concur03gk-final.ps},
abstract = {Temporal logics over Mazurkiewicz
traces have been extensively studied over the past
fifteen years. In order to be usable for the
verification of concurrent systems they need to have
reasonable complexity for the satisfiability and the
model checking problems. Whenever a new temporal
logic was introduced, a new proof (usually non
trivial) was needed to establish the complexity of
these problems. In this paper, we introduce a
unified framework to define local temporal logics
over traces. We prove that the satisfiability
problem and the model checking problem for
asynchronous Kripke structures for local temporal
logics over traces are decidable in PSPACE. This
subsumes and sometimes improves all complexity
results previously obtained on local temporal logics
for traces.}
}
@inproceedings{GaMuNa03mfcs,
address = {Bratislava, Slovakia},
month = aug,
year = 2003,
volume = 2747,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Rovan, Branislav and Vojt{\'a}{\v{s}}, Peter},
acronym = {{MFCS}'03},
booktitle = {{P}roceedings of the 28th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'03)},
author = {Gastin, Paul and Mukund, Madhavan and Narayan Kumar, K.},
title = {Local {LTL} with past constants is expressively complete for
{M}azurkiewicz traces},
pages = {429-438},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/mfcs03gmn-final.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/mfcs03gmn-final.ps},
abstract = {To obtain an expressively complete
linear-time temporal logic (LTL) over
Mazurkiewicz traces that is computationally
tractable, we need to interpret formulas locally,
at individual events in a trace, rather than
globally, at configurations. Such local logics
necessarily require past modalities, in contrast
to the classical setting of LTL over sequences.
Earlier attempts at defining expressively
complete local logics have used very general past
modalities as well as filters (side-conditions)
that {"}look sideways{"} and talk of concurrent
events. In this paper, we show that it is
possible to use unfiltered future modalities in
conjunction with past constants and still obtain
a logic that is expressively complete over
traces.}
}
@inproceedings{GaOd03mfcs,
address = {Bratislava, Slovakia},
month = aug,
year = 2003,
volume = 2747,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Rovan, Branislav and Vojt{\'a}{\v{s}}, Peter},
acronym = {{MFCS}'03},
booktitle = {{P}roceedings of the 28th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'03)},
author = {Gastin, Paul and Oddoux, Denis},
title = {{LTL} with past and two-way very-weak alternating automata},
pages = {439-448},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/mfcs03go-final.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/mfcs03go-final.ps},
abstract = {It is crucial for a model
checker using LTL as a specification
language to have very efficient translation
of LTL formulas to B{\"u}chi automata. Most such
algorithms are based on a tableau
construction. Recently, an implementation
using very-weak alternating automata as an
intermediary step proved to be dramatically
faster than previous implementations based
on the tableau construction. In this paper,
we want to generalize this method to PLTL
(LTL with past modalities). For this, we
study two-way very-weak alternating automata
(\(2\)VWAA). Our main result is an efficient
translation of \(2\)VWAA to generalized B{\"u}chi
automata (GBA). Since we can easily
transform a PLTL formula to an equivalent
\(2\)VWAA, this algorithm allows to use PLTL
specifications with classical model checkers
such as SPIN.}
}
@misc{gastin-movep2004,
author = {Gastin, Paul},
title = {Basics of model checking},
year = 2004,
month = dec,
nonote = {-- pages},
howpublished = {Invited tutorial, 6th {W}inter {S}chool on
{M}odelling and {V}erifying {P}arallel {P}rocesses
({MOVEP}'04), Brussels, Belgium}
}
@misc{gastin-epit32,
author = {Gastin, Paul},
title = {Specifications for distributed systems},
year = 2004,
month = apr,
howpublished = {Invited lecture, 32nd {S}pring {S}chool on
{T}heoretical {C}omputer {S}cience ({C}oncurrency {T}heory),
Luminy, France}
}
@article{icomp-DG2004,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Diekert, Volker and Gastin, Paul},
title = {Local temporal logic is expressively complete for
cograph dependence alphabets},
volume = {195},
number = {1-2},
pages = {30-52},
year = 2004,
month = nov,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG04-icomp.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DG04-icomp.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG04-icomp.pdf},
doi = {10.1016/j.ic.2004.08.001},
abstract = {Recently, local logics for Mazurkiewicz
traces are of increasing interest. This is mainly
due to the fact that the satisfiability problem has
the same complexity as in the word case. If we focus
on a purely local interpretation of formulae at
vertices (or events) of a trace, then the
satisfiability problem of linear temporal logics
over traces turns out to be PSPACE-complete. But
now the difficult problem is to obtain expressive
completeness results with respect to first order
logic. \par
The main result of the paper shows such an
expressive completeness result, if the underlying
dependence alphabet is a cograph, \emph{i.e.}
if all
traces are series parallel posets. Moreover, we show
that this is the best we can expect in our setting:
If the dependence alphabet is not a cograph, then we
cannot express all first order properties.}
}
@inproceedings{GaLeZe04fsttcs,
address = {Chennai, India},
month = dec,
year = 2004,
volume = 3328,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Lodaya, Kamal and Mahajan, Meena},
acronym = {{FSTTCS}'04},
booktitle = {{P}roceedings of the 24th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'04)},
author = {Gastin, Paul and Lerman, Benjamin and Zeitoun, Marc},
title = {Distributed games with causal memory are decidable for
series-parallel systems},
pages = {275-286},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GLZ-fsttcs04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GLZ-fsttcs04.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GLZ-fsttcs04.ps},
abstract = {This paper deals with distributed
control problems by means of distributed games
played on Mazurkiewicz traces. The main difference
with other notions of distributed games recently
introduced is that, instead of having a \emph{local} view,
strategies and controllers are able to use a more
accurate memory, based on their \emph{causal} view. Our
main result states that using the causal view makes
the control synthesis problem decidable for
series-parallel systems for \emph{all} recognizable winning
conditions on finite behaviors, while this problem
with local view was proved undecidable even for
reachability conditions.}
}
@article{GaMi04mscs,
publisher = {Cambridge University Press},
journal = {Mathematical Structures in Computer Science},
author = {Gastin, Paul and Mislove, Michael W.},
title = {A simple process algebra based on atomic actions with
resources},
year = 2004,
month = feb,
volume = 14,
number = 1,
pages = {1-55},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GM-mscs04.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GM-mscs04.ps},
doi = {10.1017/S0960129503003943},
abstract = {This paper gives the first truly
concurrent denotational, \emph{i.e.}
compositional
semantics for a simple, deterministic parallel
language. By truly concurrent we mean the
denotational model does not rely on an interleaving
of concurrent actions for its definition. Thus, our
semantics does not reduce parallelism to
nondeterminism, as is done in the more established
approaches to concurrency. We also present a natural
SOS-style operational semantics for our language,
and we prove a congruence theorem relating the two
semantics. This implies the operational model itself
is compositional. The congruence theorem also
implies the denotational model is adequate with
respect to the operational semantics, and we
characterize the relatively mild conditions under
which the denotational semantics is fully abstract
with respect to the operational semantics. \par
Our simple language includes a (weak) sequential
composition operator which takes advantage of the
truly concurrent nature of the semantics, as well as
a parallel composition operator which allows local
events to execute asynchronously, while requiring
synchronizing events to execute simultaneously. In
addition, the language supports a restriction
operator and includes recursion. \par
The denotational semantics also is novel for its
treatment of recursion. The meaning of a recursive
process is defined using a least fixed point on a
subdomain that is determined by the body of the
recursion, and that varies from one process to
another. Nonetheless, the recursion operators in the
language have continuous interpretations in the
denotational model.
Our denotational model is based on a
domain-theoretic generalization of Mazurkiewicz
traces in which the concatenation operator, as well
as the other operators from our language can be
given continuous interpretations.}
}
@inproceedings{GaMoZe04spin,
address = {Barcelona, Spain},
month = apr,
year = 2004,
volume = 2989,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Graf, Susanne and Mounier, Laurent},
acronym = {{SPIN}'04},
booktitle = {{P}roceedings of the 11th {I}nternational
{SPIN} {W}orkshop on {M}odel {C}hecking {S}oftware
({SPIN}'04)},
author = {Gastin, Paul and Moro, Pierre and
Zeitoun, Marc},
title = {Minimization of counterexamples in
{SPIN}},
pages = {92-108},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GMZ-spin04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GMZ-spin04.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GMZ-spin04.ps},
abstract = {We propose an algorithm to find a
counterexample to some property in a finite state
program. This algorithm is derived from SPIN's
one, but it finds a counterexample faster than
SPIN does. In particular it still works in linear
time. Compared with SPIN's algorithm, it requires
only one additional bit per state stored. We
further propose another algorithm to compute a
counterexample of minimal size. Again, this
algorithm does not use more memory than SPIN does
to approximate a minimal counterexample. The cost
to find a counterexample of minimal size is that
one has to revisit more states than SPIN. We
provide an implementation and discuss
experimental results.}
}
@inproceedings{GaLeZe04latin,
address = {Buenos Aires, Argentina},
month = apr,
year = 2004,
volume = 2976,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Farach-Colton, Martin},
acronym = {{LATIN}'04},
booktitle = {{P}roceedings of the 6th {L}atin {A}merican
{S}ymposium on {T}heoretical {I}nformatics
({LATIN}'04)},
author = {Gastin, Paul and Lerman, Benjamin and Zeitoun, Marc},
title = {Distributed games and distributed control for asynchronous
systems},
pages = {455-465},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GLZ-latin04.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GLZ-latin04.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GLZ-latin04.pdf},
abstract = {We introduce distributed games over
asynchronous transition systems to model a
distributed controller synthesis problem. A game
involves two teams and is not turn-based: several
players of both teams may simultaneously be enabled.
We define distributed strategies based on the causal
view that players have of the system. We reduce the
problem of finding a winning distributed strategy
with a given memory to finding a memoryless winning
distributed strategy in a larger distributed game.
We reduce the latter problem to finding a strategy
in a classical \(2\)-player game. This allows to
transfer results from the sequential case to this
distributed setting.}
}
@inproceedings{DiGa04latin,
address = {Buenos Aires, Argentina},
month = apr,
year = 2004,
volume = 2976,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Farach-Colton, Martin},
acronym = {{LATIN}'04},
booktitle = {{P}roceedings of the 6th {L}atin {A}merican
{S}ymposium on {T}heoretical {I}nformatics
({LATIN}'04)},
author = {Diekert, Volker and Gastin, Paul},
title = {Pure future local temporal logics are expressively complete
for {M}azurkiewicz traces},
pages = {232-241},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-latin04.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DG-latin04.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-latin04.pdf},
abstract = {The paper settles a long standing
problem for Mazurkiewicz traces: the pure future
local temporal logic defined with the basic
modalities exists-next and until is expressively
complete. The analogous result with a global
interpretation was solved some years ago by
Thiagarajan and Walukiewicz (1997) and in its
final form without any reference to past tense
constants by Diekert and Gastin (2000). Each, the
(previously known) global or the (new) local
result generalizes Kamp's Theorem for words,
because for sequences local and global viewpoints
coincide. But traces are labelled partial orders
and then the difference between an interpretation
globally over cuts (configurations) or locally at
points (events) is significant. For global
temporal logics the satisfiability problem is
non-elementary (Walukiewicz, 1998), whereas for
local temporal logics both the satisfiability
problem and the model checking problem are sovable
in PSPACE (Gastin and Kuske, 2003) as in the case
of words. This makes local temporal logics much
more attractive.}
}
@misc{gastin-wpv05,
author = {Gastin, Paul},
title = {On the synthesis of distributed controllers},
year = 2005,
month = nov,
howpublished = {Invited talk, Workshop Perspectives in
Verification, in honor of Wolfgang Thomas on the occasion of his
Doctorate Honoris Causa, Cachan, France}
}
@inproceedings{Gastin-ICALP2005,
address = {Lisboa, Portugal},
month = jul,
year = 2005,
volume = {3580},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Caires, Lu{\'\i}s and Italiano, Giuseppe F. and
Monteiro, Lu{\'\i}s and Palamidessi, Catuscia and Yung, Moti},
acronym = {{ICALP}'05},
booktitle = {{P}roceedings of the 32nd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming
({ICALP}'05)},
author = {Droste, Manfred and Gastin, Paul},
title = {Weighted Automata and Weighted Logics},
pages = {513-525},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/icalp05dg-final.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/icalp05dg-final.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/icalp05dg-final.pdf},
doi = {10.1007/11523468_42},
abstract = {Weighted automata are used to
describe quantitative properties in various
areas such as probabilistic systems, image
compression, speech-to-text processing. The
behaviour of such an automaton is a mapping,
called a formal power series, assigning to
each word a weight in some semiring. We
generalize B{\"{u}}chi's and Elgot's
fundamental theorems to this quantitative
setting. We introduce a weighted version of
MSO~logic and prove that, for commutative
semirings, the behaviours of weighted
automata are precisely the formal power
series definable with our weighted logic. We
also consider weighted first-order logic and
show that aperiodic series coincide with the
first-order definable ones, if the semiring
is locally finite, commutative and has some
aperiodicity property.}
}
@inproceedings{GK-concur05,
address = {San Francisco, California, USA},
month = aug,
year = 2005,
volume = 3653,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abadi, Mart{\'\i}n and de Alfaro, Luca},
acronym = {{CONCUR}'05},
booktitle = {{P}roceedings of the 16th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'05)},
author = {Gastin, Paul and Kuske, Dietrich},
title = {Uniform Satisfiability Problem for Local Temporal Logics
over {M}azurkiewicz Traces},
pages = {533-547},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/concur05gk-final.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/concur05gk-final.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/concur05gk-final.ps},
doi = {10.1007/11539452_40},
abstract = {We continue our study of the complexity
of temporal logics over concurrent systems that can be
described by Mazurkiewicz traces. In a previous paper
(CONCUR~2003), we investigated the class of local and
MSO definable temporal logics that capture all known
temporal logics and we showed that the satisfiability
problem for any such logic is in PSPACE (provided the
dependence alphabet is fixed). In this paper, we
concentrate on the uniform satisfiability problem: we
consider the dependence alphabet (\emph{i.e.}, the
architecture of the distributed system) as part of the
input. We prove lower and upper bounds for the uniform
satisfiability problem that depend on the number of
monadic quantifier alternations present in the chosen
MSO-modalities.}
}
@misc{gastin-prefsttcs06,
author = {Gastin, Paul},
title = {Refinements and Abstractions of Signal-Event (Timed) Languages},
year = 2006,
month = dec,
howpublished = {Invited talk, Advances and Issues in Timed Systems,
Kolkata, India}
}
@misc{gastin-wata06,
author = {Gastin, Paul},
title = {Weigthed logics and weighted automata},
year = 2006,
month = mar,
howpublished = {Invited talk, Workshop Weighted Automata: Theory and Applications,
Leipzig, Germany}
}
@misc{gastin-epit06,
author = {Gastin, Paul},
title = {Distributed synthesis: synchronous and asynchronous semantics},
year = 2006,
month = may,
howpublished = {Invited talk, 34{\`e}me {\'E}cole de Printemps en
Informatique Th{\'e}orique, Ile de R{\'e}, France}
}
@misc{gastin-mfps22,
author = {Gastin, Paul},
title = {Refinements and Abstractions of Signal-Event (Timed) Languages},
year = 2006,
month = may,
howpublished = {Invited talk, 22nd {C}onference on
{M}athematical {F}oundations of {P}rogramming
{S}emantics ({MFPS}'06)}
}
@inproceedings{GSZ-fsttcs2006,
address = {Kolkata, India},
month = dec,
year = 2006,
volume = 4337,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Garg, Naveen and Arun-Kumar, S.},
acronym = {{FSTTCS}'06},
booktitle = {{P}roceedings of the 26th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'06)},
author = {Gastin, Paul and Sznajder, Nathalie and Zeitoun, Marc},
title = {Distributed synthesis for well-connected architectures},
pages = {321-332},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GSZ-fsttcs2006.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GSZ-fsttcs2006.pdf},
doi = {10.1007/11944836_30},
abstract = {We study the synthesis problem for external linear or branching
specifications and distributed, synchronous architectures with arbitrary
delays on processes. External means that the specification only relates input
and output variables. We~introduce the subclass of uniformly
well-connected~(UWC) architectures for which there exists a routing allowing
each output process to get the values of all inputs it is connected to, as
soon as possible. We~prove that the distributed synthesis problem is decidable
on UWC architectures if and only if the set of all sets of input variables
visible by output variables is totally ordered, under set inclusion. We~also
show that if we extend this class by letting the routing depend on the output
process, then the previous decidability result fails. Finally, we provide a
natural restriction on specifications under which the whole class of~UWC
architectures is decidable.}
}
@inproceedings{BGP1-formats06,
address = {Paris, France},
month = sep,
year = 2006,
volume = 4202,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Asarin, Eug{\`e}ne and Bouyer, Patricia},
acronym = {{FORMATS}'06},
booktitle = {{P}roceedings of the 4th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'06)},
author = {B{\'e}rard, B{\'e}atrice and Gastin, Paul and Petit, Antoine},
title = {Refinements and abstractions of signal-event (timed) languages},
pages = {67-81},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP1-formats06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP1-formats06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BGP1-formats06.ps},
doi = {10.1007/11867340_6},
abstract = {In the classical framework of formal languages, a refinement
operation is modeled by a substitution and an abstraction by an inverse
substitution. These mechanisms have been widely studied, because they describe
a change in the specification level, from an abstract view to a more concrete
one, or conversely. For~timed systems, there is up to now no uniform notion of
substitutions. In~this paper, we study the timed substitutions in the general
framework of signal-event languages, where both signals and events are taken
into account. We~prove that regular signal-event languages are closed under
substitutions and inverse substitutions. }
}
@inproceedings{BGP2-formats06,
address = {Paris, France},
month = sep,
year = 2006,
volume = 4202,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Asarin, Eug{\`e}ne and Bouyer, Patricia},
acronym = {{FORMATS}'06},
booktitle = {{P}roceedings of the 4th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'06)},
author = {B{\'e}rard, B{\'e}atrice and Gastin, Paul and Petit, Antoine},
title = {Intersection of regular signal-event (timed) languages},
pages = {52-66},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP2-formats06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP2-formats06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BGP2-formats06.ps},
doi = {10.1007/11867340_5},
abstract = {We propose in this paper a construction for a {"}well known{"}
result: regular signal-event languages are closed by intersection. In~fact,
while this result is indeed trivial for languages defined by Alur and Dill's
timed automata (the proof is an immediate extension of the one in the untimed
case), it turns out that the construction is much more tricky when considering
the most involved model of signal-event automata. While several constructions
have been proposed in particular cases, it is the first time, up to our
knowledge, that a construction working on finite and infinite signal-event
words and taking into account signal stuttering, unobservability of
zero-duration \(\tau\)-signals and Zeno runs is proposed.}
}
@inproceedings{BGM-atva2006,
address = {Beijing, China},
month = oct,
year = {2006},
volume = 4218,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Graf, Susanne and Zhang, Wenhui},
acronym = {{ATVA}'06},
booktitle = {{P}roceedings of the 4th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'06)},
author = {Bhateja, Puneet and Gastin, Paul and Mukund, Madhavan},
title = {A fresh look at testing for asynchronous communication},
pages = {369-383},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGM-atva06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGM-atva06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BGM-atva06.ps},
doi = {10.1007/11901914_28},
abstract = {Testing is one of the fundamental techniques for verifying if a
computing system conforms to its specification. We~take a fresh look at the
theory of testing for message-passing systems based on a natural notion of
observability in terms of input-output relations. We~propose two notions of
test equivalence: one which corresponds to presenting all test inputs up front
and the other which corresponds to interactively feeding inputs to the system
under test. We compare our notions with those studied earlier, notably the
equivalence proposed by Tretmans. In~Tretmans' framework, asynchrony is
modelled using synchronous communication by augmenting the state space of the
system with queues. We~show that the first equivalence we consider is strictly
weaker than Tretmans' equivalence and undecidable, whereas the second notion
is incomparable. We~also establish (un)decidability results for these
equivalences.}
}
@article{DG-icomp2006,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Diekert, Volker and Gastin, Paul},
title = {Pure future local temporal logics are expressively complete for
{M}azurkiewicz traces},
pages = {1597-1619},
year = 2006,
month = nov,
volume = 204,
number = 11,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-icomp06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-icomp06.pdf},
doi = {10.1016/j.ic.2006.07.002},
abstract = {The paper settles a long standing problem for Mazurkiewicz
traces: the pure future local temporal logic defined with the basic modalities
exists-next and until is expressively complete. This means every first-order
definable language of Mazurkiewicz traces can be defined in a pure future
local temporal logic. The~analogous result with a global interpretation has
been known, but the treatment of a local interpretation turned out to be much
more involved. Local logics are interesting because both the satisfiability
problem and the model checking problem are solvable in PSPACE for these logics
whereas they are non-elementary for global logics. Both, the (previously
known) global and the (new) local results generalize Kamp's Theorem for words,
because for sequences local and global viewpoints coincide. }
}
@article{DG06-TCS,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Diekert, Volker and Gastin, Paul},
title = {From local to global temporal logics over {M}azurkiewicz traces},
year = 2006,
month = may,
volume = 356,
number = {1-2},
pages = {126-135},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG06-TCS.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG06-TCS.pdf},
doi = {10.1016/j.tcs.2006.01.035},
abstract = {We review some results on global and local temporal logic on
Mazurkiewicz traces. Our~main contribution is to show how to derive the
expressive completeness of global temporal logic with respect to first-order
logic [V.~Diekert, P.~Gastin, LTL~is expressively complete for Mazurkiewicz
traces, J.~Comput. System Sci.~64 (2002) 396-418] from the similar result on
local temporal logic [V.~Diekert, P.~Gastin, Pure future local temporal logics
are expressively complete for Mazurkiewicz traces, in: M.~Farach-Colton~(Ed.),
Proc.~LATIN'04, Lecture Notes in Computer Science, Vol.~2976, Springer,
Berlin, 2004, pp.~232-241, Full version available as Research Report
LSV-05-22, Laboratoire Sp\'ecification et V\'erification, ENS Cachan, France].}
}
@inproceedings{ABG-fsttcs07,
address = {New~Delhi, India},
month = dec,
year = 2007,
volume = 4855,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Arvind, V. and Prasad, Sanjiva},
acronym = {{FSTTCS}'07},
booktitle = {{P}roceedings of the 27th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'07)},
author = {Akshay, S. and Bollig, Benedikt and Gastin, Paul},
title = {Automata and Logics for Timed Message Sequence Charts},
pages = {290-302},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABG-fsttcs07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABG-fsttcs07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ABG-fsttcs07.ps},
doi = {10.1007/978-3-540-77050-3_24},
abstract = {We provide a framework for distributed systems that impose timing constraints
on their executions. We~propose a timed model of communicating finite-state machines,
which communicate by exchanging messages through channels and use event clocks to
generate collections of timed message sequence charts~(T-MSCs). As~a specification
language, we~propose a monadic second-order logic equipped with timing predicates and
interpreted over~T-MSCs. We establish expressive equivalence of our automata and logic.
Moreover, we prove that, for (existentially) bounded channels, emptiness and
satisfiability are decidable for our automata and logic.}
}
@inproceedings{BGMN-fct07,
address = {Budapest, Hungary},
month = aug,
year = 2007,
volume = 4639,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Csuhaj-Varj{\'u}, Erzs{\'e}bet and {\'E}sik, Zolt{\'a}n},
acronym = {{FCT}'07},
booktitle = {{P}roceedings of the 16th {I}nternational {S}ymposium
on {F}undamentals of {C}omputation {T}heory
({FCT}'07)},
author = {Bhateja, Puneet and Gastin, Paul and Mukund, Madhavan and Narayan
Kumar, K.},
title = {Local testing of message sequence charts is difficult},
pages = {76-87},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGMN-fct07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGMN-fct07.pdf},
doi = {10.1007/978-3-540-74240-1_8},
abstract = {Message sequence charts are an attractive visual formalism used
to specify distributed communicating systems. One~way to test such a
system is to substitute a component by a test process and observe its
interaction with the rest of the system. We~study the question of whether
we can characterize the distributed behaviour of the system based on such
local observations. The~main difficulty is that local observations can
combine in unexpected ways to define implied scenarios not present in the
original specification. It~is known that checking whether a scenario
specification is closed with respect to implied scenarios is undecidable
when observations are made one process at a time, even for regular
specifications. We~show that this undecidability holds even if we have
only two processes in the system. We then strengthen the observer to be
able to observe multiple processes simultaneously. Even in this stronger
framework, the problem remains undecidable. In~fact, undecidability
continues to hold even without message labels, provided we observe two or
more processes simultaneously. On~the other hand, if we do not have
message labels and we restrict observations to one process at a time, the
problem of checking for implied scenarios is decidable.}
}
@inproceedings{GM-spin07,
address = {Berlin, Germany},
month = jul,
year = 2007,
volume = 4595,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Bo{\v{s}}nacki, Dragan and Edelkamp, Stefan},
acronym = {{SPIN}'07},
booktitle = {{P}roceedings of the 14th {I}nternational
{SPIN} {W}orkshop on {M}odel {C}hecking {S}oftware
({SPIN}'07)},
author = {Gastin, Paul and Moro, Pierre},
title = {Minimal counter-example generation for {SPIN}},
pages = {24-38},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GM-spin07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GM-spin07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GM-spin07.ps},
doi = {10.1007/978-3-540-73370-6_4},
abstract = {In this paper, we propose an algorithm to compute a counter-example of
minimal size to some property in a finite state program, using the same
programmation constraints than~SPIN. This algorithm uses nested
Breadth-first searches guided by priority queues.
This algorithm works in quadratic time and is linear in memory.}
}
@misc{versydis-final,
author = {Gastin, Paul and others},
title = {{ACI} {S}{\'e}curit{\'e} {I}nformatique {VERSYDIS}~---
Rapport final},
year = 2006,
month = oct,
type = {Contract Report},
note = {10~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Versydis-final.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Versydis-final.pdf}
}
@article{GK-fi07,
publisher = {{IOS} Press},
journal = {Fundamenta Informaticae},
author = {Gastin, Paul and Kuske, Dietrich},
title = {Uniform satisfiability in {PSPACE} for local temporal logics
over {M}azurkiewicz traces},
volume = 80,
number = {1-3},
pages = {169-197},
year = 2007,
month = nov,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GK-fi07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GK-fi07.pdf},
abstract = {We study the complexity of temporal logics over
concurrent systems that can be described by Mazurkiewicz traces. We
develop a general method to prove that the uniform satisfiability
problem of local temporal logics is in~PSPACE. We~also
demonstrate that this method applies to all known local temporal
logics.}
}
@article{BGP-fmsd07,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {B{\'e}rard, B{\'e}atrice and Gastin, Paul and Petit,
Antoine},
title = {Timed substitutions for regular signal-event languages},
volume = 31,
number = 2,
pages = {101-134},
year = 2007,
month = oct,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP-fmsd07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGP-fmsd07.pdf},
doi = {10.1007/s10703-007-0034-5},
abstract = {In the classical framework of formal languages, a refinement
operation is modeled by a substitution and an abstraction by an inverse
substitution. These mechanisms have been widely studied, because they
describe a change in the specification level, from an abstract view to a
more concrete one, or conversely. For timed systems, there is up to now no
uniform notion of substitution. In~this paper, we~study timed substitutions
in the general framework of signal-event languages, where both signals and
events are taken into account. We prove that regular signal-event languages
are closed under substitution and inverse substitution.\par
To obtain these results, we use in a crucial way a {"}well known{"} result:
regular signal-event languages are closed under intersection. In fact,
while this result is indeed easy for languages defined by Alur and Dill's
timed automata, it turns out that the construction is much more tricky when
considering the most involved model of signal-event automata. We give here
a construction working on finite and infinite signal-event words and taking
into account signal stuttering, unobservability of zero-duration \(\tau\)-signals
and Zeno runs. Note that if several constructions have been proposed in
particular cases, it is the first time that a general construction is
provided.}
}
@article{DrGa06tocsys,
publisher = {Springer},
journal = {Theory of Computing Systems},
author = {Droste, Manfred and Gastin, Paul},
title = {On aperiodic and star-free formal power series in
partially commuting variables},
year = 2008,
month = may,
volume = 42,
number = 4,
pages = {608-631},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-12.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-12.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2005-12.ps},
doi = {10.1007/s00224-007-9064-z},
abstract = {Formal power series over non-commuting variables have been
investigated as representations of the behavior of automata with
multiplicities. Here we introduce and investigate the concepts of
aperiodic and of star-free formal power series over semirings and
partially commuting variables. We prove that if the semiring~\(K\) is
idempotent and commutative, or if \(K\) is idempotent and the variables
are non-commuting, then the product of any two aperiodic series is again
aperiodic. We also show that if \(K\) is idempotent and the matrix monoids
over~\(K\) have a Burnside property (satisfied, \textit{e.g.}~by the
tropical semiring), then the aperiodic and the star-free series coincide.
This generalizes a classical result of Sch{\"u}tzenberger~(1961) for
aperiodic regular languages and subsumes a result of Guaiana, Restivo and
Salemi~(1992) on aperiodic trace languages. }
}
@article{DrGa07tcs,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Droste, Manfred and Gastin, Paul},
title = {Weighted automata and weighted logics},
year = 2007,
month = jun,
volume = 380,
number = {1-2},
pages = {69-86},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-13.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2005-13.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2005-13.ps},
doi = {10.1016/j.tcs.2007.02.055},
abstract = {Weighted automata are used to describe quantitative properties
in various areas such as probabilistic systems, image
compression, speech-to-text processing. The~behaviour of
such an automaton is a mapping, called a formal power
series, assigning to each word a weight in some semiring.
We~generalize B{\"u}chi's and Elgot's fundamental theorems to this
quantitative setting. We~introduce a weighted version of MSO
logic and prove that, for commutative semirings, the
behaviours of weighted automata are precisely the formal
power series definable with particular sentences of our
weighted logic. We~also consider weighted first-order logic
and show that aperiodic series coincide with the first-order
definable ones, if the semiring is locally finite,
commutative and has some aperiodicity property.},
oldnote = {Special issue of ICALP'05. To appear.
Also available as Research Report LSV-05-13,
Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan,
France, July 2005.}
}
@misc{dots-3.1,
author = {Bollig, Benedikt and Bouyer, Patricia and Cassez, Franck and
Chatain, {\relax Th}omas and Gastin, Paul and Haddad, Serge
and Jard, Claude},
title = {Model for distributed timed systems},
howpublished = {Deliverable DOTS~3.1 (ANR-06-SETI-003)},
year = 2008,
month = sep
}
@incollection{DG-hwa08,
year = 2009,
series = {EATCS Monographs in Theoretical Computer Science},
publisher = {Springer},
editor = {Kuich, Werner and Vogler, Heiko and Droste, Manfred},
booktitle = {Handbook of Weighted Automata},
author = {Droste, Manfred and Gastin, Paul},
title = {Weighted automata and weighted logics},
pages = {175-211},
chapter = 5,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-hwa08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-hwa08.pdf}
}
@incollection{DG-pct08,
futureaddress = {},
month = jan,
year = 2009,
series = {IARCS-Universities},
publisher = {Universities Press},
booktitle = {Perspectives in Concurrency Theory},
editor = {Lodaya, Kamal and Mukund, Madhavan and
Ramanujam, R.},
author = {Diekert, Volker and Gastin, Paul},
title = {Local safety and local liveness for distributed systems},
pages = {86-106},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-pct08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-pct08.pdf},
abstract = {We introduce local safety and local liveness for distributed
systems whose executions are modeled by Mazurkiewicz traces. We
characterize local safety by local closure and local liveness by local
density. Restricting to first-order definable properties, we prove a
decomposition theorem in the spirit of the separation theorem for linear
temporal logic. We then characterize local safety and local liveness by
means of canonical local temporal logic formulae.}
}
@inproceedings{ABGMN-concur08,
address = {Toronto, Canada},
month = aug,
year = 2008,
volume = 5201,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {van Breugel, Franck and Chechik, Marsha},
acronym = {{CONCUR}'08},
booktitle = {{P}roceedings of the 19th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'08)},
author = {Akshay, S. and Bollig, Benedikt and Gastin, Paul and Mukund,
Madhavan and Narayan Kumar, K.},
title = {Distributed Timed Automata with Independently Evolving
Clocks},
pages = {82-97},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABGMN-concur08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/ABGMN-concur08.pdf},
doi = {10.1007/978-3-540-85361-9_10},
abstract = { We propose a model of distributed timed systems where each
component is a timed automaton with a set of local clocks that evolve at a
rate independent of the clocks of the other components. A clock can be
read by any component in the system, but it can only be reset by the
automaton it belongs to.\par
There are two natural semantics for such systems. The \emph{universal}
semantics captures behaviors that hold under any choice of clock rates for
the individual components. This is a natural choice when checking that a
system always satisfies a positive specification. However, to check if a
system avoids a negative specification, it is better to use the
\emph{existential} semantics---the set of behaviors that the system can
possibly exhibit under some choice of clock rates.\par
We show that the existential semantics always describes a regular set of
behaviors. However, in the case of universal semantics, checking emptiness
turns out to be undecidable. As an alternative to the universal semantics,
we propose a \emph{reactive} semantics that allows us to check positive
specifications and yet describes a regular set of behaviors. }
}
@article{DGK-ijfcs08,
publisher = {World Scientific},
journal = {International Journal of Foundations of Computer Science},
author = {Diekert, Volker and Gastin, Paul and Kufleitner,
Manfred},
title = {A Survey on Small Fragments of First-Order Logic over
Finite Words},
volume = 19,
number = 3,
pages = {513-548},
year = 2008,
month = jun,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DGK-ijfcs08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DGK-ijfcs08.pdf},
doi = {10.1142/S0129054108005802},
abstract = {We consider fragments of first-order logic over finite
words. In~particular, we~deal with
first-order logic with a restricted number of
variables and with the lower levels of the
alternation hierarchy. We~use the algebraic
approach to show decidability of
expressibility within these fragments. As~a
byproduct, we~survey several characterizations
of the respective fragments. We~give complete
proofs for all characterizations and we
provide all necessary background. Some of the
proofs seem to be new and simpler than those
which can be found elsewhere. We also give a
proof of Simon's theorem on factorization
forests restricted to aperiodic monoids
because this is simpler and sufficient for our
purpose.}
}
@unpublished{PG-algo,
author = {Gastin, Paul},
title = {Algorithmique},
year = {2007},
month = nov,
note = {Course notes, {M}agist{\`e}re STIC, ENS Cachan, France}
}
@unpublished{PG-languages,
author = {Gastin, Paul},
title = {Langages formels},
year = {2007},
month = may,
note = {Course notes, {M}agist{\`e}re STIC, ENS Cachan, France}
}
@misc{ltl2ba-v1.1,
author = {Gastin, Paul and Oddoux, Denis},
title = {LTL2BA~v1.1},
year = {2007},
month = aug,
nohowpublished = {Available at http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/},
note = {Written in~C++ (about 4000 lines)},
note-fr = {\'Ecrit en~C++ (environ 4000 lignes)},
url = {http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/}
}
@misc{gastex-v2.8,
author = {Gastin, Paul},
title = {Gas{{\TeX}}: Graphs and Automata Simplified in~{{\TeX}} (v2.8)},
year = {2006},
month = nov,
nohowpublished = {Available at http://www.lsv.ens-cachan.fr/~gastin/gastex/gastex.html},
note = {Written in~\TeX (about 2000 lines)},
note-fr = {\'Ecrit en~\TeX (environ 2000 lignes)},
url = {http://www.lsv.ens-cachan.fr/~gastin/gastex/gastex.html}
}
@incollection{DiGa08Thomas,
author = {Diekert, Volker and Gastin, Paul},
title = {First-order definable languages},
booktitle = {Logic and Automata: History and Perspectives},
editor = {Flum, J{\"o}rg and Gr{\"a}del, Erich and Wilke, Thomas},
publisher = {Amsterdam University Press},
series = {Texts in Logic and Games},
volume = 2,
year = 2008,
pages = {261-306},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-WT08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-WT08.pdf},
abstract = {We give an essentially self-contained presentation of some principal
results for first-order definable languages over finite and infinite
words. We~introduce the notion of a \emph{counter-free} B{\"u}chi
automaton; and we relate counter-freeness to \emph{aperiodicity}
and to the notion of \emph{very weak alternation}.
We also show that aperiodicity of a regular
\(\infty\)-language can be decided in polynomial
space, if the language is specified by some B{\"u}chi automaton.}
}
@misc{dots-2.2,
author = {Chatain, {\relax Th}omas and Gastin, Paul and Muscholl, Anca
and Sznajder, Nathalie and Walukiewicz, Igor and
Zeitoun, Marc},
title = {Distributed control for restricted specifications},
howpublished = {Deliverable DOTS~2.2 (ANR-06-SETI-003)},
year = 2009,
month = mar
}
@inproceedings{BG-dlt09,
address = {Stuttgart, Germany},
month = jun # {-} # jul,
year = 2009,
volume = {5583},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Diekert, Volker and Nowotka, Dirk},
acronym = {{DLT}'09},
booktitle = {{P}roceedings of the 13th {I}nternational
{C}onference on {D}evelopments in {L}anguage {T}heory
({DLT}'09)},
author = {Bollig, Benedikt and Gastin, Paul},
title = {Weighted versus Probabilistic Logics},
pages = {18-38},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BG-dlt09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BG-dlt09.pdf},
doi = {10.1007/978-3-642-02737-6_2},
abstract = {While a mature theory around logics such as MSO, LTL, and CTL
has been developed in the pure boolean setting of finite automata,
weighted automata lack such a natural connection with (temporal) logic and
related verification algorithms. In this paper, we will identify weighted
versions of MSO and CTL that generalize the classical logics and even
other quantitative extensions such as probabilistic CTL. We establish
expressiveness results on our logics giving translations from weighted and
probabilistic CTL into weighted MSO.}
}
@incollection{GMN-pct08,
futureaddress = {},
month = jan,
year = 2009,
series = {IARCS-Universities},
publisher = {Universities Press},
booktitle = {Perspectives in Concurrency Theory},
editor = {Lodaya, Kamal and Mukund, Madhavan and
Ramanujam, R.},
author = {Gastin, Paul and Mukund, Madhavan and Narayan Kumar, K.},
title = {Reachability and boundedness in time-constrained {MSC} graphs},
pages = {157-183},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GMN-pct08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GMN-pct08.pdf},
abstract = {Channel boundedness is a necessary condition for a
message-passing system to exhibit regular, finite-state behaviour at the
global level. For Message Sequence Graphs~(MSGs), the most basic form of
High-level Message Sequence Charts~(HMSCs), channel boundedness can be
characterized in terms of structural conditions on the underlying graph.
We consider MSGs enriched with timing constraints between events. These
constraints restrict the global behaviour and can impose channel
boundedness even when it is not guaranteed by the graph structure of the
MSG. We~show that we can use MSGs with timing constraints to simulate
computations of a two-counter machine. As~a consequence, even the more
fundamental problem of reachability, which is trivial for untimed MSGs,
becomes undecidable when we add timing constraints. Different forms of
channel boundedness also then turn out to be undecidable, using reductions
from the reachability problem.}
}
@article{GSZ-fmsd09,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Gastin, Paul and Sznajder, Nathalie and Zeitoun, Marc},
title = {Distributed synthesis for well-connected
architectures},
volume = 34,
number = 3,
pages = {215-237},
month = jun,
year = 2009,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GSZ-fmsd09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GSZ-fmsd09.pdf},
doi = {10.1007/s10703-008-0064-7},
abstract = {We study the synthesis problem for external linear or branching
specifications and distributed, synchronous architectures with arbitrary
delays on processes. External means that the specification only relates
input and output variables. We introduce the subclass of uniformly
well-connected (UWC) architectures for which there exists a routing
allowing each output process to get the values of all inputs it is
connected to, as soon as possible. We prove that the distributed synthesis
problem is decidable on UWC architectures if and only if the output
variables are totally ordered by their knowledge of input variables. We
also show that if we extend this class by letting the routing depend on
the output process, then the previous decidability result fails. Finally,
we provide a natural restriction on specifications under which the whole
class of UWC architectures is decidable.}
}
@inproceedings{CGS-sofsem09,
address = {\v{S}pindler\r{u}v Ml\'{y}n, Czech Republic},
month = jan,
year = 2009,
volume = 5404,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Nielsen, Mogens and Ku{\v c}era, Anton{\'\i}n and Bro
Miltersen, Peter and Palamidessi, Catuscia and T{\r{u}}ma,
Petr and Valencia, Franck},
acronym = {{SOFSEM}'09},
booktitle = {{P}roceedings of the 35th International Conference on
Current Trends in Theory and Practice of
Computer Science ({SOFSEM}'09)},
author = {Chatain, {\relax Th}omas and Gastin, Paul and Sznajder, Nathalie},
title = {Natural Specifications Yield Decidability for Distributed
Synthesis of Asynchronous Systems},
pages = {141-152},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CGS-sofsem09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CGS-sofsem09.pdf},
doi = {10.1007/978-3-540-95891-8_16},
abstract = {We study the synthesis problem in an asynchronous distributed
setting: a finite set of processes interact locally with an uncontrollable
environment and communicate with each other by sending signals---actions
that are immediately received by the target process. The synthesis problem
is to come up with a local strategy for each process such that the
resulting behaviours of the system meet a given specification. We consider
external specifications over partial orders. External means that
specifications only relate input and output actions from and to the
environment and not signals exchanged by processes. We also ask for some
closure properties of the specification. We present this new setting for
studying the distributed synthesis problem, and give decidability results:
the non-distributed case, and the subclass of networks where communication
happens through a strongly connected graph. We believe that this framework
for distributed synthesis yields decidability results for many more
architectures.}
}
@inproceedings{AGMN-fsttcs10,
address = {Chennai, India},
month = dec,
year = 2010,
volume = 8,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Lodaya, Kamal and Mahajan, Meena},
acronym = {{FSTTCS}'10},
booktitle = {{P}roceedings of the 30th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'10)},
author = {Akshay, S. and Gastin, Paul and Mukund, Madhavan and Narayan Kumar, K.},
title = {Model checking time-constrained scenario-based specifications},
pages = {204-215},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGMN-fsttcs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGMN-fsttcs10.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2010.204},
abstract = {We consider the problem of model checking message-passing
systems with real-time requirements. As behavioural specifications, we use
message sequence charts (MSCs) annotated with timing constraints. Our
system model is a network of communicating finite state machines with
local clocks, whose global behaviour can be regarded as a timed automaton.
Our goal is to verify that all timed behaviours exhibited by the system
conform to the timing constraints imposed by the specification. In
general, this corresponds to checking inclusion for timed languages, which
is an undecidable problem even for timed regular languages. However, we
show that we can translate regular collections of time-constrained MSCs
into a special class of event-clock automata that can be determinized and
complemented, thus permitting an algorithmic solution to the model
checking problem.}
}
@proceedings{GL-concur10,
author = {Gastin, Paul and Laroussinie, Fran{\c{c}}ois},
editor = {Gastin, Paul and Laroussinie, Fran{\c{c}}ois},
title = {{P}roceedings of the 21st
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'10)},
booktitle = {{P}roceedings of the 21st
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'10)},
year = 2010,
month = aug # {-} # sep,
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6269},
url = {http://www.springerlink.com/content/978-3-642-15374-7},
doi = {10.1007/978-3-642-15375-4}
}
@inproceedings{BGMZ-icalp10,
address = {Bordeaux, France},
month = jul,
year = 2010,
volume = 6199,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abramsky, Samson and Meyer{ }auf{ }der{ }Heide, Friedhelm
and Spirakis, Paul},
acronym = {{ICALP}'10},
booktitle = {{P}roceedings of the 37th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'10)~-- {P}art~{II}},
author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin
and Zeitoun, Marc},
title = {Pebble weighted automata and transitive closure logics},
pages = {587-598},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-icalp10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-icalp10.pdf},
doi = {10.1007/978-3-642-14162-1_49},
abstract = {We introduce new classes of weighted automata on words. Equipped
with pebbles and a two-way mechanism, they go beyond the class of
recognizable formal power series, but capture a weighted version of
first-order logic with bounded transitive closure. In contrast to previous
work, this logic allows for unrestricted use of universal quantification.
Our main result states that pebble weighted automata, nested weighted
automata, and this weighted logic are expressively equivalent. We also
give new logical characterizations of the recognizable series.}
}
@article{GK-icomp10,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Gastin, Paul and Kuske, Dietrich},
title = {Uniform satisfiability problem for local temporal logics over
{M}azurkiewicz traces},
volume = 208,
number = 7,
month = jul,
year = 2010,
pages = {797-816},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GK-icomp10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GK-icomp10.pdf},
doi = {10.1016/j.ic.2009.12.003},
abstract = {We continue our study of the complexity of MSO-definable local
temporal logics over concurrent systems that can be described by
Mazurkiewicz traces. In previous papers, we showed that the satisfiability
problem for any such logic is in PSPACE (provided the dependence alphabet
is fixed) and remains in PSPACE for all classical local temporal logics
even if the dependence alphabet is part of the input. In~this paper, we
consider the uniform satisfiability problem for arbitrary MSO-definable
local temporal logics. For this problem, we prove multi-exponential lower
and upper bounds that depend on the number of alternations of set
quantifiers present in the chosen MSO-modalities.}
}
@inproceedings{BCGK-fossacs12,
address = {Tallinn, Estonia},
month = mar,
year = 2012,
volume = 7213,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Birkedal, Lars},
acronym = {{FoSSaCS}'12},
booktitle = {{P}roceedings of the 15th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'12)},
author = {Bollig, Benedikt and Cyriac, Aiswarya and Gastin, Paul and
Narayan Kumar, K.},
title = {Model Checking Languages of Data Words},
pages = {391-405},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGK-fossacs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGK-fossacs12.pdf},
doi = {10.1007/978-3-642-28729-9_26},
abstract = {We consider the model-checking problem for data multi-pushdown
automata (DMPA). DMPA generate data words, i.e, strings enriched with
values from an infinite domain. The latter can be used to represent an
unbounded number of process identifiers so that DMPA are suitable to model
concurrent programs with dynamic process creation. To specify properties
of data words, we use monadic second-order (MSO) logic, which comes with a
predicate to test two word positions for data equality. While
satisfiability for MSO logic is undecidable (even for weaker fragments
such as first-order logic), our main result states that one can decide if
all words generated by a DMPA satisfy a given formula from the full MSO
logic.}
}
@inproceedings{BCGZ-mfcs11,
address = {Warsaw, Poland},
month = aug,
year = 2011,
volume = 6907,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Murlak, Filip and Sankowski, Piotr},
acronym = {{MFCS}'11},
booktitle = {{P}roceedings of the 36th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'11)},
author = {Bollig, Benedikt and Cyriac, Aiswarya and Gastin, Paul and Zeitoun, Marc},
title = {Temporal Logics for Concurrent Recursive Programs: Satisfiability
and Model Checking},
pages = {132-144},
url = {http://hal.archives-ouvertes.fr/hal-00591139/en/},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGZ-mfcs11.pdf},
doi = {10.1007/978-3-642-22993-0_15},
abstract = {We develop a general framework for the design of temporal logics
for concurrent recursive programs. A program execution is modeled as a
partial order with multiple nesting relations. To specify properties of
executions, we consider any temporal logic whose modalities are definable
in monadic second-order logic and that, in addition, allows PDL-like path
expressions. This captures, in a unifying framework, a wide range of
logics defined for trees, nested words, and Mazurkiewicz traces that have
been studied separately. We show that satisfiability and model checking
are decidable in EXPTIME and 2EXPTIME, depending on the precise path
modalities.}
}
@techreport{rr-lsv-11-08,
author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin and
Zeitoun, Marc},
title = {Weighted Expressions and {DFS} Tree Automata},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2011},
month = apr,
type = {Research Report},
number = {LSV-11-08},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2011-08.pdf},
note = {32~pages},
abstract = {We introduce weighted expressions, a~calculus to express
quantitative properties over unranked trees. They involve products and
sums from a semiring as well as classical boolean formulas. We~show that
weighted expressions are expressively equivalent to a new class of
weighted tree-walking automata. This new automata model is equipped with
pebbles, and follows a depth-first-search policy in the tree.}
}
@incollection{DG-iis09,
author = {Demri, St{\'e}phane and Gastin, Paul},
title = {Specification and Verification using Temporal Logics},
booktitle = {Modern applications of automata theory},
editor = {D'Souza, Deepak and Shankar, Priti},
series = {IISc Research Monographs},
volume = 2,
publisher = {World Scientific},
chapter = 15,
pages = {457-494},
year = 2012,
month = jul,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DG-iis09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DG-iis09.pdf},
abstract = {This chapter illustrates two aspects of automata theory related
to linear-time temporal logic LTL used for the verification of computer
systems. First, we present a translation from LTL formulae to B{\"u}chi
automata. The aim is to design an elementary translation which is
reasonably efficient and produces small automata so that it can be easily
taught and used by hand on real examples. Our translation is in the spirit
of the classical tableau constructions but is optimized in several ways.
Secondly, we recall how temporal operators can be defined from regular
languages and we explain why adding even a single operator definable by a
context-free language can lead to undecidability.}
}
@article{ABG-fmsd12,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Akshay, S. and Bollig, Benedikt and Gastin, Paul},
title = {Event-clock Message Passing Automata: A~Logical
Characterization and an Emptiness-Checking Algorithm},
year = 2013,
month = jun,
volume = 42,
number = {3},
pages = {262-300},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABG-fmsd12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABG-fmsd12.pdf},
doi = {10.1007/s10703-012-0179-8},
abstract = {We are interested in modeling behaviors and verifying
properties of systems in which time and concurrency play a crucial
role. We introduce a model of distributed automata which are
equipped with event clocks as in [Alur, Fix,
Henzinger. Event-clock automata: A~determinizable class of timed
automata. TCS 211(1-2):253-273, 1999.], which we call Event Clock
Message Passing Automata (ECMPA). To describe the behaviors of
such systems we use timed partial orders (modeled as message
sequence charts with timing).\par
Our first goal is to extend the classical
B{\"u}chi-Elgot-Trakhtenbrot equivalence to the timed and
distributed setting, by showing an equivalence between ECMPA and a
timed extension of monadic second-order (MSO) logic. We obtain
such a constructive equivalence in two different ways:
(1)~by~restricting the semantics by bounding the set of timed
partial orders (2)~by~restricting the timed MSO logic to its
existential fragment. We next consider the emptiness problem for
ECMPA, which asks if a given ECMPA has some valid timed
execution. In general this problem is undecidable and we show that
by considering only bounded timed executions, we can obtain
decidability. We do this by constructing a timed automaton which
accepts all bounded timed executions of the ECMPA and checking
emptiness of this timed automaton.}
}
@article{GS-tocl12,
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
author = {Gastin, Paul and Sznajder, Nathalie},
title = {Fair Synthesis for Asynchronous Distributed Systems},
nopages = {},
volume = 14,
number = {2:9},
month = jun,
year = 2013,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GS-tocl12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GS-tocl12.pdf},
doi = {10.1145/2480759.2480761},
abstract = {We study the synthesis problem in an asynchronous distributed
setting: a finite set of processes interact locally with an uncontrollable
environment and communicate with each other by sending signals---actions
controlled by a sender process and that are immediately received by the
target process. The fair synthesis problem is to come up with a local
strategy for each process such that the resulting fair behaviors of the
system meet a given specification. We consider external specifications
satisfying some natural closure properties related to the architecture. We
present this new setting for studying the fair synthesis problem for
distributed systems, and give decidability results for the subclass of
networks where communications happen through a strongly connected graph.
We claim that this framework for distributed synthesis is natural,
convenient and avoids most of the usual sources of undecidability for the
synthesis problem. Hence, it may open the way to a decidable theory of
distributed synthesis.}
}
@article{GS-ipl12,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Gastin, Paul and Sznajder, Nathalie},
title = {Decidability of well-connectedness for distributed synthesis},
pages = {963-968},
volume = {112},
number = {24},
month = dec,
year = 2012,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GS-ipl12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GS-ipl12.pdf},
doi = {10.1016/j.ipl.2012.08.018},
abstract = {Although the synthesis problem is often undecidable for
distributed, synchronous systems, it becomes decidable for the subclass of
uniformly well-connected (UWC) architectures, provided that only robust
specifications are considered. It is then an important issue to be able to
decide whether a given architecture falls in this class. This is the
problem addressed in this paper: we establish the decidability and precise
complexity of checking this property. This problem is in EXPSPACE and
NP-hard in the general case, but falls into PSPACE when restricted to a
natural subclass of architectures.}
}
@inproceedings{GM-ciaa12,
address = {Porto, Portugal},
month = jul,
year = 2012,
volume = {7381},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {Moreira, Nelma and Reis, Rog{\'e}rio},
acronym = {{CIAA}'12},
booktitle = {{P}roceedings of the 17th {I}nternational
{C}onference on {I}mplementation and
{A}pplication of {A}utomata
({CIAA}'12)},
author = {Gastin, Paul and Monmege, Benjamin},
title = {Adding Pebbles to Weighted Automata},
pages = {28-51},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GM-ciaa12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GM-ciaa12.pdf},
doi = {10.1007/978-3-642-31606-7_4},
abstract = {We extend weighted automata and weighted rational expressions
with 2-way moves and (reusable) pebbles. We show with examples from
natural language modeling and quantitative model-checking that weighted
expressions and automata with pebbles are more expressive and allow much
more natural and intuitive specifications than classical ones.\par
We extend Kleene-Sch{\"u}tzenberger theorem showing that weighted
expressions and automata with pebbles have the same expressive power. We
focus on an efficient translation from expressions to automata.\par
We also prove that the evaluation problem for weighted automata can be
done very efficiently if the number of (reusable) pebbles is low.}
}
@inproceedings{BGMZ-atva12,
address = {Thiruvananthapuram, India},
month = oct,
year = {2012},
volume = {7561},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Mukund, Madhavan and Chakraborty, Supratik},
acronym = {{ATVA}'12},
booktitle = {{P}roceedings of the 10th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'12)},
author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin and
Zeitoun, Marc},
title = {A Probabilistic {K}leene Theorem},
pages = {400-415},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-atva12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-atva12.pdf},
doi = {10.1007/978-3-642-33386-6_31},
abstract = {We provide a Kleene Theorem for (Rabin) probabilistic automata
over finite words. Probabilistic automata generalize deterministic finite
automata and assign to a word an acceptance probability. We provide
probabilistic expressions with probabilistic choice, guarded choice,
concatenation, and a star operator. We prove that probabilistic
expressions and probabilistic automata are expressively equivalent. Our
result actually extends to two-way probabilistic automata with pebbles and
corresponding expressions.}
}
@inproceedings{CGN-concur12,
address = {Newcastle, UK},
month = sep,
year = 2012,
volume = 7454,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Koutny, Maciej and Ulidowski, Irek},
acronym = {{CONCUR}'12},
booktitle = {{P}roceedings of the 23rd
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'12)},
author = {Cyriac, Aiswarya and Gastin, Paul and Narayan Kumar, K.},
title = {{MSO} Decidability of Multi-Pushdown Systems via Split-Width},
pages = {547-561},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CGN-concur12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CGN-concur12.pdf},
doi = {10.1007/978-3-642-32940-1_38},
abstract = {Multi-threaded programs with recursion are naturally modeled as
multi-pushdown systems. The behaviors are represented as multiply nested
words (MNWs), which are words enriched with additional binary relations
for each stack matching a push operation with the corresponding pop
operation. Any MNW can be decomposed by two basic and natural operations:
shuffle of two sequences of factors and merge of consecutive factors of a
sequence. We say that the split-width of a MNW is~\(k\) if it admits a
decomposition where the number of factors in each sequence is at most~\(k\).
The MSO theory of MNWs with split-width~\(k\) is decidable. We introduce two
very general classes of MNWs that strictly generalize known decidable
classes and prove their MSO decidability via their split-width and obtain
comparable or better bounds of tree-width of known classes.}
}
@inproceedings{BGM-fossacs13,
address = {Rome, Italy},
month = mar,
year = 2013,
volume = {7794},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Pfenning, Frank},
acronym = {{FoSSaCS}'13},
booktitle = {{P}roceedings of the 16th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'13)},
author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin},
title = {Weighted Specifications over Nested Words},
pages = {385-400},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-fossacs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-fossacs13.pdf},
doi = {10.1007/978-3-642-37075-5_25},
abstract = {This paper studies several formalisms to specify quantitative
properties of finite nested words (or~equivalently finite unranked trees).
These can be used for XML documents or recursive programs: for~instance,
counting how often a given entry occurs in an XML document, or~computing
the memory required for a recursive program execution. Our main interest
is to translate these properties, as efficiently as possible, into an
automaton, and to use this computational device to decide problems related
to the properties (e.g.,~emptiness, model checking, simulation) or to
compute the value of a quantitative specification over a given nested
word. The specification formalisms are weighted regular expressions (with
forward and backward moves following linear edges or call-return edges),
weighted first-order logic, and weighted temporal logics. We~introduce
weighted automata walking in nested words, possibly dropping\slash lifting
(reusable) pebbles during the traversal. We prove that the evaluation
problem for such automata can be done very efficiently if the number of
pebble names is small, and we also consider the emptiness problem.}
}
@inproceedings{AG-fsttcs14,
address = {New~Dehli, India},
month = dec,
year = 2014,
volume = {29},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Raman, Venkatesh and Suresh, S.~P.},
acronym = {{FSTTCS}'14},
booktitle = {{P}roceedings of the 34th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'14)},
author = {Aiswarya, C. and Gastin, Paul},
title = {Reasoning about distributed systems: {WYSIWYG}},
pages = {11-30},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AG-fsttcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AG-fsttcs14.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2014.11},
abstract = {There are two schools of thought on reasoning about distributed
systems: one~following interleaving based semantics, and one following
partial-order{{\slash}}graph based semantics. This paper compares these two
approaches and argues in favour of the latter. An~introductory treatment
of the split-width technique is also provided.}
}
@inproceedings{BGK-fsttcs14,
address = {New~Dehli, India},
month = dec,
year = 2014,
volume = {29},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Raman, Venkatesh and Suresh, S.~P.},
acronym = {{FSTTCS}'14},
booktitle = {{P}roceedings of the 34th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'14)},
author = {Bollig, Benedikt and Gastin, Paul and Kumar, Akshay},
title = {Parameterized Communicating Automata: Complementation and
Model Checking},
pages = {625-637},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGK-fsttcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGK-fsttcs14.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2014.625},
abstract = {We study the language-theoretical aspects of parameterized
communicating automata (PCAs), in which processes communicate via
rendez-vous. A given PCA can be run on any topology of bounded degree such
as pipelines, rings, ranked trees, and grids. We show that, under a
context bound, which restricts the local behavior of each process, PCAs
are effectively complementable. Complementability is considered a key
aspect of robust automata models and can, in particular, be exploited for
verification. In this paper, we use it to obtain a characterization of
context-bounded PCAs in terms of monadic second-order (MSO) logic. As the
emptiness problem for context-bounded PCAs is decidable for the classes of
pipelines, rings, and trees, their model-checking problem wrt. MSO
properties also becomes decidable. While previous work on model checking
parameterized systems typically uses temporal logics without next
operator, our MSO logic allows one to express several natural next
modalities.}
}
@article{BCGZ-jal14,
publisher = {Elsevier Science Publishers},
journal = {Journal of Applied Logic},
author = {Bollig, Benedikt and Cyriac, Aiswarya and Gastin, Paul and
Zeitoun, Marc},
title = {Temporal logics for concurrent recursive programs:
Satisfiability and model checking},
volume = 12,
number = 4,
pages = {395-416},
month = dec,
year = 2014,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGZ-jal14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGZ-jal14.pdf},
doi = {10.1016/j.jal.2014.05.001},
abstract = {We develop a general framework for the design of temporal logics
for concurrent recursive programs. A program execution is modeled as a
partial order with multiple nesting relations. To specify properties of
executions, we consider any temporal logic whose modalities are definable
in monadic second-order logic and which, in addition, allows PDL-like path
expressions. This captures, in a unifying framework, a wide range of
logics defined for ranked and unranked trees, nested words, and
Mazurkiewicz traces that have been studied separately. We show that
satisfiability and model checking are decidable in EXPTIME and 2EXPTIME,
depending on the precise path modalities.}
}
@inproceedings{BGS-rp14,
address = {Oxford, UK},
month = sep,
year = 2014,
volume = {8762},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ouaknine, Jo{\"e}l and Potapov, Igor and Worrell, James},
acronym = {{RP}'14},
booktitle = {{P}roceedings of the 8th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'14)},
author = {Bollig, Benedikt and Gastin, Paul and Schubert, Jana},
title = {Parameterized Verification of Communicating Automata under Context Bounds},
pages = {45-57},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGS-rp14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGS-rp14.pdf},
doi = {10.1007/978-3-319-11439-2_4},
abstract = {We study the verification problem for parameterized
communicating automata~(PCA), in which processes synchronize via message
passing. A~given PCA can be run on any topology of bounded degree (such as
pipelines, rings, or ranked trees), and communication may take place
between any two processes that are adjacent in the topology. Parameterized
verification asks if there is a topology from a given topology class that
allows for an accepting run of the given PCA. In general, this problem is
undecidable even for synchronous communication and simple pipeline
topologies. We therefore consider context-bounded verification, which
restricts the behavior of each single process. For several variants of
context bounds, we show that parameterized verification over pipelines,
rings, and ranked trees is decidable. Our approach is automata-theoretic
and uniform. We introduce a notion of graph acceptor that identifies those
topologies allowing for an accepting run. Depending on the given topology
class, the topology acceptor can then be restricted, or adjusted, so that
the verification problem reduces to checking emptiness of finite automata
or tree automata.}
}
@inproceedings{AGN-atva14,
address = {Sydney, Australia},
month = nov,
year = {2014},
volume = 8837,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Cassez, Franck and Raskin, Jean-Fran{\c{c}}ois},
acronym = {{ATVA}'14},
booktitle = {{P}roceedings of the 12th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'14)},
author = {Aiswarya, C. and Gastin, Paul and Narayan Kumar, K.},
title = {Verifying Communicating Multi-pushdown Systems via Split-width},
pages = {1-17},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGN-atva14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGN-atva14.pdf},
doi = {10.1007/978-3-319-11936-6_1},
abstract = {Communicating multi-pushdown systems model networks of
multi-threaded recursive programs communicating via reliable FIFO
channels. We extend the notion of split-width to this setting, improving
and simplifying the earlier definition. Split-width, while having the same
power of clique-{{\slash}}tree-width, gives a divide-and-conquer technique
to prove the bound of a class, thanks to the two basic operations, shuffle
and merge, of the split-width algebra. We illustrate this technique on
examples. We also obtain simple, uniform and optimal decision procedures
for various verification problems parametrised by split-width.}
}
@inproceedings{CGK-concur14,
address = {Rome, Italy},
month = sep,
year = 2014,
volume = 8704,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Baldan, Paolo and Gorla, Daniele},
acronym = {{CONCUR}'14},
booktitle = {{P}roceedings of the 25th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'14)},
author = {Cyriac, Aiswarya and Gastin, Paul and Narayan Kumar, K.},
title = {Controllers for the Verification of Communicating Multi-Pushdown Systems},
pages = {297-311},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CGK-concur14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CGK-concur14.pdf},
doi = {10.1007/978-3-662-44584-6_21},
abstract = {Multi-pushdowns communicating via queues are formal models of
multi-threaded programs communicating via channels. They are turing
powerful and much of the work on their verification has focussed on
under-approximation techniques. Any error detected in the
under-approximation implies an error in the system. However the successful
verification of the under-approximation is not as useful if the system
exhibits unverified behaviours. Our aim is to design controllers that
observe/restrict the system so that it stays within the verified
under-approximation. We identify some important properties that a good
controller should satisfy. We consider an extensive under-approximation
class, construct a distributed controller with the desired properties and
also establish the decidability of verification problems for this class.}
}
@inproceedings{BGMZ-csllics14,
address = {Vienna, Austria},
month = jul,
year = 2014,
publisher = {ACM Press},
acronym = {{CSL\slash LICS}'14},
booktitle = {{P}roceedings of the Joint Meeting of the 23rd {EACSL} {A}nnual {C}onference on
{C}omputer {S}cience {L}ogic and the 29th {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({CSL\slash LICS}'14)},
author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin and
Zeitoun, Marc},
title = {Logical Characterization of Weighted Pebble Walking Automata},
nopages = {},
chapter = 19,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-csllics14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-csllics14.pdf},
doi = {10.1145/2603088.2603118},
abstract = {Weighted automata are a conservative quantitative extension of
finite automata that enjoys applications, e.g., in language processing and
speech recognition. Their expressive power, however, appears to be
limited, especially when they are applied to more general structures than
words, such as graphs. To address this drawback, weighted automata have
recently been generalized to weighted pebble walking automata, which
proved useful as a tool for the specification and evaluation of
quantitative properties over words and nested words. In this paper, we
establish the expressive power of weighted pebble walking automata in
terms of transitive closure logic, lifting a similar result by Engelfriet
and Hoogeboom from the Boolean case to a quantitative setting. This result
applies to general classes of graphs, including all the aforementioned
classes.}
}
@article{ABGMN-fi13,
publisher = {{IOS} Press},
journal = {Fundamenta Informaticae},
author = {Akshay, S. and Bollig, Benedikt and Gastin, Paul and
Mukund, Madhavan and Narayan Kumar, K.},
title = {Distributed Timed Automata with Independently Evolving Clocks},
volume = {130},
number = {4},
month = apr,
year = 2014,
pages = {377-407},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGMN-fi13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGMN-fi13.pdf},
doi = {10.3233/FI-2014-996},
abstract = {We propose a model of distributed timed systems where each
component is a timed automaton with a set of local clocks that evolve at a
rate independent of the clocks of the other components. A~clock can be
read by any component in the system, but it can only be reset by the
automaton it belongs~to.\par
There are two natural semantics for such systems. The \emph{universal}
semantics captures behaviors that hold under any choice of clock rates for
the individual components. This is a natural choice when checking that a
system always satisfies a positive specification. To check if a system
avoids a negative specification, it is better to use the
\emph{existential} semantics—the set of behaviors that the system
can possibly exhibit under some choice of clock rates.\par
We show that the existential semantics always describes a regular set of
behaviors. However, in the case of universal semantics, checking emptiness
or universality turns out to be undecidable. As an alternative to the
universal semantics, we propose a \emph{reactive} semantics that allows us
to check positive specifications and yet describes a regular set of
behaviors.}
}
@article{BGMZ-tocl13,
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
author = {Bollig, Benedikt and Gastin, Paul and Monmege, Benjamin and Zeitoun, Marc},
title = {Pebble Weighted Automata and Weighted Logics},
volume = 15,
number = {2:15},
month = apr,
year = 2014,
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-tocl13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMZ-tocl13.pdf},
doi = {10.1145/2579819},
abstract = {We introduce new classes of weighted automata on words. Equipped
with pebbles, they go beyond the class of recognizable formal power
series: they capture weighted first-order logic enriched with a
quantitative version of transitive closure. In contrast to previous work,
this calculus allows for unrestricted use of existential and universal
quantifications over positions of the input word. We actually consider
both two-way and one-way pebble weighted automata. The latter class
constrains the head of the automaton to walk left-to-right, resetting it
each time a pebble is dropped. Such automata have already been considered
in the Boolean setting, in the context of data words. Our main result
states that two-way pebble weighted automata, one-way pebble weighted
automata, and our weighted logic are expressively equivalent. We also give
new logical characterizations of standard recognizable series.}
}
@article{GM-tcs14,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Gastin, Paul and Monmege, Benjamin},
title = {Adding Pebbles to Weighted Automata~-- Easy Specification
{\&} Efficient Evaluation},
volume = {534},
month = may,
year = 2014,
pages = {24-44},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GM-tcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GM-tcs14.pdf},
doi = {10.1016/j.tcs.2014.02.034},
abstract = {We extend weighted automata and weighted rational expressions
with 2-way moves and reusable pebbles. We show with examples from natural
language modeling and quantitative model-checking that weighted
expressions and automata with pebbles are more expressive and allow much
more natural and intuitive specifications than classical ones. We extend
Kleene-Sch{\"u}tzenberger theorem showing that weighted expressions and
automata with pebbles have the same expressive power. We focus on an
efficient translation from expressions to automata. We also prove that the
evaluation problem for weighted automata can be done very efficiently if
the number of reusable pebbles is low.}
}
@article{AGMN-tcs15,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Akshay, S. and Gastin, Paul and Mukund,
Madhavan and Kumar, K. Narayan},
title = {Checking conformance for time-constrained scenario-based specifications},
volume = {594},
pages = {24-43},
month = aug,
year = {2015},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AGMN-tcs15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGMN-tcs15.pdf},
doi = {10.1016/j.tcs.2015.03.030},
abstract = {We consider the problem of model checking message-passing
systems with real-time requirements. As behavioral specifications, we use
message sequence charts (MSCs) annotated with timing constraints. Our
system model is a network of communicating finite state machines with
local clocks, whose global behavior can be regarded as a timed automaton.
Our goal is to verify that all timed behaviors exhibited by the system
conform to the timing constraints imposed by the specification. In
general, this corresponds to checking inclusion for timed languages, which
is an undecidable problem even for timed regular languages. However, we
show that we can translate regular collections of time-constrained MSCs
into a special class of event-clock automata that can be determinized and
complemented, thus permitting an algorithmic solution to the model
checking/conformance problem.}
}
@inproceedings{ABG-concur15,
address = {Madrid, Spain},
month = sep,
year = 2015,
volume = {42},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Aceto, Luca and de Frutos-Escrig, David},
acronym = {{CONCUR}'15},
booktitle = {{P}roceedings of the 26th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'15)},
author = {Aiswarya, C. and Bollig, Benedikt and Gastin, Paul},
title = {An Automata-Theoretic Approach to the Verification of Distributed Algorithms},
pages = {340-353},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABG-concur15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABG-concur15.pdf},
doi = {10.4230/LIPIcs.CONCUR.2015.340},
abstract = {We introduce an automata-theoretic method for the verification
of distributed algorithms running on ring networks. In a distributed
algorithm, an arbitrary number of processes cooperate to achieve a common
goal (e.g., elect a leader). Processes have unique identifiers (pids) from
an infinite, totally ordered domain. An algorithm proceeds in synchronous
rounds, each round allowing a process to perform a bounded sequence of
actions such as send or receive a pid, store it in some register, and
compare register contents wrt. the associated total order. An algorithm is
supposed to be correct independently of the number of processes. To
specify correctness properties, we introduce a logic that can reason about
processes and pids. Referring to leader election, it may say that, at the
end of an execution, each process stores the maximum pid in some dedicated
register. Since the verification of distributed algorithms is undecidable,
we propose an underapproximation technique, which bounds the number of
rounds. This is an appealing approach, as the number of rounds needed by a
distributed algorithm to conclude is often exponentially smaller than the
number of processes. We provide an automata-theoretic solution, reducing
model checking to emptiness for alternating two-way automata on words.
Overall, we show that round-bounded verification of distributed algorithms
over rings is PSPACE-complete.}
}
@inproceedings{AGS-concur16,
address = {Qu{\'e}bec City, Canada},
month = aug,
year = 2016,
volume = {59},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Desharnais, Jos{\'e}e and Jagadeesan, Radha},
acronym = {{CONCUR}'16},
booktitle = {{P}roceedings of the 27th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'16)},
author = {Akshay, S. and Paul Gastin and Krishna, Shankara Narayanan},
title = {Analyzing Timed Systems Using Tree Automata},
pages = {27:1-27:14},
url = {http://arxiv.org/abs/1604.08443},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGS-concur16.pdf},
doi = {10.4230/LIPIcs.CONCUR.2016.27},
abstract = {Timed systems, such as timed automata, are usually analyzed
using their operational semantics on timed words. The classical region
abstraction for timed automata reduces them to (untimed) finite state
automata with the same time-abstract properties, such as state
reachability. We propose a new technique to analyze such timed systems
using finite tree automata instead of finite word automata. The main idea
is to consider timed behaviors as graphs with matching edges capturing
timing constraints. Such graphs can be interpreted in trees opening the
way to tree automata based techniques which are more powerful than
analysis based on word automata. The technique is quite general and
applies to many timed systems. In this paper, as an example, we develop
the technique on timed pushdown systems, which have recently received
considerable attention. Further, we also demonstrate how we can use it on
timed automata and timed multi-stack pushdown systems (with boundedness
restrictions).}
}
@comment{{B-arxiv16,
author = Bollig, Benedikt,
affiliation = aff-LSVmexico,
title = One-Counter Automata with Counter Visibility,
institution = Computing Research Repository,
number = 1602.05940,
month = feb,
nmonth = 2,
year = 2016,
type = RR,
axeLSV = mexico,
NOcontrat = "",
url = http://arxiv.org/abs/1602.05940,
PDF = "http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf",
lsvdate-new = 20160222,
lsvdate-upd = 20160222,
lsvdate-pub = 20160222,
lsv-category = "rapl",
wwwpublic = "public and ccsb",
note = 18~pages,
abstract = "In a one-counter automaton (OCA), one can read a letter
from some finite alphabet, increment and decrement the counter by
one, or test it for zero. It is well-known that universality and
language inclusion for OCAs are undecidable. We consider here OCAs
with counter visibility: Whenever the automaton produces a letter,
it outputs the current counter value along with~it. Hence, its
language is now a set of words over an infinite alphabet. We show
that universality and inclusion for that model are in PSPACE, thus
no harder than the corresponding problems for finite automata, which
can actually be considered as a special case. In fact, we show that
OCAs with counter visibility are effectively determinizable and
closed under all boolean operations. As~a~strict generalization, we
subsequently extend our model by registers. The general nonemptiness
problem being undecidable, we impose a bound on the number of
register comparisons and show that the corresponding nonemptiness
problem is NP-complete.",
}}
@inproceedings{FG-fossacs16,
address = {Eindhoven, The~Netherlands},
month = apr,
year = 2016,
volume = {9634},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Jacobs, Bart and L{\"o}ding, Christof},
acronym = {{FoSSaCS}'16},
booktitle = {{P}roceedings of the 19th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'16)},
author = {Fortin, Marie and Gastin, Paul},
title = {Verification of parameterized communicating automata via split-width},
pages = {197-213},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FG-fossacs16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FG-fossacs16.pdf},
doi = {10.1007/978-3-662-49630-5_12},
abstract = {We~study verification problems for distributed systems
communicating via unbounded FIFO channels. The number of processes
of the system as well as the communication topology are not fixed
a~priori. Systems are given by parameterized communicating automata
(PCAs) which can be run on any communication topology of bounded
degree, with arbitrarily many processes. Such systems are Turing
powerful so we concentrate on under-approximate verification. We
extend the notion of split-width to behaviors of PCAs. We show that
emptiness, reachability and model-checking problems of PCAs are
decidable when restricted to behaviors of bounded split-width.
Reachability and emptiness are EXPTIME-complete, but only polynomial
in the size of the PCA. We also describe several concrete classes of
bounded split-width, for which we prove similar results.}
}
@inproceedings{BFG-stacs18,
address = {Caen, France},
month = feb,
volume = {96},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Niedermeier, Rolf and Vall{\'e}e, Brigitte},
acronym = {{STACS}'18},
booktitle = {{P}roceedings of the 35th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'18)},
author = {Bollig, Benedikt and Fortin, Marie and Gastin, Paul},
title = {Communicating Finite-State Machines and Two-Variable Logic},
pages = {17:1-17:14},
year = {2018},
doi = {10.4230/LIPIcs.STACS.2018.17},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/8529/pdf/LIPIcs-STACS-2018-17.pdf},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=8529},
abstract = {Communicating finite-state machines are a fundamental, well-studied model of finite-state processes that communicate via unbounded first-in first-out channels. We show that they are expressively equivalent to existential MSO logic with two first-order variables and the order relation.}
}
@inproceedings{AGKS-concur17,
address = {Berlin, Germany},
month = sep,
year = 2017,
volume = {85},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Meyer, Roland and Nestmann, Uwe},
acronym = {{CONCUR}'17},
booktitle = {{P}roceedings of the 28th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'17)},
author = {Akshay, S. and Gastin, Paul and Krishna, Shankara Narayanan and Sarkar, Ilias},
title = {Towards an Efficient Tree Automata based technique for Timed Systems},
pages = {39:1--39:15},
url = {http://drops.dagstuhl.de/opus/volltexte/2017/7801},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/7801/pdf/LIPIcs-CONCUR-2017-39.pdf},
doi = {10.4230/LIPIcs.CONCUR.2017.39},
abstract = {The focus of this paper is the analysis of real-time systems with recursion, through the development of good theoretical techniques which are implementable. Time is modeled using clock variables, and recursion using stacks. Our technique consists of modeling the behaviours of the timed system as graphs, and interpreting these graphs on tree terms by showing a bound on their tree-width. We then build a tree automaton that accepts exactly those tree terms that describe realizable runs of the timed system. The emptiness of the timed system thus boils down to emptiness of a finite tree automaton that accepts these tree terms. This approach helps us in obtaining an optimal complexity, not just in theory (as done in earlier work e.g.[concur16]), but also in going towards an efficient implementation of our technique. To do this, we make several improvements in the theory and exploit these to build a first prototype tool that can analyze timed systems with recursion.}
}
@article{ABG-ic17,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Aiswarya, C. and Bollig, Benedikt and Gastin, Paul},
title = {An Automata-Theoretic Approach to the Verification of Distributed Algorithms},
volume = {259},
month = apr,
year = {2018},
pages = {305-327},
doi = {10.1016/j.ic.2017.05.006},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABG-ic17.pdf},
abstract = {We introduce an automata-theoretic method for the verification of distributed algorithms running on ring networks. In a distributed algorithm, an arbitrary number of processes cooperate to achieve a common goal (e.g., elect a leader). Processes have unique identifiers (pids) from an infinite, totally ordered domain. An algorithm proceeds in synchronous rounds, each round allowing a process to perform a bounded sequence of actions such as send or receive a pid, store it in some register, and compare register contents wrt. the associated total order. An algorithm is supposed to be correct independently of the number of processes. To specify correctness properties, we introduce a logic that can reason about processes and pids. Referring to leader election, it may say that, at the end of an execution, each process stores the maximum pid in some dedicated register.
We show that the verification problem of distributed algorithms can be reduced to satisfiability of a formula from propositional dynamic logic with loop and converse (LCPDL), interpreted over grids over a finite alphabet. This translation is independent of any restriction imposed on the algorithm. However, since the verification problem (and satisfiability for LCPDL) is undecidable, we propose an underapproximation technique, which bounds the number of rounds. This is an appealing approach, as the number of rounds needed by a distributed algorithm to conclude is often exponentially smaller than the number of processes. Using our reduction to LCPDL, we provide an automata-theoretic solution, reducing model checking to emptiness for alternating two-way automata on words. Overall, we show that round-bounded verification of distributed algorithms over rings is PSPACE-complete, provided the number of rounds is given in unary.}
}
@inproceedings{GMS-concur18,
address = {Beijing, China},
month = sep,
year = 2018,
volume = {118},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Schewe, Sven and Zhang, Lijun},
acronym = {{CONCUR}'18},
booktitle = {{P}roceedings of the 29th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'18)},
author = {Paul Gastin and Sayan Mukherjee and B. Srivathsan},
title = {Reachability in timed automata with diagonal constraints},
pages = {28:1-28:17},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9566},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/9566/pdf/LIPIcs-CONCUR-2018-28.pdf},
doi = {10.4230/LIPIcs.CONCUR.2018.28},
abstract = {We consider the reachability problem for timed automata having diagonal constraints (like x - y < 5) as guards in transitions. The best algorithms for timed automata proceed by enumerating reachable sets of its configurations, stored in a data structure called ''zones''. Simulation relations between zones are essential to ensure termination and efficiency. The algorithm employs a simulation test Z <= Z' which ascertains that zone Z does not reach more states than zone Z', and hence further enumeration from Z is not necessary. No effective simulations are known for timed automata containing diagonal constraints as guards. We propose a simulation relation <=_{LU}^d for timed automata with diagonal constraints. On the negative side, we show that deciding Z not <=_{LU}^d Z' is NP-complete. On the positive side, we identify a witness for Z not <=_{LU}^d Z' and propose an algorithm to decide the existence of such a witness using an SMT solver. The shape of the witness reveals that the simulation test is likely to be efficient in practice.}
}
@inproceedings{BFG-concur18,
address = {Beijing, China},
month = sep,
year = 2018,
volume = {118},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Schewe, Sven and Zhang, Lijun},
acronym = {{CONCUR}'18},
booktitle = {{P}roceedings of the 29th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'18)},
author = {Bollig, Benedikt and Fortin, Marie and Gastin, Paul},
title = {It Is Easy to Be Wise After the Event: Communicating Finite-State
Machines Capture First-Order Logic with ''Happened Before''},
pages = {7:1-7:17},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9545},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/9545/pdf/LIPIcs-CONCUR-2018-7.pdf},
doi = {10.4230/LIPIcs.CONCUR.2018.7},
abstract = {Message sequence charts (MSCs) naturally arise as executions of communicating finite-state machines (CFMs), in which finite-state processes exchange messages through unbounded FIFO channels. We study the first-order logic of MSCs, featuring Lamport's happened-before relation. We introduce a star-free version of propositional dynamic logic (PDL) with loop and converse. Our main results state that (i) every first-order sentence can be transformed into an equivalent star-free PDL sentence (and conversely), and (ii) every star-free PDL sentence can be translated into an equivalent CFM. This answers an open question and settles the exact relation between CFMs and fragments of monadic second-order logic. As a byproduct, we show that first-order logic over MSCs has the three-variable property.}
}
@article{AGK-lmcs18,
journal = {Logical Methods in Computer Science},
author = {Akshay, S. and Gastin, Paul and Krishna, Shankara Narayanan},
title = {Analyzing Timed Systems Using Tree Automata},
volume = {14},
number = {2},
pages = {1-35},
year = {2018},
month = may,
doi = {10.23638/LMCS-14(2:8)2018},
pdf = {https://lmcs.episciences.org/4489/pdf},
url = {https://lmcs.episciences.org/4489},
abstract = {Timed systems, such as timed automata, are usually analyzed using their operational semantics on timed words. The classical region abstraction for timed automata reduces them to (untimed) finite state automata with the same time-abstract properties, such as state reachability. We propose a new technique to analyze such timed systems using finite tree automata instead of finite word automata. The main idea is to consider timed behaviors as graphs with matching edges capturing timing constraints. When a family of graphs has bounded tree-width, they can be interpreted in trees and MSO-definable properties of such graphs can be checked using tree automata. The technique is quite general and applies to many timed systems. In this paper, as an example, we develop the technique on timed pushdown systems, which have recently received considerable attention. Further, we also demonstrate how we can use it on timed automata and timed multi-stack pushdown systems (with boundedness restrictions).}
}
@inproceedings{DGK-lics18,
address = {Oxford, UK},
publisher = {ACM Press},
editor = {Hofmann, Martin and Dawar, Anuj and Gr{\"a}del, Erich},
acronym = {{LICS}'18},
booktitle = {{P}roceedings of the 33rd {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'18)},
author = {Dave, Vrunda and Gastin, Paul and Krishna, Shankara Narayanan},
month = jul,
title = {{Regular Transducer Expressions for Regular Transformations}},
year = {2018},
url = {https://arxiv.org/abs/1802.02094},
pdf = {https://arxiv.org/pdf/1802.02094.pdf},
pages = {315-324},
doi = {10.1145/3209108.3209182},
abstract = {Functional MSO transductions, deterministic two-way transducers, as well as streaming string transducers are all equivalent models for regular functions. In this paper, we show that every regular function, either on finite words or on infinite words, captured by a deterministic two-way transducer, can be described with a regular transducer expression (RTE). For infinite words, the transducer uses Muller acceptance and \(\omega\)-regular look-ahead. RTEs are constructed from constant functions using the combinators if-then-else (deterministic choice), Hadamard product, and unambiguous versions of the Cauchy product, the 2-chained Kleene-iteration and the 2-chained omega-iteration. Our proof works for transformations of both finite and infinite words, extending the result on finite words of Alur et al. in LICS'14. In order to construct an RTE associated with a deterministic two-way Muller transducer with look-ahead, we introduce the notion of transition monoid for such two-way transducers where the look-ahead is captured by some backward deterministic Büchi automaton. Then, we use an unambiguous version of Imre Simon's famous forest factorization theorem in order to derive a ''good'' (\(\omega\)-)regular expression for the domain of the two-way transducer. ''Good'' expressions are unambiguous and Kleene-plus as well as \(\omega\)-iterations are only used on subexpressions corresponding to idempotent elements of the transition monoid. The combinator expressions are finally constructed by structural induction on the ''Good'' (\(\omega\)-)regular expression describing the domain of the transducer.}
}
@article{GM-softc18,
publisher = {Springer},
journal = {Soft Computing},
author = {Gastin, Paul and Monmege, Benjamin},
title = {{A unifying survey on weighted logics and weighted automata}},
volume = {22},
number = {4},
year = {2018},
month = feb,
pages = {1047-1065},
doi = {10.1007/s00500-015-1952-6},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/softc2016-GM.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/softc2016-GM.pdf},
abstract = {Logical formalisms equivalent to weighted automata have been the topic of numerous research papers in the recent years. It started with the seminal result by Droste and Gastin on weighted logics over semirings for words. It has been extended in two dimensions by many authors. First, the weight domain has been extended to valuation monoids, valuation structures, etc. to capture more quantitative properties. Along another dimension, different structures such as ranked or unranked trees, nested words, Mazurkiewicz traces, etc. have been considered. The long and involved proofs of equivalences in all these papers are implicitly based on the same core arguments. This article provides a meta-theorem which unifies these different approaches. Towards this, we first revisit weighted automata by defining a new semantics for them in two phases---an abstract semantics based on multisets of weight structures (independent of particular weight domains) followed by a concrete semantics. Then, we introduce a core weighted logic with a minimal number of features and a simplified syntax, and lift the new semantics to this logic. We show at the level of the abstract semantics that weighted automata and core weighted logic have the same expressive power. Finally, we show how previous results can be recovered from our result by logical reasoning. In this paper, we prove the meta-theorem for words, ranked and unranked trees, showing the robustness of our approach.}
}
@inproceedings{GMG-dlt19,
address = {Warsaw, Poland},
month = aug,
volume = {11647},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Piotrek Hofman and Micha\l Skrzypczak},
acronym = {{DLT}'19},
booktitle = {{P}roceedings of the 23th {I}nternational
{C}onference on {D}evelopments in {L}anguage {T}heory
({DLT}'19)},
author = {Paul Gastin and Amaldev Manuel and R. Govind},
title = {Logics for Reversible Regular Languages and Semigroups with Involution},
pages = {182-191},
doi = {10.1007/978-3-030-24886-4_13},
year = 2019,
pdf = {https://arxiv.org/pdf/1907.01214.pdf},
url = {https://arxiv.org/abs/1907.01214},
abstract = {We present MSO and FO logics with predicates ``between'' and
``neighbour'' that characterise various fragments of the class of regular
languages that are closed under the reverse operation. The standard
connections that exist between MSO and FO logics and varieties of finite
semigroups extend to this setting with semigroups extended with an
involution. The case is different for FO with neighbour relation where
we show that one needs additional equations to characterise the class.}
}
@inproceedings{Gastin-cai19,
address = {Ni{\u s}, Serbia},
month = jun,
volume = 11545,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Miroslav {\'C}iri{\'c} and Manfred Droste and Jean-{\'E}ric Pin},
acronym = {{CAI}'19},
booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on
{A}lgebraic {I}nformatics ({CAI}'19)},
author = {Gastin, Paul},
title = {Modular Descriptions of Regular Functions},
pages = {3-9},
note = {Invited talk},
year = 2019,
pdf = {https://arxiv.org/abs/1908.01137},
doi = {10.1007/978-3-030-21363-3_1},
abstract = {We discuss various formalisms to describe string-to-string
transformations. Many are based on automata and can be seen as operational
descriptions, allowing direct implementations when the input scanner is
deterministic. Alternatively, one may use more human friendly descriptions
based on some simple basic transformations (e.g., copy, duplicate, erase,
reverse) and various combinators such as function com- position or extensions
of regular operations.}
}
@inproceedings{GMS-cav19,
address = {New York, USA},
month = jul,
volume = {11561},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Isil Dillig and Serdar Tasiran},
acronym = {{CAV}'19},
booktitle = {{P}roceedings of the 31st
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'19)},
author = {Paul Gastin and Sayan Mukherjee and B. Srivathsan},
title = {Fast algorithms for handling diagonal constraints in timed automata},
pages = {41-59},
year = 2019,
doi = {10.1007/978-3-030-25540-4_3},
pdf = {https://arxiv.org/pdf/1904.08590.pdf},
url = {https://arxiv.org/abs/1904.08590}
}
@inproceedings{BBM-mfcs19,
address = {Aachen, Germany},
month = aug,
volume = {138},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Pinar Heggernes and Joost-Pieter Katoen and Peter Rossmanith},
acronym = {{MFCS}'19},
booktitle = {{P}roceedings of the 42nd
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'19)},
author = {Manfred Droste and Paul Gastin},
title = {Aperiodic Weighted Automata and Weighted First-Order Logic},
pages = {76:1-76:15},
year = 2019,
doi = {10.4230/LIPIcs.MFCS.2019.76},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2019/11020/pdf/LIPIcs-MFCS-2019-76.pdf},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11020}
}
@inproceedings{AGJK-lics19,
address = {Vancouver, Canada},
month = jun,
publisher = {{IEEE} Press},
editor = {Bouyer, Patricia},
acronym = {{LICS}'19},
booktitle = {{P}roceedings of the 34th {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'19)},
author = {Akshay, S. and Gastin, Paul and Jug{\'e}, Vincent and Krishna, Shankara Narayanan},
title = {Timed systems through the lens of logic},
pages = {1-13},
year = 2019,
doi = {10.1109/LICS.2019.8785684},
pdf = {https://arxiv.org/pdf/1903.03773.pdf},
url = {https://arxiv.org/abs/1903.03773},
abstract = {In this paper, we analyze timed systems with data structures, using a rich interplay of logic and properties of graphs. We start by describing behaviors of timed systems using graphs with timing constraints. Such a graph is called realizable if we can assign time-stamps to nodes or events so that they are consistent with the timing constraints. The logical definability of several graph properties has been a challenging problem, and we show, using a highly non-trivial argument, that the realizability property for collections of graphs with strict timing constraints is logically definable in a class of propositional dynamic logic (EQ-ICPDL), which is strictly contained in MSO. Using this result, we propose a novel, algorithmically efficient and uniform proof technique for the analysis of timed systems enriched with auxiliary data structures, like stacks and queues. Our technique unravels new results (for emptiness checking as well as model checking) for timed systems with richer features than considered so far, while also recovering existing results.}
}
@article{GMG-fi20,
publisher = {{IOS} Press},
journal = {Fundamenta Informaticae},
author = {Gastin, Paul and Manuel, Amaldev and Govind, R.},
title = {{Reversible Regular Languages: Logical and Algebraic Characterisations}},
year = {2020},
note = {To appear}
}
@inproceedings{BBRRV-fsttcs20,
address = {Goa, India},
month = dec,
volume = {182},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Nitin Saxena and Sunil Simon},
acronym = {{FSTTCS}'20},
booktitle = {{P}roceedings of the 40th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'20)},
author = {Paul Gastin and Sayan Mukherjee and B Srivathsan},
title = {Reachability for updatable timed automata made faster and more effective},
pages = {47:1--47:17},
year = {2020},
doi = {https://doi.org/10.4230/LIPIcs.FSTTCS.2020.47},
pdf = {https://drops.dagstuhl.de/opus/volltexte/2020/13288/pdf/LIPIcs-FSTTCS-2020-47.pdf},
url = {https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=13288}
}
@inproceedings{AG-fsttcs20,
address = {Goa, India},
month = dec,
volume = {182},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Nitin Saxena and Sunil Simon},
acronym = {{FSTTCS}'20},
booktitle = {{P}roceedings of the 40th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'20)},
author = {C. Aiswarya and Paul Gastin},
title = {Weighted Tiling Systems for Graphs: Evaluation Complexity},
year = {2020},
doi = {https://doi.org/10.4230/LIPIcs.FSTTCS.2020.34},
pdf = {https://drops.dagstuhl.de/opus/volltexte/2020/13275/pdf/LIPIcs-FSTTCS-2020-34.pdf},
url = {https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=13275}
}
@article{DGN-ic20,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Dave, Vrunda and Gastin, Paul and Krishna, Shankara Narayanan},
title = {Regular Transducer Expressions for Regular Transformations},
year = {2020},
url = {https://doi.org/10.1016/j.ic.2020.104655},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DGK20-IC-final.pdf}
}
@inproceedings{DFG-mfcs20,
address = {Prague, Czech Republic},
month = aug,
volume = {170},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Javier Esparza and Dan Kr{\'a}l},
acronym = {{MFCS}'20},
booktitle = {{P}roceedings of the 43rd
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'20)},
author = {Dou{\'e}neau-Tabot, Ga{\"e}tan and Filiot, Emmanuel and Gastin, Paul},
title = {Register transducers are marble transducers},
pages = {29:1--29:14},
year = 2020,
doi = {https://doi.org/10.4230/LIPIcs.MFCS.2020.29},
pdf = {https://drops.dagstuhl.de/opus/volltexte/2020/12697/pdf/LIPIcs-MFCS-2020-29.pdf},
url = {https://drops.dagstuhl.de/opus/volltexte/2020/12697/}
}
@inproceedings{AGSW-concur20,
address = {Vienna, Austria},
month = sep,
volume = {171},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Igor Konnov and Laura Kovacs},
acronym = {{CONCUR}'20},
booktitle = {{P}roceedings of the 31st
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'20)},
author = {Bharat Adsul and Paul Gastin and Saptarshi Sarkar and Pascal Weil},
title = {Wreath/cascade products and related decomposition results for the concurrent setting of {M}azurkiewicz traces},
pages = {19:1--19:17},
year = 2020,
doi = {10.4230/LIPIcs.CONCUR.2020.19},
url = {https://drops.dagstuhl.de/opus/volltexte/2020/12831}
}
@article{BFG-jcss20,
publisher = {Elsevier Science Publishers},
journal = {Journal of Computer and System Sciences},
author = {Benedikt Bollig and Marie Fortin and Paul Gastin},
title = {Communicating Finite-State Machines, First-Order Logic, and Star-Free Propositional Dynamic Logic},
pages = {22-53},
doi = {10.1016/j.jcss.2020.06.006},
year = {2020},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFG20-JCSS.pdf},
abstract = {Message sequence charts (MSCs) naturally arise as executions of communicating
finite-state machines (CFMs), in which finite-state processes exchange
messages through unbounded FIFO channels. We study the first-order logic of
MSCs, featuring Lamport's happened-before relation. To this end, we introduce a star-free
version of propositional dynamic logic (PDL) with loop and converse. Our main
results state that (i) every first-order sentence can be transformed into an
equivalent star-free PDL sentence (and conversely), and (ii) every star-free
PDL sentence can be translated into an equivalent CFM. This answers an open
question and settles the exact relation between CFMs and fragments of monadic
second-order logic. As a byproduct, we show that first-order logic over MSCs
has the three-variable property.}
}
@proceedings{CG-fsttcs2019,
address = {Bombay, India},
month = dec,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Arkadev Chattopadhyay and Paul Gastin},
acronym = {{FSTTCS}'19},
booktitle = {{P}roceedings of the 39th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'19)},
title = {{P}roceedings of the 39th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'19)},
author = {Arkadev Chattopadhyay and Paul Gastin},
year = {2019},
url = {http://www.dagstuhl.de/dagpub/978-3-95977-131-3}
}
@inproceedings{AGKR-tacas2020,
address = {Dublin, Ireland},
month = apr,
volume = {12078},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Armin Biere and David Parker},
acronym = {{TACAS}'20},
booktitle = {{P}roceedings of the 26th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'20)},
author = {Akshay, S. and Gastin, Paul and Krishna, Shankara Narayanan and Roychoudhary, Sparsa},
title = {Revisiting Underapproximate Reachability for Multipushdown Systems},
pages = {387--404},
doi = {10.1007/978-3-030-45190-5_21},
year = 2020,
pdf = {https://arxiv.org/pdf/2002.05950.pdf},
url = {https://link.springer.com/chapter/10.1007/978-3-030-45190-5_21},
longurl = {https://arxiv.org/abs/2002.05950}
}
This file was generated by bibtex2html 1.98.