@inproceedings{LA-PB-AB-KL-fsttcs98,
address = {Chennai, India},
month = dec,
year = 1998,
volume = 1530,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Arvind, Vikraman and Ramanujam, R.},
acronym = {{FSTTCS}'98},
booktitle = {{P}roceedings of the 18th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'98)},
author = {Aceto, Luca and Bouyer, Patricia and
Burgue{\~n}o, Augusto and Larsen, Kim G.},
title = {The Power of Reachability Testing for
Timed Automata},
pages = {245-256},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ABBL-fsttcs98.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ABBL-fsttcs98.ps},
abstract = {In this paper we provide a
complete characterization of the class of
properties of (networks of) timed automata for
which model checking
can be reduced to reachability checking in the
context of testing
automata.}
}
@mastersthesis{PB-dea98,
author = {Bouyer, Patricia},
title = {Automates temporis{\'e}s et modularit{\'e}},
year = {1998},
month = jun,
type = {Rapport de {DEA}},
school = {{DEA} Algorithmique, Paris, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bou-dea98.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bou-dea98.ps},
lsv-lang = {FR}
}
@inproceedings{PB-AP-icalp99,
address = {Prague, Czech Republic},
month = jul,
year = 1999,
volume = 1644,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Wiedermann, Jir{\'i} and van Emde Boas, Peter and
Nielsen, Mogens},
acronym = {{ICALP}'99},
booktitle = {{P}roceedings of the 26th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming
({ICALP}'99)},
author = {Bouyer, Patricia and Petit, Antoine},
title = {Decomposition and Composition of Timed Automata},
pages = {210-219},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BP-icalp99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BP-icalp99.ps},
abstract = {We propose in this paper a
decomposition theorem for the timed
automata introduced by Alur and Dill. To this
purpose, we define a new
simple and natural concatenation operation,
indexed by the set of
clocks to be reset, on timed automata
generalizing the classical
untimed concatenation. \par
Then we extend the famous Kleene's and B{\"u}chi's
theorems on classical
untimed automata by simply changing the basic
objects to take time
into account, keeping the union operation and
replacing the
concatenation, finite and infinite iterations by
the new timed
concatenations and their induced iterations.\par
Thus, and up to our knowledge, our result
provides the simplest known
algebraic characterization of recognizable timed
languages.}
}
@inproceedings{BDFP-mfcs-2000,
address = {Bratislava, Slovakia},
month = aug,
year = 2000,
volume = 1893,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Nielsen, Mogens and Rovan, Branislav},
acronym = {{MFCS} 2000},
booktitle = {{P}roceedings of the 25th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS} 2000)},
author = {Bouyer, Patricia and Dufourd, Catherine and
Fleury, Emmanuel and Petit, Antoine},
title = {Expressiveness of Updatable Timed Automata},
pages = {232-242},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BDFP-mfcs2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BDFP-mfcs2000.ps},
abstract = {Since their introduction by Alur
and Dill, timed automata have been
one of the most widely studied models for
real-time systems. The
syntactic extension of so-called updatable timed
automata allows more
powerful updates of clocks than the reset
operation proposed in the
original model.\par
We prove that any language accepted by an
updatable timed automaton
(from classes where emptiness is decidable) is
also accepted by a
{"}classical{"} timed automaton. We propose even
more precise results on
bisimilarity between updatable and classical
timed automata.}
}
@misc{Calife-4.2,
author = {Bouyer, Patricia and Fleury, Emmanuel and
Petit, Antoine},
title = {Document de synth{\`e}se sur les proc{\'e}dures de
v{\'e}rification des syst{\`e}mes temps r{\'e}el :
Les automates temporis{\'e}s},
year = {2000},
month = jan,
howpublished = {Fourniture~4.2 du projet RNRT Calife},
lsv-lang = {FR}
}
@inproceedings{PB-CD-EF-AP-cav2000,
address = {Chicago, Illinois, USA},
month = jul,
year = 2000,
volume = 1855,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Emerson, E. Allen and Sistla, A. Prasad},
acronym = {{CAV} 2000},
booktitle = {{P}roceedings of the 12th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV} 2000)},
author = {Bouyer, Patricia and Dufourd, Catherine and
Fleury, Emmanuel and Petit, Antoine},
title = {Are Timed Automata Updatable?},
pages = {464-479},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BDEP-cav2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BDEP-cav2000.ps},
abstract = {In classical timed automata, as
defined by Alur and Dill and since
widely studied, the only operation allowed to
modify the clocks is the
reset operation. For instance, a clock can
neither be set to a
non-null constant value, nor be set to the value
of another clock nor,
in a non-deterministic way, to some value lower
or higher than a given
constant. In this paper we study in details such
updates.\par
We characterize in a thin way the frontier
between decidability and
undecidability. Our main contributions are the
following:\par
1)~We exhibit many classes of updates for which
emptiness is
undecidable. These classes depend on the clock
constraints that are
used ---~diagonal-free or not~--- whereas it is
well-known that these
two kinds of constraints are equivalent for
classical timed
automata.\par
2)~We propose a generalization of the region
automaton proposed by Alur
and Dill, allowing to handle larger classes of
updates. The
complexity of the decision procedure remains
PSPACE-complete.}
}
@inproceedings{BPT-concur-2001,
address = {Aalborg, Denmark},
month = aug,
year = 2001,
volume = 2154,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Larsen, Kim G. and Nielsen, Modens},
acronym = {{CONCUR}'01},
booktitle = {{P}roceedings of the 12th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'01)},
author = {Bouyer, Patricia and Petit, Antoine and
Th{\'e}rien, Denis},
title = {An Algebraic Characterization of Data and Timed
Languages},
pages = {248-261},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BPT-concur2001.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BPT-concur2001.ps},
abstract = {Algebra offers an elegant and
powerful approach to understand regular
languages and finite automata. Such framework
has been notoriously
lacking for timed languages and timed automata.
We introduce the
notion of monoid recognizability for data
languages, which include
timed languages as special case, in a way that
respects the spirit of
the classical situation. We study closure
properties and hierarchies
in this model, and prove that emptiness is
decidable under natural
hypotheses. Our class of recognizable languages
properly includes many
families of deterministic timed languages that
have been proposed
until now, and the same holds for
non-deterministic versions.}
}
@techreport{Calife-4.4,
author = {B{\'e}rard, B{\'e}atrice and Bouyer, Patricia and
Petit, Antoine},
title = {Mod{\'e}lisation du protocole~{PGM} et de certaines de ses
propri{\'e}t{\'e}s en {UPPAAL}},
year = {2001},
month = nov,
type = {Contract Report},
number = {4.4},
institution = {projet RNRT Calife},
note = {18 pages}
}
@article{BP-JALC2002,
journal = {Journal of Automata, Languages and Combinatorics},
author = {Bouyer, Patricia and Petit, Antoine},
title = {A {K}leene{\slash}B{\"u}chi-like Theorem for Clock Languages},
volume = {7},
number = {2},
pages = {167-186},
year = {2002},
missingmonth = {},
missingnmonth = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BP-JALC2001.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BP-JALC2001.ps},
abstract = {We propose in this paper a
generalization of the famous Kleene\slash B{\"u}chi's
theorem on formal languages, one of the
cornerstones of theoretical
computer science, to the timed model of clock
languages. These
languages extend the now classical timed
languages introduced by Alur
and Dill as a suitable model of real-time
systems. As a corollary of
our main result, we get a simple algebraic
characterization of timed
languages recognized by (updatable) timed
automata.}
}
@article{Bou-IPL2002,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Bouyer, Patricia},
title = {A Logical Characterization of Data Languages},
volume = {84},
number = {2},
pages = {75-85},
year = {2002},
month = oct,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bou-IPL2002.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bou-IPL2002.ps}
}
@phdthesis{THESE-BOUYER-2002,
author = {Bouyer, Patricia},
title = {Mod{\`e}les et algorithmes pour la v{\'e}rification des
syst{\`e}mes temporis{\'e}s},
year = {2002},
month = apr,
type = {Th{\`e}se de doctorat},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bouyer-these.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bouyer-these.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bouyer-these.ps}
}
@inproceedings{bbp-rttools02,
address = {Copenhagen, Denmark},
month = aug,
year = 2002,
howpublished = {Technical Report 2002-025,
Department of Information Technology,
Uppsala University, Sweden},
publisher = {Uppsala University},
editor = {Petterson, Paul and Yi, Wang},
acronym = {{RT-TOOLS}'02},
booktitle = {{P}roceedings of the 2nd {W}orkshop
on {R}eal-{T}ime {T}ools
({RT-TOOLS}'02)},
author = {B{\'e}rard, B{\'e}atrice and Bouyer, Patricia and
Petit, Antoine},
title = {Analysing the {PGM} Protocol with {UPPAAL}},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/pgmfin.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/pgmfin.ps},
abstract = {Pragmatic General Multicast (PGM)
is a reliable multicast protocol,
designed to minimize both the probability of
negative acknowledgements
(NAK) implosion and the loading of the network
due to retransmissions
of lost packets. This protocol was presented to
the Internet
Engineering Task Force as an open reference
specification. \par
In this paper, we focus on the main reliability
property which PGM
intends to guarantee: a receiver either receives
all data packets from
transmissions and repairs or is able to detect
unrecoverable data
packet loss.\par
To this purpose, we propose a modelization of (a
simplified version
of) PGM via a network of timed automata. Using
Uppaal model-checker,
we then study the validity of the reliability
property above, which
turns out to not be always verified but to
depend of the values of
several parameters that we underscore.}
}
@article{ABBL02,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Aceto, Luca and Bouyer, Patricia and
Burgue{\~n}o, Augusto and Larsen, Kim G.},
title = {The Power of Reachability Testing for Timed Automata},
volume = {300},
number = {1-3},
pages = {411-475},
year = {2003},
month = may,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bou-ABBL02.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bou-ABBL02.ps},
doi = {10.1016/S0304-3975(02)00334-1},
abstract = {The computational engine of the verification tool Uppaal
consists of a collection of efficient reachability properties of systems.
Model-checking of properties other than plain reachability ones may
currently be carried out in such a tool as follows. Given a property
\(\phi\) to model-check, the user must provide a test
automaton~\(T_{\phi}\) for it. This test automaton must be such that the
original system \(S\) has the property expressed by \(\phi\) precisely
when none of the distinguished reject states of~\(T_{\phi}\) can be
reached in the synchronized parallel composition of \(S\) with
\(T_{\phi}\). This raises the question of which properties may be analyzed
by {\scshape Uppaal} in such a way. This paper gives an answer to this
question by providing a complete characterization of the class of
properties for which model-checking can be reduced to reachability testing
in the sense outlined above. This result is obtained as a corollary of a
stronger statement pertaining to the compositionality of the property
language considered in this study. In particular, it is shown that our
language is the least expressive compositional language that can express a
simple safety property stating that no reject state can ever be
reached.\par
Finally, the property language characterizing the power of reachability
testing is used to provide a definition of characteristic properties with
respect to a timed version of the ready simulation preorder, for nodes of
\(\tau\)-free, deterministic timed automata.}
}
@inproceedings{BBFL-tacas-2003,
address = {Warsaw, Poland},
month = apr,
year = 2003,
volume = 2619,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Garavel, Hubert and Hatcliff, John},
acronym = {{TACAS}'03},
booktitle = {{P}roceedings of the 9th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'03)},
author = {Behrmann, Gerd and Bouyer, Patricia and
Fleury, Emmanuel and Larsen, Kim G.},
title = {Static Guard Analysis in Timed Automata Verification},
pages = {254-277},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBFL-tacas-2003.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBFL-tacas-2003.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBFL-tacas-2003.ps},
abstract = {By definition Timed Automata have
an infinite state-space, thus for verification
purposes, an exact finite abstraction is
required. We propose a location-based finite
zone abstraction, which computes an abstraction
based on the relevant guards for a particular
state of the model (as opposed to all guards).
We show that the location-based zone abstraction
is sound and complete with respect to location
reachability; that it generalises active-clock
reduction, in the sense that an inactive clock
has no relevant guards at all; that it enlarges
the class of timed automata, that can be
verified. We generalise the new abstraction to
the case of networks of timed automata, and
experimentally demonstrate a potentially
exponential speedup compared to the usual
abstraction.}
}
@inproceedings{BBP-msr2003,
address = {Metz, France},
month = oct,
year = 2003,
publisher = {Herm{\`e}s},
editor = {M{\'e}ry, Dominique and Rezg, Nidhal and
Xie, Xiaolan},
acronym = {{MSR}'03},
booktitle = {{A}ctes du 4{\`e}me {C}olloque sur la
{M}od{\'e}lisation des {S}yst{\`e}mes
{R}{\'e}actifs
({MSR}'03)},
author = {B{\'e}rard, B{\'e}atrice and Bouyer, Patricia and
Petit, Antoine},
title = {Une analyse du protocole {PGM} avec {UPPAAL}},
pages = {415-430},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBP-msr2003.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBP-msr2003.ps},
abstract = {Pragmatic General Multicast (PGM)
is a reliable multicast protocol,
designed to minimize both the probability of
negative acknowledgements
(NAK) implosion and the loading of the network
due to retransmissions
of lost packets. This protocol was presented to
the Internet
Engineering Task Force as an open reference
specification. In this
paper, we focus on the main reliability property
which PGM intends to
guarantee: a receiver either receives all data
packets from
transmissions and repairs or is able to detect
unrecoverable data
packet loss. To this purpose, we propose a
modelization of (a
simplified version of) PGM via a network of
timed automata. Using
Uppaal model-checker, we then study the validity
of the reliability
property above, which turns out to not be always
verified but to
depend of the values of several parameters that
we underscore.}
}
@inproceedings{BDMP-cav-2003,
address = {Boulder, Colorado, USA},
month = jul,
year = 2003,
volume = 2725,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Hunt, Jr, Warren A. and Somenzi, Fabio},
acronym = {{CAV}'03},
booktitle = {{P}roceedings of the 15th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'03)},
author = {Bouyer, Patricia and D'Souza, Deepak and
Madhusudan, P. and
Petit, Antoine},
title = {Timed Control with Partial Observability},
pages = {180-192},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDMP-CAV03.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDMP-CAV03.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BDMP-CAV03.ps},
abstract = {We consider the problem of
synthesizing controllers for timed systems
modeled using timed automata. The point of
departure from earlier work is that we
consider controllers that have only a
partial observation of the system that it
controls. In discrete event systems (where
continuous time is not modeled), it is well
known how to handle partial observability,
and decidability issues do not differ from
the complete information setting. We show
however that timed control under partial
observability is undecidable even for
internal specifications (while the analogous
problem under complete observability is
decidable) and we identify a decidable
subclass.}
}
@article{BPT03,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Bouyer, Patricia and Petit, Antoine and
Th{\'e}rien, Denis},
title = {An Algebraic Approach to Data Languages and Timed
Languages},
volume = {182},
number = {2},
pages = {137-162},
year = {2003},
month = may,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BPT-IetC.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BPT-IetC.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BPT-IetC.ps},
abstract = {Algebra offers an elegant and
powerful approach to understand regular
languages and finite automata. Such framework
has been notoriously
lacking for timed languages and timed automata.
We introduce the
notion of monoid recognizability for data
languages, which includes
timed languages as special case, in away that
respects the spirit of
the classical situation. We study closure
properties and hierarchies
in this model, and prove that emptiness is
decidable under natural
hypotheses. Our class of recognizable
languages properly includes
many families of deterministic timed languages
that have been
proposed until now, and the same holds for
non-deterministic
versions.}
}
@inproceedings{Bou-stacs-2003,
address = {Berlin, Germany},
month = feb,
year = 2003,
volume = 2607,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Alt, Helmut and Habib, Michel},
acronym = {{STACS}'03},
booktitle = {{P}roceedings of the 20th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'03)},
author = {Bouyer, Patricia},
title = {Untameable Timed Automata!},
pages = {620-631},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bou-stacs2003.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bou-stacs2003.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bou-stacs2003.ps},
abstract = {Timed automata are a widely
studied model for real-time systems. Since
8~years, several tools implement this model and
are successfully used to verify real-life
examples. In spite of this well-established
framework, we prove that the forward analysis
algorithm implemented in these tools is not
correct! However, we also prove that it is
correct for a restricted class of timed
automata, which has been sufficient for modeling
numerous real-life systems.}
}
@misc{bouyer-movep2004,
author = {Bouyer, Patricia},
title = {Timed Automata~--- {F}rom Theory to Implementation},
year = 2004,
month = dec,
note = {27~pages},
howpublished = {Invited tutorial, 6th {W}inter {S}chool on
{M}odelling and {V}erifying {P}arallel {P}rocesses
({MOVEP}'04), Brussels, Belgium}
}
@misc{bouyer-epit32,
author = {Bouyer, Patricia},
title = {Timed Models for Concurrent 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}
}
@misc{bouyer-qest04,
author = {Bouyer, Patricia},
title = {Timed Automata~--- {F}rom Theory to Implementation},
year = 2004,
month = sep,
howpublished = {Invited tutorial, 1st International Conference on the
Quantitative Evaluation of System (QEST'04),
Twente, The Netherlands}
}
@inproceedings{BBL-hscc2004,
address = {Philadelphia, Pennsylvania, USA},
month = mar,
year = 2004,
volume = 2993,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Alur, Rajeev and Pappas, George J.},
acronym = {{HSCC}'04},
booktitle = {{P}roceedings of the 7th {I}nternational {C}onference
on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
({HSCC}'04)},
author = {Bouyer, Patricia and Brinksma, Ed and
Larsen, Kim G.},
title = {Staying Alive As Cheaply As Possible},
pages = {203-218},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBL-hscc04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBL-hscc04.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBL-hscc04.ps},
abstract = {This paper is concerned with the
derivation of infinite schedules for timed automata
that are in some sense optimal. To cover a wide class
of optimality criteria we start out by introducing an
extension of the (priced) timed automata model that
includes both costs and rewards as separate modelling
features. A precise definition is then given of what
constitutes optimal infinite behaviours for this class
of models. We subsequently show that the derivation of
optimal non-terminating schedules for such
double-priced timed automata is computable. This is
done by a reduction of the problem to the determination
of optimal mean-cycles in finite graphs with weighted
edges. This reduction is obtained by introducing the
so-called corner-point abstraction, a powerful
abstraction technique of which we show that it
preserves optimal schedules. }
}
@inproceedings{BBLP-tacas04,
address = {Barcelona, Spain},
month = mar,
year = 2004,
volume = 2988,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Jensen, Kurt and Podelski, Andreas},
acronym = {{TACAS}'04},
booktitle = {{P}roceedings of the 10th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'04)},
author = {Behrmann, Gerd and Bouyer, Patricia and
Larsen, Kim G. and Pel{\'a}nek, Radek},
title = {Lower and Upper Bounds in Zone Based Abstractions of
Timed Automata},
pages = {312-326},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBLP-tacas04.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBLP-tacas04.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBLP-tacas04.pdf},
abstract = {Timed automata have an infinite
semantics. For verification purposes, one usually
uses zone based abstractions w.r.t.~the maximal
constants to which clocks of the timed automaton are
compared. We show that by distinguishing maximal
lower and upper bounds, significantly coarser
abstractions can be obtained. We show soundness and
completeness of the new abstractions
w.r.t.~reachability. We demonstrate how information
about lower and upper bounds can be used to optimise
the algorithm for bringing a difference bound matrix
into normal form. Finally, we experimentally
demonstrate that the new techniques dramatically
increases the scalability of the real-time model
checker~{\scshape Uppaal}. }
}
@article{BBP-IJPR04,
publisher = {Taylor \& Francis},
journal = {International Journal of Production Research},
author = {B{\'e}rard, B{\'e}atrice and Bouyer, Patricia and
Antoine Petit},
title = {Analysing the {PGM} Protocol with {U}ppaal},
volume = {42},
number = {14},
pages = {2773-2791},
year = {2004},
month = jul,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBP-IJPR04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBP-IJPR04.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBP-IJPR04.ps},
abstract = {Pragmatic General Multicast (PGM)
is a reliable multicast protocol, designed to
minimize both the probability of negative
acknowledgements~(NAK) implosion and the load
of the network due to retransmissions of lost
packets. This protocol was presented to the
Internet Engineering Task Force as an open
reference specification.\par
In this paper, we focus on the main
reliability property which PGM intends to
guarantee: a receiver either receives all data
packets from transmissions and repairs or is
able to detect unrecoverable data packet loss.
\par
We first propose a modelization of (a
simplified version of) PGM via a network of
timed automata. Using Uppaal model-checker, we
then study the validity of the reliability
property above, which turns out not to be
always verified but to depend on the values of
several parameters that we underscore.}
}
@inproceedings{BCFL-gdv04,
address = {Boston, Massachusetts, USA},
month = feb,
year = {2005},
number = 1,
volume = 119,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {De Alfaro, Luca},
acronym = {{GDV}'04},
booktitle = {{P}roceedings of the {W}orkshop on
{G}ames in {D}esign and {V}erification
({GDV}'04)},
author = {Bouyer, Patricia and Cassez, Franck and
Fleury, Emmanuel and
Larsen, Kim G.},
title = {Synthesis of Optimal Strategies Using {HyTech}},
pages = {11-31},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFL-gdv04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFL-gdv04.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCFL-gdv04.ps},
doi = {10.1016/j.entcs.2004.07.006},
abstract = {Priced timed (game) automata extend timed
(game) automata with costs on both locations and
transitions. The problem of synthesizing an optimal
winning strategy for a priced timed game under some
hypotheses has been shown decidable in~[BCFL04]. In this
paper, we present an algorithm for computing the optimal
cost and for synthesizing an optimal strategy in case
there exists one. We also describe the implementation of
this algorithm with the tool HyTech and present an
example. }
}
@article{BDFP04,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Bouyer, Patricia and Dufourd, Catherine and
Fleury, Emmanuel and Petit, Antoine},
title = {Updatable Timed Automata},
volume = {321},
number = {2-3},
pages = {291-345},
year = {2004},
month = aug,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/uta-BDFP04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/uta-BDFP04.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/uta-BDFP04.ps},
doi = {10.1016/j.tcs.2004.04.003},
abstract = {We investigate extensions of Alur and
Dill's timed automata, based on the possibility to
update the clocks in a more elaborate way than simply
reset them to zero. We call these automata updatable
timed automata. They form an undecidable class of
models, in the sense that emptiness checking is not
decidable. However, using an extension of the region
graph construction, we exhibit interesting decidable
subclasses. In a surprising way, decidability depends
on the nature of the clock constraints which are
used, diagonal-free or not, whereas these constraints
play identical roles in timed automata. We thus
describe in a quite precise way the thin frontier
between decidable and undecidable classes of
updatable timed automata. \par
We also study the
expressive power of updatable timed automata. It
turns out that any updatable automaton belonging to
some decidable subclass can be effectively
transformed into an equivalent timed automaton
without updates but with silent transitions. The
transformation suffers from an enormous combinatorics
blow-up which seems unavoidable. Therefore, updatable
timed automata appear to be a concise model for
representing and analyzing large classes of timed
systems. }
}
@inproceedings{BCFL-fsttcs04,
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 = {Bouyer, Patricia and Cassez, Franck and
Fleury, Emmanuel and
Larsen, Kim G.},
title = {Optimal Strategies in Priced Timed Game Automata},
pages = {148-160},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFL-fsttcs04.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/
BCFL-fsttcs04.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCFL-fsttcs04.pdf},
abstract = {Priced timed (game) automata extend
timed (game) automata with costs on both locations
and transitions. In this paper we focus on
reachability priced timed game automata and prove
that the optimal cost for winning such a game is
computable under conditions concerning the
non-zenoness of cost. Under stronger conditions
(strictness of constraints) we prove that in case an
optimal strategy exists, we can compute a
state-based winning optimal strategy.}
}
@article{bouyer-fmsd-2004,
publisher = {Kluwer Academic Publishers},
journal = {Formal Methods in System Design},
author = {Bouyer, Patricia},
title = {Forward Analysis of Updatable Timed Automata},
volume = {24},
number = {3},
pages = {281-320},
year = {2004},
month = may,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bou-FMSD2004.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bou-FMSD2004.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Bou-FMSD2004.ps},
doi = {10.1023/B:FORM.0000026093.21513.31},
abstract = {Timed automata are a widely studied
model. Its decidability has been proved using the
so-called region automaton construction. This
construction provides a correct abstraction for
the behaviours of timed automata, but it suffers
from a state explosion and is thus not used in
practice. Instead, algorithms based on the notion
of zones are implemented using adapted data
structures like~DBMs. When we focus on forward
analysis algorithms, the exact computation of all
the successors of the initial configurations does
not always terminate. Thus, some abstractions are
often used to ensure termination, among which, a
widening operator on zones.\par
In this paper, we study in detail this widening
operator and the corresponding forward analysis
algorithm. This algorithm is most used and
implemented in tools like KRONOS and UPPAAL. One
of our main results is that it is hopeless to
find a forward analysis algorithm for general
timed automata, that uses such a widening
operator, and which is correct. This goes really
against what one could think. We then study in
detail this algorithm in the more general
framework of updatable timed automata, a model
which has been introduced as a natural syntactic
extension of classical timed automata. We
describe subclasses of this model for which a
correct widening operator can be found. }
}
@inproceedings{BCM05-fsttcs,
address = {Hyderabad, India},
month = dec,
year = 2005,
volume = 3821,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ramanujam, R. and Sen, Sandeep},
acronym = {{FSTTCS}'05},
booktitle = {{P}roceedings of the 25th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'05)},
author = {Bouyer, Patricia and Chevalier, Fabrice and
Markey, Nicolas},
title = {On the Expressiveness of {TPTL} and~{MTL}},
pages = {432-443},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCM-fsttcs05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCM-fsttcs05.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCM-fsttcs05.ps},
doi = {10.1007/11590156_35},
abstract = {TPTL and MTL are two classical timed extensions of LTL.
In this paper, we positively answer a 15-year-old conjecture that TPTL
is strictly more expressive than MTL. But we show that, surprisingly,
the TPTL formula proposed by Alur and Henzinger for witnessing
this conjecture can be expressed in MTL. More generally, we show that
TPTL formulae using only the F modality can be translated into MTL.}
}
@misc{bouyer-jsi05,
author = {Bouyer, Patricia},
title = {Timed Automata and Extensions: Decidability Limits},
year = 2005,
month = mar,
howpublished = {Invited talk, 5{\`e}mes Journ{\'e}es Syst{\`e}mes Infinis ({JSI}'05),
Cachan, France}
}
@misc{bouyer-games05,
author = {Bouyer, Patricia},
title = {Synthesis of Timed Systems},
year = 2005,
month = mar,
howpublished = {Invited lecture, Spring School on Infinite Games and
Their Applications, Bonn, Germany}
}
@misc{bouyer-gdv05,
author = {Bouyer, Patricia},
title = {Partial Observation of Timed Systems},
year = 2005,
month = jul,
howpublished = {Invited talk, 2nd Workshop on Games in Design and
Verification, Edinburgh, Scotland}
}
@inproceedings{BCD-fossacs05,
address = {Edinburgh, Scotland, UK},
month = apr,
year = 2005,
volume = 3441,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Sassone, Vladimiro},
acronym = {{FoSSaCS}'05},
booktitle = {{P}roceedings of the 8th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'05)},
author = {Bouyer, Patricia and Chevalier, Fabrice and D'Souza, Deepak},
title = {Fault Diagnosis Using Timed Automata},
pages = {219-233},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/fossacs05-BCD.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/fossacs05-BCD.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/fossacs05-BCD.pdf},
doi = {10.1007/b106850},
abstract = {Fault diagnosis consists in
observing behaviours of systems, and in detecting
online whether an error has occurred or not. In the
context of discrete event systems this problem has
been well-studied, but much less work has been done
in the timed framework. In this paper, we consider
the problem of diagnosing faults in behaviours of
timed plants. We focus on the problem of
synthesizing fault diagnosers which are realizable
as deterministic timed automata, with the
motivation that such diagnosers would function as
efficient online fault detectors. We study two
classes of such mechanisms, the class of
deterministic timed automata~(DTA) and the class of
event-recording timed automata~(ERA). We show that
the problem of synthesizing diagnosers in each of
these classes is decidable, provided we are given a
bound on the resources available to the diagnoser.
We prove that under this assumption diagnosability
is 2EXPTIME-complete in the case of DTA's whereas
it becomes PSPACE-complete for ERA's.}
}
@inproceedings{BBBL-concur2005,
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 = {Bel{ }mokadem, Houda and B{\'e}rard, B{\'e}atrice and
Bouyer, Patricia and Laroussinie, Fran{\c{c}}ois},
title = {A New Modality for Almost Everywhere Properties in
Timed Automata},
pages = {110-124},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBL05-concur.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBL05-concur.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBBL05-concur.ps},
doi = {10.1007/11539452_12},
abstract = {The context of this study is timed temporal logics
for timed automata. In this paper, we propose an extension of the
classical logic TCTL with a new Until modality, called {"}Until
almost everywhere{"}. In the extended logic, it is possible, for
instance, to express that a property is true at all positions of
all runs, except on a negligible set of positions. Such
properties are very convenient, for example in the framework of
boolean program verification, where transitions result from
changing variable values. We investigate the expressive power of
this modality and in particular, we prove that it cannot be
expressed with classical TCTL modalities. However, we show that
model-checking the extended logic remains PSPACE-complete as
for~TCTL.}
}
@inproceedings{BCL-concur2005,
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 = {Bouyer, Patricia and Cassez, Franck and Laroussinie,
Fran{\c{c}}ois},
title = {Modal Logics for Timed Control},
pages = {81-94},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCL05-concur.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCL05-concur.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCL05-concur.ps},
doi = {10.1007/11539452_10},
abstract = {In this paper we use the timed
modal logic \(L_{\nu}\) to specify control
objectives for timed plants. We show that the
control problem for a large class of objectives
can be reduced to a model-checking problem for
an extension (\(L_{\nu}^{\mathrm{\small cont}}\))
of the logic \(L_{\nu}\) with a new modality.
\par
More precisely we define a fragment of~\(L_{\nu}\),
namely \(L_{\nu}^{\mathrm{\small det}}\),
such that any control objective
of~\(L_{\nu}^{\mathrm{\small det}}\)
can be translated into an \(L_{\nu}^{\mathrm{\small cont}}\)
formula that holds for the plant if and only if
there is a controller that can enforce the
control objective.
\par
We also show that the new modality
of~\(L_{\nu}^{\mathrm{\small cont}}\)
strictly increases the expressive power
of~\(L_{\nu}\), while model-checking
of~\(L_{\nu}^{\mathrm{\small cont}}\) remains
EXPTIME-complete. }
}
@inproceedings{BLR-formats2005,
address = {Uppsala, Sweden},
month = nov,
year = 2005,
volume = 3829,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Pettersson, Paul and Yi, Wang},
acronym = {{FORMATS}'05},
booktitle = {{P}roceedings of the 3rd {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'05)},
author = {Bouyer, Patricia and Laroussinie, Fran{\c{c}}ois and
Reynier, Pierre-Alain},
title = {Diagonal Constraints in Timed Automata: Forward
Analysis of Timed Systems},
pages = {112-126},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLR05-DBM.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLR05-DBM.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BLR05-DBM.ps},
doi = {10.1007/11603009_10},
abstract = {Timed automata (TA) are a
widely used model for real-time systems. Several
tools are dedicated to this model, and they mostly
implement a forward analysis for checking
reachability properties. Though diagonal
constraints do not add expressive power to
classical~TA, the standard forward analysis
algorithm is not correct for this model. In this
paper we survey several approaches to handle
diagonal constraints and propose a
refinement-based method for patching the usual
algorithm: erroneous traces found by the classical
algorithm are analyzed, and used for refining the
model.}
}
@misc{cortos05,
author = {Bouyer, Patricia and others},
title = {{ACI} {S}{\'e}curit{\'e} {I}nformatique {CORTOS}
<<~{C}ontrol and {O}bservation of {R}eal-{T}ime {O}pen
{S}ystems~>>~--- Rapport {\`a} mi-parcours},
year = 2005,
month = apr,
type = {Contract Report},
note = {6~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/cortos-MP.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/cortos-MP.pdf},
missingdoi = {}
}
@inproceedings{Cortos-MSR05-obs,
address = {Autrans, France},
month = oct,
year = 2005,
publisher = {Herm{\`e}s},
editor = {Alla, Hassane and Rutten, {\'E}ric},
acronym = {{MSR}'05},
booktitle = {{A}ctes du 5{\`e}me {C}olloque sur la
{M}od{\'e}lisation des {S}yst{\`e}mes
{R}{\'e}actifs
({MSR}'05)},
author = {Bouyer, Patricia and Chevalier, Fabrice and Krichen, Moez and
Tripakis, Stavros},
title = {Observation partielle des syst{\`e}mes temporis{\'e}s},
pages = {381-393},
nonote = {Invited paper},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSR05-obs.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSR05-obs.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MSR05-obs.ps},
abstract = {In this paper, we present the partial
observability constraint, which naturally appears when
modeling real-time systems. We have selected three
problems in which this hypothesis is fundamental but
leads to more difficult problems: control of timed
systems, fault diagnosis, and conformance testing. We
describe methods which can be used for solving such
problems. }
}
@inproceedings{Cortos-MSR05-control,
address = {Autrans, France},
month = oct,
year = 2005,
publisher = {Herm{\`e}s},
editor = {Alla, Hassane and Rutten, {\'E}ric},
acronym = {{MSR}'05},
booktitle = {{A}ctes du 5{\`e}me {C}olloque sur la
{M}od{\'e}lisation des {S}yst{\`e}mes
{R}{\'e}actifs
({MSR}'05)},
author = {Altisen, Karine and Bouyer, Patricia and Cachat, Thierry and
Cassez, Franck and Gardey, Guillaume},
title = {Introduction au contr{\^o}le des syst{\`e}mes temps-r{\'e}el},
pages = {367-380},
nonote = {Invited paper},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSR05-control.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSR05-control.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/MSR05-control.ps},
abstract = {In this paper we give a quick overview
of the area of control of real-time systems.}
}
@inproceedings{BLMR-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 = {Bouyer, Patricia and Larsen, Kim G. and Markey, Nicolas and
Rasmussen, Jacob Illum},
title = {Almost Optimal Strategies in One-Clock Priced Timed Automata},
pages = {345-356},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLMR-fsttcs06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLMR-fsttcs06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BLMR-fsttcs06.ps},
doi = {10.1007/11944836_32},
abstract = {We consider timed games extended with cost information, and
prove computability of the optimal cost and of \(\epsilon\)-optimal memoryless
strategies in timed games with one~clock. In~contrast, this problem has
recently been proved undecidable for timed games with three clocks.}
}
@inproceedings{BBBL-atva06,
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 = {Bel{ }mokadem, Houda and B{\'e}rard, B{\'e}atrice and Bouyer, Patricia
and Laroussinie, Fran{\c{c}}ois},
title = {Timed temporal logics for abstracting transient states},
pages = {337-351},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBL-atva06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBL-atva06.pdf},
doi = {10.1007/11901914_26},
abstract = {In previous work, the timed logic TCTL was extended with an
{"}almost everywhere{"} Until modality which abstracts negligible sets of
positions (i.e.,~with a null duration) along a run of a timed automaton.
We~propose here an extension of this logic with more powerful modalities, in
order to specify properties abstracting transient states, which are events
that last for less than k time units. Our main result is that modelchecking
is still decidable and PSPACE-complete for this extension. On the other
hand, a second semantics is defined, in which we consider the total duration
where the property does not hold along a run. In~this case, we prove that
model-checking is undecidable.}
}
@inproceedings{BBC-concur06,
address = {Bonn, Germany},
month = aug,
year = 2006,
volume = 4137,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Baier, Christel and Hermanns, Holger},
acronym = {{CONCUR}'06},
booktitle = {{P}roceedings of the 17th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'06)},
author = {Bouyer, Patricia and Bozzelli, Laura and Chevalier, Fabrice},
title = {Controller Synthesis for {MTL} Specifications},
pages = {450-464},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-concur06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-concur06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBC-concur06.ps},
doi = {10.1007/11817949_30},
abstract = {We consider the control problem for timed automata
against specifications given as MTL formulas. The logic MTL is a
linear-time timed temporal logic which extends LTL with timing
constraints on modalities, and recently, its model-checking has been
proved decidable in several cases. We investigate these decidable
fragments of MTL (full MTL when interpreted over finite timed
words, and SafetyMTL when interpreted over infinite timed words),
and prove two kinds of results. (1)~We first prove that,
contrary to model-checking, the control problem is
undecidable. Roughly, the computation of a lossy channel system
could be encoded as a model-checking problem, and we prove here that
a perfect channel system can be encoded as a control
problem. (2)~We then prove that if we fix the resources
of the controller (by resources we mean clocks and constants that
the controller can use), the control problem becomes decidable. This
decidability result relies on properties of well (and better)
quasi-orderings.}
}
@article{BBLP-STTT05,
publisher = {Springer},
journal = {International Journal on Software Tools
for Technology Transfer},
author = {Behrmann, Gerd and Bouyer, Patricia and Larsen, Kim G.
and Pel{\'a}nek, Radek},
title = {Lower and Upper Bounds in Zone-Based Abstractions of
Timed Automata},
year = 2006,
month = jun,
pages = {204-215},
number = 3,
volume = 8,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBLP-STTT05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBLP-STTT05.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBLP-STTT05.ps},
doi = {10.1007/s10009-005-0190-0},
abstract = {The semantics of timed automata is
defined using an infinite-state transition system.
For verification purposes, one usually uses zone
based abstractions w.r.t.~the maximal constants to
which clocks of the timed automaton are compared.
We show that by distinguishing maximal lower and
upper bounds, significantly coarser abstractions
can be obtained. We show soundness and
completeness of the new abstractions
w.r.t.~reachability. We demonstrate how
information about lower and upper bounds can be
used to optimise the algorithm for bringing a
difference bound matrix into normal form. Finally,
we experimentally demonstrate that the new
techniques dramatically increases the scalability
of the real-time model checker~{\scshape
Uppaal}.}
}
@article{BC06-beatcs,
publisher = {European Association for
Theoretical Computer Science},
journal = {EATCS Bulletin},
author = {Bouyer, Patricia and Chevalier, Fabrice},
title = {On the Control of Timed and Hybrid Systems},
volume = 89,
year = {2006},
month = jun,
pages = {79-96},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC-beatcs89.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC-beatcs89.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BC-beatcs89.ps},
abstract = {In this paper, we survey some of the results which have
been obtained the last ten years on the control of hybrid and timed
systems.}
}
@inproceedings{BBC-lics2006,
address = {Seattle, Washington, USA},
month = aug,
year = 2006,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'06},
booktitle = {{P}roceedings of the 21st
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'06)},
author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and
Chevalier, Fabrice},
title = {Control in o-Minimal Hybrid Systems},
pages = {367-378},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-lics06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-lics06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBC-lics06.ps},
doi = {10.1109/LICS.2006.22},
abstract = {In this paper, we consider
the control of general hybrid systems. In
this context we show that time-abstract
bisimulation is not adequate for solving
such a problem. That is why we consider
an other equivalence, namely the suffix
equivalence based on the encoding of
trajectories through words. We show that
this suffix equivalence is in general a
correct abstraction for control problems.
We apply this result to o-minimal hybrid
systems, and get decidability and
computability results in this framework.}
}
@article{BBM-ipl06,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and
Markey, Nicolas},
title = {Improved Undecidability Results on Weighted Timed
Automata},
year = 2006,
month = jun,
volume = 98,
number = 5,
pages = {188-194},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/IPL-BBM06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/IPL-BBM06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/IPL-BBM06.ps},
doi = {10.1016/j.ipl.2006.01.012},
abstract = {In this paper, we improve two recent undecidability
results of Brihaye, Bruy{\`e}re and Raskin about
weighted timed automata, an extension of timed automata with a
cost variable. Our results rely on a new encoding of the two
counters of a Minsky machine that only require three clocks and
one stopwatch cost, while previous reductions required five clocks
and one stopwatch cost.}
}
@inproceedings{Bouyer-MFPS22,
address = {Genova, Italy},
month = may,
year = 2006,
volume = 158,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Brookes, Steve and Mislove, Michael},
acronym = {{MFPS}'06},
booktitle = {{P}roceedings of the 22nd {C}onference on
{M}athematical {F}oundations of {P}rogramming
{S}emantics ({MFPS}'06)},
author = {Bouyer, Patricia},
title = {Weighted Timed Automata: {M}odel-Checking and Games},
pages = {3-17},
note = {Invited paper},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-mfps06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-mfps06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/bouyer-mfps06.ps},
doi = {10.1016/j.entcs.2006.04.002},
abstract = {In this paper, we present weighted\slash priced
timed automata, an extension of timed automaton with
costs, and solve several interesting problems on that model.}
}
@inproceedings{BHR06-acsd,
address = {Turku, Finland},
month = jun,
year = 2006,
publisher = {{IEEE} Computer Society Press},
editor = {Goossens, Kees and Petrucci, Laure},
acronym = {{ACSD}'06},
booktitle = {{P}roceedings of the 6th {I}nternational
{C}onference on {A}pplication of {C}oncurrency
to {S}ystem {D}esign
({ACSD}'06)},
author = {Bouyer, Patricia and Haddad, Serge and
Reynier, Pierre-Alain},
title = {Extended Timed Automata and Time {P}etri Nets},
pages = {91-100},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-01.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-01.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2006-01.ps},
doi = {10.1109/ACSD.2006.6},
abstract = {Timed Automata (TA) and Time Petri Nets (TPN) are two
well-established formal models for real-time systems. Recently, a
linear transformation of TA to TPNs preserving reachability
properties and timed languages has been proposed, which does however
not extend to larger classes of TA which would allow diagonal
constraints or more general resets of clocks. Though these features
do not add expressiveness, they yield exponentially more concise
models. \par
In this work, we propose two translations: one from extended TA to
TPNs whose size is either linear or quadratic in the size of the
original TA, depending on the features which are allowed; another
one from a parallel composition of TA to TPNs, which is also linear.
As a consequence, we get that TPNs are exponentially more concise
than~TA.}
}
@inproceedings{BHR-ICALP2006,
address = {Venice, Italy},
month = jul,
year = 2006,
volume = 4052,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Buglesi, Michele and Preneel, Bart and Sassone, Vladimiro and Wegener, Ingo},
acronym = {{ICALP}'06},
booktitle = {{P}roceedings of the 33rd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'06)~--- {P}art~{II}},
author = {Bouyer, Patricia and Haddad, Serge and Reynier, Pierre-Alain},
title = {Timed {P}etri Nets and Timed Automata: On the Discriminating Power of
{Z}eno Sequences},
pages = {420-431},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-icalp06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-icalp06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BHR-icalp06.ps},
doi = {10.1007/11787006_36},
abstract = {Timed Petri nets and timed
automata are two standard models for the
analysis of real-time systems. In this
paper, we prove that they are incomparable
for the timed language equivalence. Thus we
propose an extension of timed Petri nets
with read-arcs~(RA-TdPN), whose coverability
problem is decidable. We also show that this
model unifies timed Petri nets and timed
automata. Then, we establish numerous
expressiveness results and prove that Zeno
behaviours discriminate between several
sub-classes of RA-TdPNs. This has surprising
consequences on timed automata,
\emph{e.g.}~on the power of
non-deterministic clock resets.}
}
@inproceedings{BHR-atva06,
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 = {Bouyer, Patricia and Haddad, Serge and Reynier, Pierre-Alain},
title = {Timed Unfoldings for Networks of Timed Automata},
pages = {292-306},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-atva06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-atva06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BHR-atva06.ps},
doi = {10.1007/11901914_23},
abstract = {Whereas partial order methods have proved their efficiency for
the analysis of discrete-event systems, their application to
timed systems remains a challenging research topic. Here, we
design a verification algorithm for networks of timed automata
with invariants. Based on the unfolding technique, our method
produces a branching process as an acyclic Petri net extended
with read arcs. These arcs verify conditions on tokens without
consuming them, thus expressing concurrency between conditions
checks. They are useful for avoiding the explosion of the size
of the unfolding due to clocks which are compared with constants
but not reset. Furthermore, we attach zones to events, in addition
to markings. We~then compute a complete finite prefix of the
unfolding. The~presence of invariants goes against the concurrency
since it entails a global synchronization on time. The use of read
arcs and the analysis of the clock constraints appearing in
invariants will help increasing the concurrency relation between
events. Finally, the finite prefix we compute can be used to decide
reachability properties, and transition enabling.}
}
@incollection{BL-VAT06,
author = {Bouyer, Patricia and Laroussinie, Fran{\c{c}}ois},
title = {V{\'e}rification par automates temporis{\'e}s},
booktitle = {Syst{\`e}mes temps-r{\'e}el~1~: techniques de description
et de v{\'e}rification},
editor = {Navet, Nicolas},
publisher = {Herm{\`e}s},
year = 2006,
month = jun,
pages = {121-150},
url = {http://www.lavoisier.fr/fr/livres/index.asp?texte=2746213030&select=isbn&from=Hermes},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BL-VAT06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BL-VAT06.ps},
isbn = {2-7462-1303-6}
}
@inproceedings{BMR-latin06,
address = {Valdivia, Chile},
month = mar,
year = 2006,
volume = 3887,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Correa, Jose R. and Hevia, Alejandro and Kiwi, Marcos},
acronym = {{LATIN}'06},
booktitle = {{P}roceedings of the 7th {L}atin {A}merican
{S}ymposium on {T}heoretical {I}nformatics
({LATIN}'06)},
author = {Bouyer, Patricia and Markey, Nicolas and Reynier, Pierre-Alain},
title = {Robust Model-Checking of Linear-Time Properties in Timed Automata},
pages = {238-249},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMR-latin06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMR-latin06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BMR-latin06.ps},
doi = {10.1007/11682462_25},
abstract = {Formal verification of timed systems
is well understood, but their
\emph{implementation} is still challenging. Recent
works by Raskin \emph{et al.} have brought out a
model of parameterized timed automata that can be
used to prove \emph{implementability} of timed
systems for safety properties. We define here a
more general notion of robust model-checking for
linear-time properties, which consists in
verifying whether a property still holds even if
the transitions are slightly delayed or expedited.
We provide PSPACE algorithms for the robust
model-checking of B{\"u}chi-like and LTL
properties. We also verify bounded-response-time
properties. }
}
@inproceedings{BMR-fossacs08,
address = {Budapest, Hungary},
month = mar # {-} # apr,
year = 2008,
volume = 4962,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Amadio, Roberto},
acronym = {{FoSSaCS}'08},
booktitle = {{P}roceedings of the 11th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'08)},
author = {Bouyer, Patricia and Markey, Nicolas and Reynier, Pierre-Alain},
title = {Robust Analysis of Timed Automata {\em via} Channel Machines},
pages = {157-171},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMR-fossacs08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMR-fossacs08.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BMR-fossacs08.ps},
doi = {10.1007/978-3-540-78499-9_12},
abstract = {Whereas formal verification of timed systems has become a very
active field of research, the idealised mathematical semantics of timed
automata cannot be faithfully implemented. Several works have thus focused
on a modified semantics of timed automata which ensures implementability,
and robust model-checking algorithms for safety, and later LTL properties
have been designed. Recently, a~new approach has been proposed, which
reduces (standard) model-checking of timed automata to other verification
problems on channel machines. Thanks to a new encoding of the modified
semantics as a network of timed systems, we propose an original
combination of both approaches, and prove that robust model-checking for
coFlat-MTL, a large fragment of~MTL, is EXPSPACE-Complete.}
}
@inproceedings{BMOSW-stacs08,
address = {Bordeaux, France},
month = feb,
year = 2008,
volume = 1,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Albers, Susanne and Weil, Pascal},
acronym = {{STACS}'08},
booktitle = {{P}roceedings of the 25th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'08)},
author = {Bouyer, Patricia and Markey, Nicolas and Ouaknine, Jo{\"e}l
and Schnoebelen, {\relax Ph}ilippe and Worrell, James},
title = {On Termination for Faulty Channel Machines},
pages = {121-132},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bmosw-stacs08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bmosw-stacs08.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/bmosw-stacs08.ps},
abstract = {A channel machine consists of a finite controller together with
several fifo channels; the controller can read messages from the head of a
channel and write messages to the tail of a channel. In this paper, we
focus on channel machines with \emph{insertion errors}, \textit{i.e.},
machines in whose channels messages can spontaneously appear. Such devices
have been previously introduced in the study of Metric Temporal Logic.
We~consider the termination problem: are all the computations of a given
insertion channel machine finite? We~show that this problem has
non-elementary, yet primitive recursive complexity.}
}
@inproceedings{Bouyer-M4M5,
address = {Cachan, France},
month = mar,
year = 2009,
volume = 231,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Areces, Carlos and Demri, St{\'e}phane},
acronym = {{M4M-5}},
booktitle = {{P}roceedings of the 4th
{W}orkshop on {M}ethods for {M}odalities
({M4M-5})},
author = {Bouyer, Patricia},
title = {Model-Checking Timed Temporal Logics},
pages = {323-341},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-M4M5.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-M4M5.pdf},
doi = {10.1016/j.entcs.2009.02.044},
abstract = {In this paper, we present several timed extensions of temporal
logics, that can be used for model-checking real-time
systems. We give different formalisms and the corresponding
decidability/complexity results. We also give intuition to
explain these results.}
}
@article{BHR-ietc07,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Bouyer, Patricia and Haddad, Serge and Reynier, Pierre-Alain},
title = {Timed {P}etri Nets and Timed Automata: On the Discriminating
Power of {Z}eno Sequences},
year = {2008},
month = jan,
volume = 206,
number = 1,
pages = {73-107},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-ic07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-ic07.pdf},
doi = {10.1016/j.ic.2007.10.004},
abstract = {Timed Petri nets and timed automata are two standard models for
the analysis of real-time systems. We~study in this paper their
relationship, and prove in particular that they are incomparable w.r.t.
language equivalence. In~fact, we~study the more general model of timed
Petri nets with read-arcs (RA-TdPN), already introduced in~[Ji{\v{r}}{\'\i}~Srba,
\textit{Timed-arc petri nets vs. networks of timed
automata}, Proc.\ ICATPN'05, LNCS~3536, Springer], which
unifies both models of timed Petri nets and of timed automata, and prove
that the coverability problem remains decidable for this model. Then, we
establish numerous expressiveness results and prove that Zeno behaviours
discriminate between several sub-classes of RA-TdPNs. This has surprising
consequences on timed automata, for~instance on the power of
non-deterministic clock resets.}
}
@inproceedings{BBBBG-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 = {Baier, Christel and Bertrand, Nathalie and Bouyer, Patricia
and Brihaye, {\relax Th}omas and Gr{\"o}{\ss}er, Marcus},
title = {Probabilistic and Topological Semantics for Timed Automata},
pages = {179-191},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBBG-fsttcs07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBBG-fsttcs07.pdf},
doi = {10.1007/978-3-540-77050-3_15},
abstract = {Like most models used in model-checking, timed automata are an
idealized mathematical model used for representing systems with strong
timing requirements. In~such mathematical models, properties can be
violated, due to unlikely (sequences~of) events. We~propose two new
semantics for the satisfaction of LTL formulas, one based on
probabilities, and the other one based on topology, to rule out these
sequences. We~prove that the two semantics are equivalent and lead to a
PSPACE-Complete model-checking problem for LTL over finite executions.}
}
@inproceedings{BM-formats07,
address = {Salzburg, Austria},
month = oct,
year = 2007,
volume = 4763,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Raskin, Jean-Fran{\c{c}}ois and Thiagarajan, P. S.},
acronym = {{FORMATS}'07},
booktitle = {{P}roceedings of the 5th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'07)},
author = {Bouyer, Patricia and Markey, Nicolas},
title = {Costs are Expensive!},
pages = {53-68},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BM-formats07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BM-formats07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BM-formats07.ps},
doi = {10.1007/978-3-540-75454-1_6},
abstract = {We study the model-checking problem for WMTL,
a~cost-extension of the linear-time timed temporal logic MTL, that is
interpreted over weighted timed automata. We~draw a complete picture of
the decidability for that problem: it~is decidable only for the class of
one-clock weighted timed automata with a restricted stopwatch cost, and
any slight extension of this model leads to undecidability. We~finally
give some consequences on the undecidability of linear hybrid automata.}
}
@misc{cortos-final,
author = {Bouyer, Patricia and others},
title = {{ACI} {S}{\'e}curit{\'e} {I}nformatique {CORTOS}~---
Rapport final},
year = 2006,
month = nov,
type = {Contract Report},
note = {17~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Cortos-final.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Cortos-final.pdf}
}
@inproceedings{BMOW-lics07,
address = {Wroc{\l}aw, Poland},
month = jul,
year = 2007,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'07},
booktitle = {{P}roceedings of the 22nd
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'07)},
author = {Bouyer, Patricia and Markey, Nicolas and Ouaknine, Jo{\"e}l and
Worrell, James},
title = {The Cost of Punctuality},
pages = {109-118},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMOW-lics07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMOW-lics07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BMOW-lics07.ps},
doi = {10.1109/LICS.2007.49},
abstract = {In an influential paper titled {"}The Benefits of
Relaxing Punctuality{"}, Alur, Feder, and~Henzinger introduced
Metric Interval Temporal Logic~(MITL) as a fragment of the real-time
logic Metric Temporal Logic~(MTL) in which exact or punctual timing
constraints are banned. Their main result showed that model checking and
satisfiability for~MITL are both EXPSPACE-Complete.\par
Until recently, it was widely believed that admitting even the simplest
punctual specifications in any linear-time temporal logic would
automatically lead to undecidability. Although this was recently
disproved, until now no punctual fragment of~MTL was known to have even
primitive recursive complexity (with certain decidable fragments having
provably non-primitive recursive complexity).\par
In this paper we identify a `co-flat' subset of~MTL that is capable of
expressing a large class of punctual specifications and for which model
checking (although not satisfiability) has no complexity cost over~MITL.
Our logic is moreover qualitatively different from~MITL in that it can
express properties that are not timed-regular. Correspondingly, our
decision procedures do not involve translating formulas into
finite-state automata, but rather into certain kinds of reversal-bounded
Turing machines. Using this translation we show that the model checking
problem for our logic is EXPSPACE-Complete, and is even PSPACE-Complete
if timing constraints are encoded in unary.}
}
@inproceedings{BBC-lfcs2007,
address = {New~York, New~York, USA},
month = jun,
year = 2007,
volume = 4514,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Artemov, Sergei N. and Nerode, Anil},
acronym = {{LFCS}'07},
booktitle = {{P}roceedings of the {S}ymposium on {L}ogical {F}oundations of
{C}omputer {S}cience ({LFCS}'07)},
author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and
Chevalier, Fabrice},
title = {Weighted O-Minimal Hybrid Systems are more
Decidable than Weighted Timed Automata!},
pages = {69-83},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-lfcs07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-lfcs07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBC-lfcs07.ps},
doi = {10.1007/978-3-540-72734-7_6},
abstract = {We consider weighted o-minimal hybrid systems, which
extend classical o-minimal hybrid systems with cost functions. These cost
functions are {"}observer variables{"} which increase while the system evolves
but do not constrain the behaviour of the system. In this paper, we prove
two main results: (i)~optimal o-minimal hybrid games are decidable; (ii)~the
model-checking of~WCTL, an extension of CTL which can constrain the cost
variables, is decidable over that model. This has to be compared with the
same problems in the framework of timed automata where both problems are
undecidable in general, while they are decidable for the restricted class of
one-clock timed automata. }
}
@inproceedings{BLM-fossacs07,
address = {Braga, Portugal},
month = mar,
year = 2007,
volume = 4423,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Seidl, Helmut},
acronym = {{FoSSaCS}'07},
booktitle = {{P}roceedings of the 10th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'07)},
author = {Bouyer, Patricia and Larsen, Kim G. and Markey, Nicolas},
title = {Model-Checking One-Clock Priced Timed Automata},
pages = {108-122},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLM-fossacs07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLM-fossacs07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BLM-fossacs07.ps},
doi = {10.1007/978-3-540-71389-0_9},
abstract = {We consider the model of priced (a.k.a.~weighted) timed
automata, an extension of timed automata with cost information on both
locations and transitions. We prove that model-checking this class of models
against the logic~WCTL, CTL~with cost-constrained modalities, is
PSPACE-complete under the {"}single-clock{"} assumption. In~contrast, it~has been
recently proved that the model-checking problem is undecidable for this model
as soon as the system has three clocks. We also prove that the model-checking
of~WCTL becomes undecidable, even under this {"}single-clock{"} assumption. }
}
@article{BBBR-fmsd06,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and
Bruy{\`e}re, V{\'e}ronique and Raskin, Jean-Fran{\c{c}}ois},
title = {On the optimal reachability problem on weighted timed
automata},
volume = 31,
number = 2,
year = 2007,
month = oct,
pages = {135-175},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBR-FMSD06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBR-FMSD06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBBR-FMSD06.ps},
doi = {10.1007/s10703-007-0035-4},
abstract = {We study the cost-optimal reachability problem for weighted
timed automata such that positive and negative costs are allowed on edges
and locations. By~optimality, we mean an infimum cost as well as a
supremum cost. We show that this problem is PSPACE-complete. Our~proof
uses techniques of linear programming, and thus exploits an important
property of optimal runs : their time-transitions use a time which is
arbitrarily closed to an integer. We~then propose an extension of the
region graph, the weighted discrete graph, whose structure gives light on
the way to solve the cost-optimal reachability problem. We~also give an
application of the cost-optimal reachability problem in the context of
timed games.}
}
@article{BBL-fmsd06,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Bouyer, Patricia and Brinksma, Ed and Larsen, Kim G.},
title = {Optimal Infinite Scheduling for Multi-Priced
Timed Automata},
volume = {32},
number = {1},
pages = {2-23},
year = 2008,
month = feb,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBL-FMSD04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBL-FMSD04.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBL-FMSD04.ps},
doi = {10.1007/s10703-007-0043-4},
abstract = {This paper is concerned with the derivation of infinite
schedules for timed automata that are in some sense optimal. To~cover a wide
class of optimality criteria we start out by introducing an extension of the
(priced) timed automata model that includes both costs and rewards as
separate modelling features. A~precise definition is then given of what
constitutes optimal infinite behaviours for this class of models. We
subsequently show that the derivation of optimal non-terminating schedules
for such double-priced timed automata is computable. This is done by a
reduction of the problem to the determination of optimal mean-cycles in
finite graphs with weighted edges. This reduction is obtained by introducing
the so-called corner-point abstraction, a~powerful abstraction technique
of which we show that it preserves optimal schedules.}
}
@article{BC-JALC2005,
journal = {Journal of Automata, Languages and Combinatorics},
author = {Bouyer, Patricia and Chevalier, Fabrice},
title = {On Conciseness of Extensions of Timed Automata},
year = 2005,
volume = 10,
number = 4,
pages = {393-405},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC05-jalc.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BC05-jalc.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BC05-jalc.ps},
abstract = {In this paper we study conciseness of
various extensions of timed automata, and prove
that several features like diagonal constraints or
updates lead to exponentially more concise timed
models.}
}
@misc{PB-AV2008,
author = {Bouyer, Patricia},
title = {Probabilities in Timed Automata},
year = 2008,
month = aug,
noslides = {},
howpublished = {Invited talk, Workshop {A}utomata and {V}erification
({AV}'08), Mons, Belgium}
}
@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
}
@inproceedings{bbjlr-formats08,
address = {Saint-Malo, France},
month = sep,
year = 2008,
volume = 5215,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Cassez, Franck and Jard, Claude},
acronym = {{FORMATS}'08},
booktitle = {{P}roceedings of the 6th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'08)},
author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and
Jurdzi{\'n}ski, Marcin and Lazi{\'c}, Ranko and
Rutkowski, Micha{\l}},
title = {Average-Price and Reachability-Price Games on Hybrid
Automata with Strong Resets},
pages = {63-77},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bbjlr-formats08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bbjlr-formats08.pdf},
doi = {10.1007/978-3-540-85778-5_6},
abstract = {We introduce and study hybrid automata with strong resets. They
generalize o-minimal hybrid automata, a class of hybrid automata which
allows modeling of complex continuous dynamics. A number of analysis
problems, such as reachability testing and controller synthesis, are
decidable for classes of o-minimal hybrid automata. We generalize existing
decidability results for controller synthesis on hybrid automata and we
establish new ones by proving that average-price and reachability-price
games on hybrid systems with strong resets are decidable, provided that
the structure on which the hybrid automaton is defined has a decidable
first-order theory. Our proof techniques include a novel characterization
of values in games on hybrid systems by optimality equations, and a
definition of a new finitary equivalence relation on the states of a
hybrid system which enables a reduction of games on hybrid systems to
games on finite graphs. }
}
@inproceedings{bflms-formats08,
address = {Saint-Malo, France},
month = sep,
year = 2008,
volume = 5215,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Cassez, Franck and Jard, Claude},
acronym = {{FORMATS}'08},
booktitle = {{P}roceedings of the 6th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'08)},
author = {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim G.
and Markey, Nicolas and Srba, Ji{\v{r}}{\'\i}},
title = {Infinite Runs in Weighted Timed Automata with Energy
Constraints},
pages = {33-47},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFLMS-formats08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFLMS-formats08.pdf},
doi = {10.1007/978-3-540-85778-5_4},
abstract = {We~study the problems of existence and construction of
infinite schedules for finite weighted automata and one-clock weighted
timed automata, subject to boundary constraints on the accumulated
weight. More specifically, we~consider automata equipped with positive
and negative weights on transitions and locations, corresponding to the
production and consumption of some resource (\emph{e.g.}~energy). We~ask the
question whether there exists an infinite path for which the accumulated
weight for any finite prefix satisfies certain constraints (\emph{e.g.}~remains
between~\(0\) and some given upper-bound). We~also consider a game version
of the above, where certain transitions may be uncontrollable.}
}
@inproceedings{BBBM-qest08,
address = {Saint~Malo, France},
month = sep,
year = 2008,
publisher = {{IEEE} Computer Society Press},
acronym = {{QEST}'08},
booktitle = {{P}roceedings of the 5th {I}nternational
{C}onference on {Q}uantitative
{E}valuation of {S}ystems
({QEST}'08)},
author = {Bertrand, Nathalie and Bouyer, Patricia and Brihaye,
{\relax Th}omas and Markey, Nicolas},
title = {Quantitative Model-Checking of One-Clock Timed Automata under
Probabilistic Semantics},
pages = {55-64},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBM-qest08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBBM-qest08.pdf},
doi = {10.1109/QEST.2008.19},
abstract = {In [Baier \emph{et~al.}, \textit{Probabilistic and Topological
Semantics for Timed Automata}, FSTTCS'07] a probabilistic semantics for
timed automata has been defined in order to rule out unlikely (sequences
of) events. The qualitative model-checking problem for LTL properties has
been investigated, where the aim is to check whether a given LTL property
holds with probability~\(1\) in a timed automaton, and solved for the class of
single-clock timed automata.\par
In this paper, we consider the quantitative model-checking problem for
\(\omega\)-regular properties: we aim at computing the exact probability
that a given timed automaton satisfies an \(\omega\)-regular property. We
develop a framework in which we can compute a closed-form expression for
this probability; we furthermore give an approximation algorithm, and
finally prove that we can decide the threshold problem in that
framework.}
}
@article{BLM-lmcs08,
journal = {Logical Methods in Computer Science},
author = {Bouyer, Patricia and Larsen, Kim G. and Markey, Nicolas},
title = {Model Checking One-clock Priced Timed Automata},
volume = 4,
number = {2\string:9},
nopages = {},
month = jun,
year = 2008,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLM-lmcs08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLM-lmcs08.pdf},
doi = {10.2168/LMCS-4(2:9)2008},
abstract = {We consider the model of priced (a.k.a.~weighted) timed automata, an
extension of timed automata with cost information on both locations and
transitions, and we study various model-checking problems for that model
based on extensions of classical temporal logics with cost constraints on
modalities. We prove that, under the assumption that the model has only one
clock, model-checking this class of models against the logic~WCTL, CTL
with cost-constrained modalities, is PSPACE-complete (while it has been
shown undecidable as soon as the model has three clocks).
We~also prove that model checking WMTL (LTL with cost-constrained
modalities) is decidable only if there is a single clock in the model and a
single stopwatch cost variable (\textit{i.e.}, whose slopes lie
in~\(\{0,1\}\)).}
}
@inproceedings{BMOW-icalp08,
address = {Reykjavik, Iceland},
month = jul,
year = 2008,
volume = 5126,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Aceto, Luca and Damg{\aa}rd, Ivan and
Goldberg, Leslie~Ann and Halld{\'o}rsson, Magn{\'u}s M.
and Ing{\'o}lfsd{\'o}ttir, Anna and Walukiewicz, Igor},
acronym = {{ICALP}'08},
booktitle = {{P}roceedings of the 35th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'08)~-- {P}art~{II}},
author = {Bouyer, Patricia and Markey, Nicolas and Ouaknine, Jo{\"e}l
and Worrell, James},
title = {On Expressiveness and Complexity in Real-time Model Checking},
pages = {124-135},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMOW-icalp08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMOW-icalp08.pdf},
doi = {10.1007/978-3-540-70583-3_11},
abstract = {Metric Interval Temporal Logic (MITL) is a popular formalism for
expressing real-time specifications. This logic achieves decidability by
restricting the precision of timing constraints, in particular, by banning
so-called \emph{punctual} specifications. In~this paper we~introduce a
significantly more expressive logic that can express a wide variety of
punctual specifications, but whose model-checking problem has the same
complexity as that of~MITL. We~conclude that for model checking the most
commonly occurring specifications, such as invariance and bounded
response, punctuality can be accommodated at no cost.}
}
@inproceedings{poti-TFIT2008,
address = {Taipei, Taiwan},
month = mar,
year = 2008,
editor = {Kuo, Tei-Wei and Cruz-Lara, Samuel},
acronym = {{TFIT}'08},
booktitle = {{P}roceedings of the 4th {T}aiwanese-{F}rench
{C}onference on {I}nformation {T}echnology ({TFIT}'08)},
author = {Bouyer, Patricia},
title = {Model-Checking Timed Temporal Logics},
pages = {132-142},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bouyer-tfit08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Bouyer-tfit08.pdf},
abstract = {In this paper, we~present several timed extensions of
temporal logics, that can be used for model-checking real-time
systems. We~give different formalisms and the corresponding
decidability\slash complexity results. We also give intuition
to explain these results.}
}
@misc{bouyer-cortos06,
author = {Bouyer, Patricia},
title = {Weighted Timed Automata: Model-Checking and Games},
year = {2005},
month = aug,
howpublished = {Invited talk, Workshop CORTOS'06, Bonn, Germany}
}
@misc{bouyer-avocs05,
author = {Bouyer, Patricia},
title = {Optimal Timed Games},
year = {2005},
month = sep,
howpublished = {Invited talk, 5th {I}nternational {W}orkshop
on {A}utomated {V}erification of {C}ritical {S}ystems
({AVoCS}'05), Warwick, UK}
}
@misc{bouyer-infinity05,
author = {Bouyer, Patricia},
title = {Optimal Reachability Timed Games},
year = {2005},
month = aug,
howpublished = {Invited talk, 7th {I}nternational {W}orkshop
on {V}erification of {I}nfinite {S}tate {S}ystems
({INFINITY}'05), San Francisco, USA}
}
@misc{bouyer-fac04,
author = {Bouyer, Patricia},
title = {Automates temporis{\'e}s, de la th{\'e}orie {\`a} l'impl{\'e}mentation},
year = {2004},
month = mar,
howpublished = {Invited talk, Journ\'ees Formalisation des Activit?s
Concurrentes (FAC'04), Toulouse, France}
}
@inproceedings{bouyer-etr05,
address = {Nancy, France},
month = sep,
year = 2005,
noeditor = {},
acronym = {{ETR}'05},
booktitle = {{A}ctes de la 4{\`e}me {\'E}cole {T}emps-{R}{\'e}el ({ETR}'05)},
author = {Bouyer, Patricia},
title = {An Introduction to Timed Automata},
pages = {111-123},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-etr05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-etr05.pdf}
}
@inproceedings{bouyer-artist2-05,
author = {Bouyer, Patricia},
title = {Foundations of Timed Systems},
booktitle = {Proc. of the ARTIST2 Summer School on Component \&
Modelling, Testing \& Verification, and Statical Analysis of Embedded
Systems},
address = {N{\"a}sslingen, Sweden},
month = sep # {-} # oct,
year = {2005},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-nasslingen.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-nasslingen.pdf}
}
@incollection{BL-litron08,
author = {Bouyer, Patricia and Laroussinie, Fran{\c{c}}ois},
title = {Model Checking Timed Automata},
booktitle = {Modeling and Verification of Real-Time Systems},
editor = {Merz, Stephan and Navet, Nicolas},
year = {2008},
month = jan,
pages = {111-140},
publisher = {ISTE Ltd. -- John Wiley \& Sons, Ltd.},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BL-litron08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BL-litron08.pdf}
}
@inproceedings{BFLM-hscc10,
address = {Stockholm, Sweden},
month = apr,
year = 2010,
publisher = {ACM Press},
editor = {Johansson, Karl Henrik and Yi, Wang},
acronym = {{HSCC}'10},
booktitle = {{P}roceedings of the 13th {I}nternational {C}onference
on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
({HSCC}'10)},
author = {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim G.
and Markey, Nicolas},
title = {Timed Automata with Observers under Energy Constraints},
pages = {61-70},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLM-hscc10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLM-hscc10.pdf},
doi = {10.1145/1755952.1755963},
abstract = {In this paper, we study one-clock priced timed automata in which
prices can grow linearly (\(\frac{dp}{dt}=k\)) or exponentially
(\(\frac{dp}{dt}=kp\)), with discontinuous updates on edges. We propose
EXPTIME algorithms to decide the existence of controllers that ensure
existence of infinite runs or reachability of some goal location with
non-negative observer value all along the run. These algorithms consist in
computing the optimal delays that should be elapsed in each location along
a run, so that the final observer value is maximized (and never goes below
zero).}
}
@article{bbc09-lmcs,
journal = {Logical Methods in Computer Science},
author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and Chevalier, Fabrice},
title = {O-Minimal Hybrid Reachability Games},
year = 2010,
month = jan,
volume = 6,
number = {1:1},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBC-lmcs09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBC-lmcs09.pdf},
doi = {10.2168/LMCS-6(1:1)2010},
abstract = {In this paper, we consider reachability games over general
hybrid systems, and distinguish between two possible observation
frameworks for those games: either the precise dynamics of the system is
seen by the players (this is the perfect observation framework), or only
the starting point and the delays are known by the players (this is the
partial observation framework). In the first more classical framework, we
show that time-abstract bisimulation is not adequate for solving this
problem, although it is sufficient in the case of timed automata. That is
why we consider an other equivalence, namely the suffix equivalence based on
the encoding of tra jectories through words. We show that this suffix
equivalence is in general a correct abstraction for games. We apply this
result to o-minimal hybrid systems, and get decidability and computability
results in this framework. For the second framework which assumes a
partial observation of the dynamics of the system, we propose another
abstraction, called the superword encoding, which is suitable to solve the
games under that assumption. In that framework, we also provide
decidability and computability results.}
}
@article{BCM-icomp2009,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Bouyer, Patricia and Chevalier, Fabrice and Markey, Nicolas},
title = {On the Expressiveness of {TPTL} and~{MTL}},
volume = {208},
number = 2,
pages = {97-116},
month = feb,
year = 2010,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCM-icomp09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCM-icomp09.pdf},
doi = {10.1016/j.ic.2009.10.004},
abstract = {TPTL and MTL are two classical timed extensions of~LTL. In~this
paper, we prove the 20-year-old conjecture that TPTL is strictly more
expressive than~MTL. But we show that, surprisingly, the TPTL~formula
proposed by Alur and Henzinger for witnessing this conjecture \emph{can}
be expressed in~MTL. More generally, we show that TPTL formulae using only
modality~F can be translated into~MTL.}
}
@article{BBC-apal09,
publisher = {Elsevier Science Publishers},
journal = {Annals of Pure and Applied Logics},
author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and
Chevalier, Fabrice},
title = {Weighted O-Minimal Hybrid Systems},
year = {2009},
month = dec,
volume = {161},
number = {3},
pages = {268-288},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-apal09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBC-apal09.pdf},
doi = {10.1016/j.apal.2009.07.014},
abstract = {We consider weighted o-minimal hybrid systems, which extend
classical o-minimal hybrid systems with cost functions. These cost
functions are 'observer variables' which increase while the system evolves
but do not constrain the behaviour of the system. In this paper, we prove
two main results: (i)~optimal o-minimal hybrid games are decidable;
(ii)~the~model-checking of~WCTL, an~extension of CTL which can constrain
the cost variables, is decidable over that model. This has to be compared
with the same problems in the framework of timed automata where both
problems are undecidable in general, while they are decidable for the
restricted class of one-clock timed automata.}
}
@inproceedings{BDMR-concur09,
address = {Bologna, Italy},
month = sep,
year = 2009,
volume = 5710,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Bravetti, Mario and Zavattaro, Gianluigi},
acronym = {{CONCUR}'09},
booktitle = {{P}roceedings of the 20th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'09)},
author = {Bouyer, Patricia and Duflot, Marie and Markey, Nicolas and
Renault, Gabriel},
title = {Measuring Permissivity in Finite Games},
pages = {196-210},
doi = {10.1007/978-3-642-04081-8_14},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDMR-concur09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDMR-concur09.pdf},
abstract = {In this paper, we extend the classical notion of strategies in
turn-based finite games by allowing several moves to be selected.
We~define and study a quantitative measure for permissivity of such
strategies by assigning penalties when blocking transitions. We~prove that
for reachability objectives, most permissive strategies exist, can be
chosen memoryless, and can be computed in polynomial time, while it is in
\(\textsf{NP}\cap\textsf{coNP}\) for discounted and mean penalties.}
}
@misc{dots-1.2a,
author = {Bouyer, Patricia and Laroussinie, Fran{\c{c}}ois and
Lime, Didier and Markey, Nicolas},
title = {Synthesis of timed controllers},
howpublished = {Deliverable DOTS~1.2a (ANR-06-SETI-003)},
year = 2009,
month = mar
}
@inproceedings{BF-icalp09,
address = {Rhodes, Greece},
month = jul,
year = 2009,
volume = 5556,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Albers, Susanne and Marchetti-Spaccamela, Alberto and
Matias, Yossi and Thomas, Wolfgang},
acronym = {{ICALP}'09},
booktitle = {{P}roceedings of the 36th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'09)},
author = {Bouyer, Patricia and Forejt, Vojt{\v e}ch},
title = {Reachability in Stochastic Timed Games},
pages = {103-114},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BF-icalp09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BF-icalp09.pdf},
doi = {10.1007/978-3-642-02930-1_9},
abstract = {We define stochastic timed games, which extend two-player timed
games with probabilities (following a recent approach by Baier
\textit{et~al.}), and which extend in a natural way continuous-time Markov
decision processes. We~focus on the reachability problem for these games,
and ask whether one of the players has a strategy to ensure that the
probability of reaching a fixed set of states is equal~to (or~below,
resp.~above) a~certain number~\(r\), whatever the second player does.
We~show that the problem is undecidable in general, but that it becomes
decidable if we restrict to single-clock 1\(\frac{1}{2}\)-player games and
ask whether the player can ensure that the probability of reaching the set
is~\(=1\) (or~\(>0\),~\(=0\)).}
}
@article{BHR-fi09,
publisher = {{IOS} Press},
journal = {Fundamenta Informaticae},
author = {Bouyer, Patricia and Haddad, Serge and Reynier, Pierre-Alain},
title = {Undecidability Results for Timed Automata with Silent
Transitions},
year = 2009,
volume = 92,
number = {1-2},
pages = {1-25},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-12.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-12.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2007-12.ps},
abstract = {In this work, we study decision problems related to timed
automata with silent transitions (TA-epsilon) which strictly extend the
expressiveness of timed automata~(TA). First, we answer negatively a
central question raised by the introduction of silent transitions: can we
decide whether the language recognized by a TA-epsilon can be recognized
by some TA? Then we establish in the framework of TA-epsilon some old open
conjectures that O.~Finkel has recently solved for~TA. Its proofs follow a
generic scheme which relies on the fact that only a finite number of
configurations can be reached by a TA while reading a timed word. This
property does not hold for TA-epsilon, the proofs in the framework of
TA-epsilon thus require more elaborated arguments. We~establish
undecidability of complementability, minimization of the number of clocks,
and closure under shuffle. We~also show these results in the framework of
infinite timed languages.}
}
@misc{Quasimodo-3.1,
author = {Bouyer, Patricia and Katoen, Joost-Pieter and
Langerak, Rom and Laroussinie, Fran{\c{c}}ois and
Markey, Nicolas and Raskin, Jean-Fran{\c{c}}ois},
title = {Transfer of correctness from models to implementation},
howpublished = {Deliverable QUASIMODO~3.1 (ICT-FP7-STREP-214755)},
year = 2009,
month = jan
}
@phdthesis{bouyer-hab2009,
author = {Bouyer, Patricia},
title = {From Qualitative to Quantitative Analysis of Timed Systems},
school = {Universit{\'e} Paris~7, Paris, France},
type = {M{\'e}moire d'habilitation},
year = 2009,
month = jan,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PB-hdr09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/PB-hdr09.pdf}
}
@incollection{BP-pct08,
futureaddress = {},
month = jan,
year = 2009,
series = {IARCS-Universities},
publisher = {Universities Press},
booktitle = {Perspectives in Concurrency Theory},
editor = {Lodaya, Kamal and Mukund, Madhavan and
Ramanujam, R.},
author = {Bouyer, Patricia and Petit, Antoine},
title = {On extensions of timed automata},
pages = {35-63},
abstract = {Since their definition in the early nineties, timed automata have
been one of the most used and widely studied models for
representing and analyzing real-time systems. In their seminal
paper, Alur and Dill proved the probably most important property
of timed automata: checking emptiness of the language accepted by
a timed automaton, or equivalently checking a reachability
property in a timed automaton, is decidable. This result relies on
the construction of the so-called region automaton, which
abstracts behaviours of a timed automaton into behaviours of a
finite automaton. Since then, symbolic algorithms have been
developed to solve that problem, several model-checkers have been
implemented, and numerous case studies have been verified.\par
Lots of works have naturally aimed at proposing extensions of
timed automata with new features, while preserving the
above-mentioned fundamental decidability result. The motivation
for these extensions is basically twofold. First it can increase the
expressiveness of timed automata, allowing to model larger classes
of systems. Then it can improve the conciseness (and hence the
readability) of models by constructing more compact
representations for a given system.\par
In this paper, we discuss and compare some of the most important
extensions of timed automata that have been considered in the
literature.}
}
@inproceedings{HBMOW-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 = {Hunter, Paul and Bouyer, Patricia and Markey, Nicolas and
Ouaknine, Jo{\"e}l and Worrell, James},
title = {Computing rational radical sums in uniform \(\textsf{TC}^{0}\)},
pages = {308-316},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HBMOW-fsttcs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HBMOW-fsttcs10.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2010.308},
abstract = {A~fundamental problem in numerical computation and computational
geometry is to determine the sign of arithmetic expressions in radicals.
Here we consider the simpler problem of deciding whether \(\sum_{i=1}^m
C_i \cdot A_i^{X_i}\) is zero for given rational numbers~\(A_i\),
\(C_i\),~\(X_i\). It~has been known for almost twenty years that this can
be decided in polynomial time. In this paper we improve this result by
showing membership in uniform \(\textsf{TC}^0\). This requires several
significant departures from Bl{\"o}mer's polynomial-time algorithm as the
latter crucially relies on primitives, such as gcd computation and binary
search, that are not known to be in~\(\textsf{TC}^0\).}
}
@inproceedings{BBM-concur10,
address = {Paris, France},
month = aug # {-} # sep,
year = 2010,
volume = {6269},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Gastin, Paul and Laroussinie, Fran{\c{c}}ois},
acronym = {{CONCUR}'10},
booktitle = {{P}roceedings of the 21st
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'10)},
author = {Bouyer, Patricia and Brenguier, Romain and Markey, Nicolas},
title = {{N}ash Equilibria for Reachability Objectives in Multi-player Timed Games},
pages = {192-206},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBM-concur10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBM-concur10.pdf},
doi = {10.1007/978-3-642-15375-4_14},
abstract = {We propose a procedure for computing Nash equilibria in
multi-player timed games with reachability objectives. Our procedure is
based on the construction of a finite concurrent game, and on a generic
characterization of Nash equilibria in (possibly infinite) concurrent
games. Along the way, we~use our characterization to compute Nash
equilibria in finite concurrent games.}
}
@inproceedings{BBM-formats10,
address = {Vienna, Austria},
month = sep,
year = 2010,
volume = {6246},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Chatterjee, Krishnendu and Henziner, Thomas A.},
acronym = {{FORMATS}'10},
booktitle = {{P}roceedings of the 8th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'10)},
author = {Bouyer, Patricia and Brenguier, Romain and Markey, Nicolas},
title = {Computing Equilibria in Two-Player Timed Games {\textit{via}}~Turn-Based
Finite Games},
pages = {62-76},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBM-formats10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBM-formats10.pdf},
doi = {10.1007/978-3-642-15297-9_7},
abstract = {We study two-player timed games where the objectives of the two
players are not opposite. We focus on the standard notion of Nash
equilibrium and propose a series of transformations that builds two finite
turn-based games out of a timed game, with a precise correspondence
between Nash equilibria in the original and in final games. This provides
us with an algorithm to compute Nash equilibria in two-player timed games
for large classes of properties.}
}
@article{BCL-jlli10,
publisher = {Kluwer Academic Publishers},
journal = {Journal of Logic, Language and Information},
author = {Bouyer, Patricia and Cassez, Franck and Laroussinie,
Fran{\c{c}}ois},
title = {Timed Modal Logics for Real-Time Systems: Specification,
Verification and Control},
volume = 20,
number = 2,
pages = {169-203},
year = 2011,
month = apr,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCL-jlli10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCL-jlli10.pdf},
doi = {10.1007/s10849-010-9127-4},
abstract = {In this paper, a timed modal logic~\(L_{c}\) is presented for
the specification and verification of real-time systems.
Several important results for~\(L_{c}\) are discussed. First
we address the model checking problem and we show that it is
an EXPTIME-complete problem. Secondly we consider
expressiveness and we explain how to express strong timed
bisimilarity and how to build characteristic formulas for
timed automata. We also propose a compositional algorithm
for~\(L_{c}\) model checking. Finally we consider several
control problems for which \(L_{c}\) can be used to check
controllability.}
}
@inproceedings{BBMU-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 = {Bouyer, Patricia and Brenguier, Romain and Markey, Nicolas and Ummels, Michael},
title = {Concurrent games with ordered objectives},
pages = {301-315},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBMU-fossacs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBMU-fossacs12.pdf},
doi = {10.1007/978-3-642-28729-9_20},
abstract = {We consider concurrent games played on graphs, in which each
player has several qualitative (e.g. reachability or B{\"u}chi)
objectives, and a preorder on these objectives (for instance the counting
order, where the aim is to maximise the number of objectives that are
fulfilled).\par
We study two fundamental problems in that setting: (1)~the \emph{value
problem}, which aims at deciding the existence of a strategy that ensures
a given payoff; (2)~the \emph{Nash equilibrium problem}, where we want to
decide the existence of a Nash equilibrium (possibly with a condition on
the payoffs). We characterise the exact complexities of these problems for
several relevant preorders, and several kinds of objectives.}
}
@inproceedings{SBM-fsttcs11,
address = {Mumbai, India},
month = dec,
year = 2011,
volume = 13,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chakraborty, Supratik and Kumar, Amit},
acronym = {{FSTTCS}'11},
booktitle = {{P}roceedings of the 31st {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'11)},
author = {Sankur, Ocan and Bouyer, Patricia and Markey, Nicolas},
title = {Shrinking Timed Automata},
pages = {90-102},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SBM-fsttcs11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SBM-fsttcs11.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2011.90},
abstract = {We define and study a new approach to the implementability
of timed automata, where the semantics is perturbed by imprecisions and
finite frequency of the hardware. In order to circumvent these effects, we
introduce \emph{parametric shrinking} of clock constraints, which
corresponds to tightening the guards. We propose symbolic procedures to
decide the existence of (and then compute) parameters under which the
shrunk version of a given timed automaton is non-blocking and can
time-abstract simulate the exact semantics. We then define an
implementation semantics for timed automata with a digital clock and
positive reaction times, and show that for shrinkable timed automata both
properties are preserved in implementation.}
}
@inproceedings{BBMU-fsttcs11,
address = {Mumbai, India},
month = dec,
year = 2011,
volume = 13,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chakraborty, Supratik and Kumar, Amit},
acronym = {{FSTTCS}'11},
booktitle = {{P}roceedings of the 31st {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'11)},
author = {Bouyer, Patricia and Brenguier, Romain and Markey, Nicolas
and Ummels, Michael},
title = {{N}ash Equilibria in Concurrent Games with {B}{\"u}chi Objectives},
pages = {375-386},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBMU-fsttcs11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBMU-fsttcs11.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2011.375},
abstract = {We study the problem of the existence (and computation) of Nash
equilibria in multi-player concurrent games with B{\"u}chi-definable
objectives. First, when the objectives are B{\"u}chi conditions on the
game, we prove that the existence problem can be solved in polynomial
time. In a second part, we extend our technique to objectives defined by
deterministic B{\"u}chi automata, and prove that the problem then becomes
EXPTIME-complete. We prove PSPACE-completeness for the case where the
B{\"u}chi automata are 1-weak.}
}
@inproceedings{BMS-formats11,
address = {Aalborg, Denmark},
month = sep,
year = 2011,
volume = 6919,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Fahrenberg, Uli and Tripakis, Stavros},
acronym = {{FORMATS}'11},
booktitle = {{P}roceedings of the 9th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'11)},
author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan},
title = {Robust Model-Checking of Timed Automata via Pumping in
Channel Machines},
pages = {97-112},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-formats11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-formats11.pdf},
doi = {10.1007/978-3-642-24310-3_8},
abstract = {Timed automata are governed by a mathematical semantics which
assumes perfectly continuous and precise clocks. This requirement is not
satised by digital hardware on which the models are implemented. In~fact,
it~was shown that the presence of imprecisions, however small they may be,
may yield extra behaviours. Therefore correctness proven on the formal
model does not imply correctness of the real system.\par
The problem of robust model-checking was then dened to circumvent this
inconsistency. It consists in computing a bound on the imprecision under
which the system will be correct.\par
In this work, we show that robust model-checking against
\(\omega\)-regular properties for timed automata can be reduced to
standard model-checking of timed automata, by computing an adequate bound
on the imprecision. This yields a new algorithm for robust model-checking
of \(\omega\)-regular properties, which is both optimal and valid for
general timed automata.}
}
@inproceedings{BMOU-atva11,
address = {Taipei, Taiwan},
month = oct,
year = {2011},
volume = 6996,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Bultan, Tevfik and Hsiung, Pao-Ann},
acronym = {{ATVA}'11},
booktitle = {{P}roceedings of the 9th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'11)},
author = {Bouyer, Patricia and Markey, Nicolas and Olschewski, J{\"o}rg
and Ummels, Michael},
title = {Measuring Permissiveness in Parity Games: Mean-Payoff
Parity Games Revisited},
pages = {135-149},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMOU-atva11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMOU-atva11.pdf},
doi = {10.1007/978-3-642-24372-1_11},
abstract = {We study nondeterministic strategies in parity games with the
aim of computing a most permissive winning strategy. Following earlier
work, we measure permissiveness in terms of the average
number{\slash}weight of transitions blocked by a strategy. Using a
translation into mean-payoff parity games, we prove that deciding (the
permissiveness~of) a~most permissive winning strategy is in
\(\textsf{NP}\cap\textsf{coNP}\). Along the way, we~provide a new study of
mean-payoff parity games. In particular, we give a new algorithm for
solving these games, which beats all previously known algorithms for this
problem.}
}
@inproceedings{BLMST-concur11,
address = {Aachen, Germany},
month = sep,
year = 2011,
volume = 6901,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Katoen, Joost-Pieter and K{\"o}nig, Barbara},
acronym = {{CONCUR}'11},
booktitle = {{P}roceedings of the 22nd
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'11)},
author = {Bouyer, Patricia and Larsen, Kim~G. and Markey, Nicolas and
Sankur, Ocan and Thrane, Claus},
title = {Timed automata can always be made implementable},
pages = {76-91},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BLMST-concur11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BLMST-concur11.pdf},
doi = {10.1007/978-3-642-23217-6_6},
abstract = {Timed automata follow a mathematical semantics, which
assumes perfect precision and synchrony of
clocks. Since this hypothesis does not hold in
digital systems, properties proven formally on a
timed automaton may be lost at implementation. In
order to ensure implementability, several approaches
have been considered, corresponding to different
hypotheses on the implementation platform. We
address two of these: a~timed automaton is samplable
if its semantics is preserved under a discretization
of time; it is robust if its semantics is preserved
when all timing constraints are relaxed by some
small positive parameter. We propose a construction
which makes timed automata implementable in the
above sense: From any timed automaton~\(\mathcal{A}\),
we build a timed automaton~\(\mathcal{A}'\) that
exhibits the same behaviour as~\(\mathcal{A}\), and
moreover is both robust and samplable by
construction.}
}
@inproceedings{BBBS-icalp11,
address = {Z{\"u}rich, Switzerland},
month = jul,
year = 2011,
volume = 6756,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Aceto, Luca and Henzinger, Monika and Sgall, Jir{\'\i}},
acronym = {{ICALP}'11},
booktitle = {{P}roceedings of the 38th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'11)~-- {P}art~{II}},
author = {Bertrand, Nathalie and Bouyer, Patricia and Brihaye, {\relax
Th}omas and Stainer, Am{\'e}lie},
title = {Emptiness and Universality Problems in Timed Automata with Positive Frequency},
pages = {246-257},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBS-icalp11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBS-icalp11.pdf},
doi = {10.1007/978-3-642-22012-8_19},
abstract = {The languages of infinite timed words accepted by timed automata
are traditionally dened using B{\"u}chi-like conditions. These acceptance
conditions focus on the set of locations visited infinitely often along a
run, but completely ignore quantitative timing aspects. In this paper we
propose a natural quantitative semantics for timed automata based on the
so-called frequency, which measures the proportion of time spent in the
accepting locations. We study various properties of timed languages
accepted with positive frequency, and in particular the emptiness and
universality problems.}
}
@article{BFLM-cacm11,
publisher = {ACM Press},
journal = {Communications of the~{ACM}},
author = {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim~G. and
Markey, Nicolas},
title = {Quantitative analysis of real-time systems
using priced timed automata},
volume = 54,
number = 9,
month = sep,
pages = {78-87},
year = 2011,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLM-cacm11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLM-cacm11.pdf},
doi = {10.1145/1995376.1995396},
abstract = {The problems of time-dependent behavior in general, and dynamic
resource allocation in particular, pervade many aspects of modern life.
Prominent examples range from reliability and efficient use of
communication resources in a telecommunication network to the allocation
of tracks in a continental railway network, from scheduling the usage of
computational resources on a chip for durations of nano-seconds to the
weekly, monthly, or longer-range reactive planning in a factory or a
supply chain.}
}
@misc{impro-D2.1,
author = {Akshay, S. and B{\'e}rard, B{\'e}atrice and Bouyer, Patricia
and Haar, Stefan and Haddad, Serge and Jard, Claude and
Lime, Didier and Markey, Nicolas and Reynier, Pierre-Alain
and Sankur, Ocan and Thierry-Mieg, Yann},
title = {Overview of Robustness in Timed Systems},
howpublished = {Deliverable ImpRo D~2.1 (ANR-2010-BLAN-0317)},
year = 2012,
month = jan,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d21.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d21.pdf}
}
@inproceedings{BBJM-qest12,
address = {London, UK},
month = sep,
year = 2012,
publisher = {{IEEE} Computer Society Press},
acronym = {{QEST}'12},
booktitle = {{P}roceedings of the 9th {I}nternational
{C}onference on {Q}uantitative
{E}valuation of {S}ystems
({QEST}'12)},
author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and
Jurdzi{\'n}ski, Marcin and Menet, Quentin},
title = {Almost-Sure Model-Checking of Reactive Timed Automata},
pages = {138-147},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBJM-qest12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBJM-qest12.pdf},
doi = {10.1109/QEST.2012.10},
abstract = {We consider the model of stochastic timed automata, a model in
which both delays and discrete choices are made probabilistically. We are
interested in the almost-sure model-checking problem, which asks whether
the automaton satisfies a given property with probability~\(1\). While
this problem was shown decidable for single-clock automata few years ago,
it was also proven that the algorithm for this decidability result could
not be used for general timed automata. In this paper we describe the
subclass of reactive timed automata, and we prove decidability of the
almost-sure model-checking problem under that restriction. Decidability
relies on the fact that this model is almost-surely fair. As a desirable
property of real systems, we show that reactive automata are almost-surely
non-Zeno. Finally we show that the almost-sure model-checking problem can
be decided for specifications given as deterministic timed automata.}
}
@inproceedings{BLM-qest12,
address = {London, UK},
month = sep,
year = 2012,
publisher = {{IEEE} Computer Society Press},
acronym = {{QEST}'12},
booktitle = {{P}roceedings of the 9th {I}nternational
{C}onference on {Q}uantitative
{E}valuation of {S}ystems
({QEST}'12)},
author = {Bouyer, Patricia and Larsen, Kim G. and Markey, Nicolas},
title = {Lower-Bound Constrained Runs in Weighted Timed Automata},
pages = {128-137},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BLM-qest12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BLM-qest12.pdf},
doi = {10.1109/QEST.2012.28},
noontract = {},
abstract = {We investigate a number of problems related to infinite runs of
weighted timed automata, subject to lower-bound constraints on the
accumulated weight. Closing an open problem from [Bouyer \textit{et~al.},
{"}Infinite runs in weighted timed automata with energy constraints{"},
FORMATS'08], we show that the existence of an infinite
lower-bound-constrained run is---for us somewhat
unexpectedly---undecidable for weighted timed automata with four or more
clocks.\par
This undecidability result assumes a fixed and know initial credit. We
show that the related problem of existence of an initial credit for which
there ex- ist a feasible run is decidable in PSPACE. We also investigate
the variant of these problems where only bounded-duration runs are
considered, showing that this restriction makes our original problem
decidable in NEXPTIME. Finally, we prove that the universal versions of
all those problems (i.e, checking that all the considered runs satisfy the
lower-bound constraint) are decidable in PSPACE.}
}
@article{BMOSW-fac12,
publisher = {Springer},
journal = {Formal Aspects of Computing},
author = {Bouyer, Patricia and Markey, Nicolas and Ouaknine, Jo{\"e}l
and Schnoebelen, {\relax Ph}ilippe and Worrell, James},
title = {On Termination and Invariance for Faulty Channel Systems},
year = 2012,
month = jul,
volume = 24,
number = {4-6},
pages = {595-607},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMOSU-fac12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMOSU-fac12.pdf},
doi = {10.1007/s00165-012-0234-7},
abstract = {A~\emph{channel machine} consists of a finite controller
together with several fifo channels; the controller can read messages from
the head of a channel and write messages to the tail of a channel. In this
paper we focus on channel machines with \emph{insertion errors}, i.e.,
machines in whose channels messages can spontaneously appear. We consider
the invariance problem: does a given insertion channel machine have an
infinite computation all of whose configurations satisfy a given
predicate? We show that this problem is primitive-recursive if the
predicate is closed under message losses. We also give a non-elementary
lower bound for the invariance problem under this restriction. Finally,
using the previous result, we show that the satisfiability problem for the
safety fragment of Metric Temporal Logic is non-elementary.}
}
@inproceedings{BMS-icalp12,
address = {Warwick, UK},
month = jul,
year = 2012,
volume = {7392},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Czumaj, Artur and Mehlhorn, Kurt and Pitts, Andrew and Wattenhofer, Roger},
acronym = {{ICALP}'12},
booktitle = {{P}roceedings of the 39th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'12)~-- {P}art~{II}},
author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan},
title = {Robust Reachability in Timed Automata: A~Game-based
Approach},
pages = {128-140},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-icalp12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-icalp12.pdf},
doi = {10.1007/978-3-642-31585-5_15},
abstract = {Reachability checking is one of the most basic problems in
verification. By solving this problem, one synthesizes a strategy that
dictates the actions to be performed for ensuring that the target location
is reached. In this work, we are interested in synthesizing {"}robust{"}
strategies for ensuring reachability of a location in a timed automaton;
with {"}robust{"}, we mean that it must still ensure reachability even
when the delays are perturbed by the environment. We model this perturbed
semantics as a game between the controller and its environment, and solve
the parameterized robust reachability problem: we show that the existence
of an upper bound on the perturbations under which there is a strategy
reaching a target location is EXPTIME-complete.}
}
@misc{impro-D31,
author = {B{\'e}rard, B{\'e}atrice and Bouyer, Patricia and Larsen, Kim G. and
Markey, Nicolas and Mullins, John and Sankur, Ocan and Sassolas,
Mathieu and Thrane, Claus},
title = {Measuring the robustness},
howpublished = {Deliverable ImpRo~3.1, (ANR-10-BLAN-0317)},
month = jan,
year = {2013},
note = {59~pages},
type = {Contract Report},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d31.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d31.pdf}
}
@misc{impro-D51,
author = {Bouyer, Patricia and Faucou, S{\'e}bastien and Haar, Stefan and
Jovanivi{\'c}, Aleksandra and Lime, Didier and Markey, Nicolas and
Roux, Olivier H. and Sankur, Ocan},
title = {Control tasks for Timed System; Robustness issues},
howpublished = {Deliverable ImpRo~5.1, (ANR-10-BLAN-0317)},
month = jan,
year = {2013},
note = {34~pages},
type = {Contract Report},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d51.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/impro-d51.pdf}
}
@inproceedings{BMS-rp13,
address = {Uppsala, Sweden},
month = sep,
year = 2013,
volume = {8169},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abdulla, Parosh Aziz and Potapov, Igor},
acronym = {{RP}'13},
booktitle = {{P}roceedings of the 7th {W}orkshop
on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'13)},
author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan},
title = {Robustness in timed automata},
pages = {1-18},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-rp13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-rp13.pdf},
doi = {10.1007/978-3-642-41036-9_1},
abstract = {In this paper we survey several approaches to the robustness of
timed automata, that~is, the ability of a system to resist to slight
perturbations or errors. We will concentrate on robustness against timing
errors which can be due to measuring errors, imprecise clocks, and
unexpected runtime behaviors such as execution times that are longer or
shorter than expected.\par
We consider the perturbation model of guard enlargement and formulate
several robust verification problems that have been studied recently,
including robustness analysis, robust implementation, and robust control.}
}
@inproceedings{BMS-formats13,
address = {Buenos Aires, Argentina},
month = aug,
year = 2013,
volume = 8053,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Braberman, V{\'\i}ctor and Fribourg, Laurent},
acronym = {{FORMATS}'13},
booktitle = {{P}roceedings of the 11th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'13)},
author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan},
title = {Robust Weighted Timed Automata and Games},
pages = {31-46},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-formats13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-formats13.pdf},
doi = {10.1007/978-3-642-40229-6_3},
abstract = {Weighted timed automata extend timed automata with cost
variables that can be used to model the evolution of various quantities.
Although cost-optimal reachability is decidable (in polynomial space) on
this model, it becomes undecidable on weighted timed games. This paper
studies cost-optimal reachability problems on weighted timed automata and
games under robust semantics. More precisely, we consider two perturbation
game semantics that introduce imprecisions in the standard semantics, and
bring robustness properties w.r.t. timing imprecisions to controllers. We
give a polynomial-space algorithm for weighted timed automata, and prove
the undecidability of cost-optimal reachability on weighted timed games,
showing that the problem is robustly undecidable.}
}
@inproceedings{SBMR-concur13,
address = {Buenos Aires, Argentina},
month = aug,
year = 2013,
volume = 8052,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {D'Argenio, Pedro R. and Melgratti, Hern{\'a}n)},
acronym = {{CONCUR}'13},
booktitle = {{P}roceedings of the 24th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'13)},
author = {Sankur, Ocan and Bouyer, Patricia and Markey, Nicolas and
Reynier, Pierre-Alain},
title = {Robust Controller Synthesis in Timed Automata},
pages = {546-560},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SBMR-concur13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SBMR-concur13.pdf},
doi = {10.1007/978-3-642-40184-8_38},
abstract = {We consider the fundamental problem of B{\"u}chi acceptance in
timed automata in a robust setting. The problem is formalised in terms of
controller synthesis: timed automata are equipped with a parametrised
game-based semantics that models the possible perturbations of the
decisions taken by the controller. We characterise timed automata that are
robustly controllable for some parameter, with a simple graph theoretic
condition, by showing the equivalence with the existence of an aperiodic
lasso that satisfies the winning condition (aperiodicity was defined and
used earlier in different contexts to characterise convergence phenomena
in timed automata). We then show decidability and PSPACE-completeness of
our problem.}
}
@inproceedings{BMS-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 = {Bouyer, Patricia and Markey, Nicolas and Stan, Daniel},
title = {Mixed {N}ash Equilibria in Concurrent Games},
pages = {351-363},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-fsttcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-fsttcs14.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2014.351},
abstract = {We study mixed-strategy Nash equilibria in multiplayer
deterministic concurrent games played on graphs, with terminal-reward
payoffs (that is, absorbing states with a value for each player). We show
undecidability of the existence of a constrained Nash equilibrium (the
constraint requiring that one player should have maximal payoff), with
only three players and 0/1-rewards (i.e., reachability objectives). This
has to be compared with the undecidability result by Ummels and Wojtczak
for turn-based games which requires 14 players and general rewards. Our
proof has various interesting consequences: (i)~the~undecidability of the
existence of a Nash equilibrium with a constraint on the social welfare;
(ii)~the~undecidability of the existence of an (unconstrained) Nash
equilibrium in concurrent games with terminal-reward payoffs.}
}
@article{BBBMBGJ-lmcs14,
journal = {Logical Methods in Computer Science},
author = {Bertrand, Nathalie and Bouyer, Patricia and Brihaye,
{\relax Th}omas and Menet, Quentin and Baier, Christel and
Gr{\"o}{\ss}er, Marcus and Jurdzi{\'n}ski, Marcin},
title = {Stochastic Timed Automata},
volume = 10,
number = {4:6},
nopages = {},
month = dec,
year = 2014,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBMBGJ-mfcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBMBGJ-mfcs14.pdf},
doi = {10.2168/LMCS-10(4:6)2014},
abstract = {A~stochastic timed automaton is a purely stochastic process
defined on a timed automaton, in which both delays and discrete choices
are made randomly. We study the almost-sure model-checking problem for
this model, that is, given a stochastic timed automaton~\(\mathcal{A}\)
and a property~\(\varphi\), we want to decide whether \(\mathcal{A}\)
satisfies~\(\varphi\) with probability~\(1\). In this paper, we identify
several classes of automata and of properties for which this can be
decided. The proof relies on the construction of a finite abstraction,
called the thick graph, that we interpret as a finite Markov chain, and
for which we can decide the almost-sure model-checking problem.
Correctness of the abstraction holds when automata are almost-surely fair,
which we show, is the case for two large classes of systems, single-clock
automata and so-called weak-reactive automata. Techniques employed in this
article gather tools from real-time verification and probabilistic
verification, as well as topological games played on timed automata.}
}
@article{BMS-tcs14,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan},
title = {Robust Reachability in Timed Automata and Games: A~Game-based Approach},
volume = 563,
year = {2015},
month = jan,
pages = {43-74},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-tcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-tcs14.pdf},
doi = {10.1016/j.tcs.2014.08.014 },
abstract = {Reachability checking is one of the most basic problems in
verification. By solving this problem in a game, one can synthesize a
strategy that dictates the actions to be performed for ensuring that the
target location is reached. In this work, we are interested in
synthesizing {"}robust{"} strategies for ensuring reachability of a location
in timed automata. By robust, we mean that it must still ensure
reachability even when the delays are perturbed by the environment. We
model this perturbed semantics as a game between the controller and its
environment, and solve the parameterized robust reachability problem: we
show that the existence of an upper bound on the perturbations under which
there is a strategy reaching a target location is EXPTIME-complete. We
also extend our algorithm, with the same complexity, to turn-based timed
games, where the successor state is entirely determined by the environment
in some locations.}
}
@inproceedings{BGM-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 = {Bouyer, Patricia and Gardy, Patrick and Markey, Nicolas},
title = {Quantitative verification of weighted {K}ripke structures},
pages = {64-80},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-atva14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-atva14.pdf},
doi = {10.1007/978-3-319-11936-6_6},
abstract = {Extending formal verification techniques to handle quantitative
aspects, both for the models and for the properties to be checked, has
become a central research topic over the last twenty years. Following
several recent works, we study model checking for (one-dimensional)
weighted Kripke structures with positive and negative weights, and
temporal logics constraining the total and/or average weight. We prove
decidability when only accumulated weight is constrained, while allowing
average-weight constraints alone already is undecidable.}
}
@inproceedings{BMM-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 = {Bouyer, Patricia and Markey, Nicolas and Matteplackel,
Raj~Mohan},
title = {Averaging in~{LTL}},
pages = {266-280},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMM-concur14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMM-concur14.pdf},
doi = {10.1007/978-3-662-44584-6_19},
abstract = {For the accurate analysis of computerized systems, powerful
quantitative formalisms have been designed, together with efficient
verification algorithms. However, verification has mostly remained
boolean---either a property is~true, or it~is false. We~believe that this
is too crude in a context where quantitative information and constraints
are crucial: correctness should be quantified!\par In a recent line of
works, several authors have proposed quantitative semantics for temporal
logics, using e.g. \emph{discounting} modalities (which give less
importance to distant events). In~the present paper, we define and study a
quantitative semantics of~LTL with \emph{averaging} modalities, either on
the long run or within an until modality. This, in a way, relaxes the
classical Boolean semantics of~LTL, and provides a measure of certain
properties of a model. We~prove that computing and even approximating the
value of a formula in this logic is undecidable.}
}
@article{BBMU-lmcs14,
journal = {Logical Methods in Computer Science},
author = {Bouyer, Patricia and Brenguier, Romain and Markey, Nicolas
and Ummels, Michael},
title = {Pure {N}ash Equilibria in Concurrent Games},
volume = {11},
number = {2:9},
nopages = {},
month = jun,
year = 2015,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBMU-lmcs15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBMU-lmcs15.pdf},
doi = {10.2168/LMCS-11(2:9)2015},
abstract = {We study pure-strategy Nash equilibria in multiplayer concurrent
games, for a variety of omega-regular objectives. For simple objectives
(e.g. reachability, B{\"u}chi objectives), we transform the problem of
deciding the existence of a Nash equilibrium in a given concurrent game
into that of deciding the existence of a winning strategy in a turn-based
two-player game (with a refined objective). We use that transformation to
design algorithms for computing Nash equilibria, which in most cases have
optimal worst-case complexity. For automata-defined objectives, we extend
the above algorithms using a simulation relation which allows us to
consider the product of the game with the automata defining the
objectives. Building on previous algorithms for simple qualitative
objectives, we define and study a semi-quantitative framework, where all
players have several boolean objectives equipped with a preorder; a player
may for instance want to satisfy all her objectives, or to maximise the
number of objectives that she achieves. In most cases, we prove that the
algorithms we obtain match the complexity of the problem they address.}
}
@inproceedings{BMV-sr14,
address = {Grenoble, France},
month = apr,
year = 2014,
volume = 146,
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Mogavero, Fabio and Murano, Aniello},
acronym = {{SR}'14},
booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {S}trategic
{R}easoning ({SR}'14)},
author = {Bouyer, Patricia and Markey, Nicolas and Vester, Steen},
title = {Nash Equilibria in Symmetric Games with Partial Observation},
pages = {49-55},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMV-sr14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMV-sr14.pdf},
doi = {10.4204/EPTCS.146.7},
abstract = {We investigate a model for representing large multiplayer games,
which satisfy strong symmetry properties. This model is made of multiple
copies of an arena; each player plays in his own arena, and can partially
observe what the other players do. Therefore, this game has partial
information and symmetry constraints, which make the computation of Nash
equilibria difficult. We show several undecidability results, and for
bounded-memory strategies, we precisely characterize the complexity of
computing pure Nash equilibria (for qualitative objectives) in this game
model.}
}
@article{SBM-ic14,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Sankur, Ocan and Bouyer, Patricia and Markey, Nicolas},
title = {Shrinking Timed Automata},
volume = 234,
month = feb,
year = 2014,
pages = {107-132},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SBM-ic14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SBM-ic14.pdf},
doi = {10.1016/j.ic.2014.01.002},
abstract = {We define and study a new approach to the implementability of
timed automata, where the semantics is perturbed by imprecisions and
finite frequency of the hardware. In order to circumvent these effects, we
introduce \emph{parametric shrinking} of clock constraints, which
corresponds to tightening the guards. We propose symbolic procedures to
decide the existence of (and then compute) parameters under which the
shrunk version of a given timed automaton is non-blocking and can
time-abstract simulate the exact semantics. We then define an
implementation semantics for timed automata with a digital clock and
positive reaction times, and show that for shrinkable timed automata,
non-blockingness and time-abstract simulation are preserved in
implementation.}
}
@article{BLM-peva13,
publisher = {Elsevier Science Publishers},
journal = {Performance Evaluation},
author = {Bouyer, Patricia and Larsen, Kim G. and Markey, Nicolas},
title = {Lower-Bound Constrained Runs in Weighted Timed Automata},
volume = 73,
month = mar,
year = 2014,
pages = {91-109},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BLM-peva13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BLM-peva13.pdf},
doi = { 10.1016/j.peva.2013.11.002},
abstract = {We investigate a number of problems related to infinite runs of
weighted timed automata (with a single weight variable), subject to
lower-bound constraints on the accumulated weight. Closing an open problem
from an earlier paper, we show that the existence of an infinite
lower-bound-constrained run is--for us somewhat unexpectedly--undecidable
for weighted timed automata with four or more clocks.\par
This undecidability result assumes a fixed and known initial credit. We
show that the related problem of existence of an initial credit for which
there exists a feasible run is decidable in PSPACE. We also investigate
the variant of these problems where only bounded-duration runs are
considered, showing that this restriction makes our original problem
decidable in NEXPTIME. We prove that the universal versions of all those
problems (i.e, checking that all the considered runs satisfy the
lower-bound constraint) are decidable in PSPACE.\par
Finally, we extend this study to multi-weighted timed automata: the
existence of a feasible run becomes undecidable even for bounded duration,
but the existence of initial credits remains decidable (in~PSPACE).}
}
@article{BGM-ipl15,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Bouyer, Patricia and Gardy, Patrick and Markey, Nicolas},
title = {On~the semantics of Strategy Logic},
volume = {116},
number = {2},
pages = {75-79},
month = feb,
year = {2016},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-ipl15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-ipl15.pdf},
doi = {10.1016/j.ipl.2015.10.004},
abstract = {We define and study a slight variation on the semantics of
Strategy Logic: while in the classical semantics, all strategies are
shifted during the evaluation of temporal modalities, we propose to only
shift the strategies that have been assigned to a player, thus matching
the intuition that we can assign the very same strategy to the players at
different points in time. We prove that surprisingly, this renders the
model-checking problem undecidable.}
}
@inproceedings{BGM-fsttcs15,
address = {Bangalore, India},
month = dec,
year = 2015,
volume = {45},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Harsha, Prahladh and Ramalingam, G.},
acronym = {{FSTTCS}'15},
booktitle = {{P}roceedings of the 35th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'15)},
author = {Bouyer, Patricia and Gardy, Patrick and Markey, Nicolas},
title = {Weighted strategy logic with boolean goals over one-counter games},
pages = {69-83},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-fsttcs15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-fsttcs15.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2015.69},
abstract = {Strategy Logic is a powerful specification language for
expressing non-zero-sum properties of multi-player games. SL conveniently
extends the logic ATL with explicit quantification and assignment of
strategies. In this paper, we consider games over one-counter automata,
and a quantitative extension 1cSL of SL with assertions over the value of
the counter. We prove two results: we first show that, if decidable, model
checking the so-called Boolean-goal fragment of 1cSL has non-elementary
complexity; we actually prove the result for the Boolean-goal fragment of
SL over finite-state games, which was an open question in (Mogavero
\emph{et~al.} Reasoning about strategies: On the model-checking problem.
2014). As a first step towards proving decidability, we then show that the
Boolean-goal fragment of 1cSL over one-counter games enjoys a nice
periodicity property.}
}
@inproceedings{ncma2015-bou,
address = {Porto, Portugal},
month = aug,
year = 2015,
volume = 318,
series = {books@ocg.at},
publisher = {Austrian Computer Society},
editor = {Freund, Rudolf and Holzer, Markus and Moreira, Nelma and Reis, Rog{\'e}rio},
acronym = {{NCMA}'15},
booktitle = {{P}roceedings of the 7th {W}orkshop on {N}on-{C}lassical {M}odels
of {A}utomata and {A}pplications ({NCMA}'15)},
author = {Bouyer, Patricia},
title = {On the optimal reachability problem in weighted timed automata and
games},
pages = {11-36},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ncma15-bou.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ncma15-bou.pdf},
abstract = {In these notes, we survey works made on the models of weighted
timed automata and games, and more specifically on the optimal
reachability problem.}
}
@inproceedings{BFM-avocs15,
address = {Edinburgh, UK},
month = sep,
year = {2015},
volume = 72,
series = {Electronic Communications of the EASST},
publisher = {European Association of Software Science and Technology},
editor = {Grov, Gudmund and Ireland, Andrew},
acronym = {{AVoCS}'15},
booktitle = {{P}roceedings of the 15th {I}nternational
{W}orkshop on {A}utomated {V}erification
of {C}ritical {S}ystems
({AVoCS}'15)},
author = {Bouyer, Patricia and Fang, Erwin and Markey, Nicolas},
title = {Permissive strategies in timed automata and games},
nopages = {263-277},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFM-avocs15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFM-avocs15.pdf},
doi = {10.14279/tuj.eceasst.72.1015},
abstract = {Timed automata are a convenient framework for modelling and
reasoning about real-time systems. While these models are now very
well-understood, they do not offer a convenient way of taking timing
imprecisions into account. Several solutions (e.g. parametric guard
enlargement) have recently been proposed over the last ten years to take
such imprecisions into account. In this paper, we propose a new approach
for handling robust reachability, based on permissive strategies. While
classical strategies propose to play an action at an exact point in time,
permissive strategies return an interval of possible dates when to play
the selected action. With such a permissive strategy, we associate a
penalty, which is the inverse of the length of the proposed interval, and
accumulates along the run. We show that in that setting, optimal
strategies can be computed in polynomial time for one-clock timed
automata.}
}
@inproceedings{BMRLL-gandalf15,
address = {Genova, Italy},
month = sep,
year = 2015,
volume = {193},
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Esparza, Javier and Tronci, Enrico},
acronym = {{GandALF}'15},
booktitle = {{P}roceedings of the 6th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification
({GandALF}'15)},
author = {Bouyer, Patricia and Markey, Nicolas and Randour, Mickael
and Larsen, Kim G. and Laursen, Simon},
title = {Average-energy games},
pages = {1-15},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMRLL-gandalf15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMRLL-gandalf15.pdf},
doi = {10.4204/EPTCS.193.1},
abstract = {Two-player quantitative zero-sum games provide a natural
framework to synthesize controllers with performance guarantees for
reactive systems within an uncontrollable environment. Classical settings
include mean-payoff games, where the objective is to optimize the long-run
average gain per action, and energy games, where the system has to avoid
running out of energy.\par
We study \emph{average-energy} games, where the goal is to optimize the
long-run average of the accumulated energy. We show that this objective
arises naturally in several applications, and that it yields interesting
connections with previous concepts in the literature. We prove that
deciding the winner in such games is in
\textsf{NP}{{\(\cap\)}}\textsf{coNP} and at least as hard as solving
mean-payoff games, and we establish that memoryless strategies suffice to
win. We also consider the case where the system has to minimize the
average-energy while maintaining the accumulated energy within predefined
bounds at all times: this corresponds to operating with a finite-capacity
storage for energy. We give results for one-player and two-player games,
and establish complexity bounds and memory requirements.}
}
@inproceedings{BMPS-formats15,
address = {Madrid, Spain},
month = sep,
year = 2015,
volume = {9268},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Sankaranarayanan, Sriram and Vicario, Enrico},
acronym = {{FORMATS}'15},
booktitle = {{P}roceedings of the 13th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'15)},
author = {Bouyer, Patricia and Markey, Nicolas and Perrin, Nicolas
and Schlehuber, Philipp},
title = {Timed automata abstraction of switched dynamical systems
using control funnels},
pages = {60-75},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMPS-formats15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMPS-formats15.pdf},
doi = {10.1007/978-3-319-22975-1_5},
abstract = {The~development of formal methods for control design is an
important challenge with potential applications in a wide range of
safety-critical cyber-physical systems. Focusing on switched dynamical
systems, we~propose a new abstraction, based on time-varying regions of
invariance (the~\emph{control funnels}), that models behaviors of systems as
timed automata. The main advantage of this method is that it allows
automated verification of formal specifications and reactive controller
synthesis without discretizing the evolution of the state of the system.
Efficient constructions are possible in the case of linear dynamics.
We~demonstrate the potential of our approach with two examples.}
}
@inproceedings{BJM-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 = {Bouyer, Patricia and Jaziri, Samy and Markey, Nicolas},
title = {On~the Value Problem in Weighted Timed Games},
pages = {311-324},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BJM-concur15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BJM-concur15.pdf},
doi = {10.4230/LIPIcs.CONCUR.2015.311},
abstract = {A~weighted timed game is a timed game with extra quantitative
information representing e.g. energy consumption. Optimizing the cost for
reaching a target is a natural question, which has been investigated for
ten years. Existence of optimal strategies is known to be undecidable in
general, and only very restricted classes of games have been described for
which optimal cost and almost-optimal strategies can be computed.\par
In this paper, we show that the value problem is undecidable in general
weighted timed games. The undecidability proof relies on that for the
existence of optimal strategies and on a diagonalization construction
recently designed in the context of quantitative temporal logics. We then
provide an algorithm to compute arbitrary approximations of the value in a
game, and almost-optimal strategies. The algorithm applies in a large
subclass of weighted timed games, and is the first approximation scheme
which is designed in the current context.}
}
@inproceedings{BJ-fossacs17,
address = {Uppsala, Sweden},
month = apr,
year = 2017,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Esparza, Javier and Murawski, Andrzej},
acronym = {{FoSSaCS}'17},
booktitle = {{P}roceedings of the 20th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'17)},
author = {Bouyer, Patricia and Jug{\'e}, Vincent},
title = {Dynamic Complexity of the {D}yck Reachability},
pages = {265-280},
url = {https://arxiv.org/abs/1610.07499},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BJ-fossacs17.pdf},
doi = {10.1007/978-3-662-54458-7_16},
abstract = {Dynamic complexity is concerned with updating the output of a problem when the input is slightly changed. We study the dynamic complexity of Dyck reachability problems in directed and undirected graphs, where updates may add or delete edges. We show a strong dichotomy between such problems, based on the size of the Dyck alphabet. Some of them are P-complete (under a strong notion of reduction) while the others lie either in DynFO or in NL.}
}
@inproceedings{BHMRZ-fossacs17,
address = {Uppsala, Sweden},
month = apr,
year = 2017,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Esparza, Javier and Murawski, Andrzej},
acronym = {{FoSSaCS}'17},
booktitle = {{P}roceedings of the 20th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'17)},
author = {Bouyer, Patricia and Hofman, Piotr and Markey, Nicolas and Randour, Mickael and Zimmermann, Martin},
title = {Bounding Average-energy Games},
pages = {179-195},
url = {https://arxiv.org/abs/1610.07858},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHMRZ-fossacs17.pdf},
doi = {10.1007/978-3-662-54458-7_11},
abstract = {We consider average-energy games, where the goal is to minimize the long-run average of the accumulated energy. Decidability of average-energy games with a lower-bound constraint on the energy level (but no upper bound) is an open problem; in particular, there is no known upper bound on the memory that is required for winning strategies.
By reducing average-energy games with lower-bounded energy to infinite-state mean-payoff games and analyzing the frequency of low-energy configurations, we show an almost tight doubly-exponential upper bound on the necessary memory, and that the winner of average-energy games with lower-bounded energy can be determined in doubly-exponential time. We also prove EXPSPACE-hardness of this problem.
Finally, we consider multi-dimensional extensions of all types of average-energy games: without bounds, with only a lower bound, and with both a lower and an upper bound on the energy. We show that the fully-bounded version is the only case to remain decidable in multiple dimensions.}
}
@article{BMPS-rts16,
publisher = {Kluwer Academic Publishers},
journal = {Real-Time Systems},
author = {Bouyer, Patricia and Markey, Nicolas and Perrin,
Nicolas and Schlehuber{-}Caissier, Philipp},
title = {Timed automata abstraction of switched dynamical
systems using control funnels},
volume = {53},
number = {3},
year = {2017},
pages = {327-353},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMPS-rts16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMPS-rts16.pdf},
doi = {10.1007/s11241-016-9262-3},
abstract = {The development of formal methods for control design
is an important challenge with potential
applications in a wide range of safety-critical
cyber-physical systems. Focusing on switched
dynamical systems, we propose a new abstraction,
based on time-varying regions of invariance (control
funnels), that models behaviors of systems as timed
automata. The~main advantage of this method is that
it allows for the automated verification and
reactive controller synthesis without discretizing
the evolution of the state of the system. Efficient
and analytic constructions are possible in the case
of linear dynamics whereas bounding funnels with
conjectured properties based on numerical
simulations can be used for general nonlinear
dynamics. We~demonstrate the potential of our
approach with three examples.}
}
@incollection{BFLMOW-hmc18,
author = {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim G.
and Markey, Nicolas and Ouaknine, Jo{\"e}l and
Worrell, James},
title = {Model Checking Real-Time Systems},
booktitle = {Handbook of Model Checking},
editor = {Clarke, Ed and Henzinger, Tom and Veith, Helmut},
publisher = {Springer},
year = 2018,
pages = {1001-1046},
nochapter = {29},
doi = {10.1007/978-3-319-10575-8_29},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLMOW-hmc17.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLMOW-hmc17.pdf},
isbn = {978-3-319-10574-1},
abstract = {This chapter surveys timed automata as a formalism for
model checking real-time systems. We begin with introducing the
model, as an extension of finite-state automata with real-valued
variables for measuring time. We then present the main
model-checking results in this framework, and give a hint about some
recent extensions (namely weighted timed automata and timed
games).}
}
@inproceedings{BMS-gandalf16,
address = {Catania, Italy},
month = sep,
year = 2016,
volume = {226},
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Cantone, Domenico and Delzanno, Giorgio},
acronym = {{GandALF}'16},
booktitle = {{P}roceedings of the 7th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification
({GandALF}'16)},
author = {Bouyer, Patricia and Markey, Nicolas and Stan, Daniel},
title = {Stochastic Equilibria under Imprecise Deviations in
Terminal-Reward Concurrent Games},
pages = {61-75},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-gandalf16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-gandalf16.pdf},
doi = {10.4204/EPTCS.226.5},
abstract = {We study the existence of mixed-strategy equilibria in
concurrent games played on graphs. While existence is guaranteed
with safety objectives for each player, Nash equilibria need not
exist when players are given arbitrary terminal-reward objectives,
and their existence is undecidable with qualitative reachability
objectives (and~only three players). However, these results rely on
the fact that the players can enforce infinite plays while trying to
improve their payoffs. In this paper, we introduce a relaxed notion
of equilibria, where deviations are imprecise. We prove that
contrary to Nash equilibria, such (stationary) equilibria always
exist, and we develop a PSPACE algorithm to compute one.}
}
@article{BMRLL-acta16,
publisher = {Springer},
journal = {Acta Informatica},
author = {Bouyer, Patricia and Markey, Nicolas and Randour, Mickael
and Larsen, Kim G. and Laursen, Simon},
title = {Average-energy games},
volume = {55},
number = {2},
year = 2018,
month = jul,
pages = {91-127},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMRLL-acta16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMRLL-acta16.pdf},
doi = {10.1007/s00236-016-0274-1},
abstract = {Two-player quantitative zero-sum games provide a natural
framework to synthesize controllers with performance guarantees for
reactive systems within an uncontrollable environment. Classical
settings include mean-payoff games, where the objective is to
optimize the long-run average gain per action, and energy games,
where the system has to avoid running out of energy. We study
average-energy games, where the goal is to optimize the long-run
average of the accumulated energy. We show that this objective
arises naturally in several applications, and that it yields
interesting connections with previous concepts in the literature. We
prove that deciding the winner in such games is in NP coNP and at
least as hard as solving mean-payoff games, and we establish that
memoryless strategies suffice to win. We also consider the case
where the system has to minimize the average-energy while
maintaining the accumulated energy within predefined bounds at all
times: this corresponds to operating with a finite-capacity storage
for energy. We give results for one-player and two-player games, and
establish complexity bounds and memory requirements.}
}
@inproceedings{Bouyer-mfcs16,
address = {Krakow, Poland},
month = aug,
year = 2016,
volume = {58},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
acronym = {{MFCS}'16},
booktitle = {{P}roceedings of the 41st
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'16)},
author = {Bouyer, Patricia},
title = {Optimal Reachability in Weighted Timed Automata and Games},
pages = {3:1-3:3},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/bouyer-mfcs16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bouyer-mfcs16.pdf},
doi = {10.4230/LIPIcs.MFCS.2016.3},
abstract = {This is an overview of the invited talk delivered at the 41st International Symposium on Math- ematical Foundations of Computer Science (MFCS-2016).}
}
@inproceedings{ABKMT-mfcs16,
address = {Krakow, Poland},
month = aug,
year = 2016,
volume = {58},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
acronym = {{MFCS}'16},
booktitle = {{P}roceedings of the 41st
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'16)},
author = {Akshay, S. and Bouyer, Patricia and Krishna, Shankara Narayanan and
Manasa, Lakshmi and Trivedi, Ashutosh },
title = {Stochastic Timed Games Revisited},
pages = {8:1-8:14},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABKMT-mfcs16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABKMT-mfcs16.pdf},
doi = {10.4230/LIPIcs.MFCS.2016.8},
abstract = {Stochastic timed games (STGs), introduced by Bouyer and Forejt,
naturally generalize both continuous-time Markov chains and timed automata
by providing a partition of the locations between those controlled by two
players (Player Box and Player Diamond) with competing objectives and
those governed by stochastic laws. Depending on the number of
players---2,~1, or~0---subclasses of stochastic timed games are often
classified as \(2\frac{1}{2}\)-player, \(1\frac{1}{2}\)-player, and
\(\frac{1}{2}\)-player games where the \(\frac{1}{2}\) symbolizes the
presence of the stochastic {"}nature{"} player. For STGs with reachability
objectives it is known that \(1\frac{1}{2}\)-player one-clock STGs are
decidable for qualitative objectives, and that \(2\frac{1}{2}\)-player
three-clock STGs are undecidable for quantitative reachability objectives.
This paper further refines the gap in this decidability spectrum. We show
that quantitative reachability objectives are already undecidable for
\(1\frac{1}{2}\)-player four-clock STGs, and even under the time-bounded
restriction for \(2\frac{1}{2}\)-player five-clock~STGs. We~also obtain a
class of \(1\frac{1}{2}\), \(2\frac{1}{2}\)-player STGs for which the
quantitative reachability problem is decidable.}
}
@inproceedings{BBCM-csr16,
address = {St~Petersburg, Russia},
month = jun,
year = 2016,
volume = {9691},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Gerhard J. Woeginger},
acronym = {{CSR}'16},
booktitle = {{P}roceedings of the 11th {I}nternational {C}omputer {S}cience
{S}ymposium in {R}ussia ({CSR}'16)},
author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and Carlier,
Pierre
and Menet, Quentin},
title = {Compositional Design of Stochastic Timed Automata},
pages = {117-130},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBCM-csr16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBCM-csr16.pdf},
doi = {10.1007/978-3-319-34171-2_9},
abstract = {In this paper, we study the model of stochastic timed automata
and we target the definition of adequate composition operators that will
allow a compositional approach to the design of stochastic systems with
hard real-time constraints. This paper achieves the first step towards
that goal. Firstly, we define a parallel composition operator that
(we~prove) corresponds to the interleaving semantics for that model; we
give conditions over probability distributions, which ensure that the
operator is well-defined; and we exhibit problematic behaviours when this
condition is not satisfied. We furthermore identify a large and natural
subclass which is closed under parallel composition. Secondly, we define
a bisimulation notion which naturally extends that for continuous-time
Markov chains. Finally, we importantly show that the defined bisimulation
is a congruence w.r.t. the parallel composition, which is an expected
property for a proper modular approach to system design.}
}
@inproceedings{BBBC-icalp16,
address = {Rome, Italy},
month = jul,
year = 2016,
volume = {55},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chatzigiannakis, Ioannis and Mitzenmacher,
Michael and Rabani, Yuval and Sangiorgi, Davide},
acronym = {{ICALP}'16},
booktitle = {{P}roceedings of the 43rd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'16)},
author = {Bertrand, Nathalie and Bouyer, Patricia and Brihaye,
{\relax Th}omas
and Carlier, Pierre},
title = {Analysing Decisive Stochastic Processes},
pages = {101:1-101:14},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBC-icalp16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBC-icalp16.pdf},
doi = {10.4230/LIPIcs.ICALP.2016.101},
abstract = {In~2007, Abdulla \textit{et~al.} introduced the elegant concept
of decisive Markov chain. Intuitively, decisiveness allows one to lift the
good properties of finite Markov chains to infinite Markov chains. For
instance, the approximate quantitative reachability problem can be solved
for decisive Markov chains (enjoying reasonable effectiveness assumptions)
including probabilistic lossy channel systems and probabilistic vector
addition systems with states. In this paper, we extend the concept of
decisiveness to more general stochastic processes. This extension is non
trivial as we consider stochastic processes with a potentially continuous
set of states and uncountable branching (common features of real-time
stochastic processes). This allows us to obtain decidability results for
both qualitative and quantitative verification problems on some classes of
real-time stochastic processes, including generalized semi-Markov
processes and stochastic timed automata.}
}
@article{BMV-ic16,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Bouyer, Patricia and Markey, Nicolas and Vester, Steen},
title = {{N}ash Equilibria in Symmetric Graph Games with Partial Observation},
volume = {254},
number = {2},
month = jun,
year = 2017,
pages = {238-258},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMV-ic16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMV-ic16.pdf},
doi = {10.1016/j.ic.2016.10.010},
abstract = {We investigate a model for representing large multiplayer games,
which satisfy strong symmetry properties. This model is made of multiple
copies of an arena; each player plays in his own arena, and can partially
observe what the other players do. Therefore, this game has partial
information and symmetry constraints, which make the computation of Nash
equilibria difficult. We show several undecidability results, and for
bounded-memory strategies, we precisely characterize the complexity of
computing pure Nash equilibria (for qualitative objectives) in this game
model.}
}
@inproceedings{BCM-cav16,
address = {Toronto, Canada},
month = jul,
year = 2016,
volume = 9779,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Chaudhuri, Swarat and Farzan, Azadeh},
acronym = {{CAV}'16},
booktitle = {{P}roceedings of the 28th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'16)~-- {P}art~{I}},
author = {Bouyer, Patricia and Colange, Maximilien and Markey, Nicolas},
title = {Symbolic Optimal Reachability in Weighted Timed Automata},
pages = {513-530},
url = {http://arxiv.org/abs/1602.00481},
doi = {10.1007/978-3-319-41528-4_28},
abstract = {Weighted timed automata have been defined in the early 2000's
for modelling resource-consumption or -allocation problems in real-time
systems. Optimal reachability is decidable in weighted timed automata, and
a symbolic forward algorithm has been developed to solve that problem. This
algorithm uses so-called priced zones, an extension of standard zones with
cost functions. In order to ensure termination, the algorithm requires
clocks to be bounded. For unpriced timed automata, much work has been done
to develop sound abstractions adapted to the forward exploration of timed
automata, ensuring termination of the model-checking algorithm without
bounding the clocks. In this paper, we take advantage of recent
developments on abstractions for timed automata, and propose an algorithm
allowing for symbolic analysis of all weighted timed automata, without
requiring bounded clocks.}
}
@inproceedings{BMRSS-icalp16,
address = {Rome, Italy},
month = jul,
year = 2016,
volume = {55},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chatzigiannakis, Ioannis and Mitzenmacher,
Michael and Rabani, Yuval and Sangiorgi, Davide},
acronym = {{ICALP}'16},
booktitle = {{P}roceedings of the 43rd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'16)},
author = {Bouyer, Patricia and Markey, Nicolas and Randour,
Mickael and Sangnier, Arnaud and Stan, Daniel},
title = {Reachability in Networks of Register Protocols under
Stochastic Schedulers},
pages = {106:1-106:14},
url = {http://arxiv.org/abs/1602.05928},
doi = {10.4230/LIPIcs.ICALP.2016.106},
abstract = {We study the almost-sure reachability problem in a distributed
system obtained as the asynchronous composition of~\(N\) copies (called
\emph{processes}) of the same automaton (called \emph{protocol}), that can
communicate via a shared register with finite domain. The automaton has
two types of transitions: write-transitions update the value of the
register, while read-transitions move to a new state depending on the
content of the register. Non-determinism is resolved by a stochastic
scheduler. Given a protocol, we focus on almost-sure reachability of a
target state by one of the processes. The answer to this problem naturally
depends on the number~\(N\) of processes. However, we prove that our
setting has a cut-off property : the answer to the almost-sure
reachability problem is constant when \(N\) is large enough; we~then
develop an EXPSPACE algorithm deciding whether this constant answer is
positive or negative.}
}
@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.",
}}
@techreport{BJM-arxiv16,
author = {Bouyer, Patricia and Markey, Nicolas and Jug{\'e}, Vincent},
title = {Dynamic Complexity of Parity Games with Bounded Tree-Width},
institution = {Computing Research Repository},
number = {1610.00571},
year = {2016},
url = {https://arxiv.org/abs/1610.00571},
pdf = {https://arxiv.org/abs/1610.00571},
month = oct,
type = {Research Report},
note = {33~pages}
}
@inproceedings{GBM-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 = {Gardy, Patrick and Bouyer, Patricia and Markey, Nicolas},
title = {Dependences in Strategy Logic},
pages = {34:1-34:15},
year = {2018},
doi = {10.4230/LIPIcs.STACS.2018.34},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/8532/pdf/LIPIcs-STACS-2018-34.pdf},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=8532},
abstract = {Strategy Logic (SL) is a very expressive logic for specifying and verifying properties of multi-agent systems: in SL, one can quantify over strategies, assign them to agents, and express properties of the resulting plays. Such a powerful framework has two drawbacks: first, model checking SL has non-elementary complexity; second, the exact semantics of SL is rather intricate, and may not correspond to what is expected. In this paper, we focus on strategy dependences in SL, by tracking how existentially-quantified strategies in a formula may (or may not) depend on other strategies selected in the formula. We study different kinds of dependences, refining the approach of [Mogavero et al., Reasoning about strategies: On the model-checking problem, 2014], and prove that they give rise to different satisfaction relations. In the setting where strategies may only depend on what they have observed, we identify a large fragment of SL for which we prove model checking can be performed in 2-EXPTIME.}
}
@inproceedings{GBBLM-gretsi17,
address = {Juan-les-Pins, France},
month = sep,
year = 2017,
publisher = {},
editor = {},
acronym = {{GRETSI}'17},
booktitle = {Actes du XXVI$^{\text{\`eme}}$ colloque GRETSI},
author = {Mauricio Gonz{\'a}lez and Olivier Beaude and
Patricia Bouyer and Samson Lasaulce and Nicolas
Markey},
title = {Strat{\'e}gies d'ordonnancement de consommation
d'{\'e}nergie en pr{\'e}sence d'information
imparfaite de pr{\'e}vision},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GBBLM-gretsi17.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GBBLM-gretsi17.pdf}
}
@techreport{BJM-arxiv17,
author = {Bouyer, Patricia and Markey, Nicolas and
Jug{\'e}, Vincent},
institution = {Computing Research Repository},
month = feb,
note = {14~pages},
number = {1702.05183},
type = {Research Report},
title = {Courcelle's Theorem Made Dynamic},
year = {2017},
url = {https://arxiv.org/abs/1702.05183},
pdf = {https://arxiv.org/abs/1702.05183}
}
@inproceedings{BHJ-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 = {Bouyer, Patricia and Haddad, Serge and Jug{\'e}, Vincent},
title = {Unbounded product-form {P}etri nets},
pages = {31:1--31:16},
url = {http://drops.dagstuhl.de/opus/volltexte/2017/7795},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/7795/pdf/LIPIcs-CONCUR-2017-31.pdf},
doi = {10.4230/LIPIcs.CONCUR.2017.31},
abstract = {Computing steady-state distributions in infinite-state stochastic systems is in general a very difficult task. Product-form Petri nets are those Petri nets for which the steady-state distribution can be described as a natural product corresponding, up to a normalising constant, to an exponentiation of the markings. However, even though some classes of nets are known to have a product-form distribution, computing the normalising constant can be hard. The class of (closed) \(\Pi^3\)-nets has been proposed in an earlier work, for which it is shown that one can compute the steady-state distribution efficiently. However these nets are bounded. In this paper, we generalise queuing Markovian networks and closed \(\Pi^3\)-nets to obtain the class of open \(\Pi^3\)-nets, that generate infinite-state systems. We show interesting properties of these nets: (1) we prove that liveness can be decided in polynomial time, and that reachability in live \(\Pi^3\)-nets can be decided in polynomial time; (2) we show that we can decide ergodicity of such nets in polynomial time as well; (3) we provide a pseudo-polynomial time algorithm to compute the normalising constant.}
}
@inproceedings{BJM-formats17,
address = {Berlin, Germany},
month = sep,
year = 2017,
volume = {10419},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abate, Alessandro and Geeraerts, Gilles},
acronym = {{FORMATS}'17},
booktitle = {{P}roceedings of the 15th {I}nternational {C}onference
on {F}ormal {M}odelling and {A}nalysis of {T}imed
{S}ystems ({FORMATS}'17)},
author = {Bouyer, Patricia and Jaziri, Samy and Markey, Nicolas},
title = {On the Determinization of Timed Systems},
pages = {25-41},
url = {https://hal.archives-ouvertes.fr/hal-01566436/},
doi = {10.1007/978-3-319-65765-3_2},
abstract = {We introduce a new formalism called automata over a timed domain which provides an adequate framework for the determinization of timed systems. In this formalism, determinization w.r.t. timed language is always possible at the cost of changing the timed domain. We give a condition for determinizability of automata over a timed domain without changing the timed domain, which allows us to recover several known determinizable classes of timed systems, such as strongly-non-zeno timed automata, integer-reset timed automata, perturbed timed automata, etc. Moreover in the case of timed automata this condition encompasses most determinizability conditions from the literature.}
}
@incollection{BLMOW-kimfest17,
author = {Bouyer, Patricia and Laroussinie, Fran{\c{c}}ois and
Markey, Nicolas and Ouaknine, Jo{\"e}l and Worrell,
James},
title = {Timed temporal logics},
editor = {Aceto, Luca and Bacci, Giorgio and Bacci, Giovani
and Ing{\'o}lfsd{\'o}ttir, Anna and Legay, Axel and
Mardare, Radu},
booktitle = {Models, Algorithms, Logics and Tools: Essays
Dedicated to Kim Guldstrand Larsen on the Occasion
of His 60th Birthday},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {10460},
year = {2017},
pages = {211-230},
month = aug,
doi = {10.1007/978-3-319-65764-6_11},
abstract = {Since the early 1990's, classical temporal logics
have been extended with timing constraints. While
temporal logics only express contraints on the order
of events, their timed extensions can add
quantitative constraints on delays between those
events. We survey expressiveness and algorithmic
results on those logics, and discuss semantic
choices that may look unimportant but do have an
impact on the questions we consider.},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BLMOW-kimfest17.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BLMOW-kimfest17.pdf}
}
@inproceedings{BGMR-gandalf18,
address = {Saarbr{\"u}cken, Germany},
month = sep,
volume = {277},
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Andrea Orlandini and Martin Zimmermann},
acronym = {{GandALF}'18},
booktitle = {{P}roceedings of the 9th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification
({GandALF}'18)},
author = {Bouyer, Patricia and Gonz{\'a}lez, Mauricio and Markey, Nicolas and Randour, Mickael},
title = {Multi-weighted Markov Decision Processes with Reachability Objectives},
pages = {250-264},
year = {2018},
doi = {10.4204/EPTCS.277.18},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMR-gandalf18.pdf},
url = {http://arxiv.org/abs/1809.03107},
abstract = {In this paper, we are interested in the synthesis of schedulers in double-weighted Markov decision processes, which satisfy both a percentile constraint over a weighted reachability condition, and a quantitative constraint on the expected value of a random variable defined using a weighted reachability condition. This problem is inspired by the modelization of an electric-vehicle charging problem. We study the cartography of the problem, when one parameter varies, and show how a partial cartography can be obtained via two sequences of opimization problems. We discuss completeness and feasability of the method.}
}
@inproceedings{BJM-rv18,
address = {Limassol, Cyprus},
month = nov,
volume = 11237,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Colombo, Christian and Leucker, Martin},
acronym = {{RV}'18},
booktitle = {{P}roceedings of the 18th {W}orkshop on {R}untime {V}erification ({RV}'18)},
author = {Bouyer, Patricia and Jaziri, Samy and Markey, Nicolas},
title = {Efficient Timed Diagnosis Using Automata with Timed Domains},
pages = {205-221},
year = {2018},
doi = {10.1007/978-3-030-03769-7_12},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BJM-rv18.pdf},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BJM-rv18.pdf},
abstract = {We consider the problems of efficiently diagnosing and predicting what did (or will) happen in a partially-observable one-clock timed automaton. We introduce timed sets as a formalism to keep track of the evolution of the reachable configurations over time, and use our previous work on automata over timed domains to build a candidate diagnoser for our timed automaton. We report on our implementation of this approach compared to the approach of [Tripakis, Fault diagnosis for timed automata, 2002].}
}
@inproceedings{BBJ-csl18,
address = {Birmingham, UK},
month = sep,
year = 2018,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Ghica, Dan R. and Jung, Achim},
acronym = {{CSL}'18},
booktitle = {{P}roceedings of the 27th {A}nnual {EACSL} {C}onference on
{C}omputer {S}cience {L}ogic ({CSL}'18)},
author = {B{\'e}rard, B{\'e}atrice and Bouyer, Patricia and Jug{\'e}, Vincent},
title = {Finite bisimulations for dynamical systems with overlapping trajectories},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9693},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/9693/pdf/LIPIcs-CSL-2018-26.pdf},
doi = {10.4230/LIPIcs.CSL.2018.26},
abstract = {Having a finite bisimulation is a good feature for a dynamical system, since it can lead to the decidability of the verification of reachability properties. We investigate a new class of o-minimal dynamical systems with very general flows, where the classical restrictions on trajectory intersections are partly lifted. We identify conditions, that we call Finite and Uniform Crossing: When Finite Crossing holds, the time-abstract bisimulation is computable and, under the stronger Uniform Crossing assumption, this bisimulation is finite and definable.}
}
@inproceedings{BBFLMR-fm18,
address = {Oxford, UK},
month = jul,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Roscoe, {Bill W.} and Peleska, Jan},
acronym = {{FM}'18},
booktitle = {{P}roceedings of the 22nd {I}nternational {S}ymposium on {F}ormal
{M}ethods ({FM}'18)},
author = {Bacci, Giovanni and Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim G. and Markey, Nicolas and Reynier, Pierre-Alain},
title = {Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty},
pages = {203-221},
year = {2018},
doi = {10.1007/978-3-319-95582-7_12},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBFLMR-fm18.pdf},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBFLMR-fm18.pdf},
note = {Best paper award},
abstract = {In this paper, we propose a novel framework for the synthesis of robust and optimal energy-aware controllers. The framework is based on energy timed automata, allowing for easy expression of timing-constraints and variable energy-rates. We prove decidability of the energy-constrained infinite-run problem in settings with both certainty and uncertainty of the energy-rates. We also consider the optimization problem of identifying the minimal upper bound that will permit existence of energy-constrained infinite runs. Our algorithms are based on quantifier elimination for linear real arithmetic. Using Mathematica and Mjollnir, we illustrate our framework through a real industrial example of a hydraulic oil pump. Compared with previous approaches our method is completely automated and provides improved results.}
}
@article{BBBC-jlamp18,
publisher = {Elsevier Science Publishers},
journal = {Journal of Logic and Algebraic Methods in Programming},
author = {Bertrand, Nathalie and Bouyer, Patricia and Brihaye, Thomas and Carlier, Pierre},
title = {When are Stochastic Transition Systems Tameable?},
volume = {99},
pages = {41-96},
year = {2018},
month = oct,
doi = {10.1016/j.jlamp.2018.03.004},
pdf = {https://arxiv.org/pdf/1703.04806.pdf},
url = {https://doi.org/10.1016/j.jlamp.2018.03.004},
abstract = {A decade ago, Abdulla, Ben Henda and Mayr introduced the elegant concept of decisiveness for denumerable Markov chains [1]. Roughly speaking, decisiveness allows one to lift most good properties from finite Markov chains to denumerable ones, and therefore to adapt existing verification algorithms to infinite-state models. Decisive Markov chains however do not encompass stochastic real-time systems, and general stochastic transition systems (STSs for short) are needed. In this article, we provide a framework to perform both the qualitative and the quantitative analysis of STSs. First, we define various notions of decisiveness (inherited from [1]), notions of fairness and of attractors for STSs, and make explicit the relationships between them. Then, we define a notion of abstraction, together with natural concepts of soundness and completeness, and we give general transfer properties, which will be central to several verification algorithms on STSs. We further design a generic construction which will be useful for the analysis of ω-regular properties, when a finite attractor exists, either in the system (if it is denumerable), or in a sound denumerable abstraction of the system. We next provide algorithms for qualitative model-checking, and generic approximation procedures for quantitative model-checking. Finally, we instantiate our framework with stochastic timed automata (STA), generalized semi-Markov processes (GSMPs) and stochastic time Petri nets (STPNs), three models combining dense-time and probabilities. This allows us to derive decidability and approximability results for the verification of these models. Some of these results were known from the literature, but our generic approach permits to view them in a unified framework, and to obtain them with less effort. We also derive interesting new approximability results for STA, GSMPs and STPNs.}
}
@inproceedings{B-fossacs18,
address = {Thessaloniki, Greece},
month = apr,
year = 2018,
volume = {10803},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Baier, Christel and {Dal Lago}, Ugo},
acronym = {{FoSSaCS}'18},
booktitle = {{P}roceedings of the 21st {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'18)},
author = {Bouyer, Patricia},
title = {Games on graphs with a public signal monitoring},
pages = {530-547},
url = {https://arxiv.org/abs/1710.07163},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/B-fossacs18.pdf},
doi = {10.1007/978-3-319-89366-2_29},
abstract = {We study Nash equilibria in games on graphs with an imperfect monitoring based on a public signal. In such games, deviations and players responsible for those deviations can be hard to detect and track. We propose a generic epistemic game abstraction, which conveniently allows to represent the knowledge of the players about these deviations, and give a characterization of Nash equilibria in terms of winning strategies in the abstraction. We then use the abstraction to develop algorithms for some payoff functions.}
}
@inproceedings{BBM-fsttcs19,
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)},
author = {Nathalie Bertrand and Patricia Bouyer and Anirban Majumdar},
title = {Concurrent parameterized games},
pages = {31:1-31:15},
year = 2019,
doi = {10.4230/LIPIcs.FSTTCS.2019.31},
pdf = {https://drops.dagstuhl.de/opus/volltexte/2019/11593/pdf/LIPIcs-FSTTCS-2019-31.pdf},
url = {https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11593},
abstract = {Traditional concurrent games on graphs involve a fixed number of players, who take decisions simultaneously, determining the next state of the game. In this paper, we introduce a parameterized variant of concurrent games on graphs, where the parameter is precisely the number of players. Parameterized concurrent games are described by finite graphs, in which the transitions bear regular languages to describe the possible move combinations that lead from one vertex to another. We consider the problem of determining whether the first player, say Eve, has a strategy to ensure a reachability objective against any strategy profile of her opponents as a coalition. In particular Eve's strategy should be independent of the number of opponents she actually has. Technically, this paper focuses on an a priori simpler setting where the languages labeling transitions only constrain the number of opponents (but not their precise action choices). These constraints are described as semilinear sets, finite unions of intervals, or intervals. We establish the precise complexities of the parameterized reachability game problem, ranging from PTIME-complete to PSPACE-complete, in a variety of situations depending on the contraints (semilinear predicates, unions of intervals, or intervals) and on the presence or not of non-determinism.}
}
@inproceedings{BT-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 = {Patricia Bouyer and Nathan Thomasset},
title = {Nash equilibria in games over graphs equipped with a communication mechanism},
pages = {9:1-9:14},
year = 2019,
doi = {10.4230/LIPIcs.MFCS.2019.9},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2019/10953/pdf/LIPIcs-MFCS-2019-9.pdf},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=10953}
}
@inproceedings{BBM-concur19,
address = {Amsterdam, The Netherlands},
month = aug,
volume = {140},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Wan Fokkink and Rob {van Glabbeek}},
acronym = {{CONCUR}'19},
booktitle = {{P}roceedings of the 30th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'19)},
author = {Nathalie Bertrand and Patricia Bouyer and Anirban Majumdar},
title = {Reconfiguration and message losses in parameterized broadcast networks},
pages = {32:1-32:15},
year = 2019,
doi = {10.4230/LIPIcs.CONCUR.2019.32},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2019/10934/pdf/LIPIcs-CONCUR-2019-32.pdf},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=10934}
}
@article{GBM-tocsys19,
publisher = {Springer},
journal = {Theory of Computing Systems},
author = {Gardy, Patrick and Bouyer, Patricia and Markey, Nicolas},
title = {Dependences in Strategy Logic},
volume = {64},
number = {3},
year = 2020,
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GBM-tocsys19.pdf},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GBM-tocsys19.pdf}
}
@inproceedings{BKMMMP-ijcai19,
futureaddress = {},
month = jul,
publisher = {IJCAI organization},
editor = {Kraus, Sarit},
acronym = {{IJCAI}'19},
booktitle = {{P}roceedings of the 28th {I}nternational {J}oint
{C}onference on {A}rtificial {I}ntelligence
({IJCAI}'19)},
author = {Bouyer, Patricia and Kupferman, Orna and Markey, Nicolas and Maubert, Bastien and Murano, Aniello and Perelli, Giuseppe},
title = {Reasoning about Quality and Fuzziness of Strategic Behaviours},
pages = {1588-1594},
year = 2019,
doi = {10.24963/ijcai.2019/220},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKMMMP-ijcai19.pdf},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKMMMP-ijcai19.pdf}
}
@inproceedings{BBR-fossacs19,
address = {Prague, Czech Republic},
month = apr,
year = 2019,
volume = {11425},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Boja{\'n}czyk, Mikolaj and Simpson, Alex},
acronym = {{FoSSaCS}'19},
booktitle = {{P}roceedings of the 22nd {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'19)},
author = {Benedikt Bollig and Patricia Bouyer and Fabian Reiter},
title = {Identifiers in Registers - Describing Network Algorithms with Logic},
pages = {115-132},
url = {https://arxiv.org/abs/1811.08197},
pdf = {https://arxiv.org/pdf/1811.08197.pdf},
doi = {10.1007/978-3-030-17127-8},
abstract = {We propose a formal model of distributed computing based on register automata
that captures a broad class of synchronous network algorithms. The local memory
of each process is represented by a finite-state controller and a fixed number
of registers, each of which can store the unique identifier of some process in
the network. To underline the naturalness of our model, we show that it has the
same expressive power as a certain extension of first-order logic on graphs
whose nodes are equipped with a total order. Said extension lets us define new
functions on the set of nodes by means of a so-called partial fixpoint
operator. In spirit, our result bears close resemblance to a classical theorem
of descriptive complexity theory that characterizes the complexity class PSPACE
in terms of partial fixpoint logic (a proper superclass of the logic we
consider here).}
}
@inproceedings{BKMMMP-ecai20,
address = {Santiago de Compostela, Spain},
month = sep,
optvolume = {??},
optseries = {Frontiers in Artificial Intelligence and Applications},
publisher = {{IOS} Press},
editor = {Lang, J{\'e}r{\^o}me and De Giacomo, Giuseppe and Barro and Sen{\'e}n Barro and O'Sullivan, Barry},
acronym = {{ECAI}'20},
booktitle = {{P}roceedings of the 24th {E}uropean {C}onference on
{A}rtificial {I}ntelligence ({ECAI}'20)},
author = {Patricia Bouyer and Orna Kupferman and Nicolas Markey and Bastien Maubert and Aniello Murano and Giuseppe Perelli},
title = {{Reasoning About Quality and Fuzziness of Strategic Behaviours}},
pages = {2887-2888},
year = 2020,
pdf = {https://ebooks.iospress.nl/publication/55232},
url = {https://ebooks.iospress.nl/publication/55232},
doi = {10.3233/FAIA200437}
}
@article{BBFLMR-fac21,
publisher = {Springer},
journal = {Formal Aspects of Computing},
author = {Bacci, Giovanni and
Bouyer, Patricia and
Fahrenberg, Uli and
Larsen, Kim and
Markey, Nicolas and
Reynier, Pierre{-}Alain},
title = {Optimal and robust controller synthesis using energy timed automata
with uncertainty},
volume = {33},
pages = {3--25},
year = 2021,
doi = {10.1007/s00165-020-00521-4},
url = {https://link.springer.com/article/10.1007/s00165-020-00521-4}
}
@inproceedings{BBM-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 = {Nathalie Bertrand and Patricia Bouyer and Anirban Majumdar},
title = {Synthesizing safe coalition strategies},
pages = {39:1--39:17},
year = {2020},
doi = {https://doi.org/10.4230/LIPIcs.FSTTCS.2020.39},
pdf = {https://drops.dagstuhl.de/opus/volltexte/2020/13280/pdf/LIPIcs-FSTTCS-2020-39.pdf},
url = {https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=13280}
}
@inproceedings{BBRRV-gandalf20,
address = {Brussels, Belgium},
month = sep,
volume = {326},
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Bresolin, Davide and Raskin, Jean-Fran\c{c}ois},
acronym = {{GandALF}'20},
booktitle = {{P}roceedings of the 11th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification
({GandALF}'20)},
author = {Bouyer, Patricia and Brihaye, Thomas and Randour, Mickael and Rivi{\`e}re, C{\'e}dric and Vandenhove, Pierre},
title = {Decisiveness of Stochastic Systems and its Application to Hybrid Models},
pages = {149?165},
year = {2020},
doi = {10.4204/EPTCS.326.10},
pdf = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?GANDALF2020.10.pdf},
url = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?GANDALF2020.10}
}
@inproceedings{BBBFS-gandalf20,
address = {Brussels, Belgium},
month = sep,
volume = {326},
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {Bresolin, Davide and Raskin, Jean-Fran\c{c}ois},
acronym = {{GandALF}'20},
booktitle = {{P}roceedings of the 11th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification
({GandALF}'20)},
author = {B{\'e}atrice B{\'e}rard and
Benedikt Bollig and
Patricia Bouyer and
Matthias F{\"u}gger and
Nathalie Sznajder},
title = {Synthesis in Presence of Dynamic Links},
pages = {33?49},
year = {2020},
doi = {10.4204/EPTCS.326.3},
pdf = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?GANDALF2020.3.pdf},
url = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?GANDALF2020.3}
}
@inproceedings{BLORV-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 = {Bouyer, Patricia and Le Roux, St{\'e}phane and Oualhadj, Youssouf and Randour, Mickael and Vandenhove, Pierre},
title = {Games Where You Can Play Optimally with Arena-Independent Finite Memory},
pages = {24:1--24:22},
year = 2020,
doi = {10.4230/LIPIcs.CONCUR.2020.24},
url = {https://drops.dagstuhl.de/opus/volltexte/2020/12836}
}
@inproceedings{B-atva19,
address = {Taipei, Taiwan},
month = oct,
volume = {11781},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Yu{-}Fang Chen and Chih{-}Hong Cheng and Javier Esparza},
acronym = {{ATVA}'19},
booktitle = {{P}roceedings of the 17th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'19)},
author = {Patricia Bouyer},
title = {{A Note on Game Theory and Verification (Invited Talk)}},
pages = {3-22},
doi = {10.1007/978-3-030-31784-3_1},
year = 2019
}
@inproceedings{B-time19,
address = {M{\'{a}}laga, Spain},
month = oct,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Johann Gamper and Sophie Pinchinat and Guido Sciavicco},
acronym = {{TIME}'19},
booktitle = {{P}roceedings of the 26th {I}nternational {S}ymposium on
{T}emporal {R}epresentation and {R}easoning
({TIME}'19)},
author = {Patricia Bouyer},
title = {{On the Computation of Nash Equilibria in Games on Graphs (Invited Talk)}},
pages = {3:1-3:3},
doi = {10.4230/LIPIcs.TIME.2019.3},
year = 2019
}
This file was generated by bibtex2html 1.98.