LászlóBabai.
Trading Group Theory for Randomness.
In STOC'85,
pages 421-429.
ACM Press, May 1985.
@inproceedings{stoc1985-Bab,
author = {Babai, L{\'a}szl{\'o}},
title = {Trading Group Theory for Randomness},
booktitle = {{P}roceedings of the 17th {A}nnual {ACM} {S}ymposium
on the {T}heory of {C}omputing ({STOC}'85)},
acronym = {{STOC}'85},
publisher = {ACM Press},
pages = {421-429},
year = {1985},
month = may,
}
[BAS02]
ArminBiere,
CyrilleArtho, and
ViktorSchuppan.
Liveness Checking as Safety Checking.
In FMICS'02,
Electronic Notes in Theoretical Computer Science 66(2).
Elsevier, July 2002.
@inproceedings{fmics2002-BAS,
author = {Biere, Armin and Artho, Cyrille and Schuppan,
Viktor},
title = {Liveness Checking as Safety Checking},
editor = {Cleaveland, Rance and Garavel, Hubert},
booktitle = {{P}roceedings of the 7th {I}nternational {ERCIM}
{W}orkshop in {F}ormal {M}ethods for {I}ndustrial
{C}ritical {S}ystems ({FMICS}'02)},
acronym = {{FMICS}'02},
publisher = {Elsevier},
series = {Electronic Notes in Theoretical Computer Science},
volume = {66},
number = {2},
year = {2002},
month = jul,
}
[BB91]
Jos C. M.Baeten and
Jan A.Bergstra.
Real Time Process Algebra.
Formal Aspects of Computing 3(2):142-188. Springer-Verlag, 1991.
@article{fac3(2)-BB,
author = {Baeten, Jos C. M. and Bergstra, Jan A.},
title = {Real Time Process Algebra},
publisher = {Springer-Verlag},
journal = {Formal Aspects of Computing},
volume = {3},
number = {2},
pages = {142-188},
year = {1991},
}
[BB02]
DietmarBerwanger and
AchimBlumensath.
The Monadic Theory of Tree-like Structures.
In ErichGrädel,
WolfgangThomas, and
ThomasWilke (eds.),
Automata, Logics, and Infinite Games,
Lecture Notes in Computer Science 2500, pages 285-302. Springer-Verlag, 2002.
@incollection{lncs2500-BB,
author = {Berwanger, Dietmar and Blumensath, Achim},
title = {The Monadic Theory of Tree-like Structures},
editor = {Gr{\"a}del, Erich and Thomas, Wolfgang and Wilke,
Thomas},
booktitle = {Automata, Logics, and Infinite Games},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {2500},
pages = {285-302},
year = {2002},
}
[BB04]
Laura BrandánBriones and
EdBrinksma.
A Test Generation Framework for Quiescent Real-Time
Systems.
In FATES'04,
Lecture Notes in Computer Science 3395, pages 64-78. Springer-Verlag, September 2004.
@inproceedings{BB-fates2004,
author = {Briones, Laura Brand{\'a}n and Brinksma, Ed},
title = {A~Test Generation Framework for Quiescent Real-Time
Systems},
editor = {Grabowski, Jens and Nielsen, Brian},
booktitle = {{P}roceedings of the 4th {I}nternational {W}orkshop
on {F}ormal {A}pproaches to {S}oftware {T}esting
({FATES}'04)},
acronym = {{FATES}'04},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {3395},
pages = {64-78},
year = {2004},
month = sep,
doi = {10.1007/978-3-540-31848-4_5},
}
[BBB+09]
ChristelBaier,
NathalieBertrand,
PatriciaBouyer, and
ThomasBrihaye.
When are timed automata determinizable?.
In ICALP'09,
Lecture Notes in Computer Science 5556, pages 43-54. Springer-Verlag, July 2009.
@inproceedings{icalp2009-BBBB,
author = {Baier, {\relax Ch}ristel and Bertrand, Nathalie and
Bouyer, Patricia and Brihaye, {\relax Th}omas},
title = {When are timed automata determinizable?},
editor = {Albers, Susanne and Marchetti{-}Spaccamela Alberto
and Matias, Yossi and Nikoletseas, Sotiris and
Thomas, Wolfgang},
booktitle = {{P}roceedings of the 36th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'09)~-- Part~{II}},
acronym = {{ICALP}'09},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {5556},
pages = {43-54},
year = {2009},
month = jul,
doi = {10.1007/978-3-642-02930-1_4},
}
[BBB+07]
ChristelBaier,
NathalieBertrand,
PatriciaBouyer,
ThomasBrihaye, and
MarcusGrößer.
Probabilistic and Topological Semantics for Timed
Automata.
In FSTTCS'07,
Lecture Notes in Computer Science 4855, pages 179-191. Springer-Verlag, December 2007.
@inproceedings{fsttcs2007-BBBBG,
author = {Baier, {\relax Ch}ristel 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},
editor = {Arvind, Vikraman and Prasad, Sanjiva},
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)},
acronym = {{FSTTCS}'07},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {4855},
pages = {179-191},
year = {2007},
month = dec,
}
[BBB+08]
ChristelBaier,
NathalieBertrand,
PatriciaBouyer,
ThomasBrihaye, and
MarcusGrößer.
Almost-sure Model Checking of Infinite Paths in
One-clock Timed Automata.
In LICS'08,
pages 217-226.
IEEE Comp. Soc. Press, June 2008.
@inproceedings{lics2008-BBBBG,
author = {Baier, {\relax Ch}ristel and Bertrand, Nathalie and
Bouyer, Patricia and Brihaye, {\relax Th}omas and
Gr{\"o}{\ss}er, Marcus},
title = {Almost-sure Model Checking of Infinite Paths in
One-clock Timed Automata},
booktitle = {{P}roceedings of the 23rd {A}nnual {S}ymposium on
{L}ogic in {C}omputer {S}cience ({LICS}'08)},
acronym = {{LICS}'08},
publisher = {IEEE Comp. Soc. Press},
pages = {217-226},
year = {2008},
month = jun,
doi = {10.1109/LICS.2008.25},
}
[BBB+07]
ÉricBadouel,
MarekBednarczyk,
AndrzejBorzyszkowski,
BenoîtCaillaud, and
PhilippeDarondeau.
Concurrent secrets.
Discrete Event Dynamic Systems 17(4):425-446. Kluwer Academic, December 2007.
@article{deds17(4)-BBBCD,
author = {Badouel, {\'E}ric and Bednarczyk, Marek and
Borzyszkowski, Andrzej and Caillaud, Beno{\^\i}t and
Darondeau, Philippe},
title = {Concurrent secrets},
publisher = {Kluwer Academic},
journal = {Discrete Event Dynamic Systems},
volume = {17},
number = {4},
pages = {425-446},
year = {2007},
month = dec,
doi = {10.1007/s10626-007-0020-5},
}
In [Baier et al., 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.
In this paper, we
consider the quantitative model-checking problem for
ω-regular properties: we aim at computing
the exact probability that a given timed automaton
satisfies an ω-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.
@inproceedings{qest2008-BBBM,
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},
booktitle = {{P}roceedings of the 5th {I}nternational
{C}onference on {Q}uantitative {E}valuation of
{S}ystems ({QEST}'08)},
acronym = {{QEST}'08},
publisher = {IEEE Comp. Soc. Press},
pages = {55-64},
year = {2008},
month = sep,
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.},
}
[BBB+14]
NathalieBertrand,
PatriciaBouyer,
ThomasBrihaye,
QuentinMenet,
ChristelBaier,
MarcusGrößer, and
MarcinJurdziński.
Stochastic Timed Automata.
Logical Methods in Computer Science 10(4).
December 2014.
@article{lmcs10(4)-BBBMBGJ,
author = {Bertrand, Nathalie and Bouyer, Patricia and Brihaye,
{\relax Th}omas and Menet, Quentin and Baier,
{\relax Ch}ristel and Gr{\"o}{\ss}er, Marcus and
Jurdzi{\'n}ski, Marcin},
title = {Stochastic Timed Automata},
journal = {Logical Methods in Computer Science},
volume = {10},
number = {4},
year = {2014},
month = dec,
doi = {10.2168/LMCS-10(4:6)2014},
}
[BBB+07]
PatriciaBouyer,
ThomasBrihaye,
VéroniqueBruyère, and
Jean-FrançoisRaskin.
On the Optimal Reachability Problem of Weighted
Timed Automata.
Formal Methods in System Design 31(2):135-175. Springer-Verlag, October 2007.
@article{fmsd31(2)-BBBR,
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 of Weighted
Timed Automata},
publisher = {Springer-Verlag},
journal = {Formal Methods in System Design},
volume = {31},
number = {2},
pages = {135-175},
year = {2007},
month = oct,
doi = {10.1007/s10703-007-0035-4},
}
[BBC10]
AlbertBenveniste,
AnneBouillard, and
PaulCaspi.
A unifying view of loosely time-triggered
architectures.
In EMSOFT'10,
pages 189-198.
ACM Press, October 2010.
@inproceedings{emsoft2010-BBC,
author = {Benveniste, Albert and Bouillard, Anne and Caspi,
Paul},
title = {A~unifying view of loosely time-triggered
architectures},
editor = {Carloni, Luca P. and Tripakis, Stavros},
booktitle = {{P}roceedings of the 10th {I}nternational
{C}onference on {E}mbedded {S}oftware ({EMSOFT}'10)},
acronym = {{EMSOFT}'10},
publisher = {ACM Press},
pages = {189-198},
year = {2010},
month = oct,
doi = {10.1145/1879021.1879047},
}
[BBD14]
ThomasBrihaye,
VéroniqueBruyère, and
JulieDe Pril.
On Equilibria in Quantitative Games with
Reachability/Safety Objectives.
Theory of Computing Systems 54(2):150-189. Springer-Verlag, February 2014.
@article{tcsyst54(2)-BBD,
author = {Brihaye, {\relax Th}omas and Bruy{\`e}re,
V{\'e}ronique and De{~}Pril, Julie},
title = {On Equilibria in Quantitative Games with
Reachability{{\slash}}Safety Objectives},
publisher = {Springer-Verlag},
journal = {Theory of Computing Systems},
volume = {54},
number = {2},
pages = {150-189},
year = {2014},
month = feb,
}
[BBD+11]
ThomasBrihaye,
VéroniqueBruyère,
LaurentDoyen,
MarcDucobu, and
Jean-FrançoisRaskin.
Antichain-based QBF Solving.
In ATVA'11,
Lecture Notes in Computer Science 6996, pages 183-197. Springer-Verlag, October 2011.
@inproceedings{atva2011-BBDDR,
author = {Brihaye, {\relax Th}omas and Bruy{\`e}re,
V{\'e}ronique and Doyen, Laurent and Ducobu, Marc
and Raskin, Jean-Fran{\c c}ois},
title = {Antichain-based {QBF} Solving},
editor = {Bultan, Tevfik and Hsiung, Pao-Ann},
booktitle = {{P}roceedings of the 9th {I}nternational {S}ymposium
on {A}utomated {T}echnology for {V}erification and
{A}nalysis ({ATVA}'11)},
acronym = {{ATVA}'11},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {6996},
pages = {183-197},
year = {2011},
month = oct,
}
[BBD+12]
ThomasBrihaye,
VéroniqueBruyère,
JulieDe Pril, and
HugoGimbert.
Subgame Perfection for Equilibria in Quantitative
Reachability Games.
In FoSSaCS'12,
Lecture Notes in Computer Science 7213, pages 286-300. Springer-Verlag, March 2012.
@inproceedings{fossacs2012-BBDG,
author = {Brihaye, {\relax Th}omas and Bruy{\`e}re,
V{\'e}ronique and De{~}Pril, Julie and Gimbert,
Hugo},
title = {Subgame Perfection for Equilibria in Quantitative
Reachability Games},
editor = {Birkedal, Lars},
booktitle = {{P}roceedings of the 15th {I}nternational
{C}onference on {F}oundations of {S}oftware
{S}cience and {C}omputation {S}tructure
({FoSSaCS}'12)},
acronym = {{FoSSaCS}'12},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {7213},
pages = {286-300},
year = {2012},
month = mar,
}
[BBD+02]
GerdBehrmann,
JohanBengtsson,
AlexandreDavid,
Kim GuldstrandLarsen,
PaulPettersson, and
WangYi.
UPPAAL Implementation Secrets.
In FTRTFT'02,
Lecture Notes in Computer Science 2469, pages 3-22. Springer-Verlag, September 2002.
@inproceedings{ftrtft2002-BBDLPY,
author = {Behrmann, Gerd and Bengtsson, Johan and David,
Alexandre and Larsen, Kim Guldstrand and Pettersson,
Paul and Yi, Wang},
title = {UPPAAL Implementation Secrets},
editor = {Damm, Werner and Olderog, Ernst R{\"u}diger},
booktitle = {{P}roceedings of the 7th {F}ormal {T}echniques in
{R}eal-Time and {F}ault-Tolerant {S}ystems
({FTRTFT}'02)},
acronym = {{FTRTFT}'02},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {2469},
pages = {3-22},
year = {2002},
month = sep,
doi = {10.1007/3-540-45739-9_1},
}
[BBF+06]
TomášBrázdil,
VáclavBrožek,
VojtěchForejt, and
AntonínKučera.
Stochastic Games with Branching-Time Winning
Objectives.
In LICS'06,
pages 349-358.
IEEE Comp. Soc. Press, July 2006.
@inproceedings{lics2006-BBFK,
author = {Br{\'a}zdil, Tom{\'a}{ s} and V{\'a}clav
Bro{{z}}ek and Forejt, Vojt{{e}}ch and Ku{
c}era, Anton{\'\i}n},
title = {Stochastic Games with Branching-Time Winning
Objectives},
booktitle = {{P}roceedings of the 21st {A}nnual {S}ymposium on
{L}ogic in {C}omputer {S}cience ({LICS}'06)},
acronym = {{LICS}'06},
publisher = {IEEE Comp. Soc. Press},
pages = {349-358},
year = {2006},
month = jul,
}
[BBF+03]
GerdBehrmann,
PatriciaBouyer,
EmmanuelFleury, and
Kim GuldstrandLarsen.
Static Guard Analysis in Timed Automata
Verification.
In TACAS'03,
Lecture Notes in Computer Science 2619, pages 254-270. Springer-Verlag, April 2003.
@inproceedings{tacas2003-BBFL,
author = {Behrmann, Gerd and Bouyer, Patricia and Fleury,
Emmanuel and Larsen, Kim Guldstrand},
title = {Static Guard Analysis in Timed Automata
Verification},
editor = {Garavel, Hubert and Hatcliff, John},
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)},
acronym = {{TACAS}'03},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {2619},
pages = {254-270},
year = {2003},
month = apr,
}
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.
@inproceedings{fm2018-BBFLMR,
author = {Bacci, Giovanni and Bouyer, Patricia and Fahrenberg,
Uli and Larsen, Kim Guldstrand and Markey, Nicolas
and Reynier, Pierre-Alain},
title = {Optimal and Robust Controller Synthesis Using Energy
Timed Automata with Uncertainty},
editor = {Roscoe, Bill W. and Peleska, Jan},
booktitle = {{P}roceedings of the 22nd {I}nternational
{S}ymposium on {F}ormal {M}ethods ({FM}'18)},
acronym = {{FM}'18},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
year = {2018},
month = jul,
note = {To~appear},
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.},
}
[BBF+01]
BéatriceBérard,
MichelBidoit,
AlainFinkel,
FrançoisLaroussinie,
AntoinePetit,
LaurePetrucci,
PhilippeSchnoebelen, and
PierreMcKenzie.
Systems and Software Verification: Model-Checking
Techniques and Tools.
Springer-Verlag, 2001.
@book{SSV2001-BBFLPPS,
author = {B{\'e}rard, B{\'e}atrice and Bidoit, Michel and
Finkel, Alain and Laroussinie, Fran{\c c}ois and
Petit, Antoine and Petrucci, Laure and Schnoebelen,
{\relax Ph}ilippe and McKenzie, Pierre},
title = {Systems and Software Verification: Model-Checking
Techniques and Tools},
publisher = {Springer-Verlag},
year = {2001},
}
[BBF+13]
AaronBohy,
VéroniqueBruyère,
EmmanuelFiliot, and
Jean-FrançoisRaskin.
Synthesis from LTL Specifications with Mean-Payoff
Objectives.
In TACAS'13,
Lecture Notes in Computer Science 7795, pages 169-184. Springer-Verlag, March 2013.
@inproceedings{tacas2013-BBFR,
author = {Bohy, Aaron and Bruy{\`e}re, V{\'e}ronique and
Filiot, Emmanuel and Raskin, Jean-Fran{\c c}ois},
title = {Synthesis from {LTL} Specifications with Mean-Payoff
Objectives},
editor = {Piterman, Nir and Smolka, Scott A.},
booktitle = {{P}roceedings of the 19th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'13)},
acronym = {{TACAS}'13},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {7795},
pages = {169-184},
year = {2013},
month = mar,
}
[BBG+07]
ChristelBaier,
TomášBrázdil,
MarcusGrößer, and
AntonínKučera.
Stochastic Game Logic.
In QEST'07,
pages 227-236.
IEEE Comp. Soc. Press, September 2007.
@inproceedings{qest2007-BBGK,
author = {Baier, {\relax Ch}ristel and Br{\'a}zdil,
Tom{\'a}{ s} and Gr{\"o}{\ss}er, Marcus and Ku{
c}era, Anton{\'\i}n},
title = {Stochastic Game Logic},
booktitle = {{P}roceedings of the 4th {I}nternational
{C}onference on {Q}uantitative {E}valuation of
{S}ystems ({QEST}'07)},
acronym = {{QEST}'07},
publisher = {IEEE Comp. Soc. Press},
pages = {227-236},
year = {2007},
month = sep,
}
[BBJ+14]
DimitriBohlender,
HaroldBruintjes,
SebastianJunges,
JensKatelaan,
Viet YenNguyen, and
ThomasNoll.
A Review of Statistical Model Checking Pitfalls on
Real-Time Stochastic Models.
In ISoLA'14,
Lecture Notes in Computer Science 8803, pages 177-192. Springer-Verlag, October 2014.
@inproceedings{BBJKNN-isola2014,
author = {Bohlender, Dimitri and Bruintjes, Harold and Junges,
Sebastian and Katelaan, Jens and Nguyen, Viet Yen
and Noll, Thomas},
title = {A~Review of Statistical Model Checking Pitfalls on
Real-Time Stochastic Models},
editor = {Margaria, Tiziana and Steffen, Bernhard},
booktitle = {{P}roceedings of the 6th {I}nternational {S}ymposium
on {L}everaging {A}pplications of {F}ormal
{M}ethods, {V}erification and {V}alidation
({IS}o{LA}'14)~-- {P}art~{II}: {S}pecialized
{T}echniques and {A}pplications},
acronym = {{IS}o{LA}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8803},
pages = {177-192},
year = {2014},
month = oct,
doi = {10.1007/978-3-662-45231-8_13},
}
[BBL04]
PatriciaBouyer,
EdBrinksma, and
Kim GuldstrandLarsen.
Staying Alive as Cheaply as Possible.
In HSCC'04,
Lecture Notes in Computer Science 2993, pages 203-218. Springer-Verlag, March 2004.
@inproceedings{hscc2004-BBL,
author = {Bouyer, Patricia and Brinksma, Ed and Larsen, Kim
Guldstrand},
title = {Staying Alive as Cheaply as Possible},
editor = {Alur, Rajeev and Pappas, George J.},
booktitle = {{P}roceedings of the 7th {I}nternational {W}orkshop
on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
({HSCC}'04)},
acronym = {{HSCC}'04},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {2993},
pages = {203-218},
year = {2004},
month = mar,
}
[BBL08]
PatriciaBouyer,
EdBrinksma, and
Kim GuldstrandLarsen.
Optimal infinite scheduling for multi-priced timed
automata.
Formal Methods in System Design 32(1):2-23. Springer-Verlag, February 2008.
@article{fmsd32(1)-BBL,
author = {Bouyer, Patricia and Brinksma, Ed and Larsen, Kim
Guldstrand},
title = {Optimal infinite scheduling for multi-priced timed
automata},
publisher = {Springer-Verlag},
journal = {Formal Methods in System Design},
volume = {32},
number = {1},
pages = {2-23},
year = {2008},
month = feb,
}
[BBL+13]
GiorgioBacci,
GiovanniBacci,
Kim GuldstrandLarsen, and
RaduMardare.
Computing Behavioral Distances, Compositionally.
In MFCS'13,
Lecture Notes in Computer Science 8087, pages 74-85. Springer-Verlag, August 2013.
@inproceedings{mfcs2013-BBLM,
author = {Bacci, Giorgio and Bacci, Giovanni and Larsen, Kim
Guldstrand and Mardare, Radu},
title = {Computing Behavioral Distances, Compositionally},
editor = {Chatterjee, Krishnendu and Sgall, Ji{ r}{\'\i}},
booktitle = {{P}roceedings of the 38th {I}nternational
{S}ymposium on {M}athematical {F}oundations of
{C}omputer {S}cience ({MFCS}'13)},
acronym = {{MFCS}'13},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8087},
pages = {74-85},
year = {2013},
month = aug,
doi = {10.1007/978-3-642-40313-2_9},
}
[BBL+13]
GiorgioBacci,
GiovanniBacci,
Kim GuldstrandLarsen, and
RaduMardare.
The BisimDist Library: Efficient Computation of
Bisimilarity Distances for Markovian Models.
In QEST'13,
pages 278-281.
IEEE Comp. Soc. Press, August 2013.
@inproceedings{qest2013-BBLM,
author = {Bacci, Giorgio and Bacci, Giovanni and Larsen, Kim
Guldstrand and Mardare, Radu},
title = {The BisimDist Library: Efficient Computation of
Bisimilarity Distances for Markovian Models},
booktitle = {{P}roceedings of the 10th {I}nternational
{C}onference on {Q}uantitative {E}valuation of
{S}ystems ({QEST}'13)},
acronym = {{QEST}'13},
publisher = {IEEE Comp. Soc. Press},
pages = {278-281},
year = {2013},
month = aug,
doi = {10.1007/978-3-642-40196-1_23},
}
[BBL+04]
GerdBehrmann,
PatriciaBouyer,
Kim GuldstrandLarsen, and
RadekPelánek.
Lower and Upper Bounds in Zone-Based Abstractions of
Timed Automata.
In TACAS'04,
Lecture Notes in Computer Science 2988, pages 312-326. Springer-Verlag, March 2004.
@inproceedings{tacas2004-BBLP,
author = {Behrmann, Gerd and Bouyer, Patricia and Larsen, Kim
Guldstrand and Pel{\'a}nek, Radek},
title = {Lower and Upper Bounds in Zone-Based Abstractions of
Timed Automata},
editor = {Jensen, Kurt and Podelski, Andreas},
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)},
acronym = {{TACAS}'04},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {2988},
pages = {312-326},
year = {2004},
month = mar,
doi = {10.1007/978-3-540-24730-2_25},
}
[BBL+06]
GerdBehrmann,
PatriciaBouyer,
Kim GuldstrandLarsen, and
RadekPelánek.
Lower and Upper Bounds in Zone-Based Abstractions of
Timed Automata.
International Journal on Software Tools for
Technology Transfer 8(3):204-215. Springer-Verlag, June 2006.
@article{sttt8(3)-BBLP,
author = {Behrmann, Gerd and Bouyer, Patricia and Larsen, Kim
Guldstrand and Pel{\'a}nek, Radek},
title = {Lower and Upper Bounds in Zone-Based Abstractions of
Timed Automata},
publisher = {Springer-Verlag},
journal = {International Journal on Software Tools for
Technology Transfer},
volume = {8},
number = {3},
pages = {204-215},
year = {2006},
month = jun,
doi = {10.1007/s10009-005-0190-0},
}
[BBL+15]
NikolaBeneš,
PetrBezdek,
Kim GuldstrandLarsen, and
JiříSrba.
Language Emptiness of Continuous-Time Parametric
Timed Automata.
In ICALP'15,
Lecture Notes in Computer Science 9135, pages 69-81. Springer-Verlag, July 2015.
@inproceedings{icalp2015-BBLS,
author = {Bene{{s}}, Nikola and Bezdek, Petr and Larsen, Kim
Guldstrand and Srba, Ji{ r}{\'\i}},
title = {Language Emptiness of Continuous-Time Parametric
Timed Automata},
editor = {Halld{\'o}rsson, Magn{\'u}s M. and Iwana, Kazuo and
Kobayashi, Naoki and Speckmann, Bettina},
booktitle = {{P}roceedings of the 42nd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'15)~-- Part~{II}},
acronym = {{ICALP}'15},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9135},
pages = {69-81},
year = {2015},
month = jul,
doi = {10.1007/978-3-662-47666-6_6},
}
[BBM06]
RamziBen Salah,
MariusBozga, and
OdedMaler.
On Interleaving in Timed Automata.
In CONCUR'06,
Lecture Notes in Computer Science 4137, pages 465-476. Springer-Verlag, August 2006.
@inproceedings{concur2006-BBM,
author = {Ben{~}Salah, Ramzi and Bozga, Marius and Maler,
Oded},
title = {On Interleaving in Timed Automata},
editor = {Baier, {\relax Ch}ristel and Hermanns, Holger},
booktitle = {{P}roceedings of the 17th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'06)},
acronym = {{CONCUR}'06},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {4137},
pages = {465-476},
year = {2006},
month = aug,
}
[BBM06]
PatriciaBouyer,
ThomasBrihaye, and
NicolasMarkey.
Improved Undecidability Results on Weighted Timed
Automata.
Information Processing Letters 98(5):188-194. Elsevier, June 2006.
Abstract
In this paper, we improve two recent undecidability
results of Brihaye, Bruyè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.
@article{ipl98(5)-BBM,
author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and
Markey, Nicolas},
title = {Improved Undecidability Results on Weighted Timed
Automata},
publisher = {Elsevier},
journal = {Information Processing Letters},
volume = {98},
number = {5},
pages = {188-194},
year = {2006},
month = jun,
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.},
}
[BBM10]
PatriciaBouyer,
RomainBrenguier, and
NicolasMarkey.
Nash Equilibria for Reachability Objectives in
Multi-player Timed Games.
In CONCUR'10,
Lecture Notes in Computer Science 6269, pages 192-206. Springer-Verlag, September 2010.
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{concur2010-BBM,
author = {Bouyer, Patricia and Brenguier, Romain and Markey,
Nicolas},
title = {{N}ash Equilibria for Reachability Objectives in
Multi-player Timed Games},
editor = {Gastin, Paul and Laroussinie, Fran{\c c}ois},
booktitle = {{P}roceedings of the 21st {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'10)},
acronym = {{CONCUR}'10},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {6269},
pages = {192-206},
year = {2010},
month = sep,
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.},
}
[BBM10]
PatriciaBouyer,
RomainBrenguier, and
NicolasMarkey.
Computing Equilibria in Two-Player Timed Games
via Turn-Based Finite Games.
In FORMATS'10,
Lecture Notes in Computer Science 6246, pages 62-76. Springer-Verlag, September 2010.
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.
@inproceedings{formats2010-BBM,
author = {Bouyer, Patricia and Brenguier, Romain and Markey,
Nicolas},
title = {Computing Equilibria in Two-Player Timed Games
{\textit{via}}~Turn-Based Finite Games},
editor = {Chatterjee, Krishnendu and Henzinger, Thomas A.},
booktitle = {{P}roceedings of the 8th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'10)},
acronym = {{FORMATS}'10},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {6246},
pages = {62-76},
year = {2010},
month = sep,
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.},
}
[BBM18]
A. R.Balasubramanian,
NathalieBertrand, and
NicolasMarkey.
Parameterized verification of synchronization in
constrained reconfigurable broadcast networks.
In TACAS'18 (Part II),
Lecture Notes in Computer Science 10806, pages 38-54. Springer-Verlag, April 2018.
Abstract
Reconfigurable broadcast networks provide a
convenient formalism for modelling and reasoning
about networks of mobile agents broadcasting
messages to other agents following some (evolving)
communication topology. The parameterized
verification of such models aims at checking whether
a given property holds irrespective of the initial
configuration (number of agents, initial states and
initial communication topology). We focus here on
the synchronization property, asking whether
all agents converge to a set of target states after
some execution. This problem is known to be
decidable in polynomial time when no constraints are
imposed on the evolution of the communication
topology (while it is undecidable for static
broadcast networks).
In this paper we
investigate how various constraints on
reconfigurations affect the decidability and
complexity of the synchronization problem.
In particular, we show that when bounding the number
of reconfigured links between two communications
steps by a constant, synchronization becomes
undecidable; on the other hand, synchronization
remains decidable in PTIME when the bound grows with
the number of agents.
@inproceedings{tacas2018-2-BBM,
author = {Balasubramanian, A. R. and Bertrand, Nathalie and
Markey, Nicolas},
title = {Parameterized verification of synchronization in
constrained reconfigurable broadcast networks},
editor = {Beyer, Dirk and Huisman, Marieke},
booktitle = {{P}roceedings of the 24th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'18)~-- {P}art~{II}},
acronym = {{TACAS}'18 (Part~{II})},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {10806},
pages = {38-54},
year = {2018},
month = apr,
doi = {10.1007/978-3-319-89963-3_3},
abstract = {Reconfigurable broadcast networks provide a
convenient formalism for modelling and reasoning
about networks of mobile agents broadcasting
messages to other agents following some (evolving)
communication topology. The parameterized
verification of such models aims at checking whether
a given property holds irrespective of the initial
configuration (number of agents, initial states and
initial communication topology). We~focus here on
the \emph{synchronization property}, asking whether
all agents converge to a set of target states after
some execution. This~problem is known to be
decidable in polynomial time when no constraints are
imposed on the evolution of the communication
topology (while~it~is undecidable for static
broadcast networks).\par In this paper we
investigate how various constraints on
reconfigurations affect the decidability and
complexity of the synchronization problem.
In~particular, we show that when bounding the number
of reconfigured links between two communications
steps by a constant, synchronization becomes
undecidable; on~the other hand, synchronization
remains decidable in PTIME when the bound grows with
the number of agents.},
}
[BBM+11]
PatriciaBouyer,
RomainBrenguier,
NicolasMarkey, and
MichaelUmmels.
Nash Equilibria in Concurrent Games with
Büchi Objectives.
In FSTTCS'11,
Leibniz International Proceedings in Informatics 13, pages 375-386. Leibniz-Zentrum für Informatik, December 2011.
Abstract
We study the problem of the existence (and
computation) of Nash equilibria in multi-player
concurrent games with Büchi-definable
objectives. First, when the objectives are Bü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üchi automata, and
prove that the problem then becomes
EXPTIME-complete. We prove PSPACE-completeness for
the case where the Büchi automata are 1-weak.
@inproceedings{fsttcs2011-BBMU,
author = {Bouyer, Patricia and Brenguier, Romain and Markey,
Nicolas and Ummels, Michael},
title = {{N}ash Equilibria in Concurrent Games with
{B}{\"u}chi Objectives},
editor = {Chakraborty, Supratik and Kumar, Amit},
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)},
acronym = {{FSTTCS}'11},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {13},
pages = {375-386},
year = {2011},
month = dec,
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.},
}
[BBM+12]
PatriciaBouyer,
RomainBrenguier,
NicolasMarkey, and
MichaelUmmels.
Concurrent games with ordered objectives.
In FoSSaCS'12,
Lecture Notes in Computer Science 7213, pages 301-315. Springer-Verlag, March 2012.
Abstract
We consider concurrent games played on graphs, in
which each player has several qualitative (e.g.
reachability or Bü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).
We
study two fundamental problems in that setting:
(1) the value problem, which aims at deciding
the existence of a strategy that ensures a given
payoff; (2) the 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{fossacs2012-BBMU,
author = {Bouyer, Patricia and Brenguier, Romain and Markey,
Nicolas and Ummels, Michael},
title = {Concurrent games with ordered objectives},
editor = {Birkedal, Lars},
booktitle = {{P}roceedings of the 15th {I}nternational
{C}onference on {F}oundations of {S}oftware
{S}cience and {C}omputation {S}tructure
({FoSSaCS}'12)},
acronym = {{FoSSaCS}'12},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {7213},
pages = {301-315},
year = {2012},
month = mar,
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.},
}
We study pure-strategy Nash equilibria in
multiplayer concurrent games, for a variety of
omega-regular objectives. For simple objectives
(e.g. reachability, Bü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.
@article{lmcs11(2)-BBMU,
author = {Bouyer, Patricia and Brenguier, Romain and Markey,
Nicolas and Ummels, Michael},
title = {Pure {N}ash Equilibria in Concurrent Games},
journal = {Logical Methods in Computer Science},
volume = {11},
number = {2:9},
year = {2015},
month = jun,
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.},
}
[BBR04]
ThomasBrihaye,
VéroniqueBruyère, and
Jean-FrançoisRaskin.
Model-checking for weighted timed automata.
In FORMATS-FTRTFT'04,
Lecture Notes in Computer Science 3253, pages 277-292. Springer-Verlag, September 2004.
@inproceedings{formats2004-BBR,
author = {Brihaye, {\relax Th}omas and Bruy{\`e}re,
V{\'e}ronique and Raskin, Jean-Fran{\c c}ois},
title = {Model-checking for weighted timed automata},
editor = {Lakhnech, Yassine and Yovine, Sergio},
booktitle = {{P}roceedings of the {J}oint {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'04) and {F}ormal
{T}echniques in {R}eal-Time and {F}ault-Tolerant
{S}ystems ({FTRTFT}'04)},
acronym = {{FORMATS-FTRTFT}'04},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {3253},
pages = {277-292},
year = {2004},
month = sep,
}
[BBR05]
ThomasBrihaye,
VéroniqueBruyère, and
Jean-FrançoisRaskin.
On Optimal Timed Strategies.
In FORMATS'05,
Lecture Notes in Computer Science 3829, pages 49-64. Springer-Verlag, September 2005.
@inproceedings{formats2005-BBR,
author = {Brihaye, {\relax Th}omas and Bruy{\`e}re,
V{\'e}ronique and Raskin, Jean-Fran{\c c}ois},
title = {On Optimal Timed Strategies},
editor = {Pettersson, Paul and Yi, Wang},
booktitle = {{P}roceedings of the 3rd {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'05)},
acronym = {{FORMATS}'05},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {3829},
pages = {49-64},
year = {2005},
month = sep,
doi = {10.1007/11603009_5},
}
[BBS01]
JiříBarnat,
LubošBrim, and
JitkaStříbrná.
Distributed LTL Model-Checking in SPIN.
In SPIN'01,
Lecture Notes in Computer Science 2057, pages 200-216. Springer-Verlag, May 2001.
@inproceedings{spin2001-BBS,
author = {Barnat, Ji{ r}{\'\i} and Brim, Lubo{ s} and
St{ r}{\'\i}brn{\'a}, Jitka},
title = {Distributed {LTL} Model-Checking in {SPIN}},
editor = {Dwyer, Matthew B.},
booktitle = {{P}roceedings of the 8th {I}nternational {SPIN}
{W}orkshop ({SPIN}'01)},
acronym = {{SPIN}'01},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {2057},
pages = {200-216},
year = {2001},
month = may,
}
[BC03]
MarcoBenedetti and
AlessandroCimatti.
Bounded Model Checking for Past LTL.
In TACAS'03,
Lecture Notes in Computer Science 2619, pages 18-33. Springer-Verlag, April 2003.
@inproceedings{tacas2003-BC,
author = {Benedetti, Marco and Cimatti, Alessandro},
title = {Bounded Model Checking for Past {LTL}},
editor = {Garavel, Hubert and Hatcliff, John},
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)},
acronym = {{TACAS}'03},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {2619},
pages = {18-33},
year = {2003},
month = apr,
}
[BC05]
PatriciaBouyer and
FabriceChevalier.
On Conciseness of Extensions of Timed Automata.
Journal of Automata, Languages and Combinatorics 10(4):393-405. 2005.
@article{jalc10(4)-BC,
author = {Bouyer, Patricia and Chevalier, Fabrice},
title = {On Conciseness of Extensions of Timed Automata},
journal = {Journal of Automata, Languages and Combinatorics},
volume = {10},
number = {4},
pages = {393-405},
year = {2005},
}
[BC06]
PatriciaBouyer and
FabriceChevalier.
On the Control of Timed and Hybrid Systems.
EATCS Bulletin 89:79-96. EATCS, June 2006.
@article{eatcs-bull89()-BC,
author = {Bouyer, Patricia and Chevalier, Fabrice},
title = {On the Control of Timed and Hybrid Systems},
publisher = {EATCS},
journal = {EATCS Bulletin},
volume = {89},
pages = {79-96},
year = {2006},
month = jun,
}
[BC10]
LubošBrim and
JakubChaloupka.
Using Strategy Improvement to Stay Alive.
Technical Report FIMU-RS-2010-03, Faculty of Informatics, Masaryk University, Brno,
Czech Republic,
March 2010.
@techreport{FIMU-RS-2010-03-BC,
author = {Brim, Lubo{ s} and Chaloupka, Jakub},
title = {Using Strategy Improvement to Stay Alive},
number = {FIMU-RS-2010-03},
year = {2010},
month = mar,
institution = {Faculty of Informatics, Masaryk University, Brno,
Czech Republic},
}
[BCC98]
SergeyBerezin,
Sérgio Vale AguiarCampos, and
Edmund M.Clarke.
Compositional Reasoning in Model Checking.
In COMPOS'97,
Lecture Notes in Computer Science 1536, pages 81-102. Springer-Verlag, 1998.
@inproceedings{compos1997-BCC,
author = {Berezin, Sergey and Campos, S{\'e}rgio Vale Aguiar
and Clarke, Edmund M.},
title = {Compositional Reasoning in Model Checking},
editor = {de Roever, Willem-Paul and Langmaack, Hans and
Pnueli, Amir},
booktitle = {{R}evised {L}ectures of the 1st {I}nternational
{S}ymposium on {C}ompositionality: {T}he
{S}ignificant {D}ifference ({COMPOS}'97)},
acronym = {{COMPOS}'97},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {1536},
pages = {81-102},
year = {1998},
confyear = {1997},
confmonth = {9},
}
[BCC+03]
ArminBiere,
AlessandroCimatti,
Edmund M.Clarke,
OferStrichman, and
YunshanZhu.
Bounded Model Checking.
In MarvinZelkowitz (eds.),
Highly Dependable Software,
Advances in Computers 58, pages 117-148. Academic Press, 2003.
@incollection{AC58-BCCSZ,
author = {Biere, Armin and Cimatti, Alessandro and Clarke,
Edmund M. and Strichman, Ofer and Zhu, Yunshan},
title = {Bounded Model Checking},
editor = {Zelkowitz, Marvin},
booktitle = {Highly Dependable Software},
publisher = {Academic Press},
series = {Advances in Computers},
volume = {58},
pages = {117-148},
chapter = {3},
year = {2003},
}
[BCC+99]
ArminBiere,
AlessandroCimatti,
Edmund M.Clarke, and
YunshanZhu.
Symbolic Model Checking without BDDs.
In TACAS'99,
Lecture Notes in Computer Science 1579, pages 193-207. Springer-Verlag, March 1999.
@inproceedings{tacas1999-BCCZ,
author = {Biere, Armin and Cimatti, Alessandro and Clarke,
Edmund M. and Zhu, Yunshan},
title = {Symbolic Model Checking without {BDD}s},
editor = {Cleaveland, Rance},
booktitle = {{P}roceedings of the 5th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'99)},
acronym = {{TACAS}'99},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {1579},
pages = {193-207},
year = {1999},
month = mar,
}
[BCD+07]
GerdBehrmann,
AgnèsCougnard,
AlexandreDavid,
EmmanuelFleury,
Kim GuldstrandLarsen, and
DidierLime.
UPPAAL-Tiga: Time for Playing Games!.
In CAV'07,
Lecture Notes in Computer Science 4590, pages 121-125. Springer-Verlag, July 2007.
@inproceedings{cav2007-BCDFLL,
author = {Behrmann, Gerd and Cougnard, Agn{\`e}s and David,
Alexandre and Fleury, Emmanuel and Larsen, Kim
Guldstrand and Lime, Didier},
title = {{UPPAAL-Tiga}: Time for Playing Games!},
editor = {Damm, Werner and Hermanns, Holger},
booktitle = {{P}roceedings of the 19th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'07)},
acronym = {{CAV}'07},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {4590},
pages = {121-125},
year = {2007},
month = jul,
}
[BCD+11]
LubošBrim,
JakubChaloupka,
LaurentDoyen,
RaffaellaGentilini, and
Jean-FrançoisRaskin.
Faster algorithms for mean-payoff games.
Formal Methods in System Design 38(2):97-118. Springer-Verlag, April 2011.
@article{fmsd38(2)-BCDGR,
author = {Brim, Lubo{ s} and Chaloupka, Jakub and Doyen,
Laurent and Gentilini, Raffaella and Raskin,
Jean-Fran{\c c}ois},
title = {Faster algorithms for mean-payoff games},
publisher = {Springer-Verlag},
journal = {Formal Methods in System Design},
volume = {38},
number = {2},
pages = {97-118},
year = {2011},
month = apr,
doi = {10.1007/s10703-010-0105-x},
}
[BCE+98]
Jean-JacquesBorrelly,
ÈveCostemaniere,
BernardEspiau,
KonstantinosKapellos,
RogerPissard-Gibollet,
DanielSimon, and
NicolasTurro.
The ORCCAD Architecture.
International Journal of Robotics Research 17(4):338-359. April 1998.
@article{ijrr17(4)-BCEKPST,
author = {Borrelly, Jean-Jacques and Costemaniere, {\`E}ve and
Espiau, Bernard and Kapellos, Konstantinos and
Pissard{-}Gibollet, Roger and Simon, Daniel and
Turro, Nicolas},
title = {The {ORCCAD} Architecture},
journal = {International Journal of Robotics Research},
volume = {17},
number = {4},
pages = {338-359},
year = {1998},
month = apr,
}
[BCF03]
HarryBuhrman,
RichardChang, and
LanceFortnow.
One Bit of Advice.
In STACS'03,
Lecture Notes in Computer Science 2607, pages 547-558. Springer-Verlag, February 2003.
@inproceedings{stacs2003-BCF,
author = {Buhrman, Harry and Chang, Richard and Fortnow,
Lance},
title = {One Bit of Advice},
editor = {Alt, Helmut and Habib, Michel},
booktitle = {{P}roceedings of the 20th {S}ymposium on
{T}heoretical {A}spects of {C}omputer {S}cience
({STACS}'03)},
acronym = {{STACS}'03},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {2607},
pages = {547-558},
year = {2003},
month = feb,
}
[BCF+04]
PatriciaBouyer,
FranckCassez,
EmmanuelFleury, and
Kim GuldstrandLarsen.
Optimal Strategies in Priced Timed Game Automata.
In FSTTCS'04,
Lecture Notes in Computer Science 3328, pages 148-160. Springer-Verlag, December 2004.
@inproceedings{fsttcs2004-BCFL,
author = {Bouyer, Patricia and Cassez, Franck and Fleury,
Emmanuel and Larsen, Kim Guldstrand},
title = {Optimal Strategies in Priced Timed Game Automata},
editor = {Lodaya, Kamal and Mahajan, Meena},
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)},
acronym = {{FSTTCS}'04},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {3328},
pages = {148-160},
year = {2004},
month = dec,
}
[BCF+04]
PatriciaBouyer,
FranckCassez,
EmmanuelFleury, and
Kim GuldstrandLarsen.
Optimal Strategies in Priced Timed Games.
Research Report RS-04-4, Basic Research in Computer Science, Aalborg
University, Denmark,
February 2004.
@techreport{TR-brics04-4,
author = {Bouyer, Patricia and Cassez, Franck and Fleury,
Emmanuel and Larsen, Kim Guldstrand},
title = {Optimal Strategies in Priced Timed Games},
number = {RS-04-4},
year = {2004},
month = feb,
institution = {Basic Research in Computer Science, Aalborg
University, Denmark},
type = {Research Report},
}
[BCG88]
Michael C.Browne,
Edmund M.Clarke, and
OrnaGrumberg.
Characterizing Finite Kripke Structures in
Propositional Temporal Logic.
Theoretical Computer Science 59(1-2):115-131. Elsevier, July 1988.
@article{tcs59(1-2)-BCG,
author = {Browne, Michael C. and Clarke, Edmund M. and
Grumberg, Orna},
title = {Characterizing Finite {K}ripke Structures in
Propositional Temporal Logic},
publisher = {Elsevier},
journal = {Theoretical Computer Science},
volume = {59},
number = {1-2},
pages = {115-131},
year = {1988},
month = jul,
}
[BCG+92]
Samuel R.Buss,
Stephen A.Cook,
VineetGupta, and
VijayaRamachandran.
An Optimal Parallel Algorithm for Formula
Evaluation.
SIAM Journal on Computing 21(4):755-780. Society for Industrial and Applied Math., August 1992.
@article{siamcomp21(4)-BCGR,
author = {Buss, Samuel R. and Cook, Stephen A. and Gupta,
Vineet and Ramachandran, Vijaya},
title = {An Optimal Parallel Algorithm for Formula
Evaluation},
publisher = {Society for Industrial and Applied Math.},
journal = {SIAM Journal on Computing},
volume = {21},
number = {4},
pages = {755-780},
year = {1992},
month = aug,
}
[BCH+11]
UdiBoker,
KrishnenduChatterjee,
Thomas A.Henzinger, and
OrnaKupferman.
Temporal Specifications with Accumulative Values.
In LICS'11,
pages 43-52.
IEEE Comp. Soc. Press, June 2011.
@inproceedings{lics2011-BCHK,
author = {Boker, Udi and Chatterjee, Krishnendu and Henzinger,
Thomas A. and Kupferman, Orna},
title = {Temporal Specifications with Accumulative Values},
booktitle = {{P}roceedings of the 26th {A}nnual {S}ymposium on
{L}ogic in {C}omputer {S}cience ({LICS}'11)},
acronym = {{LICS}'11},
publisher = {IEEE Comp. Soc. Press},
pages = {43-52},
year = {2011},
month = jun,
doi = {10.1109/LICS.2011.33},
}
[BCH+14]
UdiBoker,
KrishnenduChatterjee,
Thomas A.Henzinger, and
OrnaKupferman.
Temporal Specifications with Accumulative Values.
ACM Transactions on Computational Logic 15(4):27:1-27:25. ACM Press, August 2014.
@article{tocl15(4)-BCHK,
author = {Boker, Udi and Chatterjee, Krishnendu and Henzinger,
Thomas A. and Kupferman, Orna},
title = {Temporal Specifications with Accumulative Values},
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
volume = {15},
number = {4},
pages = {27:1-27:25},
year = {2014},
month = aug,
doi = {10.1145/2629686},
}
[BCK+01]
LubošBrim,
IvanaČerna,
PavelKrčál, and
RadekPelánek.
Distributed LTL Model Checking Based on Negative
Cycle Detection.
In FSTTCS'01,
Lecture Notes in Computer Science 2245, pages 96-107. Springer-Verlag, December 2001.
@inproceedings{fsttcs2001-BCKP,
author = {Brim, Lubo{ s} and {{C}}erna, Ivana and
Kr{{c}}{\'a}l, Pavel and Pel{\'a}nek, Radek},
title = {Distributed {LTL} Model Checking Based on Negative
Cycle Detection},
editor = {Hariharan, Ramesh and Mukund, Madhavan and Vinay,
V.},
booktitle = {{P}roceedings of the 21st {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience ({FSTTCS}'01)},
acronym = {{FSTTCS}'01},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {2245},
pages = {96-107},
year = {2001},
month = dec,
}
[BCM05]
PatriciaBouyer,
FabriceChevalier, and
NicolasMarkey.
On the Expressiveness of TPTL and MTL.
In FSTTCS'05,
Lecture Notes in Computer Science 3821, pages 432-443. Springer-Verlag, December 2005.
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.
@inproceedings{fsttcs2005-BCM,
author = {Bouyer, Patricia and Chevalier, Fabrice and Markey,
Nicolas},
title = {On the Expressiveness of {TPTL} and {MTL}},
editor = {Ramanujam, R. and Sen, Sandeep},
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)},
acronym = {{FSTTCS}'05},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {3821},
pages = {432-443},
year = {2005},
month = dec,
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 \textbf{F} modality can be translated into
MTL.},
}
[BCM10]
PatriciaBouyer,
FabriceChevalier, and
NicolasMarkey.
On the Expressiveness of TPTL and MTL.
Information and Computation 208(2):97-116. Elsevier, February 2010.
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 can be expressed
in MTL. More generally, we show that TPTL formulae
using only modality F can be translated into MTL.
@article{icomp208(2)-BCM,
author = {Bouyer, Patricia and Chevalier, Fabrice and Markey,
Nicolas},
title = {On the Expressiveness of {TPTL} and {MTL}},
publisher = {Elsevier},
journal = {Information and Computation},
volume = {208},
number = {2},
pages = {97-116},
year = {2010},
month = feb,
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.},
}
[BCM16]
PatriciaBouyer,
MaximilienColange, and
NicolasMarkey.
Symbolic Optimal Reachability in Weighted Timed
Automata.
In CAV'16,
Lecture Notes in Computer Science 9779, pages 513-530. Springer-Verlag, July 2016.
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{cav2016-BCM,
author = {Bouyer, Patricia and Colange, Maximilien and Markey,
Nicolas},
title = {Symbolic Optimal Reachability in Weighted Timed
Automata},
editor = {Chaudhuri, Swarat and Farzan, Azadeh},
booktitle = {{P}roceedings of the 28th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'16)},
acronym = {{CAV}'16},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9779},
pages = {513-530},
year = {2016},
month = jul,
doi = {10.1007/978-3-319-41528-4_28},
url = {http://arxiv.org/abs/1602.00481},
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.},
}
[BCM+92]
Jerry R.Burch,
Edmund M.Clarke,
Kenneth L.McMillan,
David L.Dill, and
L. J.Hwang.
Symbolic model checking: 1020 states and
beyond.
Information and Computation 98(2):142-170. Academic Press, June 1992.
@article{icomp98(2)-BCMDH,
author = {Burch, Jerry R. and Clarke, Edmund M. and McMillan,
Kenneth L. and Dill, David L. and Hwang, L. J.},
title = {Symbolic model checking: {\(10^{20}\)} states and
beyond},
publisher = {Academic Press},
journal = {Information and Computation},
volume = {98},
number = {2},
pages = {142-170},
year = {1992},
month = jun,
}
[BCO+92]
FrançoisBaccelli,
GuyCohen,
Geert JanOlsder, and
Jean-PierreQuadrat.
Shynchronization and Linearity. An Algebra For
Discrete Event Systems.
John Wiley & Sons, 1992.
@book{BCOQ-des2001,
author = {Baccelli, Fran{\c c}ois and Cohen, Guy and Olsder,
Geert Jan and Quadrat, Jean-Pierre},
title = {Shynchronization and Linearity. An Algebra For
Discrete Event Systems},
publisher = {John Wiley \& Sons},
year = {1992},
url = {http://www-rocq.inria.fr/metalau/cohen/SED/book-online.html},
}
[BCZ99]
ArminBiere,
Edmund M.Clarke, and
YunshanZhu.
Combining Local and Global Model Checking.
In SMC'99,
Electronic Notes in Theoretical Computer Science 23(2).
Elsevier, July 1999.
@inproceedings{smc1999-BCZ,
author = {Biere, Armin and Clarke, Edmund M. and Zhu, Yunshan},
title = {Combining Local and Global Model Checking},
editor = {Cimatti, Alessandro and Grumberg, Orna},
booktitle = {{P}roceedings of the 1st {I}nternational {W}orkshop
on {S}ymbolic {M}odel {C}hecking ({SMC}'99)},
acronym = {{SMC}'99},
publisher = {Elsevier},
series = {Electronic Notes in Theoretical Computer Science},
volume = {23},
number = {2},
year = {1999},
month = jul,
}
[BD00]
BéatriceBérard and
CatherineDufourd.
Timed Automata and Additive Clock Constraints.
Information Processing Letters 75(1-2):1-7. Elsevier, July 2000.
@article{ipl75(1-2)-BD,
author = {B{\'e}rard, B{\'e}atrice and Dufourd, Catherine},
title = {Timed Automata and Additive Clock Constraints},
publisher = {Elsevier},
journal = {Information Processing Letters},
volume = {75},
number = {1-2},
pages = {1-7},
year = {2000},
month = jul,
}
[BDF+04]
PatriciaBouyer,
CatherineDufourd,
EmmanuelFleury, and
AntoinePetit.
Updatable timed Automata.
Theoretical Computer Science 321(2-3):291-345. Elsevier, August 2004.
@article{tcs321(2-3)-BDFP,
author = {Bouyer, Patricia and Dufourd, Catherine and Fleury,
Emmanuel and Petit, Antoine},
title = {Updatable timed Automata},
publisher = {Elsevier},
journal = {Theoretical Computer Science},
volume = {321},
number = {2-3},
pages = {291-345},
year = {2004},
month = aug,
doi = {10.1016/j.tcs.2004.04.003},
}
@inproceedings{icalp2011(2)-BDGORW,
author = {Brihaye, {\relax Th}omas and Doyen, Laurent and
Geeraerts, Gilles and Ouaknine, Jo{\"e}l and Raskin,
Jean-Fran{\c c}ois and Worrell, James},
title = {On Reachability for Hybrid Automata over Bounded
Time},
editor = {Aceto, Luca and Henzinger, Monika and Sgall, Ji{
r}{\'\i}},
booktitle = {{P}roceedings of the 38th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'11)~-- Part~{II}},
acronym = {{ICALP}'11},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {6756},
pages = {416-427},
year = {2011},
month = jul,
}
[BDG+98]
BéatriceBérard,
VolkerDiekert,
PaulGastin, and
AntoinePetit.
Characterization of the Expressive Power of Silent
Transitions in Timed Automata.
Fundamenta Informaticae 36(2-3):145-182. IOS Press, November 1998.
@article{fundi36(2-3)-BDGP,
author = {B{\'e}rard, B{\'e}atrice and Diekert, Volker and
Gastin, Paul and Petit, Antoine},
title = {Characterization of the Expressive Power of Silent
Transitions in Timed Automata},
publisher = {IOS Press},
journal = {Fundamenta Informaticae},
volume = {36},
number = {2-3},
pages = {145-182},
year = {1998},
month = nov,
}
[BDH+06]
DietmarBerwanger,
AnujDawar,
PaulHunter, and
StephanKreutzer.
DAG-Width and Parity Games.
In STACS'06,
Lecture Notes in Computer Science 3884, pages 524-536. Springer-Verlag, February 2006.
@inproceedings{stacs2006-BDHK,
author = {Berwanger, Dietmar and Dawar, Anuj and Hunter, Paul
and Kreutzer, Stephan},
title = {{DAG}-Width and Parity Games},
editor = {Durand, Bruno and Thomas, Wolfgang},
booktitle = {{P}roceedings of the 23rd {S}ymposium on
{T}heoretical {A}spects of {C}omputer {S}cience
({STACS}'06)},
acronym = {{STACS}'06},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {3884},
pages = {524-536},
year = {2006},
month = feb,
doi = {10.1007/11672142_43},
}
@proceedings{cassting-syncop2016-DJMS,
title = {{P}roceedings of the {C}assting Workshop on {G}ames
for the {S}ynthesis of {C}omplex {S}ystems
({C}assting'16) and of the 3rd {I}nternational
{W}orkshop on {S}ynthesis of {C}omplex {P}arameters
({S}yn{C}o{P}'16)},
editor = {Brihaye, {\relax Th}omas and Delahaye, Beno{\^\i}t
and Jezequel, Lo{\"\i}g and Markey, Nicolas and
Srba, Ji{ r}{\'\i}},
booktitle = {{P}roceedings of the {C}assting Workshop on {G}ames
for the {S}ynthesis of {C}omplex {S}ystems
({C}assting'16) and of the 3rd {I}nternational
{W}orkshop on {S}ynthesis of {C}omplex {P}arameters
({S}yn{C}o{P}'16)},
acronym = {{C}assting{{\slash}}{S}yn{C}o{P}'16},
series = {Electronic Proceedings in Theoretical Computer
Science},
volume = {220},
year = {2016},
month = jul,
confyear = {2016},
confmonth = {4},
doi = {10.4204/EPTCS.220},
url = {http://eptcs.web.cse.unsw.edu.au/
content.cgi?CASSTINGSynCoP2016},
}
[BDL12]
BenediktBollig,
NormannDecker, and
MartinLeucker.
Frequency Linear-time Temporal Logic.
In TASE'12,
pages 85-92.
IEEE Comp. Soc. Press, July 2012.
@inproceedings{tase2012-BDL,
author = {Bollig, Benedikt and Decker, Normann and Leucker,
Martin},
title = {Frequency Linear-time Temporal Logic},
editor = {Margaria, Tiziana and Qiu, Zongyang and Yang,
Hongli},
booktitle = {{P}roceedings of the 6th {I}nternational {S}ymposium
on {T}heoretical {A}spects of {S}oftware
{E}ngineering ({TASE}'12)},
acronym = {{TASE}'12},
publisher = {IEEE Comp. Soc. Press},
pages = {85-92},
year = {2012},
month = jul,
doi = {10.1109/TASE.2012.43},
}
[BDL+06]
GerdBehrmann,
AlexandreDavid,
Kim GuldstrandLarsen,
JohnHåkansson,
PaulPettersson,
WangYi, and
MartijnHendriks.
UPPAAL 4.0.
In QEST'06,
pages 125-126.
IEEE Comp. Soc. Press, September 2006.
@inproceedings{qest2006-BDLHPYH,
author = {Behrmann, Gerd and David, Alexandre and Larsen, Kim
Guldstrand and H{\aa}kansson, John and Pettersson,
Paul and Yi, Wang and Hendriks, Martijn},
title = {UPPAAL~4.0},
booktitle = {{P}roceedings of the 3rd {I}nternational
{C}onference on {Q}uantitative {E}valuation of
{S}ystems ({QEST}'06)},
acronym = {{QEST}'06},
publisher = {IEEE Comp. Soc. Press},
pages = {125-126},
year = {2006},
month = sep,
doi = {10.1109/QEST.2006.59},
}
[BDL+14]
PeterBulychev,
AlexandreDavid,
Kim GuldstrandLarsen, and
GuangyuanLi.
Efficient Controller Synthesis for a fragment of
MTL0,&infin.
Acta Informatica 51(3-4):165-192. Springer-Verlag, June 2014.
@article{acta51(3-4)-BDLL,
author = {Bulychev, Peter and David, Alexandre and Larsen, Kim
Guldstrand and Li, Guangyuan},
title = {Efficient Controller Synthesis for a fragment of
{{\(\textsf{MTL}_{0,\infty}\)}}},
publisher = {Springer-Verlag},
journal = {Acta Informatica},
volume = {51},
number = {3-4},
pages = {165-192},
year = {2014},
month = jun,
doi = {10.1007/s00236-013-0189-z},
}
[BDL+12]
PeterBulychev,
AlexandreDavid,
Kim GuldstrandLarsen,
AxelLegay,
GuangyuanLi,
Danny BøgstedPoulsen, and
AmélieStainer.
Monitor-based statistical model checking for
weighted metric temporal logic.
In LPAR'12,
Lecture Notes in Computer Science 7180, pages 168-182. Springer-Verlag, March 2012.
@inproceedings{lpar2012-BDLLLPS,
author = {Bulychev, Peter and David, Alexandre and Larsen, Kim
Guldstrand and Legay, Axel and Li, Guangyuan and
Poulsen, Danny B{\o}gsted and Stainer, Am{\'e}lie},
title = {Monitor-based statistical model checking for
weighted metric temporal logic},
editor = {Bj{\o}rner, Nikolaj and Voronkov, Andrei},
booktitle = {{P}roceedings of the 18th {I}nternational
{C}onference {L}ogic {P}rogramming and {A}utomated
{R}easoning ({LPAR}'12)},
acronym = {{LPAR}'12},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {7180},
pages = {168-182},
year = {2012},
month = mar,
doi = {10.1007/978-3-642-28717-6_15},
}
[BDL+12]
PeterBulychev,
AlexandreDavid,
Kim GuldstrandLarsen,
AxelLegay,
MariusMikučionis, and
Danny BøgstedPoulsen.
Checking and Distributing Statistical Model
Checking.
In NFM'12,
Lecture Notes in Computer Science 7226, pages 449-463. Springer-Verlag, April 2012.
@inproceedings{nasaFM2012-BDLLMP,
author = {Bulychev, Peter and David, Alexandre and Larsen, Kim
Guldstrand and Legay, Axel and Miku{{c}}ionis,
Marius and Poulsen, Danny B{\o}gsted},
title = {Checking and Distributing Statistical Model
Checking},
editor = {Goodloe, Alwyn and Person, Suzette},
booktitle = {{P}roceedings of the 4th {NASA} {F}ormal {M}ethods
{S}ymposium ({NFM}'12)},
acronym = {{NFM}'12},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {7226},
pages = {449-463},
year = {2012},
month = apr,
}
[BDL+09]
ThomasBrihaye,
ArnaudDa Costa,
FrançoisLaroussinie, and
NicolasMarkey.
ATL with Strategy Contexts and Bounded Memory.
In LFCS'09,
Lecture Notes in Computer Science 5407, pages 92-106. Springer-Verlag, January 2009.
Abstract
We extend the alternating-time temporal logics ATL
and ATL* with strategy
contexts and memory constraints: the first
extension make strategy quantifiers to not
"forget" the strategies being executed by the
other players. The second extension allows strategy
quantifiers to restrict to memoryless or
bounded-memory strategies.
We first consider
expressiveness issues. We show that our logics can
express important properties such as equilibria, and
we formally compare them with other similar
formalisms (ATL, ATL*, Game Logic,
Strategy Logic, ...). We then address the problem of
model-checking for our logics, providing a PSPACE
algoritm for the sublogics involving only memoryless
strategies and an EXPSPACE algorithm for the
bounded-memory case.
@inproceedings{lfcs2009-BDLM,
author = {Brihaye, {\relax Th}omas and Da{~}Costa, Arnaud and
Laroussinie, Fran{\c c}ois and Markey, Nicolas},
title = {{ATL} with Strategy Contexts and Bounded Memory},
editor = {Artemov, Sergei N. and Nerode, Anil},
booktitle = {{P}roceedings of the {I}nternational {S}ymposium
{L}ogical {F}oundations of {C}omputer {S}cience
({LFCS}'09)},
acronym = {{LFCS}'09},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {5407},
pages = {92-106},
year = {2009},
month = jan,
doi = {10.1007/978-3-540-92687-0_7},
abstract = {We extend the alternating-time temporal logics ATL
and ATL\textsuperscript{*} with \emph{strategy
contexts} and \emph{memory constraints}: the first
extension make strategy quantifiers to not
{"}forget{"} the strategies being executed by the
other players. The second extension allows strategy
quantifiers to restrict to memoryless or
bounded-memory strategies.\par We first consider
expressiveness issues. We show that our logics can
express important properties such as equilibria, and
we formally compare them with other similar
formalisms (ATL, ATL\textsuperscript{*}, Game Logic,
Strategy Logic,~...). We~then address the problem of
model-checking for our logics, providing a PSPACE
algoritm for the sublogics involving only memoryless
strategies and an EXPSPACE algorithm for the
bounded-memory case.},
}
[BDL+97]
JoshuaBerman,
ArthurDrisko,
FrançoisLemieux,
CristopherMoore, and
DenisThérien.
Circuit and Expressions with Non-Associative Gates.
In CoCo'97,
pages 193-203.
IEEE Comp. Soc. Press, June 1997.
@inproceedings{coco1997-BDLMT,
author = {Berman, Joshua and Drisko, Arthur and Lemieux,
Fran{\c c}ois and Moore, Cristopher and Th{\'e}rien,
Denis},
title = {Circuit and Expressions with Non-Associative Gates},
booktitle = {{P}roceedings of the 12th {A}nnual {IEEE}
{C}onference on {C}omputational {C}omplexity
({CoCo}'97)},
acronym = {{CoCo}'97},
publisher = {IEEE Comp. Soc. Press},
pages = {193-203},
year = {1997},
month = jun,
}
[BDL+11]
GerdBehrmann,
AlexandreDavid,
Kim GuldstrandLarsen,
PaulPettersson, and
WangYi.
Developing UPPAAL over 15 years.
Software – Practice and Experience 41(2):133-142. IEEE Comp. Soc. Press, February 2011.
@article{spe41(2)-ADGPY,
author = {Behrmann, Gerd and David, Alexandre and Larsen, Kim
Guldstrand and Pettersson, Paul and Yi, Wang},
title = {Developing {UPPAAL} over 15~years},
publisher = {IEEE Comp. Soc. Press},
journal = {Software~-- Practice and Experience},
volume = {41},
number = {2},
pages = {133-142},
year = {2011},
month = feb,
}
[BDM+03]
PatriciaBouyer,
DeepakD'Souza,
ParthasarathyMadhusudan, and
AntoinePetit.
Timed Control with Partial Observability.
In CAV'03,
Lecture Notes in Computer Science 2725, pages 180-192. Springer-Verlag, July 2003.
@inproceedings{cav2003-BDMP,
author = {Bouyer, Patricia and D'Souza, Deepak and Madhusudan,
Parthasarathy and Petit, Antoine},
title = {Timed Control with Partial Observability},
editor = {Hunt, Jr, Warren A. and Somenzi, Fabio},
booktitle = {{P}roceedings of the 15th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'03)},
acronym = {{CAV}'03},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {2725},
pages = {180-192},
year = {2003},
month = jul,
}
[BDM+09]
PatriciaBouyer,
MarieDuflot,
NicolasMarkey, and
GabrielRenault.
Measuring Permissivity in Finite Games.
In CONCUR'09,
Lecture Notes in Computer Science 5710, pages 196-210. Springer-Verlag, September 2009.
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
NP∩coNP for discounted and
mean penalties.
@inproceedings{concur2009-BDMR,
author = {Bouyer, Patricia and Duflot, Marie and Markey,
Nicolas and Renault, Gabriel},
title = {Measuring Permissivity in Finite Games},
editor = {Bravetti, Mario and Zavattaro, Gianluigi},
booktitle = {{P}roceedings of the 20th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'09)},
acronym = {{CONCUR}'09},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {5710},
pages = {196-210},
year = {2009},
month = sep,
doi = {10.1007/978-3-642-04081-8_14},
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.},
}
[BDR03]
VéroniqueBruyère,
EmmanuelDall'Olio, and
Jean-FrançoisRaskin.
Durations, Parametric Model Checking in Timed
Automata with Presburger Arithmetic.
In STACS'03,
Lecture Notes in Computer Science 2607, pages 687-698. Springer-Verlag, February 2003.
@inproceedings{stacs2003-BDR,
author = {Bruy{\`e}re, V{\'e}ronique and Dall'Olio, Emmanuel
and Raskin, Jean-Fran{\c c}ois},
title = {Durations, Parametric Model Checking in Timed
Automata with {P}resburger Arithmetic},
editor = {Alt, Helmut and Habib, Michel},
booktitle = {{P}roceedings of the 20th {S}ymposium on
{T}heoretical {A}spects of {C}omputer {S}cience
({STACS}'03)},
acronym = {{STACS}'03},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {2607},
pages = {687-698},
year = {2003},
month = feb,
}
[BDS+09]
HansBherer,
JulesDesharnais, and
RichardSt-Denis.
Control of Parameterized Discrete Event Systems.
Discrete Event Dynamic Systems 19(2):213-165. Kluwer Academic, June 2009.
@article{deds19(2)-BDSD,
author = {Bherer, Hans and Desharnais, Jules and St-Denis,
Richard},
title = {Control of Parameterized Discrete Event Systems},
publisher = {Kluwer Academic},
journal = {Discrete Event Dynamic Systems},
volume = {19},
number = {2},
pages = {213-165},
year = {2009},
month = jun,
doi = {10.1007/s10626-008-0040-9},
}
[Bea03]
DanièleBeauquier.
On probabilistic timed automata.
Theoretical Computer Science 292(1):65-84. Elsevier, January 2003.
@article{tcs292(1)-Bea,
author = {Beauquier, Dani{\`e}le},
title = {On~probabilistic timed automata},
publisher = {Elsevier},
journal = {Theoretical Computer Science},
volume = {292},
number = {1},
pages = {65-84},
year = {2003},
month = jan,
doi = {10.1016/S0304-3975(01)00215-8},
}
[Bed01]
NicolasBedon.
Logic over Words on Denumerable Ordinals.
Journal of Computer and System Sciences 63(3):394-431. Academic Press, November 2001.
@article{jcss63(3)-Bed,
author = {Bedon, Nicolas},
title = {Logic over Words on Denumerable Ordinals},
publisher = {Academic Press},
journal = {Journal of Computer and System Sciences},
volume = {63},
number = {3},
pages = {394-431},
year = {2001},
month = nov,
}
[BEG+15]
EndreBoros,
KhaledElbassioni,
VladimirGurvich, and
KazuhisaMakino.
Markov Decision Processes and Stochastic Games
with Total Effective Payoff.
In STACS'15,
Leibniz International Proceedings in Informatics 30, pages 103-115. Leibniz-Zentrum für Informatik, March 2015.
@inproceedings{stacs2015-BEGM,
author = {Boros, Endre and Elbassioni, Khaled and Gurvich,
Vladimir and Makino, Kazuhisa},
title = {{M}arkov Decision Processes and Stochastic Games
with Total Effective Payoff},
editor = {Mayr, Ernst W. and Ollinger, Nicolas},
booktitle = {{P}roceedings of the 32nd {S}ymposium on
{T}heoretical {A}spects of {C}omputer {S}cience
({STACS}'15)},
acronym = {{STACS}'15},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {30},
pages = {103-115},
year = {2015},
month = mar,
doi = {10.4230/LIPIcs.STACS.2015.103},
}
[Bei91]
RichardBeigel.
Bounded Queries to SAT and the Boolean
Hierarchy.
Theoretical Computer Science 84(2):199-223. Elsevier, 1991.
@article{tcs84(2)-Bei,
author = {Beigel, Richard},
title = {Bounded Queries to {SAT} and the {B}oolean
Hierarchy},
publisher = {Elsevier},
journal = {Theoretical Computer Science},
volume = {84},
number = {2},
pages = {199-223},
year = {1991},
}
@book{DP-Bel,
author = {Bellman, Richard},
title = {Dynamic Programming},
publisher = {Princeton University},
year = {1957},
}
[Bel58]
RichardBellman.
On a Routing Problem.
Quarterly of Applied Mathematics 16(1):87-90. 1958.
@article{qam16(1)-Bel,
author = {Bellman, Richard},
title = {On a Routing Problem},
journal = {Quarterly of Applied Mathematics},
volume = {16},
number = {1},
pages = {87-90},
year = {1958},
}
[BEM96]
Julian C.Bradfield,
JavierEsparza, and
AngelikaMader.
An effective tableau system for the linear time
mu-calculus.
In ICALP'96,
Lecture Notes in Computer Science 1099, pages 98-109. Springer-Verlag, July 1996.
@inproceedings{icalp1996-BEM,
author = {Bradfield, Julian C. and Esparza, Javier and Mader,
Angelika},
title = {An effective tableau system for the linear time
mu-calculus},
editor = {Meyer auf der Heide, Friedhelm and Monien, Burkhard},
booktitle = {{P}roceedings of the 23rd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'96)},
acronym = {{ICALP}'96},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {1099},
pages = {98-109},
year = {1996},
month = jul,
}
[Ber00]
GérardBerry.
The foundations of Esterel.
In Gordon D.Plotkin,
ColinStirling, and
MadsTofte (eds.),
Proof, Language, and Interaction – Essays in Honour
of Robin Milner.
MIT Press, 2000.
@incollection{PLI2000-Ber,
author = {Berry, G{\'e}rard},
title = {The foundations of {E}sterel},
editor = {Plotkin, Gordon D. and Stirling, Colin and Tofte,
Mads},
booktitle = {Proof, Language, and Interaction~-- Essays in Honour
of {R}obin {M}ilner},
publisher = {MIT Press},
pages = {425-454},
year = {2000},
}
[Bey01]
DirkBeyer.
Rabbit: Verification of Real-Time Systems.
In RT-TOOLS'01,
pages 13-21.
August 2001.
@inproceedings{rttools2001-Bey,
author = {Beyer, Dirk},
title = {Rabbit: Verification of Real-Time Systems},
editor = {Pettersson, Paul and Yovine, Sergio},
booktitle = {{P}roceedings of the 1st {W}orkshop on {R}eal-Time
{T}ools ({RT-TOOLS}'01)},
acronym = {{RT-TOOLS}'01},
pages = {13-21},
year = {2001},
month = aug,
}
[BF09]
PatriciaBouyer and
VojtěchForejt.
Reachability in Stochastic Timed Games.
In ICALP'09,
Lecture Notes in Computer Science 5556, pages 103-114. Springer-Verlag, July 2009.
@inproceedings{icalp2009-BF,
author = {Bouyer, Patricia and Forejt, Vojt{{e}}ch},
title = {Reachability in Stochastic Timed Games},
editor = {Albers, Susanne and Marchetti{-}Spaccamela Alberto
and Matias, Yossi and Nikoletseas, Sotiris and
Thomas, Wolfgang},
booktitle = {{P}roceedings of the 36th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'09)~-- Part~{II}},
acronym = {{ICALP}'09},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {5556},
pages = {103-114},
year = {2009},
month = jul,
}
[BFD02]
AlexanderBolotov,
Michael J.Fischer, and
ClareDixon.
On the Relationship between ω-Automata
and Temporal Logic Normal Forms.
Journal of Logic and Computation 12(4):561-581. Oxford University Press, August 2002.
@article{jlc12(4)-BFD,
author = {Bolotov, Alexander and Fischer, Michael J. and
Dixon, Clare},
title = {On the Relationship between {\(\omega\)}-Automata
and Temporal Logic Normal Forms},
publisher = {Oxford University Press},
journal = {Journal of Logic and Computation},
volume = {12},
number = {4},
pages = {561-581},
year = {2002},
month = aug,
}
[BFH09]
FelixBrandt,
FelixFischer, and
MarkusHolzer.
Symmetries and the complexity of pure Nash
equilibrium.
Journal of Computer and System Sciences 75(3):163-177. Elsevier, May 2009.
@article{jcss75(3)-BFH,
author = {Brandt, Felix and Fischer, Felix and Holzer, Markus},
title = {Symmetries and the complexity of pure {N}ash
equilibrium},
publisher = {Elsevier},
journal = {Journal of Computer and System Sciences},
volume = {75},
number = {3},
pages = {163-177},
year = {2009},
month = may,
}
[BFH+01]
GerdBehrmann,
AnsgarFehnker,
ThomasHune,
Kim GuldstrandLarsen,
PaulPettersson, and
JudiRomijn.
Efficient Guiding Towards Cost-Optimality in UPPAAL.
In TACAS'01,
Lecture Notes in Computer Science 2031, pages 174-188. Springer-Verlag, April 2001.
@inproceedings{tacas2001-BFHLPR,
author = {Behrmann, Gerd and Fehnker, Ansgar and Hune, Thomas
and Larsen, Kim Guldstrand and Pettersson, Paul and
Romijn, Judi},
title = {Efficient Guiding Towards Cost-Optimality in UPPAAL},
editor = {Margaria, Tiziana and Yi, Wang},
booktitle = {{P}roceedings of the 7th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'01)},
acronym = {{TACAS}'01},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {2031},
pages = {174-188},
year = {2001},
month = apr,
}
[BFH+01]
GerdBehrmann,
AnsgarFehnker,
ThomasHune,
Kim GuldstrandLarsen,
PaulPettersson,
JudiRomijn, and
FritsVaandrager.
Minimum-Cost Reachability for Priced Timed Automata.
In HSCC'01,
Lecture Notes in Computer Science 2034, pages 147-161. Springer-Verlag, March 2001.
@inproceedings{hscc2001-BFHLPRV,
author = {Behrmann, Gerd and Fehnker, Ansgar and Hune, Thomas
and Larsen, Kim Guldstrand and Pettersson, Paul and
Romijn, Judi and Vaandrager, Frits},
title = {Minimum-Cost Reachability for Priced Timed Automata},
editor = {Di{~}Benedetto, Maria Domenica and
Sangiovani{-}Vincentelli, Alberto L.},
booktitle = {{P}roceedings of the 4th {I}nternational {W}orkshop
on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
({HSCC}'01)},
acronym = {{HSCC}'01},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {2034},
pages = {147-161},
year = {2001},
month = mar,
doi = {10.1007/3-540-45351-2_15},
}
In this paper, we study one-clock priced timed
automata in which prices can grow linearly
(dp/dt=k) or exponentially
(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).
@inproceedings{hscc2010-BFLM,
author = {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim
Guldstrand and Markey, Nicolas},
title = {Timed Automata with Observers under Energy
Constraints},
editor = {Johansson, Karl Henrik and Yi, Wang},
booktitle = {{P}roceedings of the 13th {I}nternational {W}orkshop
on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
({HSCC}'10)},
acronym = {{HSCC}'10},
publisher = {ACM Press},
pages = {61-70},
year = {2010},
month = apr,
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).},
}
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.
@article{cacm54(9)-BFLM,
author = {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim
Guldstrand and Markey, Nicolas},
title = {Quantitative analysis of real-time systems using
priced timed automata},
publisher = {ACM Press},
journal = {Communications of the ACM},
volume = {54},
number = {9},
pages = {78-87},
year = {2011},
month = sep,
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.},
}
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).
@incollection{hmc2017-BFLMOW,
author = {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim
Guldstrand and Markey, Nicolas and Ouaknine,
Jo{\"e}l and Worrell, James},
title = {Model Checking Real-Time Systems},
editor = {Clarke, Edmund M. and Henzinger, Thomas A. and
Veith, Helmut and Bloem, Roderick},
booktitle = {Handbook of Model Checking},
publisher = {Springer-Verlag},
pages = {1001-1046},
chapter = {29},
year = {2018},
month = may,
doi = {10.1007/978-3-319-10575-8_29},
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).},
}
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 (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
(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{formats2008-BFLMS,
author = {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim
Guldstrand and Markey, Nicolas and Srba, Ji{
r}{\'\i}},
title = {Infinite Runs in Weighted Timed Automata with Energy
Constraints},
editor = {Cassez, Franck and Jard, Claude},
booktitle = {{P}roceedings of the 6th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'08)},
acronym = {{FORMATS}'08},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {5215},
pages = {33-47},
year = {2008},
month = sep,
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.},
}
[BFM15]
PatriciaBouyer,
ErwinFang, and
NicolasMarkey.
Permissive strategies in timed automata and games.
In AVOCS'15,
Electronic Communications of the EASST 72.
European Association of Software Science and
Technology, September 2015.
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{avocs2015-BFM,
author = {Bouyer, Patricia and Fang, Erwin and Markey,
Nicolas},
title = {Permissive strategies in timed automata and games},
editor = {Grov, Gudmund and Ireland, Andrew},
booktitle = {{P}roceedings of the 15th {I}nternational {W}orkshop
on {A}utomated {V}erification of {C}ritical
{S}ystems ({AVOCS}'15)},
acronym = {{AVOCS}'15},
publisher = {European Association of Software Science and
Technology},
series = {Electronic Communications of the EASST},
volume = {72},
year = {2015},
month = sep,
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.},
}
[BFP+73]
ManuelBlum,
Robert W.Floyd,
Vaughan R.Pratt,
Ronald L.Rivest, and
Robert EndreTarjan.
Time Bounds for Selection.
Journal of Computer and System Sciences 7(4):448-461. Academic Press, August 1973.
@article{jcss7(4)-BFPRT,
author = {Blum, Manuel and Floyd, Robert W. and Pratt, Vaughan
R. and Rivest, Ronald L. and Tarjan, Robert Endre},
title = {Time Bounds for Selection},
publisher = {Academic Press},
journal = {Journal of Computer and System Sciences},
volume = {7},
number = {4},
pages = {448-461},
year = {1973},
month = aug,
}
[BFS14]
NathalieBertrand,
PaulinFournier, and
ArnaudSangnier.
Playing with Probabilities in Reconfigurable
Broadcast Networks.
In FoSSaCS'14,
Lecture Notes in Computer Science 8412, pages 134-148. Springer-Verlag, April 2014.
@inproceedings{fossacs2014-BFS,
author = {Bertrand, Nathalie and Fournier, Paulin and
Sangnier, Arnaud},
title = {Playing with Probabilities in Reconfigurable
Broadcast Networks},
editor = {Muscholl, Anca},
booktitle = {{P}roceedings of the 17th {I}nternational
{C}onference on {F}oundations of {S}oftware
{S}cience and {C}omputation {S}tructure
({FoSSaCS}'14)},
acronym = {{FoSSaCS}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8412},
pages = {134-148},
year = {2014},
month = apr,
doi = {10.1007/978-3-642-54830-7_9},
}
[BFS15]
NathalieBertrand,
PaulinFournier, and
ArnaudSangnier.
Distributed Local Strategies in Broadcast Networks.
In CONCUR'15,
Leibniz International Proceedings in Informatics 42, pages 44-57. Leibniz-Zentrum für Informatik, September 2015.
@inproceedings{concur2015-BFS,
author = {Bertrand, Nathalie and Fournier, Paulin and
Sangnier, Arnaud},
title = {Distributed Local Strategies in Broadcast Networks},
editor = {Aceto, Luca and de Frutos{-}Escrig, David},
booktitle = {{P}roceedings of the 26th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'15)},
acronym = {{CONCUR}'15},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {42},
pages = {44-57},
year = {2015},
month = sep,
doi = {10.4230/LIPIcs.CONCUR.2015.44},
}
[BG85]
John P.Burgess and
YuriGurevich.
The Decision Problem for Linear Temporal Logic.
Notre Dame Journal of Formal Logic 26(2):115-128. April 1985.
@article{ndjfl26(2)-BG,
author = {Burgess,John P. and Gurevich, Yuri},
title = {The Decision Problem for Linear Temporal Logic},
journal = {Notre Dame Journal of Formal Logic},
volume = {26},
number = {2},
pages = {115-128},
year = {1985},
month = apr,
}
[BG93]
OrnaBernholtz and
OrnaGrumberg.
Branching Time Temporal Logic and A
m o r p H
O u s Tree Automata.
In CONCUR'93,
Lecture Notes in Computer Science 715, pages 262-277. Springer-Verlag, August 1993.
@inproceedings{concur1993-BG,
author = {Bernholtz, Orna and Grumberg, Orna},
title = {Branching Time Temporal Logic and {{\(\mathcal{A}
\textup{m} \textbf{o} r \textsc{p} \mathcal{H}
\texttt{O} u \textbf{s}\)}} Tree Automata},
editor = {Best, Eike},
booktitle = {{P}roceedings of the 4th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'93)},
acronym = {{CONCUR}'93},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {715},
pages = {262-277},
year = {1993},
month = aug,
}
[BG99]
GlennBruns and
PatriceGodefroid.
Model Checking Partial State Spaces with
3-Valued Temporal Logics.
In CAV'99,
Lecture Notes in Computer Science 1633, pages 274-287. Springer-Verlag, July 1999.
@inproceedings{cav1999-BG,
author = {Bruns, Glenn and Godefroid, Patrice},
title = {Model Checking Partial State Spaces with
{\(3\)}-Valued Temporal Logics},
editor = {Halbwachs, Nicolas and Peled, Doron A.},
booktitle = {{P}roceedings of the 11th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'99)},
acronym = {{CAV}'99},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {1633},
pages = {274-287},
year = {1999},
month = jul,
}
[BG01]
GlennBruns and
PatriceGodefroid.
Temporal Logic Query Checking (Extended Abstract).
In LICS'01,
pages 409-417.
IEEE Comp. Soc. Press, June 2001.
@inproceedings{lics2001-BG,
author = {Bruns, Glenn and Godefroid, Patrice},
title = {Temporal Logic Query Checking (Extended Abstract)},
booktitle = {{P}roceedings of the 16th {A}nnual {S}ymposium on
{L}ogic in {C}omputer {S}cience ({LICS}'01)},
acronym = {{LICS}'01},
publisher = {IEEE Comp. Soc. Press},
pages = {409-417},
year = {2001},
month = jun,
}
[BG02]
RobertBaumgartner and
GeorgGottlob.
Propositional Default Logics made Easier:
Computational Complexity of Model Checking.
Theoretical Computer Science 289(1):591-627. Elsevier, October 2002.
@article{tcs289(1)-BG,
author = {Baumgartner, Robert and Gottlob, Georg},
title = {Propositional Default Logics made Easier:
Computational Complexity of Model Checking},
publisher = {Elsevier},
journal = {Theoretical Computer Science},
volume = {289},
number = {1},
pages = {591-627},
year = {2002},
month = oct,
}
[BG03]
RégisBarbanchon and
ÉtienneGrandjean.
The Minimal Logically-Defined NP-Complete Problem.
In STACS'04,
Lecture Notes in Computer Science 2996, pages 338-349. Springer-Verlag, March 2003.
@inproceedings{stacs2004-BG,
author = {Barbanchon, R{\'e}gis and Grandjean, {\'E}tienne},
title = {The Minimal Logically-Defined {NP}-Complete Problem},
editor = {Diekert, Volker and Habib, Michel},
booktitle = {{P}roceedings of the 21st {S}ymposium on
{T}heoretical {A}spects of {C}omputer {S}cience
({STACS}'04)},
acronym = {{STACS}'04},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {2996},
pages = {338-349},
year = {2003},
month = mar,
}
[BG04]
DietmarBerwanger and
ErichGrädel.
Fixed-Point Logics and Solitaire Games.
Theory of Computing Systems 37(6):675-694. Springer-Verlag, December 2004.
@article{TCSyst37(6)-BG,
author = {Berwanger, Dietmar and Gr{\"a}del, Erich},
title = {Fixed-Point Logics and Solitaire Games},
publisher = {Springer-Verlag},
journal = {Theory of Computing Systems},
volume = {37},
number = {6},
pages = {675-694},
year = {2004},
month = dec,
doi = {10.1007/s00224-004-1147-5},
}
[BG05]
DietmarBerwanger and
ErichGrädel.
Entanglement –-mdash; A Measure for the Complexity of
Directed Graphs with Applications to Logic and
Games.
In LPAR'04,
Lecture Notes in Computer Science 3452, pages 209-223. Springer-Verlag, March 2005.
@inproceedings{lpar2004-BG,
author = {Berwanger, Dietmar and Gr{\"a}del, Erich},
title = {Entanglement~--- {A} Measure for the Complexity of
Directed Graphs with Applications to Logic and
Games},
editor = {Baader, Franz and Voronkov, Andrei},
booktitle = {{P}roceedings of the 11th {I}nternational
{C}onference {L}ogic {P}rogramming and {A}utomated
{R}easoning ({LPAR}'04)},
acronym = {{LPAR}'04},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {3452},
pages = {209-223},
year = {2005},
month = mar,
}
[BGH13]
OlivierBournez,
Daniel S.Graça, and
EmmanuelHainry.
Computation with perturbed dynamical systems.
Journal of Computer and System Sciences 79(5):714-724. Elsevier, August 2013.
@article{jcss79(5)-BGH,
author = {Bournez, Olivier and Gra{\c c}a, Daniel S. and
Hainry, Emmanuel},
title = {Computation with perturbed dynamical systems},
publisher = {Elsevier},
journal = {Journal of Computer and System Sciences},
volume = {79},
number = {5},
pages = {714-724},
year = {2013},
month = aug,
}
[BGH+09]
RoderickBloem,
KarinGreimel,
Thomas A.Henzinger, and
BarbaraJobstmann.
Synthesizing robust systems.
In FMCAD'09,
pages 85-92.
IEEE Comp. Soc. Press, November 2009.
@inproceedings{fmcad2009-BGHJ,
author = {Bloem, Roderick and Greimel, Karin and Henzinger,
Thomas A. and Jobstmann, Barbara},
title = {Synthesizing robust systems},
booktitle = {{P}roceedings of the 9th {I}nternational
{C}onference on {F}ormal {M}ethods in
{C}omputer-{A}ided {D}esign ({FMCAD}'09)},
acronym = {{FMCAD}'09},
publisher = {IEEE Comp. Soc. Press},
pages = {85-92},
year = {2009},
month = nov,
}
[BGH+15]
ThomasBrihaye,
GillesGeeraerts,
AxelHaddad,
EngelLefaucheux, and
BenjaminMonmege.
Simple priced timed games are not that simple.
In FSTTCS'15,
Leibniz International Proceedings in Informatics 45, pages 278-292. Leibniz-Zentrum für Informatik, December 2015.
@inproceedings{fsttcs2005-BGHLM,
author = {Brihaye, {\relax Th}omas and Geeraerts, Gilles and
Haddad, Axel and Lefaucheux, Engel and Monmege,
Benjamin},
title = {Simple priced timed games are not that simple},
editor = {Harsha, Prahladh and Ramalingam, G.},
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)},
acronym = {{FSTTCS}'15},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {45},
pages = {278-292},
year = {2015},
month = dec,
doi = {10.4230/LIPIcs.FSTTCS.2015.278},
}
[BGH+17]
ThomasBrihaye,
GillesGeeraerts,
AxelHaddad, and
BenjaminMonmege.
Pseudopolynomial iterative algorithm to solve
total-payoff games and min-cost reachability game.
Acta Informatica 54(1):85-125. Springer-Verlag, February 2017.
@article{acta54(1)-BGHM,
author = {Brihaye, {\relax Th}omas and Geeraerts, Gilles and
Haddad, Axel and Monmege, Benjamin},
title = {Pseudopolynomial iterative algorithm to solve
total-payoff games and min-cost reachability game},
publisher = {Springer-Verlag},
journal = {Acta Informatica},
volume = {54},
number = {1},
pages = {85-125},
year = {2017},
month = feb,
doi = {10.1007/s00236-016-0276-z},
}
[BGI+01]
BoazBarak,
OdedGoldreich,
RusellImpagliazzo,
StevenRudich,
AmitSahai,
SalilVadhan, and
KeYang.
On the (Im)possibility of Obfuscating Programs.
In CRYPTO'01,
Lecture Notes in Computer Science 2139, pages 1-18. Springer-Verlag, August 2001.
@inproceedings{crypto2001-BGIRSVY,
author = {Barak, Boaz and Goldreich, Oded and Impagliazzo,
Rusell and Rudich, Steven and Sahai, Amit and
Vadhan, Salil and Yang, Ke},
title = {On the (Im)possibility of Obfuscating Programs},
editor = {Kilian, Joe},
booktitle = {{P}roceedings of the 21st {A}nnual {I}nternational
{C}ryptology {C}onference ({CRYPTO}'01)},
acronym = {{CRYPTO}'01},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {2139},
pages = {1-18},
year = {2001},
month = aug,
}
[BGI+01]
BoazBarak,
OdedGoldreich,
RusellImpagliazzo,
StevenRudich,
AmitSahai,
SalilVadhan, and
KeYang.
On the (Im)possibility of Obfuscating Programs.
Research Report 01-057, Electronic Colloquium on Computational Complexity,
August 2001.
@techreport{eccc2001-BGIRSVY,
author = {Barak, Boaz and Goldreich, Oded and Impagliazzo,
Rusell and Rudich, Steven and Sahai, Amit and
Vadhan, Salil and Yang, Ke},
title = {On the (Im)possibility of Obfuscating Programs},
number = {01-057},
year = {2001},
month = aug,
institution = {Electronic Colloquium on Computational Complexity},
type = {Research Report},
}
[BGK+96]
JohanBengtsson,
W. O. DavidGriffioen,
Kåre J.Kristoffersen,
Kim GuldstrandLarsen,
FredrikLarsson,
PaulPettersson, and
WangYi.
Verification of an Audio Protocol with Bus Collision
Using Uppaal.
In CAV'96,
Lecture Notes in Computer Science 1102, pages 244-256. Springer-Verlag, July 1996.
@inproceedings{cav1996-BGKLLPY,
author = {Bengtsson, Johan and Griffioen, W. O. David and
Kristoffersen, K{\aa}re J. and Larsen, Kim
Guldstrand and Larsson, Fredrik and Pettersson, Paul
and Yi, Wang},
title = {Verification of an Audio Protocol with Bus Collision
Using {\scshape {U}ppaal}},
editor = {Alur, Rajeev and Henzinger, Thomas A.},
booktitle = {{P}roceedings of the 8th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'96)},
acronym = {{CAV}'96},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {1102},
pages = {244-256},
year = {1996},
month = jul,
}
[BGM14]
PatriciaBouyer,
PatrickGardy, and
NicolasMarkey.
Quantitative verification of weighted Kripke
structures.
In ATVA'14,
Lecture Notes in Computer Science 8837, pages 64-80. Springer-Verlag, November 2014.
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{atva2014-BGM,
author = {Bouyer, Patricia and Gardy, Patrick and Markey,
Nicolas},
title = {Quantitative verification of weighted {K}ripke
structures},
editor = {Cassez, Franck and Raskin, Jean-Fran{\c c}ois},
booktitle = {{P}roceedings of the 12th {I}nternational
{S}ymposium on {A}utomated {T}echnology for
{V}erification and {A}nalysis ({ATVA}'14)},
acronym = {{ATVA}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8837},
pages = {64-80},
year = {2014},
month = nov,
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.},
}
[BGM15]
PatriciaBouyer,
PatrickGardy, and
NicolasMarkey.
Weighted strategy logic with boolean goals over
one-counter games.
In FSTTCS'15,
Leibniz International Proceedings in Informatics 45, pages 69-83. Leibniz-Zentrum für Informatik, December 2015.
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
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{fsttcs2015-BGM,
author = {Bouyer, Patricia and Gardy, Patrick and Markey,
Nicolas},
title = {Weighted strategy logic with boolean goals over
one-counter games},
editor = {Harsha, Prahladh and Ramalingam, G.},
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)},
acronym = {{FSTTCS}'15},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {45},
pages = {69-83},
year = {2015},
month = dec,
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.},
}
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.
@article{ipl116(2)-BGM,
author = {Bouyer, Patricia and Gardy, Patrick and Markey,
Nicolas},
title = {On the semantics of Strategy Logic},
publisher = {Elsevier},
journal = {Information Processing Letters},
volume = {116},
number = {2},
pages = {75-79},
year = {2016},
month = feb,
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.},
}
[BGM+08]
ThomasBrihaye,
MohamedGhannem,
NicolasMarkey, and
LionelRieg.
Good friends are hard to find!.
In TIME'08,
pages 32-40.
IEEE Comp. Soc. Press, June 2008.
Abstract
We focus on the problem of finding (the size of)
a minimal winning coalition in a multi-player game.
More precisely, we prove that deciding whether there
is a winning coalition of size at most k is
NP-complete, while deciding whether k is the
optimal size is DP-complete. We also study different
variants of our original problem: the function
problem, where the aim is to effectively compute the
coalition; more succinct encoding of the game; and
richer families of winning objectives.
@inproceedings{time2008-BGMR,
author = {Brihaye, {\relax Th}omas and Ghannem, Mohamed and
Markey, Nicolas and Rieg, Lionel},
title = {Good friends are hard to find!},
booktitle = {{P}roceedings of the 15th {I}nternational
{S}ymposium on {T}emporal {R}epresentation and
{R}easoning ({TIME}'08)},
acronym = {{TIME}'08},
publisher = {IEEE Comp. Soc. Press},
pages = {32-40},
year = {2008},
month = jun,
doi = {10.1109/TIME.2008.10},
abstract = {We focus on the problem of finding (the~size of)
a~minimal winning coalition in a multi-player game.
More precisely, we~prove that deciding whether there
is a winning coalition of size at most~\(k\) is
NP-complete, while deciding whether \(k\) is the
optimal size is DP-complete. We~also study different
variants of our original problem: the function
problem, where the aim is to effectively compute the
coalition; more succinct encoding of the game; and
richer families of winning objectives.},
}
[BGN+14]
ThomasBrihaye,
GillesGeeraerts,
ShankaraNarayanan Krishna,
LakshmiManasa,
BenjaminMonmege, and
AshutoshTrivedi.
Adding negative prices to priced timed games.
In CONCUR'14,
Lecture Notes in Computer Science 8704, pages 560-575. Springer-Verlag, September 2014.
@inproceedings{concur2014-BGKMMT,
author = {Brihaye, {\relax Th}omas and Geeraerts, Gilles and
Narayanan Krishna, Shankara and Manasa, Lakshmi and
Monmege, Benjamin and Trivedi, Ashutosh},
title = {Adding negative prices to priced timed games},
editor = {Baldan, Paolo and Gorla, Daniele},
booktitle = {{P}roceedings of the 25th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'14)},
acronym = {{CONCUR}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8704},
pages = {560-575},
year = {2014},
month = sep,
doi = {10.1007/978-3-662-44584-6_38},
}
[BGP96]
BéatriceBérard,
PaulGastin, and
AntoinePetit.
Timed Automata with non Observable Actions:
Expressive power and refinement.
In STACS'96,
Lecture Notes in Computer Science 1046, pages 257-268. Springer-Verlag, February 1996.
@inproceedings{stacs1996-BGP,
author = {B{\'e}rard, B{\'e}atrice and Gastin, Paul and Petit,
Antoine},
title = {Timed Automata with non Observable Actions:
Expressive power and refinement},
editor = {Puech, Claude and Reischuk, R{\"u}diger},
booktitle = {{P}roceedings of the 13th {S}ymposium on
{T}heoretical {A}spects of {C}omputer {S}cience
({STACS}'96)},
acronym = {{STACS}'96},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {1046},
pages = {257-268},
year = {1996},
month = feb,
}
[BGS92]
JoséBalcázar,
JoaquimGabarró, and
MiklósSántha.
Deciding bisimilarity is P-complete.
Formal Aspects of Computing 4(1 supplement):638-648. Springer-Verlag, November 1992.
@article{fac4(1sup)-BGSC,
author = {Balc{\'a}zar, Jos{\'e} and Gabarr{\'o}, Joaquim and
S{\'a}ntha, Mikl{\'o}s},
title = {Deciding bisimilarity is {P}-complete},
publisher = {Springer-Verlag},
journal = {Formal Aspects of Computing},
volume = {4},
number = {1 supplement},
pages = {638-648},
year = {1992},
month = nov,
}
[BGS14]
BenediktBollig,
PaulGastin, and
JanaSchubert.
Parameterized verification of communicating automata
under context bounds.
In RP'14,
Lecture Notes in Computer Science 8762, pages 45-57. Springer-Verlag, September 2014.
@inproceedings{rp2014-BGS,
author = {Bollig, Benedikt and Gastin, Paul and Schubert,
Jana},
title = {Parameterized verification of communicating automata
under context bounds},
editor = {Ouaknine, Jo{\"e}l and Potapov, Igor and Worrell,
James},
booktitle = {{P}roceedings of the 8th {W}orkshop on
{R}eachability {P}roblems in {C}omputational
{M}odels ({RP}'14)},
acronym = {{RP}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8762},
pages = {45-57},
year = {2014},
month = sep,
doi = {10.1007/978-3-319-11439-2_4},
}
[BGW01]
NikitaBorisov,
IanGoldberg, and
Klaus W.Wagner.
Intercepting Mobile Communications: The Insecurity
of 802.11.
In MOBICOM'01,
pages 180-189.
ACM Press, July 2001.
@inproceedings{mobicom2001-BGW,
author = {Borisov, Nikita and Goldberg, Ian and Wagner, Klaus
W.},
title = {Intercepting Mobile Communications: The Insecurity
of~{\(802.11\)}},
booktitle = {{P}roceedings of the 7th {A}nnual {I}nternational
{C}onference on {M}obile {C}omputing and
{N}etworking ({MOBICOM}'01)},
acronym = {{MOBICOM}'01},
publisher = {ACM Press},
pages = {180-189},
year = {2001},
month = jul,
}
[BH67]
ManuelBlum and
CarlHewitt.
Automata on a 2-Dimensional Tape.
In FOCS'67,
pages 155-160.
IEEE Comp. Soc. Press, October 1967.
@inproceedings{focs1967-BH,
author = {Blum, Manuel and Hewitt, Carl},
title = {Automata on a 2-Dimensional Tape},
booktitle = {{P}roceedings of the 8th {A}nnual {S}ymposium on
{F}oundations of {C}omputer {S}cience ({FOCS}'67)},
acronym = {{FOCS}'67},
publisher = {IEEE Comp. Soc. Press},
pages = {155-160},
year = {1967},
month = oct,
}
[BH81]
Arthur J.Bernstein and
Jr.Harter.
Proving Real-Time Properties of Programs with
Temporal Logic.
In SOSP'81,
Operating System Review 15(5), pages 1-11. ACM Press, December 1981.
@inproceedings{sosp1981-BH,
author = {Bernstein, Arthur J. and Harter, Paul K., Jr.},
title = {Proving Real-Time Properties of Programs with
Temporal Logic},
booktitle = {{P}roceedings of the 8th {ACM} {S}ymposium on
{O}perating {S}ystems {P}rinciples ({SOSP}'81)},
acronym = {{SOSP}'81},
publisher = {ACM Press},
series = {Operating System Review},
volume = {15},
number = {5},
pages = {1-11},
year = {1981},
month = dec,
}
[BH04]
AnneBergeron and
SylvieHamel.
From Cascade Decompositions to Bit-Vector
Algotithms.
Theoretical Computer Science 313(1):3-16. Elsevier, February 2004.
@article{tcs313(1)-BH,
author = {Bergeron, Anne and Hamel, Sylvie},
title = {From Cascade Decompositions to Bit-Vector
Algotithms},
publisher = {Elsevier},
journal = {Theoretical Computer Science},
volume = {313},
number = {1},
pages = {3-16},
year = {2004},
month = feb,
}
[BH05]
DraganBosnacki and
Gerard J.Holzmann.
Improving Spin's Partial-Order Reduction for
Breadth-First Search.
In SPIN'05,
Lecture Notes in Computer Science 3639, pages 91-105. Springer-Verlag, April 2005.
@inproceedings{spin2005-BH,
author = {Bosnacki, Dragan and Holzmann, Gerard J.},
title = {Improving {S}pin's Partial-Order Reduction for
Breadth-First Search},
editor = {Godefroid, Patrice},
booktitle = {{P}roceedings of the 12th {I}nternational {SPIN}
{W}orkshop ({SPIN}'05)},
acronym = {{SPIN}'05},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {3639},
pages = {91-105},
year = {2005},
month = apr,
doi = {10.1007/11537328_10},
}
[BH06]
BernardBoigelot and
FrédéricHerbreteau.
The Power of Hybrid Acceleration.
In CAV'06,
Lecture Notes in Computer Science 4144, pages 438-451. Springer-Verlag, July 2006.
@inproceedings{cav2006-BH,
author = {Boigelot, Bernard and Herbreteau, Fr{\'e}d{\'e}ric},
title = {The Power of Hybrid Acceleration},
editor = {Ball, Thomas and Jones, Robert},
booktitle = {{P}roceedings of the 18th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'06)},
acronym = {{CAV}'06},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {4144},
pages = {438-451},
year = {2006},
month = jul,
doi = {10.1007/11817963_40},
}
@phdthesis{bherer09,
author = {Bherer, Hans},
title = {Controller Synthesis for Parameterized Discrete
Event Systems},
year = {2009},
school = {Universit{\'e} Laval, Qu\'ebec, Canada},
}
[BHJ03]
BernardBoigelot,
FrédéricHerbreteau, and
SébastienJodogne.
Hybrid Acceleration using Real Vector Automata
(extended abstract).
In CAV'03,
Lecture Notes in Computer Science 2725, pages 193-205. Springer-Verlag, July 2003.
@inproceedings{cav2003-BHJ,
author = {Boigelot, Bernard and Herbreteau, Fr{\'e}d{\'e}ric
and Jodogne, S{\'e}bastien},
title = {Hybrid Acceleration using Real Vector Automata
(extended abstract)},
editor = {Hunt, Jr, Warren A. and Somenzi, Fabio},
booktitle = {{P}roceedings of the 15th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'03)},
acronym = {{CAV}'03},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {2725},
pages = {193-205},
year = {2003},
month = jul,
doi = {10.1007/978-3-540-45069-6_19},
}
[BHJ03]
BernardBoigelot,
FrédéricHerbreteau, and
SébastienJodogne.
Hybrid Acceleration using Real Vector Automata.
Technical Report 2003.18, Centre Fédéré en Vérification, Bruxelles,
Belgium,
2003.
@techreport{TR-cfv0318,
author = {Boigelot, Bernard and Herbreteau, Fr{\'e}d{\'e}ric
and Jodogne, S{\'e}bastien},
title = {Hybrid Acceleration using Real Vector Automata},
number = {2003.18},
year = {2003},
institution = {Centre F\'ed\'er\'e en V\'erification, Bruxelles,
Belgium},
type = {Technical Report},
}
[BHK00]
StevenBradley,
WilliamHenderson, and
DavidKendall.
Using Timed Automata for Response Time Analysis and
Distributer Real-Time Systems.
In WRTP'99,
pages 143-148.
Pergamon Press, January 2000.
@inproceedings{wrtp1999-BHK,
author = {Bradley, Steven and Henderson, William and Kendall,
David},
title = {Using Timed Automata for Response Time Analysis and
Distributer Real-Time Systems},
editor = {Frigeri, Alceu Heinke and Halang, Wolfgang A. and
Son, Sang H.},
booktitle = {{P}roceedings of the 24th {IFAC}/{IFIP} {W}orkshop
on {R}eal-{T}ime {P}rogramming ({WRTP}'99)},
acronym = {{WRTP}'99},
publisher = {Pergamon Press},
pages = {143-148},
year = {2000},
month = jan,
confyear = {1999},
confmonth = {5},
}
[BHM08]
Aske WiidBrekling,
Michael R.Hansen, and
JanMadsen.
Models and formal verification of multiprocessor
system-on-chips.
Journal of Logic and Algebraic Programming 77(1-2):1-19. Elsevier, October 2008.
@article{jlap77(1-2)-BHM,
author = {Brekling, Aske Wiid and Hansen, Michael R. and
Madsen, Jan},
title = {Models and formal verification of multiprocessor
system-on-chips},
publisher = {Elsevier},
journal = {Journal of Logic and Algebraic Programming},
volume = {77},
number = {1-2},
pages = {1-19},
year = {2008},
month = oct,
}
[BHM14]
BernardBoigelot,
FrédéricHerbreteau, and
IsabelleMainz.
Acceleration of Affine Hybrid Transformations.
In ATVA'14,
Lecture Notes in Computer Science 8837, pages 31-46. Springer-Verlag, November 2014.
@inproceedings{atva2014-BHM,
author = {Boigelot, Bernard and Herbreteau, Fr{\'e}d{\'e}ric
and Mainz, Isabelle},
title = {Acceleration of Affine Hybrid Transformations},
editor = {Cassez, Franck and Raskin, Jean-Fran{\c c}ois},
booktitle = {{P}roceedings of the 12th {I}nternational
{S}ymposium on {A}utomated {T}echnology for
{V}erification and {A}nalysis ({ATVA}'14)},
acronym = {{ATVA}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8837},
pages = {31-46},
year = {2014},
month = nov,
doi = {10.1007/978-3-319-11936-6_4},
}
[BHM17]
BéatriceBérard,
LoïcHélouët, and
JohnMullins.
Non-interference in partial order models.
ACM Transactions on Embedded Computing Systems.
ACM Press, 2017. To appear.
@article{tecs-BHM,
author = {B{\'e}rard, B{\'e}atrice and H{\'e}lou{\"e}t,
Lo{\"\i}c and Mullins, John},
title = {Non-interference in partial order models},
publisher = {ACM Press},
journal = {ACM Transactions on Embedded Computing Systems},
year = {2017},
note = {To~appear},
}
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.
@inproceedings{fossacs2017-BHMRZ,
author = {Bouyer, Patricia and Hofman, Piotr and Markey,
Nicolas and Randour, Mickael and Zimmermann, Martin},
title = {Bounding Average-energy Games},
editor = {Esparza, Javier and Murawski, Andrzej},
booktitle = {{P}roceedings of the 20th {I}nternational
{C}onference on {F}oundations of {S}oftware
{S}cience and {C}omputation {S}tructure
({FoSSaCS}'17)},
acronym = {{FoSSaCS}'17},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {10203},
pages = {179-195},
year = {2017},
month = apr,
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.\par 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.\par
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.},
}
[BHP+07]
ThomasBrihaye,
Thomas A.Henzinger,
Vinayak S.Prabhu, and
Jean-FrançoisRaskin.
Minimum-Time Reachability in Timed Games.
In ICALP'07,
Lecture Notes in Computer Science 4596, pages 825-837. Springer-Verlag, July 2007.
@inproceedings{icalp2007-BHPR,
author = {Brihaye, {\relax Th}omas and Henzinger, Thomas A.
and Prabhu, Vinayak S. and Raskin, Jean-Fran{\c
c}ois},
title = {Minimum-Time Reachability in Timed Games},
editor = {Arge, Lars and Cachin, Christian and Jurdzi{\'n}ski,
Tomasz and Tarlecki, Andrzej},
booktitle = {{P}roceedings of the 34th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'07)},
acronym = {{ICALP}'07},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {4596},
pages = {825-837},
year = {2007},
month = jul,
}
[BHR06]
PatriciaBouyer,
SergeHaddad, and
Pierre-AlainReynier.
Timed Unfoldings for Networks of Timed Automata.
In ATVA'06,
Lecture Notes in Computer Science 4218, pages 292-306. Springer-Verlag, October 2006.
@inproceedings{atva2006-BHR,
author = {Bouyer, Patricia and Haddad, Serge and Reynier,
Pierre-Alain},
title = {Timed Unfoldings for Networks of Timed Automata},
editor = {Graf, Susanne and Zhang, Wenhui},
booktitle = {{P}roceedings of the 4th {I}nternational {S}ymposium
on {A}utomated {T}echnology for {V}erification and
{A}nalysis ({ATVA}'06)},
acronym = {{ATVA}'06},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {4218},
pages = {292-306},
year = {2006},
month = oct,
doi = {10.1007/11901914_23},
}
[BHR09]
PatriciaBouyer,
SergeHaddad, and
Pierre-AlainReynier.
Undecidability Results for Timed Automata with
Silent Transitions.
Fundamenta Informaticae 92(1-2):1-25. IOS Press, 2009.
@article{fundi92(1-2)-BHR,
author = {Bouyer, Patricia and Haddad, Serge and Reynier,
Pierre-Alain},
title = {Undecidability Results for Timed Automata with
Silent Transitions},
publisher = {IOS Press},
journal = {Fundamenta Informaticae},
volume = {92},
number = {1-2},
pages = {1-25},
year = {2009},
}
[BHR+02]
DanièleBeauquier,
YoramHirshfeld,
AlexanderRabinovich, and
AnatolSlissenko.
The Probablity Nesting Game.
In EXPRESS'02,
Electronic Notes in Theoretical Computer Science 68(2), pages 3-13. Elsevier, August 2002.
@inproceedings{express2002-BHRS,
author = {Beauquier, Dani{\`e}le and Hirshfeld, Yoram and
Rabinovich, Alexander and Slissenko, Anatol},
title = {The Probablity Nesting Game},
editor = {Nestmann, Uwe and Panangaden, Prakash},
booktitle = {{P}roceedings of the 9th {I}nternational {W}orkshop
on {E}xpressiveness in {C}oncurrency ({EXPRESS}'02)},
acronym = {{EXPRESS}'02},
publisher = {Elsevier},
series = {Electronic Notes in Theoretical Computer Science},
volume = {68},
number = {2},
pages = {3-13},
year = {2002},
month = aug,
}
[BHT07]
DirkBeyer,
Thomas A.Henzinger, and
GrégoryThéoduloz.
Configurable Software Verification: Concretizing the
Convergence of Model Checking and Program Analysis.
In CAV'07,
Lecture Notes in Computer Science 4590.
Springer-Verlag, July 2007.
@inproceedings{cav2007-BHT,
author = {Beyer, Dirk and Henzinger, Thomas A. and
Th{\'e}oduloz, Gr{\'e}gory},
title = {Configurable Software Verification: Concretizing the
Convergence of Model Checking and Program Analysis},
editor = {Damm, Werner and Hermanns, Holger},
booktitle = {{P}roceedings of the 19th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'07)},
acronym = {{CAV}'07},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {4590},
year = {2007},
month = jul,
doi = {10.1007/978-3-540-73368-3_51},
}
[BIL06]
MariusBozga,
RaduIosif, and
YassineLakhnech.
Flat Parametric Counter Automata.
Research Report TR-2005-15, Lab. VERIMAG, Grenoble, France,
March 2006.
@techreport{TR-verimag2005-15,
author = {Bozga, Marius and Iosif, Radu and Lakhnech, Yassine},
title = {Flat Parametric Counter Automata},
number = {TR-2005-15},
year = {2006},
month = mar,
institution = {Lab. VERIMAG, Grenoble, France},
type = {Research Report},
}
[BIL06]
MariusBozga,
RaduIosif, and
YassineLakhnech.
Flat Parametric Counter Automata.
In ICALP'06,
Lecture Notes in Computer Science 4052, pages 577-588. Springer-Verlag, July 2006.
@inproceedings{icalp2006-BIL,
author = {Bozga, Marius and Iosif, Radu and Lakhnech, Yassine},
title = {Flat Parametric Counter Automata},
editor = {Bugliesi, Michele and Preneel, Bart and Sassone,
Vladimiro and Wegener, Ingo},
booktitle = {{P}roceedings of the 33rd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'06))~-- Part~{II}},
acronym = {{ICALP}'06},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {4052},
pages = {577-588},
year = {2006},
month = jul,
doi = {10.1007/11787006_49},
}
[BIS90]
David A. MixBarrington,
NeilImmerman, and
HowardStraubing.
On Uniformity Within NC1.
Journal of Computer and System Sciences 41(3):274-306. Academic Press, December 1990.
@article{jcss41(3)-BIS,
author = {Barrington, David A. Mix and Immerman, Neil and
Straubing, Howard},
title = {On Uniformity Within {{\(\mathit{NC}^1\)}}},
publisher = {Academic Press},
journal = {Journal of Computer and System Sciences},
volume = {41},
number = {3},
pages = {274-306},
year = {1990},
month = dec,
}
[BJ10]
NilsBulling and
WojciechJamroga.
Model Checking Agents with Memory Is Harder than It
Seemed.
In AAMAS'10,
pages 633-640.
International Foundation for Autonomous Agents and
Multiagent Systems, May 2010.
@inproceedings{aamas2010-BJ,
author = {Bulling, Nils and Jamroga, Wojciech},
title = {Model Checking Agents with Memory Is Harder than It
Seemed},
editor = {van der Hoek, Wiebe and Kaminka, Gal A. and
Lesp{\'e}rance, Yves and Luck, Michael and Sen,
Sandeep},
booktitle = {{P}roceedings of the 9th {I}nternational
{C}onference on {A}utonomous {A}gents and
{M}ultiagent {S}ystems ({AAMAS}'10)},
acronym = {{AAMAS}'10},
publisher = {International Foundation for Autonomous Agents and
Multiagent Systems},
pages = {633-640},
year = {2010},
month = may,
}
[BJK10]
TomášBrázdil,
PetrJančar, and
AntonínKučera.
Reachability Games on Extended Vector Addition
Systems with States.
In ICALP'10,
Lecture Notes in Computer Science 6199, pages 478-489. Springer-Verlag, July 2010.
@inproceedings{icalp2010-BJK,
author = {Br{\'a}zdil, Tom{\'a}{ s} and Jan{ c}ar, Petr
and Ku{ c}era, Anton{\'\i}n},
title = {Reachability Games on Extended Vector Addition
Systems with States},
editor = {Abramsky, Samson and Gavoille, Cyril and Kirchner,
Claude and Meyer auf der Heide, Friedhelm and
Spirakis, Paul G.},
booktitle = {{P}roceedings of the 37th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'10)~-- Part~{II}},
acronym = {{ICALP}'10},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {6199},
pages = {478-489},
year = {2010},
month = jul,
doi = {10.1007/978-3-642-14162-1_40},
}
[BJK+05]
ManfredBroy,
BengtJonsson,
Joost-PieterKatoen,
MartinLeucker, and
AlexanderPretschner.
Model-Based Testing of Reactive Systems – Advanced
lectures.
Lecture Notes in Computer Science 3472.
Springer-Verlag, 2005.
@book{mbt-bjklp,
author = {Broy, Manfred and Jonsson, Bengt and Katoen,
Joost-Pieter and Leucker, Martin and Pretschner,
Alexander},
title = {Model-Based Testing of Reactive Systems~-- Advanced
lectures},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {3472},
year = {2005},
}
[BJL+10]
ThomasBrihaye,
MarcJungers,
SamsonLasaulce,
NicolasMarkey, and
GhassanOreiby.
Using Model Checking for Analyzing Distributed Power
Control Problems.
EURASIP Journal on Wireless Communications and
Networking 2010(861472).
Hindawi Publishing Corp., June 2010.
Abstract
Model checking (MC) is a formal verification
technique which has been known and still knows a
resounding success in the computer science
community. Realizing that the distributed power
control (PC) problem can be modeled by a timed game
between a given transmitter and its environment, the
authors wanted to know whether this approach can be
applied to distributed PC. It turns out that it can
be applied successfully and allows one to analyze
realistic scenarios including the case of discrete
transmit powers and games with incomplete
information. The proposed methodology is as follows.
We state some objectives a transmitter-receiver pair
would like to reach. The network is modeled by a
game where transmitters are considered as timed
automata interacting with each other. The objectives
are then translated into timed alternating-time
temporal logic formulae and MC is exploited to know
whether the desired properties are verified and
determine a winning strategy.
@article{jwcn2010(861472)-BJLMO,
author = {Brihaye, {\relax Th}omas and Jungers, Marc and
Lasaulce, Samson and Markey, Nicolas and Oreiby,
Ghassan},
title = {Using Model Checking for Analyzing Distributed Power
Control Problems},
publisher = {Hindawi Publishing Corp.},
journal = {EURASIP Journal on Wireless Communications and
Networking},
volume = {2010},
number = {861472},
year = {2010},
month = jun,
doi = {10.1155/2010/861472},
abstract = {Model checking~(MC) is a formal verification
technique which has been known and still knows a
resounding success in the computer science
community. Realizing that the distributed power
control~(PC) problem can be modeled by a timed game
between a given transmitter and its environment, the
authors wanted to know whether this approach can be
applied to distributed~PC. It~turns out that it can
be applied successfully and allows one to analyze
realistic scenarios including the case of discrete
transmit powers and games with incomplete
information. The proposed methodology is as follows.
We state some objectives a transmitter-receiver pair
would like to reach. The network is modeled by a
game where transmitters are considered as timed
automata interacting with each other. The objectives
are then translated into timed alternating-time
temporal logic formulae and MC is exploited to know
whether the desired properties are verified and
determine a winning strategy.},
}
[BJL+98]
JohanBengtsson,
BengtJonsson,
JohanLilius, and
WangYi.
Partial-Order Reductions for Timed Systems.
In CONCUR'98,
Lecture Notes in Computer Science 1466, pages 485-500. Springer-Verlag, September 1998.
@inproceedings{concur1998-BJLY,
author = {Bengtsson, Johan and Jonsson, Bengt and Lilius,
Johan and Yi, Wang},
title = {Partial-Order Reductions for Timed Systems},
editor = {Sangiorgi, Davide and de Simone, Robert},
booktitle = {{P}roceedings of the 9th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'98)},
acronym = {{CONCUR}'98},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {1466},
pages = {485-500},
year = {1998},
month = sep,
doi = {10.1007/BFb0055643},
}
[BJM15]
PatriciaBouyer,
SamyJaziri, and
NicolasMarkey.
On the Value Problem in Weighted Timed Games.
In CONCUR'15,
Leibniz International Proceedings in Informatics 42, pages 311-324. Leibniz-Zentrum für Informatik, September 2015.
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.
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{concur2015-BJM,
author = {Bouyer, Patricia and Jaziri, Samy and Markey,
Nicolas},
title = {On~the Value Problem in Weighted Timed Games},
editor = {Aceto, Luca and de Frutos{-}Escrig, David},
booktitle = {{P}roceedings of the 26th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'15)},
acronym = {{CONCUR}'15},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {42},
pages = {311-324},
year = {2015},
month = sep,
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.},
}
[BJM17]
PatriciaBouyer,
SamyJaziri, and
NicolasMarkey.
On the determinization of timed systems.
In FORMATS'17,
Lecture Notes in Computer Science 10419, pages 25-41. Springer-Verlag, September 2017.
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.
@inproceedings{formats2017-BJM,
author = {Bouyer, Patricia and Jaziri, Samy and Markey,
Nicolas},
title = {On the determinization of timed systems},
editor = {Abate, Alessandro and Geeraerts, Gilles},
booktitle = {{P}roceedings of the 15th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'17)},
acronym = {{FORMATS}'17},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {10419},
pages = {25-41},
year = {2017},
month = sep,
doi = {10.1007/978-3-319-65765-3 2},
abstract = {We introduce a new formalism called \emph{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.},
}
Dynamic complexity is concerned with updating the
output of a problem when the input is slightly
changed. We study the dynamic complexity of model
checking a fixed monadic second-order formula over
evolving subgraphs of a fixed maximal graph having
bounded tree-width; here the subgraph evolves by
losing or gaining edges (from the maximal graph).
We show that this problem is in DynFO (with LOGSPACE
precomputation), via a reduction to a Dyck
reachability problem on an acyclic automaton.
@techreport{arxiv1702.05183-BJM,
author = {Bouyer, Patricia and Jug{\'e}, Vincent and Markey,
Nicolas},
title = {{C}ourcelle's Theorem Made Dynamic},
number = {1702.05183},
year = {2017},
month = feb,
institution = {arXiv},
abstract = {Dynamic complexity is concerned with updating the
output of a problem when the input is slightly
changed. We study the dynamic complexity of model
checking a fixed monadic second-order formula over
evolving subgraphs of a fixed maximal graph having
bounded tree-width; here the subgraph evolves by
losing or gaining edges (from the maximal graph).
We~show that this problem is in DynFO (with LOGSPACE
precomputation), via a reduction to a Dyck
reachability problem on an acyclic automaton.},
}
[BJM+02]
MariusBozga,
HouJianmin,
OdedMaler, and
SergioYovine.
Verification of Asynchronous Circuits using Timed
Automata.
In TPTS'02,
Electronic Notes in Theoretical Computer Science 65(6), pages 47-59. Elsevier, April 2002.
@inproceedings{tpts2002-BJMY,
author = {Bozga, Marius and Jianmin, Hou and Maler, Oded and
Yovine, Sergio},
title = {Verification of Asynchronous Circuits using Timed
Automata},
editor = {Asarin, Eugene and Maler, Oded and Yovine, Sergio},
booktitle = {{P}roceedings of the 1st {W}orkshop on {T}heory and
{P}ractice of {T}imed {S}ystems ({TPTS}'02)},
acronym = {{TPTS}'02},
publisher = {Elsevier},
series = {Electronic Notes in Theoretical Computer Science},
volume = {65},
number = {6},
pages = {47-59},
year = {2002},
month = apr,
}
[BJS09]
JoakimByg,
Kenneth YrkeJørgensen, and
JiříSrba.
TAPAAL: Editor, Simulator and Verifier of
Timed-Arc Petri Nets.
In ATVA'09,
Lecture Notes in Computer Science 5799, pages 84-89. Springer-Verlag, October 2009.
@inproceedings{atva2009-BJS,
author = {Byg, Joakim and J{\o}rgensen, Kenneth Yrke and Srba,
Ji{ r}{\'\i}},
title = {{TAPAAL}: Editor, Simulator and Verifier of
Timed-Arc {P}etri Nets},
editor = {Liu, Zhiming and Ravn, Anders P.},
booktitle = {{P}roceedings of the 7th {I}nternational {S}ymposium
on {A}utomated {T}echnology for {V}erification and
{A}nalysis ({ATVA}'09)},
acronym = {{ATVA}'09},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {5799},
pages = {84-89},
year = {2009},
month = oct,
doi = {10.1007/978-3-642-04761-9_7},
}
[BJS+12]
NathalieBertrand,
ThierryJéron,
AmélieStainer, and
MoezKrichen.
Off-line test selection with test purposes for
non-deterministic timed automata.
Logical Methods in Computer Science 8(4).
2012.
@article{lmcs8(4)-BJSK,
author = {Bertrand, Nathalie and J{\'e}ron, Thierry and
Stainer, Am{\'e}lie and Krichen, Moez},
title = {Off-line test selection with test purposes for
non-deterministic timed automata},
journal = {Logical Methods in Computer Science},
volume = {8},
number = {4},
year = {2012},
doi = {10.2168/LMCS-8(4:8)2012},
}
[BJV10]
JasperBerendsen,
David N.Jansen, and
FritsVaandrager.
Fortuna: model checking priced probabilistic timed
automata.
In QEST'10,
pages 273-281.
IEEE Comp. Soc. Press, September 2010.
@inproceedings{qest2010-BJV,
author = {Berendsen, Jasper and Jansen, David N. and
Vaandrager, Frits},
title = {Fortuna: model checking priced probabilistic timed
automata},
booktitle = {{P}roceedings of the 7th {I}nternational
{C}onference on {Q}uantitative {E}valuation of
{S}ystems ({QEST}'10)},
acronym = {{QEST}'10},
publisher = {IEEE Comp. Soc. Press},
pages = {273-281},
year = {2010},
month = sep,
}
[BJW02]
JulienBernet,
DavidJanin, and
IgorWalukiewicz.
Permissive strategies: from parity games to safety
games.
RAIRO – Theoretical Informatics and Applications 36(3):261-275. EDP Sciences, 2002.
@article{rairo-tia36(3)-BJW,
author = {Bernet, Julien and Janin, David and Walukiewicz,
Igor},
title = {Permissive strategies: from parity games to safety
games},
publisher = {EDP Sciences},
journal = {RAIRO~-- Theoretical Informatics and Applications},
volume = {36},
number = {3},
pages = {261-275},
year = {2002},
}
[BK08]
ChristelBaier and
Joost-PieterKatoen.
Principles of Model-Checking.
MIT Press, May 2008.
@book{PoMC2008-BK,
author = {Baier, {\relax Ch}ristel and Katoen, Joost-Pieter},
title = {Principles of Model-Checking},
publisher = {MIT Press},
year = {2008},
month = may,
}
[BKK11]
ChristelBaier,
JoachimKlein, and
SaschaKlüppelholz.
A Compositional Framework for Controller Synthesis.
In CONCUR'11,
Lecture Notes in Computer Science 6901, pages 512-527. Springer-Verlag, September 2011.
@inproceedings{concur2011-BKK,
author = {Baier, {\relax Ch}ristel and Klein, Joachim and
Kl{\"u}ppelholz, Sascha},
title = {A Compositional Framework for Controller Synthesis},
editor = {Katoen, Joost-Pieter and K{\"o}nig, Barbara},
booktitle = {{P}roceedings of the 22nd {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'11)},
acronym = {{CONCUR}'11},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {6901},
pages = {512-527},
year = {2011},
month = sep,
}
[BKK+14]
TomášBrázdil,
DavidKlaška,
AntonínKučera, and
PetrNovotný.
Minimizing Running Costs in Consumption Systems.
In CAV'14,
Lecture Notes in Computer Science 8559, pages 457-472. Springer-Verlag, July 2014.
@inproceedings{cav2014-BKKN,
author = {Br{\'a}zdil, Tom{\'a}{ s} and Kla{{s}}ka, David
and Ku{ c}era, Anton{\'\i}n and Novotn{\'y}, Petr},
title = {Minimizing Running Costs in Consumption Systems},
editor = {Biere, Armin and Bloem, Roderick},
booktitle = {{P}roceedings of the 26th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'14)},
acronym = {{CAV}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8559},
pages = {457-472},
year = {2014},
month = jul,
}
[BKM+06]
Jeremy W.Bryans,
MaciejKoutny,
LaurentMazaré, and
Peter Y. A.Ryan.
Opacity generalised to transition systems.
In FAST'05,
Lecture Notes in Computer Science 3866, pages 81-95. Springer-Verlag, 2006.
@inproceedings{fast2005-BKMR,
author = {Bryans, Jeremy W. and Koutny, Maciej and Mazar{\'e},
Laurent and Ryan, Peter Y. A.},
title = {Opacity generalised to transition systems},
editor = {Dimitrakos, Theo and Martinelli, Fabio and Ryan,
Peter Y. A. and Schneider, Steve},
booktitle = {{R}evised {S}elected {P}apers of the 3rd
{I}nternational {W}orkshop on {F}ormal {A}spects in
{S}ecurity and {T}rust ({FAST}'05)},
acronym = {{FAST}'05},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {3866},
pages = {81-95},
year = {2006},
confyear = {2005},
confmonth = {7},
doi = {10.1007/11679219_7},
}
[BKO+08]
ThomasBøgholm,
HenrikKargh-hansen,
PeturOlsen,
BentThomsen, and
Kim GuldstrandLarsen.
Model-based schedulability analysis of safety
critical hard real-time Java programs.
In JTRES'08,
ACM International Conference Proceeding Series 343, pages 106-114. ACM Press, September 2008.
@inproceedings{jtres2008-BKOTL,
author = {B{\o}gholm, Thomas and Kargh{-}hansen, Henrik and
Olsen, Petur and Thomsen, Bent and Larsen, Kim
Guldstrand},
title = {Model-based schedulability analysis of safety
critical hard real-time Java programs},
editor = {Bollella, Gregory and Locke, C. Douglas},
booktitle = {{P}roceedings of the 6th {I}nternational {W}orkshop
on {J}ava {T}echnologies for {R}eal-time and
{E}mbedded {S}ystems ({JTRES}'08)},
acronym = {{JTRES}'08},
publisher = {ACM Press},
series = {ACM International Conference Proceeding Series},
volume = {343},
pages = {106-114},
year = {2008},
month = sep,
doi = {10.1145/1434790.1434807},
}
[BKP86]
HowardBarringer,
RuurdKuiper, and
AmirPnueli.
A Really Abstract Concurrent Model and its Temporal
Logic.
In POPL'86,
pages 173-183.
ACM Press, January 1986.
@inproceedings{popl1986-BKP,
author = {Barringer, Howard and Kuiper, Ruurd and Pnueli,
Amir},
title = {A Really Abstract Concurrent Model and its Temporal
Logic},
booktitle = {Conference Record of the 13th {ACM} {S}ymposium on
{P}rinciples of {P}rogramming {L}anguages
({POPL}'86)},
acronym = {{POPL}'86},
publisher = {ACM Press},
pages = {173-183},
year = {1986},
month = jan,
}
[BKP11]
DietmarBerwanger,
łukaszKaiser, and
BerndPuchala.
A Perfect-Information Construction for Coordination
in Games.
In FSTTCS'11,
Leibniz International Proceedings in Informatics 13, pages 387-398. Leibniz-Zentrum für Informatik, December 2011.
@inproceedings{fsttcs2011-BKP,
author = {Berwanger, Dietmar and Kaiser, {\L}ukasz and
Puchala, Bernd},
title = {A~Perfect-Information Construction for Coordination
in Games},
editor = {Chakraborty, Supratik and Kumar, Amit},
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)},
acronym = {{FSTTCS}'11},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {13},
pages = {387-398},
year = {2011},
month = dec,
}
[BL69]
Julius R.Büchi and
Lawrence H.Landweber.
Solving Sequential Conditions by Finite-State
Strategies.
Transactions of the American Mathematical Society 138:295-311. American Mathematical Society, April 1969.
@article{TAMS138-BL,
author = {B{\"u}chi, Julius R. and Landweber, Lawrence H.},
title = {Solving Sequential Conditions by Finite-State
Strategies},
publisher = {American Mathematical Society},
journal = {Transactions of the American Mathematical Society},
volume = {138},
pages = {295-311},
year = {1969},
month = apr,
}
[BL95]
AhmedBouajjani and
YassineLakhnech.
Temporal Logic + Timed Automata: Expressiveness and
Decidability.
In CONCUR'95,
Lecture Notes in Computer Science 962, pages 531-545. Springer-Verlag, August 1995.
@inproceedings{concur1995-BL,
author = {Bouajjani, Ahmed and Lakhnech, Yassine},
title = {Temporal Logic + Timed Automata: Expressiveness and
Decidability},
editor = {Lee, Insup and Smolka, Scott A.},
booktitle = {{P}roceedings of the 6th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'95)},
acronym = {{CONCUR}'95},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {962},
pages = {531-545},
year = {1995},
month = aug,
}
[BL12]
MikołajBojańczyk and
SławomirLasota.
A Machine-Independent Characterization of Timed
Languages.
In ICALP'12,
Lecture Notes in Computer Science 7392, pages 92-103. Springer-Verlag, July 2012.
@inproceedings{icalp2012-BL,
author = {Boja{\'n}czyk, Miko{\l}aj and Lasota, S{\l}awomir},
title = {A~Machine-Independent Characterization of Timed
Languages},
editor = {Czumaj, Artur and Mehlhorn, Kurt and Pitts, Andrew
and Wattenhofer, Roger},
booktitle = {{P}roceedings of the 39th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'12)~-- Part~{II}},
acronym = {{ICALP}'12},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {7392},
pages = {92-103},
year = {2012},
month = jul,
doi = {10.1007/978-3-642-31585-5_12},
}
[Bla00]
PatrickBlackburn.
Representations, Reasoning and Relational
Structures: a Hybrid Logic Manifesto.
Logic Journal of the IGPL 8(3):339-365. Oxford University Press, May 2000.
@article{jigpl8(3)-Bla,
author = {Blackburn, Patrick},
title = {Representations, Reasoning and Relational
Structures: a Hybrid Logic Manifesto},
publisher = {Oxford University Press},
journal = {Logic Journal of the IGPL},
volume = {8},
number = {3},
pages = {339-365},
year = {2000},
month = may,
}
[BLM07]
PatriciaBouyer,
Kim GuldstrandLarsen, and
NicolasMarkey.
Model Checking One-clock Priced Timed Automata.
In FoSSaCS'07,
Lecture Notes in Computer Science 4423, pages 108-122. Springer-Verlag, March 2007.
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.
@inproceedings{fossacs2007-BLM,
author = {Bouyer, Patricia and Larsen, Kim Guldstrand and
Markey, Nicolas},
title = {Model Checking One-clock Priced Timed Automata},
editor = {Seidl, Helmut},
booktitle = {{P}roceedings of the 10th {I}nternational
{C}onference on {F}oundations of {S}oftware
{S}cience and {C}omputation {S}tructure
({FoSSaCS}'07)},
acronym = {{FoSSaCS}'07},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {4423},
pages = {108-122},
year = {2007},
month = mar,
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.},
}
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 (i.e., whose slopes
lie in {0,1}).
@article{lmcs4(2)-BLM,
author = {Bouyer, Patricia and Larsen, Kim Guldstrand and
Markey, Nicolas},
title = {Model Checking One-clock Priced Timed Automata},
journal = {Logical Methods in Computer Science},
volume = {4},
number = {2},
year = {2008},
month = may,
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\}\)).},
}
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
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–-mdash;for us somewhat
unexpectedly–-mdash;undecidable for weighted timed
automata with four or more clocks.
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.
@inproceedings{qest2012-BLM,
author = {Bouyer, Patricia and Larsen, Kim Guldstrand and
Markey, Nicolas},
title = {Lower-Bound Constrained Runs in Weighted Timed
Automata},
booktitle = {{P}roceedings of the 9th {I}nternational
{C}onference on {Q}uantitative {E}valuation of
{S}ystems ({QEST}'12)},
acronym = {{QEST}'12},
publisher = {IEEE Comp. Soc. Press},
pages = {128-137},
year = {2012},
month = sep,
doi = {10.1109/QEST.2012.28},
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.},
}
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.
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.
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{peva73()-BLM,
author = {Bouyer, Patricia and Larsen, Kim Guldstrand and
Markey, Nicolas},
title = {Lower-Bound Constrained Runs in Weighted Timed
Automata},
publisher = {Elsevier},
journal = {Performance Evaluation},
volume = {73},
pages = {91-109},
year = {2014},
month = mar,
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).},
}
[BLM+07]
ThomasBrihaye,
FrançoisLaroussinie,
NicolasMarkey, and
GhassanOreiby.
Timed Concurrent Game Structures.
In CONCUR'07,
Lecture Notes in Computer Science 4703, pages 445-459. Springer-Verlag, September 2007.
Abstract
We propose a new model for timed games, based on
concurrent game structures (CGSs). Compared to the
classical timed game automata of Asarin
et al., our timed CGSs are "more
concurrent", in the sense that they always allow
all the agents to act on the system, independently
of the delay they want to elapse before their
action. Timed CGSs weaken the "element of
surprise" of timed game automata reported by
de Alfaro et al.
We prove that our model
has nice properties, in particular that
model-checking timed CGSs against timed
ATL is decidable via region
abstraction, and in particular that strategies are
"region-stable" if winning objectives are. We
also propose a new extension of TATL,
containing ATL*, which we
call TALTL. We prove that
model-checking this logic remains decidable on timed
CGSs. Last, we explain how our algorithms can be
adapted in order to rule out Zeno (co-)strategies,
based on the ideas of Henzinger et al.
@inproceedings{concur2007-BLMO,
author = {Brihaye, {\relax Th}omas and Laroussinie, Fran{\c
c}ois and Markey, Nicolas and Oreiby, Ghassan},
title = {Timed Concurrent Game Structures},
editor = {Caires, Lu{\'\i}s and Vasconcelos, Vasco T.},
booktitle = {{P}roceedings of the 18th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'07)},
acronym = {{CONCUR}'07},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {4703},
pages = {445-459},
year = {2007},
month = sep,
doi = {10.1007/978-3-540-74407-8_30},
abstract = {We propose a new model for timed games, based on
concurrent game structures~(CGSs). Compared to the
classical \emph{timed game automata} of~Asarin
\emph{et~al.}, our timed~CGSs are {"}more
concurrent{"}, in the sense that they always allow
all the agents to act on the system, independently
of the delay they want to elapse before their
action. Timed CGSs weaken the {"}element of
surprise{"} of timed game automata reported by
de~Alfaro \emph{et~al.}\par We prove that our model
has nice properties, in particular that
model-checking timed CGSs against timed
\(\textsf{ATL}\) is decidable \emph{via} region
abstraction, and in particular that strategies are
{"}region-stable{"} if winning objectives are. We
also propose a new extension of \(\textsf{TATL}\),
containing~\(\textsf{ATL}^{*}\), which we
call~\(\textsf{TALTL}\). We~prove that
model-checking this logic remains decidable on timed
CGSs. Last, we explain how our algorithms can be
adapted in order to rule out Zeno (co-)strategies,
based on the ideas of Henzinger \emph{et~al.}},
}
[BLM+17]
PatriciaBouyer,
FrançoisLaroussinie,
NicolasMarkey,
JoëlOuaknine, and
JamesWorrell.
Timed temporal logics.
In LucaAceto,
GiorgioBacci,
GiovanniBacci,
AnnaIngólfsdóttir,
AxelLegay, and
RaduMardare (eds.),
Models, Algorithms, Logics and Tools: Essays
Dedicated to Kim Guldstrand Larsen on the Occasion
of His 60th Birthday,
Lecture Notes in Computer Science 10460, pages 211-230. Springer-Verlag, August 2017.
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.
@incollection{kimfest2017-BLMOW,
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, Giovanni
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-Verlag},
series = {Lecture Notes in Computer Science},
volume = {10460},
pages = {211-230},
year = {2017},
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.},
}
[BLM+06]
PatriciaBouyer,
Kim GuldstrandLarsen,
NicolasMarkey, and
Jacob IllumRasmussen.
Almost Optimal Strategies in One-Clock Priced Timed
Automata.
In FSTTCS'06,
Lecture Notes in Computer Science 4337, pages 345-356. Springer-Verlag, December 2006.
Abstract
We consider timed games extended with cost
information, and prove computability of the optimal
cost and of ε-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{fsttcs2006-BLMR,
author = {Bouyer, Patricia and Larsen, Kim Guldstrand and
Markey, Nicolas and Rasmussen, Jacob Illum},
title = {Almost Optimal Strategies in One-Clock Priced Timed
Automata},
editor = {Arun-Kumar, S. and Garg, Naveen},
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)},
acronym = {{FSTTCS}'06},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {4337},
pages = {345-356},
year = {2006},
month = dec,
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.},
}
[BLM+97]
David A. MixBarrington,
Chi-JenLu,
Peter BroMiltersen, and
SvenSkyum.
On Uniformity Within NC1.
Research Report 97-044, Electronic Colloquium on Computational Complexity,
September 1997.
@techreport{eccc1997-BLMS,
author = {Barrington, David A. Mix and Lu, Chi-Jen and
Miltersen, Peter Bro and Skyum, Sven},
title = {On Uniformity Within {{\(\mathit{NC}^1\)}}},
number = {97-044},
year = {1997},
month = sep,
institution = {Electronic Colloquium on Computational Complexity},
type = {Research Report},
}
[BLM+11]
PatriciaBouyer,
Kim GuldstrandLarsen,
NicolasMarkey,
OcanSankur, and
ClausThrane.
Timed automata can always be made implementable.
In CONCUR'11,
Lecture Notes in Computer Science 6901, pages 76-91. Springer-Verlag, September 2011.
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 A, we build a timed
automaton A' that exhibits the same
behaviour as A, and moreover is both
robust and samplable by construction.
@inproceedings{concur2011-BLMST,
author = {Bouyer, Patricia and Larsen, Kim Guldstrand and
Markey, Nicolas and Sankur, Ocan and Thrane, Claus},
title = {Timed automata can always be made implementable},
editor = {Katoen, Joost-Pieter and K{\"o}nig, Barbara},
booktitle = {{P}roceedings of the 22nd {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'11)},
acronym = {{CONCUR}'11},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {6901},
pages = {76-91},
year = {2011},
month = sep,
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.},
}
[BLN03]
DirkBeyer,
ClausLewerentz, and
AndreasNoack.
Rabbit: A Tool for BDD-Based Verification of
Real-Time Systems.
In CAV'03,
Lecture Notes in Computer Science 2725, pages 122-125. Springer-Verlag, July 2003.
@inproceedings{cav2003-BLN,
author = {Beyer, Dirk and Lewerentz, Claus and Noack, Andreas},
title = {Rabbit: A~Tool for {BDD}-Based Verification of
Real-Time Systems},
editor = {Hunt, Jr, Warren A. and Somenzi, Fabio},
booktitle = {{P}roceedings of the 15th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'03)},
acronym = {{CAV}'03},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {2725},
pages = {122-125},
year = {2003},
month = jul,
doi = {10.1007/978-3-540-45069-6_13},
}
[Blo93]
JohannesBlömer.
Computing Sums of Radicals in Polynomial Time.
Technical Report B93-13, Department of Computer Science, University of
Paderborn, Germany,
August 1993.
@techreport{UPad-B93-13-Blo,
author = {Bl{\"o}mer, Johannes},
title = {Computing Sums of Radicals in Polynomial Time},
number = {B93-13},
year = {1993},
month = aug,
institution = {Department of Computer Science, University of
Paderborn, Germany},
}
[BLP03]
GerdBehrmann,
Kim GuldstrandLarsen, and
RadekPelánek.
To Store or not to Store.
In CAV'03,
Lecture Notes in Computer Science 2725, pages 433-445. Springer-Verlag, July 2003.
@inproceedings{cav2003-BLP,
author = {Behrmann, Gerd and Larsen, Kim Guldstrand and
Pel{\'a}nek, Radek},
title = {To Store or not to Store},
editor = {Hunt, Jr, Warren A. and Somenzi, Fabio},
booktitle = {{P}roceedings of the 15th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'03)},
acronym = {{CAV}'03},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {2725},
pages = {433-445},
year = {2003},
month = jul,
}
[BLP+98]
GerdBehrmann,
Kim GuldstrandLarsen,
JustinPearson,
CarstenWeise, and
WangYi.
Efficient Timed Reachability Analysis using Clock
Difference Diagrams.
Research Report RS-98-47, Basic Research in Computer Science, Aalborg
University, Denmark,
December 1998.
@techreport{TR-brics9847,
author = {Behrmann, Gerd and Larsen, Kim Guldstrand and
Pearson, Justin and Weise, Carsten and Yi, Wang},
title = {Efficient Timed Reachability Analysis using Clock
Difference Diagrams},
number = {RS-98-47},
year = {1998},
month = dec,
institution = {Basic Research in Computer Science, Aalborg
University, Denmark},
type = {Research Report},
}
[BLP+99]
GerdBehrmann,
Kim GuldstrandLarsen,
JustinPearson,
CarstenWeise, and
WangYi.
Efficient Timed Reachability Analysis using Clock
Difference Diagrams.
In CAV'99,
Lecture Notes in Computer Science 1633, pages 341-353. Springer-Verlag, July 1999.
@inproceedings{cav1999-BLPWY,
author = {Behrmann, Gerd and Larsen, Kim Guldstrand and
Pearson, Justin and Weise, Carsten and Yi, Wang},
title = {Efficient Timed Reachability Analysis using Clock
Difference Diagrams},
editor = {Halbwachs, Nicolas and Peled, Doron A.},
booktitle = {{P}roceedings of the 11th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'99)},
acronym = {{CAV}'99},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {1633},
pages = {341-353},
year = {1999},
month = jul,
}
[BLR05]
PatriciaBouyer,
FrançoisLaroussinie, and
Pierre-AlainReynier.
Diagonal Constraints in Timed Automata: Forward
Analysis of Timed Systems.
In FORMATS'05,
Lecture Notes in Computer Science 3829, pages 112-126. Springer-Verlag, September 2005.
@inproceedings{formats2005-BLR,
author = {Bouyer, Patricia and Laroussinie, Fran{\c c}ois and
Reynier, Pierre-Alain},
title = {Diagonal Constraints in Timed Automata: Forward
Analysis of Timed Systems},
editor = {Pettersson, Paul and Yi, Wang},
booktitle = {{P}roceedings of the 3rd {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'05)},
acronym = {{FORMATS}'05},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {3829},
pages = {112-126},
year = {2005},
month = sep,
doi = {10.1007/11603009_10},
}
[BLR05]
GerdBehrmann,
Kim GuldstrandLarsen, and
Jacob IllumRasmussen.
Optimal scheduling using priced timed automata.
SIGMETRICS Performance Evaluation Review 32(4):34-40. March 2005.
@article{SIGper32(4)-BLR,
author = {Behrmann, Gerd and Larsen, Kim Guldstrand and
Rasmussen, Jacob Illum},
title = {Optimal scheduling using priced timed automata},
journal = {SIGMETRICS Performance Evaluation Review},
volume = {32},
number = {4},
pages = {34-40},
year = {2005},
month = mar,
}
[BLW01]
BenediktBollig,
MartinLeucker, and
MichaelWeber.
Local Parallel Model Checking for the Alternation
Free μ-Calculus.
Technical Report AIB-2001-04, Aachener Informatik Berichte, Aachen, Germany,
March 2001.
@techreport{TR-Aachen0104,
author = {Bollig, Benedikt and Leucker, Martin and Weber,
Michael},
title = {Local Parallel Model Checking for the Alternation
Free {\(\mu\)}-Calculus},
number = {AIB-2001-04},
year = {2001},
month = mar,
institution = {Aachener Informatik Berichte, Aachen, Germany},
type = {Technical Report},
}
[BM83]
BernardBerthomieu and
MiguelMenasche.
An Enumerative Approach for Analyzing Time Petri
Nets.
In WCC'83,
pages 41-46.
North-Holland/IFIP, September 1983.
@inproceedings{ifipwcc1983-BM,
author = {Berthomieu, Bernard and Menasche, Miguel},
title = {An Enumerative Approach for Analyzing Time {P}etri
Nets},
editor = {Mason, R. E. A.},
booktitle = {{I}nformation {P}rocessing~83~-- {P}roceedings of
the 9th {IFIP} {W}orld {C}omputer {C}ongress
({WCC}'83)},
acronym = {{WCC}'83},
publisher = {North-Holland/IFIP},
pages = {41-46},
year = {1983},
month = sep,
}
[BM95]
Michael S.Branicky and
Sanjoy K.Mitter.
Algorithms for Optimal Hybrid Control.
In CDC'95,
pages 2661-2666.
IEEE Comp. Soc. Press, December 1995.
@inproceedings{cdc1995-BM,
author = {Branicky, Michael S. and Mitter, Sanjoy K.},
title = {Algorithms for Optimal Hybrid Control},
booktitle = {{P}roceedings of the 34th {IEEE} {C}onference on
{D}ecision and {C}ontrol ({CDC}'95)},
acronym = {{CDC}'95},
publisher = {IEEE Comp. Soc. Press},
pages = {2661-2666},
year = {1995},
month = dec,
}
[BM00]
EdBrinksma and
AngelikaMader.
Verification and Optimization of a PLC Control
Schedule.
In SPIN'00,
Lecture Notes in Computer Science 1885, pages 73-92. Springer-Verlag, August 2000.
@inproceedings{spin2000-BM,
author = {Brinksma, Ed and Mader, Angelika},
title = {Verification and Optimization of a {PLC} Control
Schedule},
editor = {Havelund, Klaus and Penix, John and Viser, Willem},
booktitle = {{P}roceedings of the 7th {I}nternational {SPIN}
{W}orkshop ({SPIN}'00)},
acronym = {{SPIN}'00},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {1885},
pages = {73-92},
year = {2000},
month = aug,
}
[BM07]
PatriciaBouyer and
NicolasMarkey.
Costs are Expensive!.
In FORMATS'07,
Lecture Notes in Computer Science 4763, pages 53-68. Springer-Verlag, October 2007.
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.
@inproceedings{formats2007-BM,
author = {Bouyer, Patricia and Markey, Nicolas},
title = {Costs are Expensive!},
editor = {Raskin, Jean-Fran{\c c}ois and Thiagarajan, P. S.},
booktitle = {{P}roceedings of the 5th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'07)},
acronym = {{FORMATS}'07},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {4763},
pages = {53-68},
year = {2007},
month = oct,
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.},
}
[BMF02]
EdBrinksma,
AngelikaMader, and
AnsgarFehnker.
Verification and Optimization of a PLC Control
Schedule.
International Journal on Software Tools for
Technology Transfer 4(1):21-33. Springer-Verlag, 2002.
@article{sttt4(1)-BMF,
author = {Brinksma, Ed and Mader, Angelika and Fehnker,
Ansgar},
title = {Verification and Optimization of a {PLC} Control
Schedule},
publisher = {Springer-Verlag},
journal = {International Journal on Software Tools for
Technology Transfer},
volume = {4},
number = {1},
pages = {21-33},
year = {2002},
}
[BMM14]
PatriciaBouyer,
NicolasMarkey, and
Raj MohanMatteplackel.
Averaging in LTL.
In CONCUR'14,
Lecture Notes in Computer Science 8704, pages 266-280. Springer-Verlag, September 2014.
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–-mdash;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!
In a
recent line of works, several authors have proposed
quantitative semantics for temporal logics, using
e.g. discounting modalities (which give less
importance to distant events). In the present paper,
we define and study a quantitative semantics of LTL
with 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.
@inproceedings{concur2014-BMM,
author = {Bouyer, Patricia and Markey, Nicolas and
Matteplackel, Raj~Mohan},
title = {Averaging in~{LTL}},
editor = {Baldan, Paolo and Gorla, Daniele},
booktitle = {{P}roceedings of the 25th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'14)},
acronym = {{CONCUR}'14},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8704},
pages = {266-280},
year = {2014},
month = sep,
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.},
}
[BMM+00]
Jean-CamilleBirget,
Stuart W.Margolis,
John C.Meakin, and
PascalWeil.
PSPACE-Completeness of Certain Algorithmic
Problems on the Subgroups of Free Groups.
Theoretical Computer Science 242(1-2):247-281. Elsevier, July 2000.
@article{tcs242(1-2)-BMMW,
author = {Birget, Jean-Camille and Margolis, Stuart W. and
Meakin, John C. and Weil, Pascal},
title = {{PSPACE}-Completeness of Certain Algorithmic
Problems on the Subgroups of Free Groups},
publisher = {Elsevier},
journal = {Theoretical Computer Science},
volume = {242},
number = {1-2},
pages = {247-281},
year = {2000},
month = jul,
}
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
insertion errors, 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{stacs2008-BMOSW,
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},
editor = {Albers, Susanne and Weil, Pascal},
booktitle = {{P}roceedings of the 25th {S}ymposium on
{T}heoretical {A}spects of {C}omputer {S}cience
({STACS}'08)},
acronym = {{STACS}'08},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {1},
pages = {121-132},
year = {2008},
month = feb,
doi = {10.4230/LIPIcs.STACS.2008.1339},
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.},
}
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
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.
@article{fac24(4-6)-BMOSW,
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},
publisher = {Springer-Verlag},
journal = {Formal Aspects of Computing},
volume = {24},
number = {4-6},
pages = {595-607},
year = {2012},
month = jul,
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.},
}
[BMO+11]
PatriciaBouyer,
NicolasMarkey,
JörgOlschewski, and
MichaelUmmels.
Measuring Permissiveness in Parity Games:
Mean-Payoff Parity Games Revisited.
In ATVA'11,
Lecture Notes in Computer Science 6996, pages 135-149. Springer-Verlag, October 2011.
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/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 NP∩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{atva2011-BMOU,
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},
editor = {Bultan, Tevfik and Hsiung, Pao-Ann},
booktitle = {{P}roceedings of the 9th {I}nternational {S}ymposium
on {A}utomated {T}echnology for {V}erification and
{A}nalysis ({ATVA}'11)},
acronym = {{ATVA}'11},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {6996},
pages = {135-149},
year = {2011},
month = oct,
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.},
}
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.
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).
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{lics2007-BMOW,
author = {Bouyer, Patricia and Markey, Nicolas and Ouaknine,
Jo{\"e}l and Worrell, James},
title = {The Cost of Punctuality},
booktitle = {{P}roceedings of the 22nd {A}nnual {S}ymposium on
{L}ogic in {C}omputer {S}cience ({LICS}'07)},
acronym = {{LICS}'07},
publisher = {IEEE Comp. Soc. Press},
pages = {109-118},
year = {2007},
month = jul,
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.},
}
[BMO+08]
PatriciaBouyer,
NicolasMarkey,
JoëlOuaknine, and
JamesWorrell.
On Expressiveness and Complexity in Real-time Model
Checking.
In ICALP'08,
Lecture Notes in Computer Science 5126, pages 124-135. Springer-Verlag, July 2008.
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 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{icalp2008-BMOW,
author = {Bouyer, Patricia and Markey, Nicolas and Ouaknine,
Jo{\"e}l and Worrell, James},
title = {On Expressiveness and Complexity in Real-time Model
Checking},
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},
booktitle = {{P}roceedings of the 35th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'08)~-- Part~{II}},
acronym = {{ICALP}'08},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {5126},
pages = {124-135},
year = {2008},
month = jul,
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.},
}
[BMP10]
LauraBozzelli,
AnielloMurano, and
AdrianoPeron.
Pushdown module checking.
Formal Methods in System Design 36(1):65-95. Springer-Verlag, February 2010.
@article{fmsd36(1)-BMP,
author = {Bozzelli, Laura and Murano, Aniello and Peron,
Adriano},
title = {Pushdown module checking},
publisher = {Springer-Verlag},
journal = {Formal Methods in System Design},
volume = {36},
number = {1},
pages = {65-95},
year = {2010},
month = feb,
}
[BMP+15]
PatriciaBouyer,
NicolasMarkey,
NicolasPerrin, and
PhilippSchlehuber-Caissier.
Timed automata abstraction of switched dynamical
systems using control funnels.
In FORMATS'15,
Lecture Notes in Computer Science 9268, pages 60-75. Springer-Verlag, September 2015.
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 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{formats2015-BMPS,
author = {Bouyer, Patricia and Markey, Nicolas and Perrin,
Nicolas and Schlehuber{-}Caissier, Philipp},
title = {Timed automata abstraction of switched dynamical
systems using control funnels},
editor = {Sankaranarayanan, Sriram and Vicario, Enrico},
booktitle = {{P}roceedings of the 13th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'15)},
acronym = {{FORMATS}'15},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9268},
pages = {60-75},
year = {2015},
month = sep,
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.},
}
[BMP+17]
PatriciaBouyer,
NicolasMarkey,
NicolasPerrin, and
PhilippSchlehuber-Caissier.
Timed automata abstraction of switched dynamical
systems using control funnels.
Real-Time Systems 53(3):327-353. Kluwer Academic, May 2017.
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.
@article{rts53(3)-BMPS,
author = {Bouyer, Patricia and Markey, Nicolas and Perrin,
Nicolas and Schlehuber{-}Caissier, Philipp},
title = {Timed automata abstraction of switched dynamical
systems using control funnels},
publisher = {Kluwer Academic},
journal = {Real-Time Systems},
volume = {53},
number = {3},
pages = {327-353},
year = {2017},
month = may,
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.},
}
[BMP+97]
MartinBeaudry,
PierreMcKenzie,
PierrePéladeau, and
DenisThérien.
Finite Monoids: From Word to Circuit Evaluation.
SIAM Journal on Computing 26(1):138-152. Society for Industrial and Applied Math., February 1997.
@article{siamcomp26(1)-BMPT,
author = {Beaudry, Martin and McKenzie, Pierre and
P{\'e}ladeau, Pierre and Th{\'e}rien, Denis},
title = {Finite Monoids: From Word to Circuit Evaluation},
publisher = {Society for Industrial and Applied Math.},
journal = {SIAM Journal on Computing},
volume = {26},
number = {1},
pages = {138-152},
year = {1997},
month = feb,
}
[BMR06]
PatriciaBouyer,
NicolasMarkey, and
Pierre-AlainReynier.
Robust Model-Checking of Linear-Time Properties in
Timed Automata.
In LATIN'06,
Lecture Notes in Computer Science 3887, pages 238-249. Springer-Verlag, March 2006.
Abstract
Formal verification of timed systems is well
understood, but their implementation is still
challenging. Recent works by Raskin et al.
have brought out a model of parameterized timed
automata that can be used to prove
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üchi-like and LTL
properties. We also verify bounded-response-time
properties.
@inproceedings{latin2006-BMR,
author = {Bouyer, Patricia and Markey, Nicolas and Reynier,
Pierre-Alain},
title = {Robust Model-Checking of Linear-Time Properties in
Timed Automata},
editor = {Correa, Jos{\'e} R. and Hevia, Alejandro and Kiwi,
Marcos},
booktitle = {{P}roceedings of the 7th {L}atin {A}merican
{S}ymposium on {T}heoretical {IN}formatics
({LATIN}'06)},
acronym = {{LATIN}'06},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {3887},
pages = {238-249},
year = {2006},
month = mar,
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.},
}
[BMR08]
PatriciaBouyer,
NicolasMarkey, and
Pierre-AlainReynier.
Robust Analysis of Timed Automata via Channel
Machines.
In FoSSaCS'08,
Lecture Notes in Computer Science 4962, pages 157-171. Springer-Verlag, March 2008.
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{fossacs2008-BMR,
author = {Bouyer, Patricia and Markey, Nicolas and Reynier,
Pierre-Alain},
title = {Robust Analysis of Timed Automata via Channel
Machines},
editor = {Amadio, Roberto},
booktitle = {{P}roceedings of the 11th {I}nternational
{C}onference on {F}oundations of {S}oftware
{S}cience and {C}omputation {S}tructure
({FoSSaCS}'08)},
acronym = {{FoSSaCS}'08},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {4962},
pages = {157-171},
year = {2008},
month = mar,
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.},
}
[BMR14]
VéroniqueBruyère,
NoëmieMeunier, and
Jean-FrançoisRaskin.
Secure Equilibria in Weighted Games.
In CSL/ LICS'14.
ACM Press, July 2014.
@inproceedings{csllics2014-BMR,
author = {Bruy{\`e}re, V{\'e}ronique and Meunier, No{\"e}mie
and Raskin, Jean-Fran{\c c}ois},
title = {Secure Equilibria in Weighted Games},
booktitle = {{P}roceedings of the Joint Meeting of the 23rd
{EACSL} {A}nnual {C}onference on {C}omputer
{S}cience {L}ogic and the 29th {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer
{S}cience ({CSL\slash LICS}'14)},
acronym = {{CSL\slash LICS}'14},
publisher = {ACM Press},
chapter = {26},
year = {2014},
month = jul,
doi = {10.1145/2603088.2603109},
}
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{gandalf2015-BMRLL,
author = {Bouyer, Patricia and Markey, Nicolas and Randour,
Mickael and Larsen, Kim Guldstrand and Laursen,
Simon},
title = {Average-energy games},
editor = {Esparza, Javier and Tronci, Enrico},
booktitle = {{P}roceedings of the 6th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics and {F}ormal
{V}erification ({GandALF}'15)},
acronym = {{GandALF}'15},
series = {Electronic Proceedings in Theoretical Computer
Science},
volume = {193},
pages = {1-15},
year = {2015},
month = sep,
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.},
}
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.
@article{acta55(2)-BMRLL,
author = {Bouyer, Patricia and Markey, Nicolas and Randour,
Mickael and Larsen, Kim Guldstrand and Laursen,
Simon},
title = {Average-energy games},
publisher = {Springer-Verlag},
journal = {Acta Informatica},
volume = {55},
number = {2},
year = {2018},
month = mar,
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
\(\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.},
}
[BMR+16]
PatriciaBouyer,
NicolasMarkey,
MickaelRandour,
ArnaudSangnier, and
DanielStan.
Reachability in Networks of Register Protocols under
Stochastic Schedulers.
In ICALP'16,
Leibniz International Proceedings in Informatics 55, pages 106:1-106:14. Leibniz-Zentrum für Informatik, July 2016.
Abstract
We study the almost-sure reachability problem in a
distributed system obtained as the asynchronous
composition of N copies (called
processes) of the same automaton (called
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.
@inproceedings{icalp2016-BMRSS,
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},
editor = {Chatzigiannakis, Ioannis and Mitzenmacher, Michael
and Rabani, Yuval and Sangiorgi, Davide},
booktitle = {{P}roceedings of the 43rd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'16)~-- Part~{II}},
acronym = {{ICALP}'16},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {55},
pages = {106:1-106:14},
year = {2016},
month = jul,
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.},
}
[BMS11]
PatriciaBouyer,
NicolasMarkey, and
OcanSankur.
Robust Model-Checking of Timed Automata via Pumping
in Channel Machines.
In FORMATS'11,
Lecture Notes in Computer Science 6919, pages 97-112. Springer-Verlag, September 2011.
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.
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.
In this work, we show that robust
model-checking against ω-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
ω-regular properties, which is both optimal
and valid for general timed automata.
@inproceedings{formats2011-BMS,
author = {Bouyer, Patricia and Markey, Nicolas and Sankur,
Ocan},
title = {Robust Model-Checking of Timed Automata via Pumping
in Channel Machines},
editor = {Fahrenberg, Uli and Tripakis, Stavros},
booktitle = {{P}roceedings of the 9th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'11)},
acronym = {{FORMATS}'11},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {6919},
pages = {97-112},
year = {2011},
month = sep,
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.},
}
[BMS12]
PatriciaBouyer,
NicolasMarkey, and
OcanSankur.
Robust reachability in timed automata: a game-based
approach.
In ICALP'12,
Lecture Notes in Computer Science 7392, pages 128-140. Springer-Verlag, July 2012.
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.
@inproceedings{icalp2012-BMS,
author = {Bouyer, Patricia and Markey, Nicolas and Sankur,
Ocan},
title = {Robust reachability in timed automata: a~game-based
approach},
editor = {Czumaj, Artur and Mehlhorn, Kurt and Pitts, Andrew
and Wattenhofer, Roger},
booktitle = {{P}roceedings of the 39th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'12)~-- Part~{II}},
acronym = {{ICALP}'12},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {7392},
pages = {128-140},
year = {2012},
month = jul,
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.},
}
[BMS13]
PatriciaBouyer,
NicolasMarkey, and
OcanSankur.
Robustness in timed automata.
In RP'13,
Lecture Notes in Computer Science 8169, pages 1-18. Springer-Verlag, September 2013.
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.
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{rp2013-BMS,
author = {Bouyer, Patricia and Markey, Nicolas and Sankur,
Ocan},
title = {Robustness in timed automata},
editor = {Abdulla, Parosh Aziz and Potapov, Igor},
booktitle = {{P}roceedings of the 7th {W}orkshop on
{R}eachability {P}roblems in {C}omputational
{M}odels ({RP}'13)},
acronym = {{RP}'13},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8169},
pages = {1-18},
year = {2013},
month = sep,
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.},
}
[BMS13]
PatriciaBouyer,
NicolasMarkey, and
OcanSankur.
Robust Weighted Timed Automata and Games.
In FORMATS'13,
Lecture Notes in Computer Science 8053, pages 31-46. Springer-Verlag, August 2013.
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{formats2013-BMS,
author = {Bouyer, Patricia and Markey, Nicolas and Sankur,
Ocan},
title = {Robust Weighted Timed Automata and Games},
editor = {Braberman, V{\'\i}ctor and Fribourg, Laurent},
booktitle = {{P}roceedings of the 11th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'13)},
acronym = {{FORMATS}'13},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {8053},
pages = {31-46},
year = {2013},
month = aug,
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.},
}
[BMS14]
PatriciaBouyer,
NicolasMarkey, and
DanielStan.
Mixed Nash Equilibria in Concurrent Games.
In FSTTCS'14,
Leibniz International Proceedings in Informatics 29, pages 351-363. Leibniz-Zentrum für Informatik, December 2014.
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.
@inproceedings{fsttcs2014-BMS,
author = {Bouyer, Patricia and Markey, Nicolas and Stan,
Daniel},
title = {Mixed {N}ash Equilibria in Concurrent Games},
editor = {Raman, Venkatesh and Suresh, S. P.},
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)},
acronym = {{FSTTCS}'14},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {29},
pages = {351-363},
year = {2014},
month = dec,
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.},
}
[BMS15]
PatriciaBouyer,
NicolasMarkey, and
OcanSankur.
Robust Reachability in Timed Automata and Games:
A Game-based Approach.
Theoretical Computer Science 563:43-74. Elsevier, January 2015.
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.
@article{tcs563()-BMS,
author = {Bouyer, Patricia and Markey, Nicolas and Sankur,
Ocan},
title = {Robust Reachability in Timed Automata and Games:
A~Game-based Approach},
publisher = {Elsevier},
journal = {Theoretical Computer Science},
volume = {563},
pages = {43-74},
year = {2015},
month = jan,
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.},
}
[BMS16]
PatriciaBouyer,
NicolasMarkey, and
DanielStan.
Stochastic Equilibria under Imprecise Deviations in
Terminal-Reward Concurrent Games.
In GandALF'16,
Electronic Proceedings in Theoretical Computer
Science 226, pages 61-75. September 2016.
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.
@inproceedings{gandalf2016-BMS,
author = {Bouyer, Patricia and Markey, Nicolas and Stan,
Daniel},
title = {Stochastic Equilibria under Imprecise Deviations in
Terminal-Reward Concurrent Games},
editor = {Cantone, Domenico and Delzanno, Giorgio},
booktitle = {{P}roceedings of the 7th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics and {F}ormal
{V}erification ({GandALF}'16)},
acronym = {{GandALF}'16},
series = {Electronic Proceedings in Theoretical Computer
Science},
volume = {226},
pages = {61-75},
year = {2016},
month = sep,
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.},
}
[BMT99]
AugustinBaziramwabo,
PierreMcKenzie, and
DenisThérien.
Modular Temporal Logic.
In LICS'99,
pages 344-351.
IEEE Comp. Soc. Press, July 1999.
@inproceedings{lics1999-BMT,
author = {Baziramwabo, Augustin and McKenzie, Pierre and
Th{\'e}rien, Denis},
title = {Modular Temporal Logic},
booktitle = {{P}roceedings of the 14th {A}nnual {S}ymposium on
{L}ogic in {C}omputer {S}cience ({LICS}'99)},
acronym = {{LICS}'99},
publisher = {IEEE Comp. Soc. Press},
pages = {344-351},
year = {1999},
month = jul,
}
[BMV14]
PatriciaBouyer,
NicolasMarkey, and
SteenVester.
Nash Equilibria in Symmetric Games with Partial
Observation.
In SR'14,
Electronic Proceedings in Theoretical Computer
Science 146, pages 49-55. March 2014.
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{sr2014-BMV,
author = {Bouyer, Patricia and Markey, Nicolas and Vester,
Steen},
title = {Nash Equilibria in Symmetric Games with Partial
Observation},
booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop
on {S}trategic {R}easoning ({SR}'14)},
acronym = {{SR}'14},
series = {Electronic Proceedings in Theoretical Computer
Science},
volume = {146},
pages = {49-55},
year = {2014},
month = mar,
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.},
}
[BMV15]
DietmarBerwanger,
Anup BasilMathew, and
MarieVan den Bogaard.
Hierarchical Information Patterns and Distributed
Strategy Synthesis.
In ATVA'15,
Lecture Notes in Computer Science 9364, pages 378-393. Springer-Verlag, October 2015.
@inproceedings{atva2015-BMV,
author = {Berwanger, Dietmar and Mathew, Anup Basil and
Van{~}den{ }Bogaard, Marie},
title = {Hierarchical Information Patterns and Distributed
Strategy Synthesis},
editor = {Finkbeiner, Bernd and Pu, Geguang and Zhang, Lijun},
booktitle = {{P}roceedings of the 13th {I}nternational
{S}ymposium on {A}utomated {T}echnology for
{V}erification and {A}nalysis ({ATVA}'15)},
acronym = {{ATVA}'15},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {9364},
pages = {378-393},
year = {2015},
month = oct,
}
[BMV17]
PatriciaBouyer,
NicolasMarkey, and
SteenVester.
Nash Equilibria in Symmetric Graph Games with
Partial Observation.
Information and Computation 254(2):238-258. Elsevier, June 2017.
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{icomp254()-BMV,
author = {Bouyer, Patricia and Markey, Nicolas and Vester,
Steen},
title = {{N}ash Equilibria in Symmetric Graph Games with
Partial Observation},
publisher = {Elsevier},
journal = {Information and Computation},
volume = {254},
number = {2},
pages = {238-258},
year = {2017},
month = jun,
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.},
}
[BO04]
Stephen J.Bellantoni and
IsabelOitavem.
Separating NC along the
δ axis.
Theoretical Computer Science 318(1-2):57-78. Elsevier, June 2004.
@article{tcs318(1-2)-BO,
author = {Bellantoni, Stephen J. and Oitavem, Isabel},
title = {Separating {{\(\mathrm{NC}\)}} along the
{{\(\delta\)}} axis},
publisher = {Elsevier},
journal = {Theoretical Computer Science},
volume = {318},
number = {1-2},
pages = {57-78},
year = {2004},
month = jun,
doi = {10.1016/j.tcs.2003.10.021},
}
[Bod88]
Hans L.Bodlaender.
Dynamic Programming on Graphs with Bounded
Treewidth.
In ICALP'88,
Lecture Notes in Computer Science 317, pages 105-118. Springer-Verlag, July 1988.
@inproceedings{icalp1988-Bod,
author = {Bodlaender, Hans L.},
title = {Dynamic Programming on Graphs with Bounded
Treewidth},
editor = {Lepist{\"o}, Timo and Salomaa, Arto},
booktitle = {{P}roceedings of the 15th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'88)},
acronym = {{ICALP}'88},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {317},
pages = {105-118},
year = {1988},
month = jul,
doi = {10.1007/3-540-19488-6_110},
}
[Bod93]
Hans L.Bodlaender.
A Tourist Guide through Treewidth.
Acta Cybernetica 11(1-2):1-21. Institute of Informatics, University of Szeged, 1993.
@article{actacyb11(1-2)-Bod,
author = {Bodlaender, Hans L.},
title = {A~Tourist Guide through Treewidth},
publisher = {Institute of Informatics, University of Szeged},
journal = {Acta Cybernetica},
volume = {11},
number = {1-2},
pages = {1-21},
year = {1993},
}
[Bod96]
Hans L.Bodlaender.
A linear-time algorithm for finding
tree-decompositions of small treewidth.
SIAM Journal on Computing 25(6):1305-1317. Society for Industrial and Applied Math., December 1996.
@article{siamcomp25(6)-Bod,
author = {Bodlaender, Hans L.},
title = {A~linear-time algorithm for finding
tree-decompositions of small treewidth},
publisher = {Society for Industrial and Applied Math.},
journal = {SIAM Journal on Computing},
volume = {25},
number = {6},
pages = {1305-1317},
year = {1996},
month = dec,
doi = {10.1137/S0097539793251219},
}
[Boj08]
MikołajBojańczyk.
The Common Fragment of ACTL and LTL.
In FoSSaCS'08,
Lecture Notes in Computer Science 4962, pages 172-185. Springer-Verlag, March 2008.
@inproceedings{fossacs2008-Boj,
author = {Boja{\'n}czyk, Miko{\l}aj},
title = {The Common Fragment of {ACTL} and~{LTL}},
editor = {Amadio, Roberto},
booktitle = {{P}roceedings of the 11th {I}nternational
{C}onference on {F}oundations of {S}oftware
{S}cience and {C}omputation {S}tructure
({FoSSaCS}'08)},
acronym = {{FoSSaCS}'08},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {4962},
pages = {172-185},
year = {2008},
month = mar,
}
[Bou02]
PatriciaBouyer.
Timed Automata May Cause some Troubles.
Research Report LSV-02-09, Lab. Spécification & Vérification, ENS Cachan,
France,
July 2002.
@techreport{LSV0209-Bou,
author = {Bouyer, Patricia},
title = {Timed Automata May Cause some Troubles},
number = {LSV-02-09},
year = {2002},
month = jul,
institution = {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
France},
type = {Research Report},
}
[Bou03]
PatriciaBouyer.
Untameable Timed Automata!.
In STACS'03,
Lecture Notes in Computer Science 2607, pages 620-631. Springer-Verlag, February 2003.
@inproceedings{stacs2003-Bou,
author = {Bouyer, Patricia},
title = {Untameable Timed Automata!},
editor = {Alt, Helmut and Habib, Michel},
booktitle = {{P}roceedings of the 20th {S}ymposium on
{T}heoretical {A}spects of {C}omputer {S}cience
({STACS}'03)},
acronym = {{STACS}'03},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {2607},
pages = {620-631},
year = {2003},
month = feb,
doi = {10.1007/3-540-36494-3_54},
}
[Bou04]
PatriciaBouyer.
Forward Analysis of Updatable Timed Automata.
Formal Methods in System Design 24(3):281-320. Kluwer Academic, May 2004.
@article{fmsd24(3)-Bou,
author = {Bouyer, Patricia},
title = {Forward Analysis of Updatable Timed Automata},
publisher = {Kluwer Academic},
journal = {Formal Methods in System Design},
volume = {24},
number = {3},
pages = {281-320},
year = {2004},
month = may,
doi = {10.1023/B:FORM.0000026093.21513.31},
}
[Boz08]
LauraBozzelli.
The complexity of CTL* + Linear
Past.
In FoSSaCS'08,
Lecture Notes in Computer Science 4962, pages 186-200. Springer-Verlag, March 2008.
@inproceedings{fossacs2008-Boz,
author = {Bozzelli, Laura},
title = {The complexity of CTL\textsuperscript{*} + Linear
Past},
editor = {Amadio, Roberto},
booktitle = {{P}roceedings of the 11th {I}nternational
{C}onference on {F}oundations of {S}oftware
{S}cience and {C}omputation {S}tructure
({FoSSaCS}'08)},
acronym = {{FoSSaCS}'08},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {4962},
pages = {186-200},
year = {2008},
month = mar,
}
[BP03]
BrunoBlanchet and
AndreasPodelski.
Verification of Cryptographic Protocols: Tagging
Enforces Temrination.
In FoSSaCS'03,
Lecture Notes in Computer Science 2620, pages 136-152. Springer-Verlag, April 2003.
@inproceedings{fossacs2003-BP,
author = {Blanchet, Bruno and Podelski, Andreas},
title = {Verification of Cryptographic Protocols: Tagging
Enforces Temrination},
editor = {Gordon, Andrew D.},
booktitle = {{P}roceedings of the 6th {I}nternational
{C}onference on {F}oundations of {S}oftware
{S}cience and {C}omputation {S}tructure
({FoSSaCS}'03)},
acronym = {{FoSSaCS}'03},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {2620},
pages = {136-152},
year = {2003},
month = apr,
}
[BPM81]
MordechaiBen-Ari,
AmirPnueli, and
ZoharManna.
The Temporal Logic of Branching Time.
In POPL'81,
pages 164-176.
ACM Press, January 1981.
@inproceedings{popl1981-BPM,
author = {Ben{-}Ari, Mordechai and Pnueli, Amir and Manna,
Zohar},
title = {The Temporal Logic of Branching Time},
booktitle = {Conference Record of the 8th {ACM} {S}ymposium on
{P}rinciples of {P}rogramming {L}anguages
({POPL}'81)},
acronym = {{POPL}'81},
publisher = {ACM Press},
pages = {164-176},
year = {1981},
month = jan,
}
[BPM83]
MordechaiBen-Ari,
AmirPnueli, and
ZoharManna.
The Temporal Logic of Branching Time.
Acta Informatica 20:207-226. Springer-Verlag, 1983.
@article{acta20()-BPM,
author = {Ben{-}Ari, Mordechai and Pnueli, Amir and Manna,
Zohar},
title = {The Temporal Logic of Branching Time},
publisher = {Springer-Verlag},
journal = {Acta Informatica},
volume = {20},
pages = {207-226},
year = {1983},
}
[BR02]
DanièleBeauquier and
AlexanderRabinovich.
Monadic Logic of Order over Naturals has no Finite
Base.
Journal of Logic and Computation 12(2):243-253. Oxford University Press, April 2002.
@article{jlc12(2)-BR,
author = {Beauquier, Dani{\`e}le and Rabinovich, Alexander},
title = {Monadic Logic of Order over Naturals has no Finite
Base},
publisher = {Oxford University Press},
journal = {Journal of Logic and Computation},
volume = {12},
number = {2},
pages = {243-253},
year = {2002},
month = apr,
}
[BR03]
VéroniqueBruyère and
Jean-FrançoisRaskin.
Real-Time Model-Checking: Parameters Everywhere.
In FSTTCS'03,
Lecture Notes in Computer Science 2914, pages 100-111. Springer-Verlag, December 2003.
@inproceedings{fsttcs2003-BR,
author = {Bruy{\`e}re, V{\'e}ronique and Raskin, Jean-Fran{\c
c}ois},
title = {Real-Time Model-Checking: {P}arameters Everywhere},
editor = {Pandya, Paritosh K. and Radhakrishnan, Jaikumar},
booktitle = {{P}roceedings of the 23rd {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience ({FSTTCS}'03)},
acronym = {{FSTTCS}'03},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {2914},
pages = {100-111},
year = {2003},
month = dec,
}
[Bra98]
Julian C.Bradfield.
The Modal Mu-Calculus Alternation Hierarchy is
Strict.
Theoretical Computer Science 195(2):133-153. Elsevier, March 1998.
@article{tcs195(2)-Bra,
author = {Bradfield, Julian C.},
title = {The Modal Mu-Calculus Alternation Hierarchy is
Strict},
publisher = {Elsevier},
journal = {Theoretical Computer Science},
volume = {195},
number = {2},
pages = {133-153},
year = {1998},
month = mar,
}
[BRB90]
Karl S.Brace,
Richard L.Ruddel, and
Randal E.Bryant.
Efficient Implementation of a BDD package.
In DAC'90,
pages 40-45.
IEEE Comp. Soc. Press, June 1990.
@inproceedings{dac1990-BRB,
author = {Brace, Karl S. and Ruddel, Richard L. and Bryant,
Randal E.},
title = {Efficient Implementation of a {BDD} package},
booktitle = {{P}roceedings of the 27th {D}esign {A}utomation
{C}onference ({DAC}'90)},
acronym = {{DAC}'90},
publisher = {IEEE Comp. Soc. Press},
pages = {40-45},
year = {1990},
month = jun,
}
[Bre12]
RomainBrenguier.
Nash Equilibria in Concurrent Games –Application to
Timed Games.
Thèse de doctorat,
Lab. Spécification & Vérification, ENS Cachan,
France,
November 2012.
@phdthesis{phd-brenguier,
author = {Brenguier, Romain},
title = {Nash Equilibria in Concurrent Games~--Application to
Timed Games},
year = {2012},
month = nov,
school = {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
France},
type = {Th\`ese de doctorat},
}
[Bre16]
RomainBrenguier.
Optimal Assumptions for Synthesis.
In CONCUR'16,
Leibniz International Proceedings in Informatics 59, pages 8:1-8:15. Leibniz-Zentrum für Informatik, August 2016.
@inproceedings{concur2016-Bre,
author = {Brenguier, Romain},
title = {Optimal Assumptions for Synthesis},
editor = {Desharnais, Jules and Jagadeesan, Radha},
booktitle = {{P}roceedings of the 27th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'16)},
acronym = {{CONCUR}'16},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {59},
pages = {8:1-8:15},
year = {2016},
month = aug,
doi = {10.4230/LIPIcs.CONCUR.2016.8},
}
[BRS13]
Marcello MariaBersani,
MatteoRossi, and
PierluigiSan Pietro.
Deciding the Satisfiability of MITL
Specifications.
In GandALF'13,
Electronic Proceedings in Theoretical Computer
Science 119, pages 64-78. August 2013.
@inproceedings{gandalf2013-BRS,
author = {Bersani, Marcello Maria and Rossi, Matteo and
San{~}Pietro, Pierluigi},
title = {Deciding the Satisfiability of {MITL}
Specifications},
editor = {Puppis, Gabriele and Villa, Tiziano},
booktitle = {{P}roceedings of the 4th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics and {F}ormal
{V}erification ({GandALF}'13)},
acronym = {{GandALF}'13},
series = {Electronic Proceedings in Theoretical Computer
Science},
volume = {119},
pages = {64-78},
year = {2013},
month = aug,
doi = {10.4204/EPTCS.119.8},
}
[BRS14]
RomainBrenguier,
Jean-FrançoisRaskin, and
MathieuSassolas.
The complexity of admissibility in omega-regular
games.
In CSL/ LICS'14,
pages 23:1-23:10.
ACM Press, July 2014.
@inproceedings{csllics2014-BRS,
author = {Brenguier, Romain and Raskin, Jean-Fran{\c c}ois and
Sassolas, Mathieu},
title = {The complexity of admissibility in omega-regular
games},
booktitle = {{P}roceedings of the Joint Meeting of the 23rd
{EACSL} {A}nnual {C}onference on {C}omputer
{S}cience {L}ogic and the 29th {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer
{S}cience ({CSL\slash LICS}'14)},
acronym = {{CSL\slash LICS}'14},
publisher = {ACM Press},
pages = {23:1-23:10},
year = {2014},
month = jul,
doi = {10.1145/2603088.2603143},
}
@article{acta54(1)-BRS,
author = {Brenguier, Romain and Raskin, Jean-Fran{\c c}ois and
Sankur, Ocan},
title = {Assume-admissible synthesis},
publisher = {Springer-Verlag},
journal = {Acta Informatica},
volume = {54},
number = {1},
pages = {41-83},
year = {2017},
month = feb,
doi = {10.1007/s00236-016-0273-2},
}
[Bru13]
BenediktBrütsch.
Synthesizing structured reactive programs via
deterministic tree automata.
In SR'13,
Electronic Proceedings in Theoretical Computer
Science 112, pages 107-113. March 2013.
@inproceedings{sr2013-Bru,
author = {Br{\"u}tsch, Benedikt},
title = {Synthesizing structured reactive programs via
deterministic tree automata},
booktitle = {{P}roceedings of the 1st {I}nternational {W}orkshop
on {S}trategic {R}easoning ({SR}'13)},
acronym = {{SR}'13},
series = {Electronic Proceedings in Theoretical Computer
Science},
volume = {112},
pages = {107-113},
year = {2013},
month = mar,
doi = {10.4204/EPTCS.112.16},
}
[Bry86]
Randal E.Bryant.
Graph-Based Algorithms for Boolean Function
Manipulation.
IEEE Transactions on Computers 35(8):677-691. IEEE Comp. Soc. Press, August 1986.
@article{tc35(8)-Bry,
author = {Bryant, Randal E.},
title = {Graph-Based Algorithms for Boolean Function
Manipulation},
publisher = {IEEE Comp. Soc. Press},
journal = {IEEE Transactions on Computers},
volume = {35},
number = {8},
pages = {677-691},
year = {1986},
month = aug,
}
[BS91]
Janusz A.Brzozowski and
Carl-Johan H.Seger.
Advances in Asynchronous Circuit Theory Part II:
Bounded Inertial Delay Models, MOS Circuits,
Design Techniques.
EATCS Bulletin 43:199-263. EATCS, February 1991.
@article{eatcs-bull43()-BS,
author = {Brzozowski, Janusz A. and Seger, Carl-Johan H.},
title = {Advances in Asynchronous Circuit Theory Part~{II}:
Bounded Inertial Delay Models, {MOS} Circuits,
Design Techniques},
publisher = {EATCS},
journal = {EATCS Bulletin},
volume = {43},
pages = {199-263},
year = {1991},
month = feb,
}
[BS95]
PatrickBlackburn and
JerrySeligman.
Hybrid Languages.
Journal of Logic, Language and Information 4(3):251-272. Kluwer Academic, 1995.
@article{jolli4(3)-BS,
author = {Blackburn, Patrick and Seligman, Jerry},
title = {Hybrid Languages},
publisher = {Kluwer Academic},
journal = {Journal of Logic, Language and Information},
volume = {4},
number = {3},
pages = {251-272},
year = {1995},
}
[BS98]
PatrickBlackburn and
JerrySeligman.
What are Hybrid Languages?.
In AIML'96,
pages 41-62.
CSLI Publications, 1998.
@inproceedings{aiml1996-BS,
author = {Blackburn, Patrick and Seligman, Jerry},
title = {What are Hybrid Languages?},
editor = {Kracht, Marcus and de Rijke, Marteen and Wansing,
Heinrich and Zakharyaschev, Michael},
booktitle = {{P}roceedings of the 1st {W}orkshop on {A}dvances in
{M}odal {L}ogic ({AIML}'96)},
acronym = {{AIML}'96},
publisher = {CSLI Publications},
pages = {41-62},
year = {1998},
confyear = {1996},
confmonth = {10},
}
[BS01]
Julian C.Bradfield and
ColinStirling.
Modal Logics and Mu-Calculi: An Introduction.
In Jan A.Bergstra,
AlbanPonse, and
Scott A.Smolka (eds.),
Handbook of Process Algebra.
Elsevier, 2001.
@incollection{HPA-BS,
author = {Bradfield, Julian C. and Stirling, Colin},
title = {Modal Logics and Mu-Calculi: An Introduction},
editor = {Bergstra, Jan A. and Ponse, Alban and Smolka, Scott
A.},
booktitle = {Handbook of Process Algebra},
publisher = {Elsevier},
chapter = {1.4},
year = {2001},
}
[BS12]
NathalieBertrand and
SvenSchewe.
Playing Optimally on Timed Automata with Random
Delays.
In FORMATS'12,
Lecture Notes in Computer Science 7595, pages 43-58. Springer-Verlag, September 2012.
@inproceedings{formats2012-BS,
author = {Bertrand, Nathalie and Schewe, Sven},
title = {Playing Optimally on Timed Automata with Random
Delays},
editor = {Jurdzi{\'n}ski, Marcin and Nickovic, Dejan},
booktitle = {{P}roceedings of the 10th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'12)},
acronym = {{FORMATS}'12},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {7595},
pages = {43-58},
year = {2012},
month = sep,
doi = {10.1007/978-3-642-33365-1_5},
}
[BSJ+15]
NathalieBertrand,
AmélieStainer,
ThierryJéron, and
MoezKrichen.
A game approach to determinize timed automata.
Formal Methods in System Design 46(1):42-80. Springer-Verlag, February 2015.
@article{fmsd46(1)-BSJK,
author = {Bertrand, Nathalie and Stainer, Am{\'e}lie and
J{\'e}ron, Thierry and Krichen, Moez},
title = {A~game approach to determinize timed automata},
publisher = {Springer-Verlag},
journal = {Formal Methods in System Design},
volume = {46},
number = {1},
pages = {42-80},
year = {2015},
month = feb,
doi = {10.1007/s10703-014-0220-1},
}
[BST98]
SébastienBornot,
JosephSifakis, and
StavrosTripakis.
Modeling Urgency in Timed Systems.
In COMPOS'97,
Lecture Notes in Computer Science 1536, pages 103-129. Springer-Verlag, 1998.
@inproceedings{compos1997-BST,
author = {Bornot, S{\'e}bastien and Sifakis, Joseph and
Tripakis, Stavros},
title = {Modeling Urgency in Timed Systems},
editor = {de Roever, Willem-Paul and Langmaack, Hans and
Pnueli, Amir},
booktitle = {{R}evised {L}ectures of the 1st {I}nternational
{S}ymposium on {C}ompositionality: {T}he
{S}ignificant {D}ifference ({COMPOS}'97)},
acronym = {{COMPOS}'97},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {1536},
pages = {103-129},
year = {1998},
confyear = {1997},
confmonth = {9},
}
[BST98]
PaulBeame,
MichaelSaks, and
Jayram S.Thathachar.
Time-Space Tradeoffs for Branching Programs.
Research Report 98-053, Electronic Colloquium on Computational Complexity,
September 1998.
@techreport{eccc1998-BST,
author = {Beame, Paul and Saks, Michael and Thathachar, Jayram
S.},
title = {Time-Space Tradeoffs for Branching Programs},
number = {98-053},
year = {1998},
month = sep,
institution = {Electronic Colloquium on Computational Complexity},
type = {Research Report},
}
[BSV04]
HenrikBjörklund,
SvenSandberg, and
SergeiVorobyov.
Memoryless Determinacy of Parity and Mean Payoff
Games: A Simple Proof.
Theoretical Computer Science 310(1-3):365-378. Elsevier, January 2004.
@article{tcs310(1-3)-BSV,
author = {Bj{\"o}rklund, Henrik and Sandberg, Sven and
Vorobyov, Sergei},
title = {Memoryless Determinacy of Parity and Mean Payoff
Games: A~Simple Proof},
publisher = {Elsevier},
journal = {Theoretical Computer Science},
volume = {310},
number = {1-3},
pages = {365-378},
year = {2004},
month = jan,
doi = {10.1016/S0304-3975(03)00427-4},
}
[BT96]
Dimitri P.Bertsekas and
John N.Tsitsiklis.
Neuro-Dynamic Programming.
Anthropological Field Studies 3.
Athena Scientific, 1996.
@book{NDP-BT,
author = {Bertsekas, Dimitri P. and Tsitsiklis, John N.},
title = {Neuro-Dynamic Programming},
publisher = {Athena Scientific},
series = {Anthropological Field Studies},
volume = {3},
year = {1996},
}
[BT99]
PatrickBlackburn and
MiroslavaTzakova.
Hybrid Languages and Temporal Logic.
Logic Journal of the IGPL 7(1):27-54. Oxford University Press, January 1999.
@article{jigpl7(1)-BT,
author = {Blackburn, Patrick and Tzakova, Miroslava},
title = {Hybrid Languages and Temporal Logic},
publisher = {Oxford University Press},
journal = {Logic Journal of the IGPL},
volume = {7},
number = {1},
pages = {27-54},
year = {1999},
month = jan,
}
[BT05]
HarryBuhrman and
LeenTorenvliet.
A Post's Program for Complexity Theory.
EATCS Bulletin 85:41-51. EATCS, February 2005.
@article{eatcs-bull85()-BT,
author = {Buhrman, Harry and Torenvliet, Leen},
title = {A {P}ost's Program for Complexity Theory},
publisher = {EATCS},
journal = {EATCS Bulletin},
volume = {85},
pages = {41-51},
year = {2005},
month = feb,
}
[BTK+02]
CécileBui Thanh,
HannaKlaudel, and
FranckPommereau.
Petri Nets with Causal Time for System
Verification.
In MTCS'02,
Electronic Notes in Theoretical Computer Science 68(5).
Elsevier, August 2002.
@inproceedings{mtcs2003-BKP,
author = {Bui Thanh, C{\'e}cile and Klaudel, Hanna and
Pommereau, Franck},
title = {{P}etri Nets with Causal Time for System
Verification},
editor = {Vogler, Walter and Larsen, Kim Guldstrand},
booktitle = {{P}roceedings of the 3rd {I}nternational {W}orkshop
on {M}odels for {T}ime-Critical {S}ystems
({MTCS}'02)},
acronym = {{MTCS}'02},
publisher = {Elsevier},
series = {Electronic Notes in Theoretical Computer Science},
volume = {68},
number = {5},
year = {2002},
month = aug,
}
[BTY97]
AhmedBouajjani,
StavrosTripakis, and
SergioYovine.
On-the-Fly Symbolic Model Checking for Real-Time
Systems.
In RTSS'97,
pages 25-35.
IEEE Comp. Soc. Press, December 1997.
@inproceedings{rts1997-BTY,
author = {Bouajjani, Ahmed and Tripakis, Stavros and Yovine,
Sergio},
title = {On-the-Fly Symbolic Model Checking for Real-Time
Systems},
booktitle = {{P}roceedings of the 18th {S}ymposium on {R}eal-Time
{S}ystems ({RTSS}'97)},
acronym = {{RTSS}'97},
publisher = {IEEE Comp. Soc. Press},
pages = {25-35},
year = {1997},
month = dec,
}
[Buc62]
Julius R.Büchi.
On a Decision Method in Restricted Second Order
Arithmetic.
In LMPS'60,
pages 1-11.
Stanford University Press, June 1962.
@inproceedings{lmps60-Buc,
author = {B{\"u}chi, Julius R.},
title = {On a Decision Method in Restricted Second Order
Arithmetic},
editor = {Nagel, Ernest and Suppes, Patrick and Tarski,
Alfred},
booktitle = {{P}roceedings of the 1960 {I}nternational {C}ongress
on {L}ogic, {M}ethodology and {P}hilosophy of
{S}cience ({LMPS}'60)},
acronym = {{LMPS}'60},
publisher = {Stanford University Press},
pages = {1-11},
year = {1962},
month = jun,
confyear = {1960},
}
[Bur79]
John P.Burgess.
Logic and Time.
Journal of Symbolic Logic 44(4):566-582. Association for Symbolic Logic, December 1979.
@article{jsl44(4)-Bur,
author = {Burgess,John P.},
title = {Logic and Time},
publisher = {Association for Symbolic Logic},
journal = {Journal of Symbolic Logic},
volume = {44},
number = {4},
pages = {566-582},
year = {1979},
month = dec,
}
[Bur80]
John P.Burgess.
Decidability for Branching Time.
Studia Logica 39(2-3):203-218. Kluwer Academic, 1980.
@article{studlog39(2-3)-Bur,
author = {Burgess,John P.},
title = {Decidability for Branching Time},
publisher = {Kluwer Academic},
journal = {Studia Logica},
volume = {39},
number = {2-3},
pages = {203-218},
year = {1980},
}
[Bus87]
Samuel R.Buss.
The Boolean Formula Value Problem is in ALOGTIME.
In STOC'87,
pages 123-131.
ACM Press, May 1987.
@inproceedings{stoc1987-Bus,
author = {Buss, Samuel R.},
title = {The Boolean Formula Value Problem is in {ALOGTIME}},
booktitle = {{P}roceedings of the 19th {A}nnual {ACM} {S}ymposium
on the {T}heory of {C}omputing ({STOC}'87)},
acronym = {{STOC}'87},
publisher = {ACM Press},
pages = {123-131},
year = {1987},
month = may,
}
[Bus93]
Samuel R.Buss.
Algorithms for Boolean Formula Evaluation and for
Tree Contraction.
In PeterClote and
JanKrajíček (eds.),
Proof Theory, Complexity, and Arithmetic.
Oxford University Press, 1993.
@incollection{PTCA-Bus,
author = {Buss, Samuel R.},
title = {Algorithms for Boolean Formula Evaluation and for
Tree Contraction},
editor = {Clote, Peter and Kraj{\'\i}{ c}ek, Jan},
booktitle = {Proof Theory, Complexity, and Arithmetic},
publisher = {Oxford University Press},
pages = {96-115},
year = {1993},
}
[Bus97]
Samuel R.Buss.
ALOGTIME Algorithm for Tree Isomorphism,
Comparison, and Canonization.
In KGC'97,
Lecture Notes in Computer Science 1289, pages 18-33. Springer-Verlag, August 1997.
@inproceedings{kgc1997-Bus,
author = {Buss, Samuel R.},
title = {{ALOGTIME} Algorithm for Tree Isomorphism,
Comparison, and Canonization},
editor = {Gottlob, Georg and Leitsch, Alexander and Mundici,
Daniele},
booktitle = {{P}roceedings of the 5th {K}urt {G}{\"o}del
{C}olloquium ({KGC}'97)},
acronym = {{KGC}'97},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {1289},
pages = {18-33},
year = {1997},
month = aug,
}
[BV07]
HenrikBjörklund and
SergeiVorobyov.
A combinatorial strongly subexponential strategy
improvement algorithm for mean payoff games.
Discrete Applied Mathematics 155(2):210-229. Elsevier, January 2007.
@article{dam155(2)-BV,
author = {Bj{\"o}rklund, Henrik and Vorobyov, Sergei},
title = {A combinatorial strongly subexponential strategy
improvement algorithm for mean payoff games},
publisher = {Elsevier},
journal = {Discrete Applied Mathematics},
volume = {155},
number = {2},
pages = {210-229},
year = {2007},
month = jan,
doi = {10.1016/j.dam.2006.04.029},
}
[BVW94]
OrnaBernholtz,
Moshe Y.Vardi, and
PierreWolper.
An Automata-Theoretic Approach to Branching-Time
Model Checking (Extended Abstract).
In CAV'94,
Lecture Notes in Computer Science 818, pages 142-155. Springer-Verlag, June 1994.
@inproceedings{cav1994-BVW,
author = {Bernholtz, Orna and Vardi, Moshe Y. and Wolper,
Pierre},
title = {An Automata-Theoretic Approach to Branching-Time
Model Checking (Extended Abstract)},
editor = {Dill, David L.},
booktitle = {{P}roceedings of the 6th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'94)},
acronym = {{CAV}'94},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {818},
pages = {142-155},
year = {1994},
month = jun,
}
[BW94]
Bertil A.Brandin and
W. MurrayWonham.
Supervisory Control of Timed Discrete-Event Systems.
IEEE Transactions on Automatic Control 39(2):329-342. IEEE Comp. Soc. Press, February 1994.
@article{tac39(2)-BW,
author = {Brandin, Bertil A. and Wonham, W. Murray},
title = {Supervisory Control of Timed Discrete-Event Systems},
publisher = {IEEE Comp. Soc. Press},
journal = {IEEE Transactions on Automatic Control},
volume = {39},
number = {2},
pages = {329-342},
year = {1994},
month = feb,
}
[BW17]
Julian C.Bradfield and
IgorWalukiewicz.
The mu-calculus and model-checking.
In Edmund M.Clarke,
Thomas A.Henzinger, and
HelmutVeith (eds.),
Handbook of Model Checking.
Springer-Verlag, 2017. To appear.
@incollection{HMC-BW,
author = {Bradfield, Julian C. and Walukiewicz, Igor},
title = {The mu-calculus and model-checking},
editor = {Clarke, Edmund M. and Henzinger, Thomas A. and
Veith, Helmut},
booktitle = {Handbook of Model Checking},
publisher = {Springer-Verlag},
year = {2017},
note = {To~appear},
}
[BY03]
JohanBengtsson and
WangYi.
On Clock Difference Constraints and Termination in
Reachability Analysis of Timed Automata.
In ICFEM'03.
Springer-Verlag, November 2003.
@incollection{icfem2003-BY,
author = {Bengtsson, Johan and Yi, Wang},
title = {On Clock Difference Constraints and Termination in
Reachability Analysis of Timed Automata},
booktitle = {{P}roceedings of the 5th {I}nternational
{C}onference on {F}ormal {E}ngineering {M}ethods
({ICFEM}'03)},
acronym = {{ICFEM}'03},
publisher = {Springer-Verlag},
pages = {491-503},
year = {2003},
month = nov,
}
[BY04]
JohanBengtsson and
WangYi.
Timed Automata: Semantics, Algorithms and Tools.
In JörgDesel,
WolfgangReisig, and
GrzegorzRozenberg (eds.),
Lectures on Concurrency and Petri Nets,
Lecture Notes in Computer Science 2098, pages 87-124. Springer-Verlag, 2004.
@incollection{lncs3098-BY,
author = {Bengtsson, Johan and Yi, Wang},
title = {Timed Automata: Semantics, Algorithms and Tools},
editor = {Desel, J{\"o}rg and Reisig, Wolfgang and Rozenberg,
Grzegorz},
booktitle = {Lectures on Concurrency and {P}etri Nets},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {2098},
pages = {87-124},
year = {2004},
doi = {10.1007/b98282},
}