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{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},
}
[BBC92]
DanièleBeauquier,
JeanBerstel, and
PhilippeChrétienne.
Éléments d'algorithmique.
Masson, 1992.
@book{BBC92,
author = {Beauquier, Dani{\`e}le and Berstel, Jean and
Chr{\'e}tienne, {\relax Ph}ilippe},
title = {{\'E}l{\'e}ments d'algorithmique},
publisher = {Masson},
year = {1992},
}
@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}{\v s} and V{\'a}clav
Bro{\v{z}}ek and Forejt, Vojt{\v{e}}ch and Ku{\v
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 = {Havelund, Klaus and Peleska, Jan and Roscoe, Bill W.
and de Vink, Erik},
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},
volume = {10951},
pages = {203-221},
year = {2018},
month = jul,
doi = {10.1007/978-3-319-95582-7_12},
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.},
}
In this paper, we propose a novel framework for the
synthesis of robust and optimal energy-aware
controllers. The framework is based on energy timed
automata, allowing for easy expression of
timing-constraints and variable energy-rates.
We prove decidability of the energy-constrained
infinite-run problem in settings with both certainty
and uncertainty of the energy-rates. We also
consider the optimization problem of identifying the
minimal upper bound that will permit existence of
energy-constrained infinite runs. Our algorithms are
based on quantifier elimination for linear real
arithmetic. Using Mathematica and Mjollnir,
we illustrate our framework through a real
industrial example of a hydraulic oil pump. Compared
with previous approaches our method is completely
automated and provides improved results.
@article{fac2020-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},
publisher = {Springer-Verlag},
journal = {Formal Aspects of Computing},
volume = {33},
number = {1},
pages = {3-25},
year = {2021},
month = jan,
doi = {10.1007/s00165-020-00521-4},
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}{\v s} and Gr{\"o}{\ss}er, Marcus and Ku{\v
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,
}
[BBG+12]
ChristelBaier,
TomášBrázdil,
MarcusGrößer, and
AntonínKučera.
Stochastic Game Logic.
Acta Informatica 49(4):203-224. Springer-Verlag, June 2012.
@article{acta49(4)-BBGK,
author = {Baier, {\relax Ch}ristel and Br{\'a}zdil,
Tom{\'a}{\v s} and Gr{\"o}{\ss}er, Marcus and Ku{\v
c}era, Anton{\'\i}n},
title = {Stochastic Game Logic},
publisher = {Springer-Verlag},
journal = {Acta Informatica},
volume = {49},
number = {4},
pages = {203-224},
year = {2012},
month = jun,
doi = {10.1007/s00236-012-0156-0},
}
[BBG+19]
ThomasBrihaye,
VéroniqueBruyère,
AlineGoeminne,
Jean-FrançoisRaskin, and
MarieVan den Bogaard.
The Complexity of Subgame Perfect Equilibria in
Quantitative Reachability Games.
In CONCUR'19,
Leibniz International Proceedings in Informatics 140, pages 13:1-13:16. Leibniz-Zentrum für Informatik, August 2019.
@inproceedings{concur2019-BBGRB,
author = {Brihaye, {\relax Th}omas and Bruy{\`e}re,
V{\'e}ronique and Goeminne, Aline and Raskin,
Jean-Fran{\c c}ois and Van{~}den{ }Bogaard, Marie},
title = {The~Complexity of Subgame Perfect Equilibria in
Quantitative Reachability Games},
editor = {Fokkink, Wan J. and van Glabbeek, Rob},
booktitle = {{P}roceedings of the 30th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'19)},
acronym = {{CONCUR}'19},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {140},
pages = {13:1-13:16},
year = {2019},
month = aug,
doi = {10.4230/LIPIcs.CONCUR.2019.13},
}
@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},
}
@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,
}
@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{\v 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},
}
@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 {M}arkovian 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},
}
@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{\v{s}}, Nikola and Bezdek, Petr and Larsen, Kim
Guldstrand and Srba, Ji{\v 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,
}
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.},
}
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.},
}
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.},
}
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+15]
ThomasBrihaye,
VéroniqueBruyère,
NoëmieMeunier, and
Jean-FrançoisRaskin.
Weak Subgame Perfect Equilibria and their
Application to Quantitative Reachability.
In CSL'15,
Leibniz International Proceedings in Informatics 41, pages 504-518. Leibniz-Zentrum für Informatik, September 2015.
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.},
}
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{\v r}{\'\i} and Brim, Lubo{\v s} and
St{\v 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{\v 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,
}
[BCD05]
PatriciaBouyer,
FabriceChevalier, and
DeepakD'Souza.
Fault Diagnosis Using Timed Automata.
In FoSSaCS'05,
Lecture Notes in Computer Science 3441, pages 219-233. Springer-Verlag, April 2005.
@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{\v 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},
}
@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,
}
@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{\v s} and {\v{C}}erna, Ivana and
Kr{\v{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,
}
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.},
}
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.},
}
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,
}
@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},
}
[BDG+17]
NathalieBertrand,
MiheerDewaskar,
BlaiseGenest, and
HugoGimbert.
Controlling a population.
In CONCUR'17,
Leibniz International Proceedings in Informatics 85, pages 12:1-12:16. Leibniz-Zentrum für Informatik, September 2017.
@inproceedings{concur2017-BDGG,
author = {Bertrand, Nathalie and Dewaskar, Miheer and Genest,
Blaise and Gimbert, Hugo},
title = {Controlling a population},
editor = {Meyer, Roland and Nestmann, Uwe},
booktitle = {{P}roceedings of the 28th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'17)},
acronym = {{CONCUR}'17},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {85},
pages = {12:1-12:16},
year = {2017},
month = sep,
doi = {10.4230/LIPIcs.CONCUR.2017.12},
}
@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{\v
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,
}
@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{\v 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},
}
[BDL04]
GerdBehrmann,
AlexandreDavid, and
Kim GuldstrandLarsen.
A Tutorial on Uppaal.
In SFM-RT'04,
Lecture Notes in Computer Science 3185, pages 200-236. Springer-Verlag, September 2004.
@inproceedings{sfm2004-BDL,
author = {Behrmann, Gerd and David, Alexandre and Larsen, Kim
Guldstrand},
title = {A~Tutorial on {U}ppaal},
editor = {Bernardo, Marco and Corradini, Flavio},
booktitle = {{F}ormal {M}ethods for the {D}esign of {R}eal-{T}ime
{S}ystems~--- {R}evised {L}ectures of the
{I}nternational {S}chool on {F}ormal {M}ethods for
the {D}esign of {C}omputer, {C}ommunication and
{S}oftware {S}ystems ({SFM-RT}'04)},
acronym = {{SFM-RT}'04},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {3185},
pages = {200-236},
year = {2004},
month = sep,
doi = {10.1007/978-3-540-30080-9_7},
}
[BDL12]
BenediktBollig,
NormannDecker, and
MartinLeucker.
Frequency Linear-time Temporal Logic.
In TASE'12,
pages 85-92.
IEEE Comp. Soc. Press, July 2012.
@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},
}
@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{\v{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,
}
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,
}
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,
}
@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,
}
@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},
}
[BEK18]
MichaelBlondin,
JavierEsparza, and
AntonínKučera.
Automatic Analysis of Expected Termination Time for
Population Protocols.
In CONCUR'18,
Leibniz International Proceedings in Informatics 118, pages 33:1-33:16. Leibniz-Zentrum für Informatik, September 2018.
@inproceedings{concur2018-BEK,
author = {Blondin, Michael and Esparza, Javier and Ku{\v
c}era, Anton{\'\i}n},
title = {Automatic Analysis of Expected Termination Time for
Population Protocols},
editor = {Schewe, Sven and Zhang, Lijun},
booktitle = {{P}roceedings of the 29th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'18)},
acronym = {{CONCUR}'18},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {118},
pages = {33:1-33:16},
year = {2018},
month = sep,
doi = {10.4230/LIPIcs.CONCUR.2018.33},
}
[Bel57]
RichardBellman.
Dynamic Programming.
Princeton University Press, 1957.
@book{DP-Bel,
author = {Bellman, Richard},
title = {Dynamic Programming},
publisher = {Princeton University Press},
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},
}
@phdthesis{phd-belmokadem,
author = {Bel{~}Mokadem, Houda},
title = {V{\'e}rification des propri{\'e}t{\'e}s
temporis{\'e}es des automates programmables
industriels},
year = {2006},
month = sep,
school = {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
France},
type = {Th\`ese de doctorat},
}
[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{\v{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,
}
[BF18]
EzioBartocci and
YlièsFalcone.
Lectures on Runtime Verification.
Lecture Notes in Computer Science 10457.
Springer-Verlag, 2018.
@book{lectRV-BF18,
title = {Lectures on Runtime Verification},
editor = {Bartocci, Ezio and Falcone, Yli{\`e}s},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {10457},
year = {2018},
doi = {10.1007/978-3-319-75632-5},
}
[BFA15]
UmangBhaskar,
LisaFleischer, and
ElliotAnshelevich.
A Stackelberg strategy for routing flow over time.
Games and Economic Behavior 92:232-247. July 2015.
@article{geb92()-BFA,
author = {Bhaskar, Umang and Fleischer, Lisa and Anshelevich,
Elliot},
title = {A~{S}tackelberg strategy for routing flow over time},
journal = {Games and Economic Behavior},
volume = {92},
pages = {232-247},
year = {2015},
month = jul,
doi = {10.1016/j.geb.2013.09.004},
}
[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,
}
[BFF+20]
RaphaëlBerthon,
NathanaëlFijalkow,
EmmanuelFiliot,
ShibashisGuha,
BastienMaubert,
AnielloMurano,
LaurelinePinault,
SophiePinchinat,
SashaRubin, and
OlivierSerre.
Alternating Tree Automata with Qualitative
Semantics.
Technical Report 2002-03664, arXiv,
February 2020.
@techreport{arxiv2002.03664-BFFGMMPPRS,
author = {Berthon, Rapha{\"e}l and Fijalkow, Nathana{\"e}l and
Filiot, Emmanuel and Guha, Shibashis and Maubert,
Bastien and Murano, Aniello and Pinault, Laureline
and Pinchinat, Sophie and Rubin, Sasha and Serre,
Olivier},
title = {Alternating Tree Automata with Qualitative
Semantics},
number = {2002-03664},
year = {2020},
month = feb,
institution = {arXiv},
}
[BFF+21]
RaphaëlBerthon,
NathanaëlFijalkow,
EmmanuelFiliot,
ShibashisGuha,
BastienMaubert,
AnielloMurano,
LaurelinePinault,
SophiePinchinat,
SashaRubin, and
OlivierSerre.
Alternating Tree Automata with Qualitative
Semantics.
ACM Transactions on Computational Logic 22(1):7:1-7:24. ACM Press, January 2021.
@article{tocl22(1)-BFFGMMPPRS,
author = {Berthon, Rapha{\"e}l and Fijalkow, Nathana{\"e}l and
Filiot, Emmanuel and Guha, Shibashis and Maubert,
Bastien and Murano, Aniello and Pinault, Laureline
and Pinchinat, Sophie and Rubin, Sasha and Serre,
Olivier},
title = {Alternating Tree Automata with Qualitative
Semantics},
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
volume = {22},
number = {1},
pages = {7:1-7:24},
year = {2021},
month = jan,
doi = {10.1145/3431860},
}
[BFF+11]
VittorioBilò,
AngeloFanelli,
MicheleFlammini, and
LucaMoscardelli.
Graphical congestion games.
Algorithmica 61(2):274-297. Springer-Verlag, October 2011.
@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+03]
AlbertBenveniste,
ÉricFabre,
StefanHaar, and
ClaudeJard.
Diagnosis of asynchronous discrete event systems:
A net-unfolding approach.
IEEE Transactions on Automatic Control 48(5):714-727. IEEE Comp. Soc. Press, 2003.
@article{tac48(5)-BFHJ,
author = {Benveniste, Albert and Fabre, {\'E}ric and Haar,
Stefan and Jard, Claude},
title = {Diagnosis of asynchronous discrete event systems:
A~net-unfolding approach},
publisher = {IEEE Comp. Soc. Press},
journal = {IEEE Transactions on Automatic Control},
volume = {48},
number = {5},
pages = {714-727},
year = {2003},
doi = {10.1109/TAC.2003.811249},
}
[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,
}
@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{hmc2018-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{\v
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.},
}
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.},
}
Synchronizing a (deterministic, finite-state)
automaton is the problem of finding a sequence of
actions to be played in the automaton in order to
end up in the same state independently of the
starting state. We consider synchronization
with LTL constraints on the executions
leading to synchronization, extending the results
of [Petra Wolf. Synchronization under dynamic
constraints. FSTTCS'20] by showing that the problem
is PSPACE-complete for LTL as well
as for restricted fragments (involving only
modality F or G), while it is
NP-complete for constraints expressed using
only modality X.
@article{ipl182()-BFM,
author = {Bertrand, Nathalie and Francon, Hugo and Markey,
Nicolas},
title = {Synchronizing words under {LTL} constraints},
publisher = {Elsevier},
journal = {Information Processing Letters},
volume = {182},
year = {2023},
month = aug,
doi = {10.1016/j.ipl.2023.106392},
abstract = {Synchronizing a (deterministic, finite-state)
automaton is the problem of finding a sequence of
actions to be played in the automaton in order to
end up in the same state independently of the
starting state. We~consider synchronization
with~\textsf{LTL} constraints on the executions
leading to synchronization, extending the results
of~[Petra~Wolf. Synchronization under dynamic
constraints. FSTTCS'20] by~showing that the problem
is \textsf{PSPACE}-complete for~\textsf{LTL} as well
as for restricted fragments (involving only
modality~\textsf{F} or~\textsf{G}), while it is
\textsf{NP}-complete for constraints expressed using
only modality~\textsf{X}.},
}
[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,
}
@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,
}
@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 – 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,
}
[BG11]
NathalieBertrand and
BlaiseGenest.
Minimal Disclosure in Partially Observable
Markov Decision Processes.
In FSTTCS'11,
Leibniz International Proceedings in Informatics 13, pages 411-422. Leibniz-Zentrum für Informatik, December 2011.
@inproceedings{fsttcs2011-BG,
author = {Bertrand, Nathalie and Genest, Blaise},
title = {Minimal Disclosure in {P}artially {O}bservable
{M}arkov {D}ecision {P}rocesses},
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 = {411-422},
year = {2011},
month = dec,
doi = {10.4230/LIPIcs.FSTTCS.2011.411},
}
[BG13]
NilsBulling and
ValentinGoranko.
How to Be Both Rich and Happy: Combining
Quantitative and Qualitative Strategic Reasoning
about Multi-Player Games (Extended Abstract).
In SR'13,
Electronic Proceedings in Theoretical Computer
Science 112, pages 33-41. March 2013.
@inproceedings{sr2013-BG,
author = {Bulling, Nils and Goranko, Valentin},
title = {How to Be Both Rich and Happy: Combining
Quantitative and Qualitative Strategic Reasoning
about Multi-Player Games (Extended Abstract)},
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 = {33-41},
year = {2013},
month = mar,
doi = {10.4204/EPTCS.112.8},
}
[BGG17]
NathalieBertrand,
BlaiseGenest, and
HugoGimbert.
Qualitative Determinacy and Decidability of
Stochastic Games with Signals.
Journal of the ACM 64(5):33:1-33:48. ACM Press, October 2017.
@article{jacm64(5)-BGG,
author = {Bertrand, Nathalie and Genest, Blaise and Gimbert,
Hugo},
title = {Qualitative Determinacy and Decidability of
Stochastic Games with Signals},
publisher = {ACM Press},
journal = {Journal of the~ACM},
volume = {64},
number = {5},
pages = {33:1-33:48},
year = {2017},
month = oct,
doi = {10.1145/3107926},
}
@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,
}
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.},
}
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.},
}
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.},
}
@inproceedings{fsttcs2018-BMR,
author = {Busatto-Gaston, Damien and Monmege, Benjamin and
Reynier, Pierre-Alain},
title = {Symbolic Approximation of Weighted Timed Games},
editor = {Ganguli, Sumit and Pandya, Paritosh K.},
booktitle = {{P}roceedings of the 38th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience ({FSTTCS}'18)},
acronym = {{FSTTCS}'18},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {122},
pages = {28:1-28:16},
year = {2018},
month = dec,
doi = {10.4230/LIPIcs.FSTTCS.2018.28},
}
In this paper, we are interested in the synthesis of
schedulers in double-weighted Markov decision
processes, which satisfy both a percentile
constraint over a weighted reachability condition,
and a quantitative constraint on the expected value
of a random variable defined using a weighted
reachability condition. This problem is inspired by
the modelization of an electric-vehicle charging
problem. We study the cartography of the problem,
when one parameter varies, and show how a partial
cartography can be obtained via two sequences of
opimization problems. We discuss completeness and
feasability of the method.
@inproceedings{gandalf2018-BGMR,
author = {Bouyer, Patricia and Gonz{\'a}lez, Mauricio and
Markey, Nicolas and Randour, Mickael},
title = {Multi-weighted Markov Decision Processes with
Reachability Objectives},
editor = {Orlandini, Andrea and Zimmermann, Martin},
booktitle = {{P}roceedings of the 9th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics and {F}ormal
{V}erification ({GandALF}'18)},
acronym = {{GandALF}'18},
series = {Electronic Proceedings in Theoretical Computer
Science},
volume = {277},
pages = {250-264},
year = {2018},
month = sep,
doi = {10.4204/EPTCS.277.18},
abstract = {In~this paper, we~are interested in the synthesis of
schedulers in double-weighted Markov decision
processes, which satisfy both a percentile
constraint over a weighted reachability condition,
and a quantitative constraint on the expected value
of a random variable defined using a weighted
reachability condition. This~problem is inspired by
the modelization of an electric-vehicle charging
problem. We study the cartography of the problem,
when one parameter varies, and show how a partial
cartography can be obtained via two sequences of
opimization problems. We~discuss completeness and
feasability of the method.},
}
[BGM+19]
DamienBusatto-Gaston,
BenjaminMonmege,
Pierre-AlainReynier, and
OcanSankur.
Robust Controller Synthesis in Timed Büchi
Automata: A Symbolic Approach.
In CAV'19,
Lecture Notes in Computer Science 11561, pages 572-590. Springer-Verlag, July 2019.
@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},
}
@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)-BGS,
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
Algorithms.
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
Algorithms},
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},
}
We consider the problems of efficiently diagnosing
(and predicting) what did (and will) happen after a
given sequence of observations of the execution of a
partially-observable one-clock timed automaton. This
is made difficult by the facts that timed automata
are infinite-state systems, and that they can in
general not be determinized.
We introduce timed
markings as a formalism to keep track of the
evolution of the set of reachable configurations
over time. We show how timed markings can be used to
efficiently represent the closure under silent
transitions of such automata. We report on our
implementation of this approach compared to the
approach of [Tripakis, Fault diagnosis for timed
automata, 2002], and provide some insight to a
generalization of our approach to n-clock
timed automata.
@article{sttt23(2)-BHJJM,
author = {Bouyer, Patricia and Henry, L{\'e}o and Jaziri, Samy
and J{\'e}ron, Thierry and Markey, Nicolas},
title = {Diagnosing timed automata using timed markings},
publisher = {Springer-Verlag},
journal = {International Journal on Software Tools for
Technology Transfer},
volume = {23},
number = {2},
pages = {229-253},
year = {2021},
month = apr,
doi = {10.1007/s10009-021-00606-2},
abstract = {We~consider the problems of efficiently diagnosing
(and~predicting) what did (and~will) happen after a
given sequence of observations of the execution of a
partially-observable one-clock timed automaton. This
is made difficult by the facts that timed automata
are infinite-state systems, and that they can in
general not be determinized. \par We~introduce timed
markings as a formalism to keep track of the
evolution of the set of reachable configurations
over time. We show how timed markings can be used to
efficiently represent the closure under silent
transitions of such automata. We report on our
implementation of this approach compared to the
approach of [Tripakis, Fault diagnosis for timed
automata,~2002], and provide some insight to a
generalization of our approach to {{\(n\)}}-clock
timed automata.},
}
[BHK00]
StevenBradley,
WilliamHenderson, and
DavidKendall.
Using Timed Automata for Response Time Analysis and
Distributed 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
Distributed 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},
}
@inproceedings{fsttcs2014-BHL,
author = {Bertrand, Nathalie and Haddad, Serge and Lefaucheux,
Engel},
title = {Foundation of Diagnosis and Predictability in
Probabilistic Systems},
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 = {417-429},
year = {2014},
month = dec,
doi = {10.4230/LIPIcs.FSTTCS.2014.417},
}
[BHL+22]
SougataBose,
Thomas A.Henzinger,
KaroliinaLehtinen,
SvenSchewe, and
PatrickTotzke.
History-deterministic timed automata are not
determinizable.
In RP'22,
Lecture Notes in Computer Science 13608, pages 67-76. Springer-Verlag, October 2022.
@inproceedings{rp2022-BHLST,
author = {Bose, Sougata and Henzinger, Thomas A. and Lehtinen,
Karoliina and Schewe, Sven and Totzke, Patrick},
title = {History-deterministic timed automata are not
determinizable},
editor = {Lin, Anthony W. and Zetzsche, Georg and Potapov,
Igor},
booktitle = {{P}roceedings of the 16th {W}orkshop on
{R}eachability {P}roblems in {C}omputational
{M}odels ({RP}'22)},
acronym = {{RP}'22},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {13608},
pages = {67-76},
year = {2022},
month = oct,
doi = {10.1007/978-3-031-19135-0_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},
}
@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,
}
@inproceedings{icalp2010-BJK,
author = {Br{\'a}zdil, Tom{\'a}{\v s} and Jan{\v c}ar, Petr
and Ku{\v 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},
}
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},
}
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.},
}
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.},
}
We consider the problems of efficiently diagnosing
and predicting what did (or will) happen in a
partially-observable one-clock timed automaton.
We introduce timed sets as a formalism to keep track
of the evolution of the reachable configurations
over time, and use our previous work on automata
over timed domains to build a candidate diagnoser
for our timed automaton. We report on our
implementation of this approach compared to the
approach of [Tripakis, Fault diagnosis for timed
autmata, 2002].
@inproceedings{rv2018-BJM,
author = {Bouyer, Patricia and Jaziri, Samy and Markey,
Nicolas},
title = {Efficient timed diagnosis using automata with timed
domains},
editor = {Colombo, Christian and Leucker, Martin},
booktitle = {{P}roceedings of the 18th {I}nternational {W}orkshop
on {R}untime {V}erification ({RV}'18)},
acronym = {{RV}'18},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {11237},
pages = {205-221},
year = {2018},
month = nov,
doi = {10.1007/978-3-030-03769-7_12},
abstract = {We consider the problems of efficiently diagnosing
and predicting what did (or~will) happen in a
partially-observable one-clock timed automaton.
We~introduce timed sets as a formalism to keep track
of the evolution of the reachable configurations
over time, and use our previous work on automata
over timed domains to build a candidate diagnoser
for our timed automaton. We~report on our
implementation of this approach compared to the
approach of [Tripakis, Fault diagnosis for timed
autmata,~2002].},
}
[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{\v 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},
}
@book{PoMC2008-BK,
author = {Baier, {\relax Ch}ristel and Katoen, Joost-Pieter},
title = {Principles of Model-Checking},
publisher = {MIT Press},
year = {2008},
month = may,
}
@inproceedings{fsttcs2018-BK,
author = {Bagnol, Marc and Kuperberg, Denis},
title = {B{\"u}chi Good-for-game Automata are Efficiently
Recognizable},
editor = {Ganguli, Sumit and Pandya, Paritosh K.},
booktitle = {{P}roceedings of the 38th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience ({FSTTCS}'18)},
acronym = {{FSTTCS}'18},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {122},
pages = {16:1-16:14},
year = {2018},
month = dec,
doi = {10.4230/LIPIcs.FSTTCS.2018.16},
}
[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}{\v s} and Kla{\v{s}}ka, David
and Ku{\v 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,
}
[BKK+13]
UdiBoker,
DenisKuperberg,
OrnaKupferman, and
MichalSkrzypczak.
Nondeterminism in the Presence of a Diverse or
Unknown Future.
In ICALP'13,
Lecture Notes in Computer Science 7966, pages 89-100. Springer-Verlag, July 2013.
@inproceedings{icalp2013-BKKS,
author = {Boker, Udi and Kuperberg, Denis and Kupferman, Orna
and Skrzypczak, Michal},
title = {Nondeterminism in the Presence of a Diverse or
Unknown Future},
editor = {Fomin, Fedor V. and Freivalds, Rusins and
Kwiatkowska, Marta and Peleg, David},
booktitle = {{P}roceedings of the 40th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'13)~-- Part~{II}},
acronym = {{ICALP}'13},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {7966},
pages = {89-100},
year = {2013},
month = jul,
doi = {10.1007/978-3-642-39212-2_11},
}
@inproceedings{fsttcs2020-BKLS,
author = {Boker, Udi and Kuperberg, Denis and Lehtinen,
Karoliina and Skrzypczak, Michal},
title = {On succinctness and recognisability of alternating
good-for-games automata},
editor = {Saxena, Nitin and Simon, Sunil},
booktitle = {{P}roceedings of the 40th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience ({FSTTCS}'20)},
acronym = {{FSTTCS}'20},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {182},
pages = {41:1-41:13},
year = {2020},
month = dec,
doi = {10.4230/LIPIcs.FSTTCS.2020.41},
}
We introduce and study
SL[F]—a quantitative
extension of SL (Strategy Logic),
one of the most natural and expressive logics
describing strategic behaviours. The satisfaction
value of an SL[F] formula
is a real value in [0,1], reflecting "how
much" or "how well" the strategic on-going
objectives of the underlying agents are satisfied.
We demonstrate the applications of
SL[F] in quantitative
reasoning about multi-agent systems, by showing how
it can express concepts of stability in multi-agent
systems, and how it generalises some fuzzy temporal
logics. We also provide a model-checking algorithm
for our logic, based on a quantitative extension of
Quantified CTL.
@inproceedings{ijcai2019-BKMMMP,
author = {Bouyer, Patricia and Kupferman, Orna and Markey,
Nicolas and Maubert, Bastien and Murano, Aniello and
Perelli, Giuseppe},
title = {Reasoning about Quality and Fuzziness of Strategic
Behaviours},
editor = {Kraus, Sarit},
booktitle = {{P}roceedings of the 28th {I}nternational {J}oint
{C}onference on {A}rtificial {I}ntelligence
({IJCAI}'19)},
acronym = {{IJCAI}'19},
publisher = {IJCAI organization},
pages = {1588-1594},
year = {2019},
month = aug,
doi = {10.24963/ijcai.2019/220},
abstract = {We~introduce and study
{\(\textsf{SL}[\mathcal{F}]\)}---a~quantitative
extension of {\(\textsf{SL}\)} (Strategy Logic),
one~of the most natural and expressive logics
describing strategic behaviours. The satisfaction
value of an {\(\textsf{SL}[\mathcal{F}]\)} formula
is a real value in~{\([0,1]\)}, reflecting {"}how
much{"} or {"}how well{"} the strategic on-going
objectives of the underlying agents are satisfied.
We~demonstrate the applications of
{\(\textsf{SL}[\mathcal{F}]\)} in quantitative
reasoning about multi-agent systems, by showing how
it can express concepts of stability in multi-agent
systems, and how it generalises some fuzzy temporal
logics. We~also provide a model-checking algorithm
for our logic, based on a quantitative extension of
Quantified~\textsf{CTL}.},
}
Temporal logics are extensively used for the
specification of on-going behaviors of computer
systems. Two significant developments in this area
are the extension of traditional temporal logics
with modalities that enable the specification of
on-going strategic behaviors in multi-agent systems,
and the transition of temporal logics to a
quantitative setting, where different satisfaction
values enable the specifier to formalize concepts
such as certainty or quality. In the first class,
SL (Strategy Logic) is one of the most natural and
expressive logics describing strategic behaviors. In
the second class, a notable logic is
LTL[F], which extends
LTL with quality operators.
In this
work we introduce and study
SL[F], which enables the
specification of quantitative strategic behaviors.
The satisfaction value of an
SL[F] formula is a real value
in [0,1], reflecting "how much" or
"how well" the strategic on-going objectives of
the underlying agents are satisfied. We demonstrate
the applications of SL[F] in
quantitative reasoning about multi-agent systems,
showing how it can express and measure concepts like
stability in multi-agent systems, and how it
generalizes some fuzzy temporal logics. We also
provide a model-checking algorithm for
SL[F], based on a
quantitative extension of
Quantified CTL*. Our algorithm
provides the first decidability result for a
quantitative extension of Strategy Logic. In
addition, it can be used for synthesizing strategies
that maximize the quality of the systems' behavior
@article{tocl24(3)-BKMMMP,
author = {Bouyer, Patricia and Kupferman, Orna and Markey,
Nicolas and Maubert, Bastien and Murano, Aniello and
Perelli, Giuseppe},
title = {Reasoning about Quality and Fuzziness of Strategic
Behaviours},
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
volume = {24},
number = {3},
pages = {21:1-21:38},
year = {2023},
month = jul,
doi = {10.1145/3582498},
abstract = {Temporal logics are extensively used for the
specification of on-going behaviors of computer
systems. Two significant developments in this area
are the extension of traditional temporal logics
with modalities that enable the specification of
on-going strategic behaviors in multi-agent systems,
and the transition of temporal logics to a
quantitative setting, where different satisfaction
values enable the specifier to formalize concepts
such as certainty or quality. In~the first class,
SL~(Strategy~Logic)~is one of the most natural and
expressive logics describing strategic behaviors. In
the second class, a notable logic is
\(\textsf{LTL}[\mathcal{F}]\), which extends
\textsf{LTL} with quality operators. \par In~this
work we introduce and study
\(\textsf{SL}[\mathcal{F}]\), which enables the
specification of quantitative strategic behaviors.
The satisfaction value of an
\(\textsf{SL}[\mathcal{F}]\) formula is a real value
in \([0,1]\), reflecting {"}how~much{"} or
{"}how~well{"} the strategic on-going objectives of
the underlying agents are satisfied. We demonstrate
the applications of \(\textsf{SL}[\mathcal{F}]\) in
quantitative reasoning about multi-agent systems,
showing how it can express and measure concepts like
stability in multi-agent systems, and how it
generalizes some fuzzy temporal logics. We also
provide a model-checking algorithm for
\(\textsf{SL}[\mathcal{F}]\), based on a
quantitative extension of
Quantified~\(\textsf{CTL}^*\). Our~algorithm
provides the first decidability result for a
quantitative extension of Strategy Logic. In
addition, it can be used for synthesizing strategies
that maximize the quality of the systems' behavior},
}
[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,
}
@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},
}
@inproceedings{concur2019-BL,
author = {Boker, Udi and Lehtinen, Karoliina},
title = {Good-for-game Automata: from Non-determinism to
Alternation},
editor = {Fokkink, Wan J. and van Glabbeek, Rob},
booktitle = {{P}roceedings of the 30th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'19)},
acronym = {{CONCUR}'19},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {140},
pages = {19:1-19:16},
year = {2019},
month = aug,
doi = {10.4230/LIPIcs.CONCUR.2019.19},
}
@inproceedings{fsttcs2021-BK,
author = {Boker, Udi and Lehtinen, Karoliina},
title = {History Determinism vs.~Good for Gameness in
Quantitative Automata},
editor = {Boja{\'n}czyk, Miko{\l}aj and Chekuri, Chandra},
booktitle = {{P}roceedings of the 41st {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience ({FSTTCS}'21)},
acronym = {{FSTTCS}'21},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {213},
pages = {38:1-38:20},
year = {2021},
month = dec,
doi = {10.4230/LIPIcs.FSTTCS.2021.38},
}
@inproceedings{fossacs2022-BL,
author = {Boker, Udi and Lehtinen, Karoliina},
title = {Token Games and History-Deterministic Quantitative
Automata},
editor = {Bouyer, Patricia and Schr{\"o}der, Lutz},
booktitle = {{P}roceedings of the 25th {I}nternational
{C}onference on {F}oundations of {S}oftware
{S}cience and {C}omputation {S}tructure
({FoSSaCS}'22)},
acronym = {{FoSSaCS}'22},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {13242},
pages = {120-139},
year = {2022},
month = apr,
doi = {10.1007/978-3-030-99253-8_7},
}
@article{siglog-news35()-BL,
author = {Boker, Udi and Lehtinen, Karoliina},
title = {When a Little Nondeterminism Goes a Long Way: an
Introduction to History-Determinism},
publisher = {ACM Press},
journal = {SIGLOG News},
volume = {35},
pages = {24-51},
year = {2023},
month = jan,
}
[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,
}
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—for us somewhat
unexpectedly—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).},
}
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.}},
}
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-63121-9_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.},
}
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},
}
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},
}
@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,
}
@inproceedings{fossacs2022-BLS,
author = {Boker, Udi and Lehtinen, Karoliina and Sickert,
Salomon},
title = {On the Translation of Automata to Linear Temporal
Logic},
editor = {Bouyer, Patricia and Schr{\"o}der, Lutz},
booktitle = {{P}roceedings of the 25th {I}nternational
{C}onference on {F}oundations of {S}oftware
{S}cience and {C}omputation {S}tructure
({FoSSaCS}'22)},
acronym = {{FoSSaCS}'22},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {13242},
pages = {140-160},
year = {2022},
month = apr,
doi = {10.1007/978-3-030-99253-8_8},
}
[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,
}
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.},
}
@article{tcs410(36)-BMI,
author = {Busch, Costas and Magdon{-}Ismail, Malik},
title = {Atomic routing games on maximum congestion},
publisher = {Elsevier},
journal = {Theoretical Computer Science},
volume = {410},
number = {36},
pages = {3337-3347},
year = {2009},
month = aug,
doi = {10.1016/j.tcs.2009.04.015},
}
[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.
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!
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.},
}
[BMM17]
RaphaëlBerthon,
BastienMaubert, and
AnielloMurano.
Decidability Results for ATL*
with Imperfect Information and Perfect Recall.
In AAMAS'17,
pages 1250-1258.
International Foundation for Autonomous Agents and
Multiagent Systems, May 2017.
@inproceedings{aamas2017-BMM,
author = {Berthon, Rapha{\"e}l and Maubert, Bastien and
Murano, Aniello},
title = {Decidability Results for {ATL\textsuperscript{*}}
with Imperfect Information and Perfect Recall},
editor = {Das, Sanmay and Durfee, Ed and Larson, Kate and
Winikoff, Michael},
booktitle = {{P}roceedings of the 16th {I}nternational
{C}onference on {A}utonomous {A}gents and
{M}ultiagent {S}ystems ({AAMAS}'17)},
acronym = {{AAMAS}'17},
publisher = {International Foundation for Autonomous Agents and
Multiagent Systems},
pages = {1250-1258},
year = {2017},
month = may,
}
[BMM+17]
RaphaëlBerthon,
BastienMaubert,
AnielloMurano,
SashaRubin, and
Moshe Y.Vardi.
Strategy Logic with Imperfect Information.
In LICS'17,
pages 1-12.
IEEE Comp. Soc. Press, June 2017.
@inproceedings{lics2017-BMMRV,
author = {Berthon, Rapha{\"e}l and Maubert, Bastien and
Murano, Aniello and Rubin, Sasha and Vardi, Moshe
Y.},
title = {Strategy Logic with Imperfect Information},
booktitle = {{P}roceedings of the 32nd {A}nnual {S}ymposium on
{L}ogic in {C}omputer {S}cience ({LICS}'17)},
acronym = {{LICS}'17},
publisher = {IEEE Comp. Soc. Press},
pages = {1-12},
year = {2017},
month = jun,
doi = {10.1109/LICS.2017.8005136},
}
[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.},
}
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.},
}
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,
}
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.},
}
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,
}
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.},
}
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.
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},
pages = {91-127},
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.},
}
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.},
}
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.},
}
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.},
}
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.},
}
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.},
}
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.},
}
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.},
}
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.},
}
Congestion games are a classical type of games
studied in game theory, in which n players choose a
resource, and their individual cost increases with
the number of other players choosing the same
resource. In network congestion games (NCGs), the
resources correspond to simple paths in a graph,
e.g. representing routing options from a source to a
target. In this paper, we introduce a variant
of NCGs, referred to as dynamic NCGs: in this
setting, players take transitions synchronously,
they select their next transitions dynamically, and
they are charged a cost that depends on the number
of players simultaneously using the same transition.
We study, from a complexity perspective,
standard concepts of game theory in dynamic NCGs:
social optima, Nash equilibria, and subgame perfect
equilibria. Our contributions are the following: the
existence of a strategy profile with social cost
bounded by a constant is in PSPACE and NP-hard.
(Pure) Nash equilibria always exist in dynamic NCGs;
the existence of a Nash equilibrium with bounded
cost can be decided in EXPSPACE, and computing a
witnessing strategy profile can be done in
doubly-exponential time. The existence of a subgame
perfect equilibrium with bounded cost can be decided
in 2EXPSPACE, and a witnessing strategy profile can
be computed in triply-exponential time.
@inproceedings{fsttcs2020-BMSS,
author = {Bertrand, Nathalie and Markey, Nicolas and
Sadhukhan, Suman and Sankur, Ocan},
title = {Dynamic network congestion games},
editor = {Saxena, Nitin and Simon, Sunil},
booktitle = {{P}roceedings of the 40th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience ({FSTTCS}'20)},
acronym = {{FSTTCS}'20},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {182},
pages = {40:1-40:16},
year = {2020},
month = dec,
doi = {10.4230/LIPIcs.FSTTCS.2020.40},
abstract = {Congestion games are a classical type of games
studied in game theory, in which n players choose a
resource, and their individual cost increases with
the number of other players choosing the same
resource. In network congestion games~(NCGs), the
resources correspond to simple paths in a graph,
e.g.~representing routing options from a source to a
target. In this paper, we introduce a variant
of~NCGs, referred to as dynamic~NCGs: in~this
setting, players take transitions synchronously,
they select their next transitions dynamically, and
they are charged a cost that depends on the number
of players simultaneously using the same transition.
\par We~study, from a complexity perspective,
standard concepts of game theory in dynamic NCGs:
social optima, Nash equilibria, and subgame perfect
equilibria. Our contributions are the following: the
existence of a strategy profile with social cost
bounded by a constant is in PSPACE and NP-hard.
(Pure)~Nash equilibria always exist in dynamic~NCGs;
the existence of a Nash equilibrium with bounded
cost can be decided in EXPSPACE, and computing a
witnessing strategy profile can be done in
doubly-exponential time. The~existence of a subgame
perfect equilibrium with bounded cost can be decided
in 2EXPSPACE, and a witnessing strategy profile can
be computed in triply-exponential~time.},
}
We consider atomic congestion games on
series-parallel networks, and study the structure of
the sets of Nash equilibria and social local optima
on a given network when the number of players
varies. We establish that these sets are definable
in Presburger arithmetic and that they admit
semilinear representations whose all period vectors
have a common direction. As an application, we prove
that the prices of anarchy and stability converge
to 1 as the number of players goes to infinity, and
show how to exploit these semilinear representations
to compute these ratios precisely for a given
network and number of players.
@inproceedings{fsttcs2022-BMSS,
author = {Bertrand, Nathalie and Markey, Nicolas and
Sadhukhan, Suman and Sankur, Ocan},
title = {Semilinear Representations for Series-Parallel
Atomic Congestion Games},
editor = {Dawar, Anuj and Guruswami, Venkatesan},
booktitle = {{P}roceedings of the 42nd {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience ({FSTTCS}'22)},
acronym = {{FSTTCS}'22},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
volume = {250},
pages = {32:1-32:20},
year = {2022},
month = dec,
doi = {10.4230/LIPIcs.FSTTCS.2022.32},
abstract = {We~consider atomic congestion games on
series-parallel networks, and study the structure of
the sets of Nash equilibria and social local optima
on a given network when the number of players
varies. We establish that these sets are definable
in Presburger arithmetic and that they admit
semilinear representations whose all period vectors
have a common direction. As~an~application, we~prove
that the prices of anarchy and stability converge
to~1 as the number of players goes to infinity, and
show how to exploit these semilinear representations
to compute these ratios precisely for a given
network and number of players.},
}
We consider the parameterized verification problem
for distributed algorithms where the goal is to
develop techniques to prove the correctness of a
given algorithm regardless of the number of
participating processes. Motivated by an
asynchronous binary consensus algorithm of
[J. Aspnes; Fast deterministic consensus in a noisy
environment; J. Algorithms, 2002], we consider
round-based distributed algorithms communicating
with shared memory. A particular challenge in these
systems is that 1) the number of processes is
unbounded, and, more importantly, 2) there is a
fresh set of registers at each round. A verification
algorithm thus needs to manage both sources of
infinity. In this setting, we prove that the safety
verification problem, which consists in deciding
whether all possible executions avoid a given error
state, is PSPACE-complete. For negative instances of
the safety verification problem, we also provide
exponential lower and upper bounds on the minimal
number of processes needed for an error execution
and on the minimal round on which the error state
can be covered.
@inproceedings{icalp2022-BMSW,
author = {Bertrand, Nathalie and Markey, Nicolas and Sankur,
Ocan and Waldburger, Nicolas},
title = {Parameterized safety verification of round-based
shared-memory systems},
editor = {Woodruff, David and Boja{\'n}czyk, Miko{\l}aj},
booktitle = {{P}roceedings of the 49th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'22)},
acronym = {{ICALP}'22},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
pages = {113:1-113:20},
year = {2022},
month = jul,
doi = {10.4230/LIPIcs.ICALP.2022.113},
abstract = {We consider the parameterized verification problem
for distributed algorithms where the goal is to
develop techniques to prove the correctness of a
given algorithm regardless of the number of
participating processes. Motivated by an
asynchronous binary consensus algorithm~of
[J.~Aspnes; Fast deterministic consensus in a noisy
environment; J.~Algorithms,~2002], we~consider
round-based distributed algorithms communicating
with shared memory. A~particular challenge in these
systems is that 1)~the~number of processes is
unbounded, and, more importantly, 2)~there is a
fresh set of registers at each round. A~verification
algorithm thus needs to manage both sources of
infinity. In~this setting, we~prove that the safety
verification problem, which consists in deciding
whether all possible executions avoid a given error
state, is PSPACE-complete. For~negative instances of
the safety verification problem, we~also provide
exponential lower and upper bounds on the minimal
number of processes needed for an error execution
and on the minimal round on which the error state
can be covered.},
}
[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,
}
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.},
}
@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,
}
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},
}
@book{BO16-CSAPP,
author = {Bryant, Randal E. and O'Hallaron, David R.},
title = {Computer Systems~-- A~programmer's perspective},
publisher = {Pearson},
year = {2016},
}
[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,
}
[Bok18]
UdiBoker.
Why these automata types?.
In LPAR'18,
EPiC Series in Computing 57, pages 143-163. EasyChair, November 2018.
@article{am3(1-4)-Bou,
author = {Bouton, Charles L.},
title = {Nim, a~game with a complete mathematical theory},
publisher = {Princeton University Press},
journal = {Annals of Mathematics},
volume = {3},
number = {1-4},
pages = {35-39},
year = {1901},
}
[Bou98]
PatriciaBouyer.
Automates temporisés et modularité.
Mémoire de D.E.A.,
Lab. Spécification & Vérification, ENS Cachan,
France,
June 1998.
@mastersthesis{dea-Bouyer,
author = {Bouyer, Patricia},
title = {Automates temporis{\'e}s et modularit{\'e}},
year = {1998},
month = jun,
school = {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
France},
type = {M\'emoire de D.E.A.},
}
[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},
}
@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,
}
@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},
}
[BPR+16]
RomainBrenguier,
Guillermo A.Pérez,
Jean-FrançoisRaskin, and
MathieuSassolas.
Admissibility in Quantitative Graph Games.
In FSTTCS'16,
Leibniz International Proceedings in Informatics, pages 42:1-42:14. Leibniz-Zentrum für Informatik, December 2016.
@inproceedings{fsttcs2016-BPRS,
author = {Brenguier, Romain and P{\'e}rez, Guillermo A. and
Raskin, Jean-Fran{\c c}ois and Sassolas, Mathieu},
title = {Admissibility in Quantitative Graph Games},
editor = {Akshay, S. and Lal, Akash and Saurabh, Saket and
Sen, Sandeep},
booktitle = {{P}roceedings of the 36th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience ({FSTTCS}'16)},
acronym = {{FSTTCS}'16},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
pages = {42:1-42:14},
year = {2016},
month = dec,
doi = {10.4230/LIPIcs.FSTTCS.2016.42},
}
[BR01]
ThomasBall and
SriramRajamani.
The SLAM toolkit.
In CAV'01,
Lecture Notes in Computer Science 2102, pages 260-264. Springer-Verlag, July 2001.
@inproceedings{cav2001-BR,
author = {Ball, Thomas and Rajamani, Sriram},
title = {The {SLAM} toolkit},
editor = {Berry, G{\'e}rard and Comon, Hubert and Finkel,
Alain},
booktitle = {{P}roceedings of the 13th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'01)},
acronym = {{CAV}'01},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {2102},
pages = {260-264},
year = {2001},
month = jul,
}
[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,
}
@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},
}
@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},
}
@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},
}
@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},
}
[BT89]
Dimitri P.Bertsekas and
John N.Tsitsiklis.
Parallel and distributed computation: numerical
methods.
Prentice Hall, 1989.
@book{BP-pdc1989,
author = {Bertsekas, Dimitri P. and Tsitsiklis, John N.},
title = {Parallel and distributed computation: numerical
methods},
publisher = {Prentice Hall},
year = {1989},
}
[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,
}
@inproceedings{lmps1960-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}{\v 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.