B
[Bab85] 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] Armin Biere, Cyrille Artho, and Viktor Schuppan. 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] Dietmar Berwanger and Achim Blumensath. The Monadic Theory of Tree-like Structures. In Erich Grädel, Wolfgang Thomas, and Thomas Wilke (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án Briones and Ed Brinksma. A Test Generation Framework for Quiescent Real-Time Systems. In FATES'04, Lecture Notes in Computer Science 3395, pages 64-78. Springer-Verlag, September 2004.
@inproceedings{BB-fates2004,
author =              {Briones, Laura Brand{\'a}n and Brinksma, Ed},
title =               {A~Test Generation Framework for Quiescent Real-Time
Systems},
editor =              {Grabowski, Jens and Nielsen, Brian},
booktitle =           {{P}roceedings of the 4th {I}nternational {W}orkshop
on {F}ormal {A}pproaches to {S}oftware {T}esting
({FATES}'04)},
acronym =             {{FATES}'04},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {3395},
pages =               {64-78},
year =                {2004},
month =               sep,
doi =                 {10.1007/978-3-540-31848-4_5},
}

[BBB+09] Christel Baier, Nathalie Bertrand, Patricia Bouyer, and Thomas Brihaye. When are timed automata determinizable?. In ICALP'09, Lecture Notes in Computer Science 5556, pages 43-54. Springer-Verlag, July 2009.
@inproceedings{icalp2009-BBBB,
author =              {Baier, {\relax Ch}ristel and Bertrand, Nathalie and
Bouyer, Patricia and Brihaye, {\relax Th}omas},
title =               {When are timed automata determinizable?},
editor =              {Albers, Susanne and Marchetti{-}Spaccamela Alberto
and Matias, Yossi and Nikoletseas, Sotiris and
Thomas, Wolfgang},
booktitle =           {{P}roceedings of the 36th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'09)~-- Part~{II}},
acronym =             {{ICALP}'09},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {5556},
pages =               {43-54},
year =                {2009},
month =               jul,
doi =                 {10.1007/978-3-642-02930-1_4},
}

[BBB+07] Christel Baier, Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, and Marcus Größ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] Christel Baier, Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, and Marcus Größ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] Éric Badouel, Marek Bednarczyk, Andrzej Borzyszkowski, Benoît Caillaud, and Philippe Darondeau. 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},
journal =             {Discrete Event Dynamic Systems},
volume =              {17},
number =              {4},
pages =               {425-446},
year =                {2007},
month =               dec,
doi =                 {10.1007/s10626-007-0020-5},
}

[BBB+08] Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, and Nicolas Markey. Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics. In QEST'08, pages 55-64. IEEE Comp. Soc. Press, September 2008.
Abstract

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] Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, Quentin Menet, Christel Baier, Marcus Größer, and Marcin Jurdziń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] Patricia Bouyer, Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. 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
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èle Beauquier, Jean Berstel, and Philippe Chré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},
}

[BBC10] Albert Benveniste, Anne Bouillard, and Paul Caspi. A unifying view of loosely time-triggered architectures. In EMSOFT'10, pages 189-198. ACM Press, October 2010.
@inproceedings{emsoft2010-BBC,
author =              {Benveniste, Albert and Bouillard, Anne and Caspi,
Paul},
title =               {A~unifying view of loosely time-triggered
architectures},
editor =              {Carloni, Luca P. and Tripakis, Stavros},
booktitle =           {{P}roceedings of the 10th {I}nternational
{C}onference on {E}mbedded {S}oftware ({EMSOFT}'10)},
acronym =             {{EMSOFT}'10},
publisher =           {ACM Press},
pages =               {189-198},
year =                {2010},
month =               oct,
doi =                 {10.1145/1879021.1879047},
}

[BBD14] Thomas Brihaye, Véronique Bruyère, and Julie De 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] Thomas Brihaye, Véronique Bruyère, Laurent Doyen, Marc Ducobu, and Jean-François Raskin. 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
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] Thomas Brihaye, Véronique Bruyère, Julie De Pril, and Hugo Gimbert. 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] Gerd Behrmann, Johan Bengtsson, Alexandre David, Kim Guldstrand Larsen, Paul Pettersson, and Wang Yi. 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áclav Brožek, Vojtěch Forejt, and Antonín Kučera. Stochastic Games with Branching-Time Winning Objectives. In LICS'06, pages 349-358. IEEE Comp. Soc. Press, July 2006.
@inproceedings{lics2006-BBFK,
author =              {Br{\'a}zdil, Tom{\'a}{ s} and V{\'a}clav
Bro{{z}}ek and Forejt, Vojt{{e}}ch and Ku{
c}era, Anton{\'\i}n},
title =               {Stochastic Games with Branching-Time Winning
Objectives},
booktitle =           {{P}roceedings of the 21st {A}nnual {S}ymposium on
{L}ogic in {C}omputer {S}cience ({LICS}'06)},
acronym =             {{LICS}'06},
publisher =           {IEEE Comp. Soc. Press},
pages =               {349-358},
year =                {2006},
month =               jul,
}

[BBF+03] Gerd Behrmann, Patricia Bouyer, Emmanuel Fleury, and Kim Guldstrand Larsen. 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,
}

[BBF+18] Giovanni Bacci, Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, and Pierre-Alain Reynier. Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty. In FM'18, Lecture Notes in Computer Science 10951, pages 203-221. Springer-Verlag, July 2018.
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.

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

[BBF+01] Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci, Philippe Schnoebelen, and Pierre McKenzie. 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] Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, and Jean-François Raskin. 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] Christel Baier, Tomáš Brázdil, Marcus Größer, and Antonín Kučera. Stochastic Game Logic. In QEST'07, pages 227-236. IEEE Comp. Soc. Press, September 2007.
@inproceedings{qest2007-BBGK,
author =              {Baier, {\relax Ch}ristel and Br{\'a}zdil,
Tom{\'a}{ s} and Gr{\"o}{\ss}er, Marcus and Ku{
c}era, Anton{\'\i}n},
title =               {Stochastic Game Logic},
booktitle =           {{P}roceedings of the 4th {I}nternational
{C}onference on {Q}uantitative {E}valuation of
{S}ystems ({QEST}'07)},
acronym =             {{QEST}'07},
publisher =           {IEEE Comp. Soc. Press},
pages =               {227-236},
year =                {2007},
month =               sep,
}

[BBG+12] Christel Baier, Tomáš Brázdil, Marcus Größer, and Antonín Kuč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}{ s} and Gr{\"o}{\ss}er, Marcus and Ku{
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},
}

[BBJ+14] Dimitri Bohlender, Harold Bruintjes, Sebastian Junges, Jens Katelaan, Viet Yen Nguyen, and Thomas Noll. A Review of Statistical Model Checking Pitfalls on Real-Time Stochastic Models. In ISoLA'14, Lecture Notes in Computer Science 8803, pages 177-192. Springer-Verlag, October 2014.
@inproceedings{BBJKNN-isola2014,
author =              {Bohlender, Dimitri and Bruintjes, Harold and Junges,
Sebastian and Katelaan, Jens and Nguyen, Viet Yen
and Noll, Thomas},
title =               {A~Review of Statistical Model Checking Pitfalls on
Real-Time Stochastic Models},
editor =              {Margaria, Tiziana and Steffen, Bernhard},
booktitle =           {{P}roceedings of the 6th {I}nternational {S}ymposium
on {L}everaging {A}pplications of {F}ormal
{M}ethods, {V}erification and {V}alidation
({IS}o{LA}'14)~-- {P}art~{II}: {S}pecialized
{T}echniques and {A}pplications},
acronym =             {{IS}o{LA}'14},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {8803},
pages =               {177-192},
year =                {2014},
month =               oct,
doi =                 {10.1007/978-3-662-45231-8_13},
}

[BBL04] Patricia Bouyer, Ed Brinksma, and Kim Guldstrand Larsen. Staying Alive as Cheaply as Possible. In HSCC'04, Lecture Notes in Computer Science 2993, pages 203-218. Springer-Verlag, March 2004.
@inproceedings{hscc2004-BBL,
author =              {Bouyer, Patricia and Brinksma, Ed and Larsen, Kim
Guldstrand},
title =               {Staying Alive as Cheaply as Possible},
editor =              {Alur, Rajeev and Pappas, George J.},
booktitle =           {{P}roceedings of the 7th {I}nternational {W}orkshop
on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
({HSCC}'04)},
acronym =             {{HSCC}'04},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {2993},
pages =               {203-218},
year =                {2004},
month =               mar,
}

[BBL08] Patricia Bouyer, Ed Brinksma, and Kim Guldstrand Larsen. Optimal infinite scheduling for multi-priced timed automata. Formal Methods in System Design 32(1):2-23. Springer-Verlag, February 2008.
@article{fmsd32(1)-BBL,
author =              {Bouyer, Patricia and Brinksma, Ed and Larsen, Kim
Guldstrand},
title =               {Optimal infinite scheduling for multi-priced timed
automata},
publisher =           {Springer-Verlag},
journal =             {Formal Methods in System Design},
volume =              {32},
number =              {1},
pages =               {2-23},
year =                {2008},
month =               feb,
}

[BBL+13] Giorgio Bacci, Giovanni Bacci, Kim Guldstrand Larsen, and Radu Mardare. Computing Behavioral Distances, Compositionally. In MFCS'13, Lecture Notes in Computer Science 8087, pages 74-85. Springer-Verlag, August 2013.
@inproceedings{mfcs2013-BBLM,
author =              {Bacci, Giorgio and Bacci, Giovanni and Larsen, Kim
title =               {Computing Behavioral Distances, Compositionally},
editor =              {Chatterjee, Krishnendu and Sgall, Ji{ r}{\'\i}},
booktitle =           {{P}roceedings of the 38th {I}nternational
{S}ymposium on {M}athematical {F}oundations of
{C}omputer {S}cience ({MFCS}'13)},
acronym =             {{MFCS}'13},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {8087},
pages =               {74-85},
year =                {2013},
month =               aug,
doi =                 {10.1007/978-3-642-40313-2_9},
}

[BBL+13] Giorgio Bacci, Giovanni Bacci, Kim Guldstrand Larsen, and Radu Mardare. The BisimDist Library: Efficient Computation of Bisimilarity Distances for Markovian Models. In QEST'13, pages 278-281. IEEE Comp. Soc. Press, August 2013.
@inproceedings{qest2013-BBLM,
author =              {Bacci, Giorgio and Bacci, Giovanni and Larsen, Kim
title =               {The BisimDist Library: Efficient Computation of
Bisimilarity Distances for Markovian Models},
booktitle =           {{P}roceedings of the 10th {I}nternational
{C}onference on {Q}uantitative {E}valuation of
{S}ystems ({QEST}'13)},
acronym =             {{QEST}'13},
publisher =           {IEEE Comp. Soc. Press},
pages =               {278-281},
year =                {2013},
month =               aug,
doi =                 {10.1007/978-3-642-40196-1_23},
}

[BBL+04] Gerd Behrmann, Patricia Bouyer, Kim Guldstrand Larsen, and Radek Pelá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
title =               {Lower and Upper Bounds in Zone-Based Abstractions of
Timed Automata},
editor =              {Jensen, Kurt and Podelski, Andreas},
booktitle =           {{P}roceedings of the 10th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'04)},
acronym =             {{TACAS}'04},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {2988},
pages =               {312-326},
year =                {2004},
month =               mar,
doi =                 {10.1007/978-3-540-24730-2_25},
}

[BBL+06] Gerd Behrmann, Patricia Bouyer, Kim Guldstrand Larsen, and Radek Pelánek. Lower and Upper Bounds in Zone-Based Abstractions of Timed Automata. International Journal on Software Tools for Technology Transfer 8(3):204-215. Springer-Verlag, June 2006.
@article{sttt8(3)-BBLP,
author =              {Behrmann, Gerd and Bouyer, Patricia and Larsen, Kim
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] Nikola Beneš, Petr Bezdek, Kim Guldstrand Larsen, and Jiří Srba. Language Emptiness of Continuous-Time Parametric Timed Automata. In ICALP'15, Lecture Notes in Computer Science 9135, pages 69-81. Springer-Verlag, July 2015.
@inproceedings{icalp2015-BBLS,
author =              {Bene{{s}}, Nikola and Bezdek, Petr and Larsen, Kim
Guldstrand and Srba, Ji{ r}{\'\i}},
title =               {Language Emptiness of Continuous-Time Parametric
Timed Automata},
editor =              {Halld{\'o}rsson, Magn{\'u}s M. and Iwana, Kazuo and
Kobayashi, Naoki and Speckmann, Bettina},
booktitle =           {{P}roceedings of the 42nd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'15)~-- Part~{II}},
acronym =             {{ICALP}'15},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {9135},
pages =               {69-81},
year =                {2015},
month =               jul,
doi =                 {10.1007/978-3-662-47666-6_6},
}

[BBM06] Ramzi Ben Salah, Marius Bozga, and Oded Maler. On Interleaving in Timed Automata. In CONCUR'06, Lecture Notes in Computer Science 4137, pages 465-476. Springer-Verlag, August 2006.
@inproceedings{concur2006-BBM,
author =              {Ben{~}Salah, Ramzi and Bozga, Marius and Maler,
Oded},
title =               {On Interleaving in Timed Automata},
editor =              {Baier, {\relax Ch}ristel and Hermanns, Holger},
booktitle =           {{P}roceedings of the 17th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'06)},
acronym =             {{CONCUR}'06},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {4137},
pages =               {465-476},
year =                {2006},
month =               aug,
}

[BBM06] Patricia Bouyer, Thomas Brihaye, and Nicolas Markey. Improved Undecidability Results on Weighted Timed Automata. Information Processing Letters 98(5):188-194. Elsevier, June 2006.
Abstract

In this paper, we improve two recent undecidability results of Brihaye, Bruyère and Raskin about weighted timed automata, an extension of timed automata with a cost variable. Our results rely on a new encoding of the two counters of a Minsky machine that only require three clocks and one stopwatch cost, while previous reductions required five clocks and one stopwatch cost.

@article{ipl98(5)-BBM,
author =              {Bouyer, Patricia and Brihaye, {\relax Th}omas and
Markey, Nicolas},
title =               {Improved Undecidability Results on Weighted Timed
Automata},
publisher =           {Elsevier},
journal =             {Information Processing Letters},
volume =              {98},
number =              {5},
pages =               {188-194},
year =                {2006},
month =               jun,
doi =                 {10.1016/j.ipl.2006.01.012},
abstract =            {In this paper, we improve two recent undecidability
weighted timed automata, an extension of timed
automata with a cost variable. Our results rely on a
new encoding of the two counters of a Minsky machine
that only require three clocks and one stopwatch
cost, while previous reductions required five clocks
and one stopwatch cost.},
}

[BBM10] Patricia Bouyer, Romain Brenguier, and Nicolas Markey. Nash Equilibria for Reachability Objectives in Multi-player Timed Games. In CONCUR'10, Lecture Notes in Computer Science 6269, pages 192-206. Springer-Verlag, September 2010.
Abstract

We propose a procedure for computing Nash equilibria in multi-player timed games with reachability objectives. Our procedure is based on the construction of a finite concurrent game, and on a generic characterization of Nash equilibria in (possibly infinite) concurrent games. Along the way, we use our characterization to compute Nash equilibria in finite concurrent games.

@inproceedings{concur2010-BBM,
author =              {Bouyer, Patricia and Brenguier, Romain and Markey,
Nicolas},
title =               {{N}ash Equilibria for Reachability Objectives in
Multi-player Timed Games},
editor =              {Gastin, Paul and Laroussinie, Fran{\c c}ois},
booktitle =           {{P}roceedings of the 21st {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'10)},
acronym =             {{CONCUR}'10},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {6269},
pages =               {192-206},
year =                {2010},
month =               sep,
doi =                 {10.1007/978-3-642-15375-4_14},
abstract =            {We propose a procedure for computing Nash equilibria
in multi-player timed games with reachability
objectives. Our procedure is based on the
construction of a finite concurrent game, and on a
generic characterization of Nash equilibria in
(possibly infinite) concurrent games. Along the way,
we~use our characterization to compute Nash
equilibria in finite concurrent games.},
}

[BBM10] Patricia Bouyer, Romain Brenguier, and Nicolas Markey. Computing Equilibria in Two-Player Timed Games via Turn-Based Finite Games. In FORMATS'10, Lecture Notes in Computer Science 6246, pages 62-76. Springer-Verlag, September 2010.
Abstract

We study two-player timed games where the objectives of the two players are not opposite. We focus on the standard notion of Nash equilibrium and propose a series of transformations that builds two finite turn-based games out of a timed game, with a precise correspondence between Nash equilibria in the original and in final games. This provides us with an algorithm to compute Nash equilibria in two-player timed games for large classes of properties.

@inproceedings{formats2010-BBM,
author =              {Bouyer, Patricia and Brenguier, Romain and Markey,
Nicolas},
title =               {Computing Equilibria in Two-Player Timed Games
{\textit{via}}~Turn-Based Finite Games},
editor =              {Chatterjee, Krishnendu and Henzinger, Thomas A.},
booktitle =           {{P}roceedings of the 8th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'10)},
acronym =             {{FORMATS}'10},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {6246},
pages =               {62-76},
year =                {2010},
month =               sep,
doi =                 {10.1007/978-3-642-15297-9_7},
abstract =            {We study two-player timed games where the objectives
of the two players are not opposite. We focus on the
standard notion of Nash equilibrium and propose a
series of transformations that builds two finite
turn-based games out of a timed game, with a precise
correspondence between Nash equilibria in the
original and in final games. This provides us with
an algorithm to compute Nash equilibria in
two-player timed games for large classes of
properties.},
}

[BBM18] A. R. Balasubramanian, Nathalie Bertrand, and Nicolas Markey. Parameterized verification of synchronization in constrained reconfigurable broadcast networks. In TACAS'18 (Part II), Lecture Notes in Computer Science 10806, pages 38-54. Springer-Verlag, April 2018.
Abstract

Reconfigurable broadcast networks provide a convenient formalism for modelling and reasoning about networks of mobile agents broadcasting messages to other agents following some (evolving) communication topology. The parameterized verification of such models aims at checking whether a given property holds irrespective of the initial configuration (number of agents, initial states and initial communication topology). We focus here on the synchronization property, asking whether all agents converge to a set of target states after some execution. This problem is known to be decidable in polynomial time when no constraints are imposed on the evolution of the communication topology (while it is undecidable for static broadcast networks).

In this paper we investigate how various constraints on reconfigurations affect the decidability and complexity of the synchronization problem. In particular, we show that when bounding the number of reconfigured links between two communications steps by a constant, synchronization becomes undecidable; on the other hand, synchronization remains decidable in PTIME when the bound grows with the number of agents.

@inproceedings{tacas2018-2-BBM,
author =              {Balasubramanian, A. R. and Bertrand, Nathalie and
Markey, Nicolas},
title =               {Parameterized verification of synchronization in
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
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
all agents converge to a set of target states after
some execution. This~problem is known to be
decidable in polynomial time when no constraints are
imposed on the evolution of the communication
topology (while~it~is undecidable for static
broadcast networks).\par In this paper we
investigate how various constraints on
reconfigurations affect the decidability and
complexity of the synchronization problem.
In~particular, we show that when bounding the number
of reconfigured links between two communications
steps by a constant, synchronization becomes
undecidable; on~the other hand, synchronization
remains decidable in PTIME when the bound grows with
the number of agents.},
}

[BBM+11] Patricia Bouyer, Romain Brenguier, Nicolas Markey, and Michael Ummels. Nash Equilibria in Concurrent Games with Büchi Objectives. In FSTTCS'11, Leibniz International Proceedings in Informatics 13, pages 375-386. Leibniz-Zentrum für Informatik, December 2011.
Abstract

We study the problem of the existence (and computation) of Nash equilibria in multi-player concurrent games with Büchi-definable objectives. First, when the objectives are Büchi conditions on the game, we prove that the existence problem can be solved in polynomial time. In a second part, we extend our technique to objectives defined by deterministic Büchi automata, and prove that the problem then becomes EXPTIME-complete. We prove PSPACE-completeness for the case where the Büchi automata are 1-weak.

@inproceedings{fsttcs2011-BBMU,
author =              {Bouyer, Patricia and Brenguier, Romain and Markey,
Nicolas and Ummels, Michael},
title =               {{N}ash Equilibria in Concurrent Games with
{B}{\"u}chi Objectives},
editor =              {Chakraborty, Supratik and Kumar, Amit},
booktitle =           {{P}roceedings of the 31st {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience ({FSTTCS}'11)},
acronym =             {{FSTTCS}'11},
publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
series =              {Leibniz International Proceedings in Informatics},
volume =              {13},
pages =               {375-386},
year =                {2011},
month =               dec,
doi =                 {10.4230/LIPIcs.FSTTCS.2011.375},
abstract =            {We study the problem of the existence (and
computation) of Nash equilibria in multi-player
concurrent games with B{\"u}chi-definable
objectives. First, when the objectives are B{\"u}chi
conditions on the game, we prove that the existence
problem can be solved in polynomial time. In a
second part, we extend our technique to objectives
defined by deterministic B{\"u}chi automata, and
prove that the problem then becomes
EXPTIME-complete. We prove PSPACE-completeness for
the case where the B{\"u}chi automata are 1-weak.},
}

[BBM+12] Patricia Bouyer, Romain Brenguier, Nicolas Markey, and Michael Ummels. Concurrent games with ordered objectives. In FoSSaCS'12, Lecture Notes in Computer Science 7213, pages 301-315. Springer-Verlag, March 2012.
Abstract

We consider concurrent games played on graphs, in which each player has several qualitative (e.g. reachability or Büchi) objectives, and a preorder on these objectives (for instance the counting order, where the aim is to maximise the number of objectives that are fulfilled).

We study two fundamental problems in that setting: (1) the value problem, which aims at deciding the existence of a strategy that ensures a given payoff; (2) the Nash equilibrium problem, where we want to decide the existence of a Nash equilibrium (possibly with a condition on the payoffs). We characterise the exact complexities of these problems for several relevant preorders, and several kinds of objectives.

@inproceedings{fossacs2012-BBMU,
author =              {Bouyer, Patricia and Brenguier, Romain and Markey,
Nicolas and Ummels, Michael},
title =               {Concurrent games with ordered objectives},
editor =              {Birkedal, Lars},
booktitle =           {{P}roceedings of the 15th {I}nternational
{C}onference on {F}oundations of {S}oftware
{S}cience and {C}omputation {S}tructure
({FoSSaCS}'12)},
acronym =             {{FoSSaCS}'12},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {7213},
pages =               {301-315},
year =                {2012},
month =               mar,
doi =                 {10.1007/978-3-642-28729-9_20},
abstract =            {We consider concurrent games played on graphs, in
which each player has several qualitative (e.g.
reachability or B{\"u}chi) objectives, and a
preorder on these objectives (for instance the
counting order, where the aim is to maximise the
number of objectives that are fulfilled).\par We
study two fundamental problems in that setting:
(1)~the \emph{value problem}, which aims at deciding
the existence of a strategy that ensures a given
payoff; (2)~the \emph{Nash equilibrium problem},
where we want to decide the existence of a Nash
equilibrium (possibly with a condition on the
payoffs). We characterise the exact complexities of
these problems for several relevant preorders, and
several kinds of objectives.},
}

[BBM+15] Patricia Bouyer, Romain Brenguier, Nicolas Markey, and Michael Ummels. Pure Nash Equilibria in Concurrent Games. Logical Methods in Computer Science 11(2:9). June 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ü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
}

[BBR04] Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. 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,
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] Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. 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,
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 Jitka Stříbrná. Distributed LTL Model-Checking in SPIN. In SPIN'01, Lecture Notes in Computer Science 2057, pages 200-216. Springer-Verlag, May 2001.
@inproceedings{spin2001-BBS,
author =              {Barnat, Ji{ r}{\'\i} and Brim, Lubo{ s} and
St{ r}{\'\i}brn{\'a}, Jitka},
title =               {Distributed {LTL} Model-Checking in {SPIN}},
editor =              {Dwyer, Matthew B.},
booktitle =           {{P}roceedings of the 8th {I}nternational {SPIN}
{W}orkshop ({SPIN}'01)},
acronym =             {{SPIN}'01},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {2057},
pages =               {200-216},
year =                {2001},
month =               may,
}

[BC03] Marco Benedetti and Alessandro Cimatti. 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] Patricia Bouyer and Fabrice Chevalier. 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] Patricia Bouyer and Fabrice Chevalier. 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 Jakub Chaloupka. Using Strategy Improvement to Stay Alive. Technical Report FIMU-RS-2010-03, Faculty of Informatics, Masaryk University, Brno, Czech Republic, March 2010.
@techreport{FIMU-RS-2010-03-BC,
author =              {Brim, Lubo{ s} and Chaloupka, Jakub},
title =               {Using Strategy Improvement to Stay Alive},
number =              {FIMU-RS-2010-03},
year =                {2010},
month =               mar,
institution =         {Faculty of Informatics, Masaryk University, Brno,
Czech Republic},
}

[BCC98] Sergey Berezin, Sérgio Vale Aguiar Campos, 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] Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, and Yunshan Zhu. Bounded Model Checking. In Marvin Zelkowitz (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},
volume =              {58},
pages =               {117-148},
chapter =             {3},
year =                {2003},
}

[BCC+99] Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. 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] Patricia Bouyer, Fabrice Chevalier, and Deepak D'Souza. Fault Diagnosis Using Timed Automata. In FoSSaCS'05, Lecture Notes in Computer Science 3441, pages 219-233. Springer-Verlag, April 2005.
@inproceedings{fossacs2005-BCD,
author =              {Bouyer, Patricia and Chevalier, Fabrice and D'Souza,
Deepak},
title =               {Fault Diagnosis Using Timed Automata},
booktitle =           {{P}roceedings of the 8th {I}nternational
{C}onference on {F}oundations of {S}oftware
{S}cience and {C}omputation {S}tructure
({FoSSaCS}'05)},
acronym =             {{FoSSaCS}'05},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {3441},
pages =               {219-233},
year =                {2005},
month =               apr,
doi =                 {10.1007/978-3-540-31982-5_14},
}

[BCD+07] Gerd Behrmann, Agnès Cougnard, Alexandre David, Emmanuel Fleury, Kim Guldstrand Larsen, and Didier Lime. UPPAAL-Tiga: Time for Playing Games!. In CAV'07, Lecture Notes in Computer Science 4590, pages 121-125. Springer-Verlag, July 2007.
@inproceedings{cav2007-BCDFLL,
author =              {Behrmann, Gerd and Cougnard, Agn{\e}s and David,
Alexandre and Fleury, Emmanuel and Larsen, Kim
Guldstrand and Lime, Didier},
title =               {{UPPAAL-Tiga}: Time for Playing Games!},
editor =              {Damm, Werner and Hermanns, Holger},
booktitle =           {{P}roceedings of the 19th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'07)},
acronym =             {{CAV}'07},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {4590},
pages =               {121-125},
year =                {2007},
month =               jul,
}

[BCD+11] Luboš Brim, Jakub Chaloupka, Laurent Doyen, Raffaella Gentilini, and Jean-François Raskin. Faster algorithms for mean-payoff games. Formal Methods in System Design 38(2):97-118. Springer-Verlag, April 2011.
@article{fmsd38(2)-BCDGR,
author =              {Brim, Lubo{ s} and Chaloupka, Jakub and Doyen,
Laurent and Gentilini, Raffaella and Raskin,
Jean-Fran{\c c}ois},
title =               {Faster algorithms for mean-payoff games},
publisher =           {Springer-Verlag},
journal =             {Formal Methods in System Design},
volume =              {38},
number =              {2},
pages =               {97-118},
year =                {2011},
month =               apr,
doi =                 {10.1007/s10703-010-0105-x},
}

[BCE+98] Jean-Jacques Borrelly, Ève Costemaniere, Bernard Espiau, Konstantinos Kapellos, Roger Pissard-Gibollet, Daniel Simon, and Nicolas Turro. 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},
journal =             {International Journal of Robotics Research},
volume =              {17},
number =              {4},
pages =               {338-359},
year =                {1998},
month =               apr,
}

[BCF03] Harry Buhrman, Richard Chang, and Lance Fortnow. 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] Patricia Bouyer, Franck Cassez, Emmanuel Fleury, and Kim Guldstrand Larsen. 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] Patricia Bouyer, Franck Cassez, Emmanuel Fleury, and Kim Guldstrand Larsen. Optimal Strategies in Priced Timed Games. Research Report RS-04-4, Basic Research in Computer Science, Aalborg University, Denmark, February 2004.
@techreport{TR-brics04-4,
author =              {Bouyer, Patricia and Cassez, Franck and Fleury,
Emmanuel and Larsen, Kim Guldstrand},
title =               {Optimal Strategies in Priced Timed Games},
number =              {RS-04-4},
year =                {2004},
month =               feb,
institution =         {Basic Research in Computer Science, Aalborg
University, Denmark},
type =                {Research Report},
}

[BCG88] Michael C. Browne, Edmund M. Clarke, and Orna Grumberg. Characterizing Finite Kripke Structures in Propositional Temporal Logic. Theoretical Computer Science 59(1-2):115-131. Elsevier, July 1988.
@article{tcs59(1-2)-BCG,
author =              {Browne, Michael C. and Clarke, Edmund M. and
Grumberg, Orna},
title =               {Characterizing Finite {K}ripke Structures in
Propositional Temporal Logic},
publisher =           {Elsevier},
journal =             {Theoretical Computer Science},
volume =              {59},
number =              {1-2},
pages =               {115-131},
year =                {1988},
month =               jul,
}

[BCG+92] Samuel R. Buss, Stephen A. Cook, Vineet Gupta, and Vijaya Ramachandran. An Optimal Parallel Algorithm for Formula Evaluation. SIAM Journal on Computing 21(4):755-780. Society for Industrial and Applied Math., August 1992.
@article{siamcomp21(4)-BCGR,
author =              {Buss, Samuel R. and Cook, Stephen A. and Gupta,
Vineet and Ramachandran, Vijaya},
title =               {An Optimal Parallel Algorithm for Formula
Evaluation},
publisher =           {Society for Industrial and Applied Math.},
journal =             {SIAM Journal on Computing},
volume =              {21},
number =              {4},
pages =               {755-780},
year =                {1992},
month =               aug,
}

[BCH+11] Udi Boker, Krishnendu Chatterjee, Thomas A. Henzinger, and Orna Kupferman. Temporal Specifications with Accumulative Values. In LICS'11, pages 43-52. IEEE Comp. Soc. Press, June 2011.
@inproceedings{lics2011-BCHK,
author =              {Boker, Udi and Chatterjee, Krishnendu and Henzinger,
Thomas A. and Kupferman, Orna},
title =               {Temporal Specifications with Accumulative Values},
booktitle =           {{P}roceedings of the 26th {A}nnual {S}ymposium on
{L}ogic in {C}omputer {S}cience ({LICS}'11)},
acronym =             {{LICS}'11},
publisher =           {IEEE Comp. Soc. Press},
pages =               {43-52},
year =                {2011},
month =               jun,
doi =                 {10.1109/LICS.2011.33},
}

[BCH+14] Udi Boker, Krishnendu Chatterjee, Thomas A. Henzinger, and Orna Kupferman. 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, Pavel Krčál, and Radek Pelánek. Distributed LTL Model Checking Based on Negative Cycle Detection. In FSTTCS'01, Lecture Notes in Computer Science 2245, pages 96-107. Springer-Verlag, December 2001.
@inproceedings{fsttcs2001-BCKP,
author =              {Brim, Lubo{ s} and {{C}}erna, Ivana and
Kr{{c}}{\'a}l, Pavel and Pel{\'a}nek, Radek},
title =               {Distributed {LTL} Model Checking Based on Negative
Cycle Detection},
editor =              {Hariharan, Ramesh and Mukund, Madhavan and Vinay,
V.},
booktitle =           {{P}roceedings of the 21st {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience ({FSTTCS}'01)},
acronym =             {{FSTTCS}'01},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {2245},
pages =               {96-107},
year =                {2001},
month =               dec,
}

[BCM05] Patricia Bouyer, Fabrice Chevalier, and Nicolas Markey. On the Expressiveness of TPTL and MTL. In FSTTCS'05, Lecture Notes in Computer Science 3821, pages 432-443. Springer-Verlag, December 2005.
Abstract

TPTL and MTL are two classical timed extensions of LTL. In this paper, we positively answer a 15-year-old conjecture that TPTL is strictly more expressive than MTL. But we show that, surprisingly, the TPTL formula proposed by Alur and Henzinger for witnessing this conjecture can be expressed in MTL. More generally, we show that TPTL formulae using only the F modality can be translated into MTL.

@inproceedings{fsttcs2005-BCM,
author =              {Bouyer, Patricia and Chevalier, Fabrice and Markey,
Nicolas},
title =               {On the Expressiveness of {TPTL} and {MTL}},
editor =              {Ramanujam, R. and Sen, Sandeep},
booktitle =           {{P}roceedings of the 25th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience ({FSTTCS}'05)},
acronym =             {{FSTTCS}'05},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {3821},
pages =               {432-443},
year =                {2005},
month =               dec,
doi =                 {10.1007/11590156_35},
abstract =            {TPTL and MTL are two classical timed extensions of
LTL. In this paper, we positively answer a
15-year-old conjecture that TPTL is strictly more
expressive than MTL. But we show that, surprisingly,
the TPTL formula proposed by Alur and Henzinger for
witnessing this conjecture can be expressed in MTL.
More generally, we show that TPTL formulae using
only the \textbf{F} modality can be translated into
MTL.},
}

[BCM10] Patricia Bouyer, Fabrice Chevalier, and Nicolas Markey. On the Expressiveness of TPTL and MTL. Information and Computation 208(2):97-116. Elsevier, February 2010.
Abstract

TPTL and MTL are two classical timed extensions of LTL. In this paper, we prove the 20-year-old conjecture that TPTL is strictly more expressive than MTL. But we show that, surprisingly, the TPTL formula proposed by Alur and Henzinger for witnessing this conjecture can be expressed in MTL. More generally, we show that TPTL formulae using only modality F can be translated into MTL.

@article{icomp208(2)-BCM,
author =              {Bouyer, Patricia and Chevalier, Fabrice and Markey,
Nicolas},
title =               {On the Expressiveness of {TPTL} and {MTL}},
publisher =           {Elsevier},
journal =             {Information and Computation},
volume =              {208},
number =              {2},
pages =               {97-116},
year =                {2010},
month =               feb,
doi =                 {10.1016/j.ic.2009.10.004},
abstract =            {TPTL and MTL are two classical timed extensions
of~LTL. In~this paper, we prove the 20-year-old
conjecture that TPTL is strictly more expressive
than~MTL. But we show that, surprisingly, the
TPTL~formula proposed by Alur and Henzinger for
witnessing this conjecture \emph{can} be expressed
in~MTL. More generally, we show that TPTL formulae
using only modality~F can be translated into~MTL.},
}

[BCM16] Patricia Bouyer, Maximilien Colange, and Nicolas Markey. Symbolic Optimal Reachability in Weighted Timed Automata. In CAV'16, Lecture Notes in Computer Science 9779, pages 513-530. Springer-Verlag, July 2016.
Abstract

Weighted timed automata have been defined in the early 2000's for modelling resource-consumption or -allocation problems in real-time systems. Optimal reachability is decidable in weighted timed automata, and a symbolic forward algorithm has been developed to solve that problem. This algorithm uses so-called priced zones, an extension of standard zones with cost functions. In order to ensure termination, the algorithm requires clocks to be bounded. For unpriced timed automata, much work has been done to develop sound abstractions adapted to the forward exploration of timed automata, ensuring termination of the model-checking algorithm without bounding the clocks. In this paper, we take advantage of recent developments on abstractions for timed automata, and propose an algorithm allowing for symbolic analysis of all weighted timed automata, without requiring bounded clocks.

@inproceedings{cav2016-BCM,
author =              {Bouyer, Patricia and Colange, Maximilien and Markey,
Nicolas},
title =               {Symbolic Optimal Reachability in Weighted Timed
Automata},
editor =              {Chaudhuri, Swarat and Farzan, Azadeh},
booktitle =           {{P}roceedings of the 28th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'16)},
acronym =             {{CAV}'16},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {9779},
pages =               {513-530},
year =                {2016},
month =               jul,
doi =                 {10.1007/978-3-319-41528-4_28},
url =                 {http://arxiv.org/abs/1602.00481},
abstract =            {Weighted timed automata have been defined in the
early 2000's for modelling resource-consumption or
-allocation problems in real-time systems. Optimal
reachability is decidable in weighted timed
automata, and a symbolic forward algorithm has been
developed to solve that problem. This algorithm uses
so-called priced zones, an extension of standard
zones with cost functions. In order to ensure
termination, the algorithm requires clocks to be
bounded. For unpriced timed automata, much work has
been done to develop sound abstractions adapted to
the forward exploration of timed automata, ensuring
termination of the model-checking algorithm without
bounding the clocks. In this paper, we take
advantage of recent developments on abstractions for
timed automata, and propose an algorithm allowing
for symbolic analysis of all weighted timed
automata, without requiring bounded clocks.},
}

[BCM+92] Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation 98(2):142-170. Academic Press, June 1992.
@article{icomp98(2)-BCMDH,
author =              {Burch, Jerry R. and Clarke, Edmund M. and McMillan,
Kenneth L. and Dill, David L. and Hwang, L. J.},
title =               {Symbolic model checking: {$$10^{20}$$} states and
beyond},
journal =             {Information and Computation},
volume =              {98},
number =              {2},
pages =               {142-170},
year =                {1992},
month =               jun,
}

[BCO+92] François Baccelli, Guy Cohen, Geert Jan Olsder, and Jean-Pierre Quadrat. Shynchronization and Linearity. An Algebra For Discrete Event Systems. John Wiley & Sons, 1992.
@book{BCOQ-des2001,
author =              {Baccelli, Fran{\c c}ois and Cohen, Guy and Olsder,
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] Armin Biere, Edmund M. Clarke, and Yunshan Zhu. 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éatrice Bérard and Catherine Dufourd. 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] Patricia Bouyer, Catherine Dufourd, Emmanuel Fleury, and Antoine Petit. 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+11] Thomas Brihaye, Laurent Doyen, Gilles Geeraerts, Joël Ouaknine, Jean-François Raskin, and James Worrell. On Reachability for Hybrid Automata over Bounded Time. In ICALP'11, Lecture Notes in Computer Science 6756, pages 416-427. Springer-Verlag, July 2011.
@inproceedings{icalp2011(2)-BDGORW,
author =              {Brihaye, {\relax Th}omas and Doyen, Laurent and
Geeraerts, Gilles and Ouaknine, Jo{\"e}l and Raskin,
Jean-Fran{\c c}ois and Worrell, James},
title =               {On Reachability for Hybrid Automata over Bounded
Time},
editor =              {Aceto, Luca and Henzinger, Monika and Sgall, Ji{
r}{\'\i}},
booktitle =           {{P}roceedings of the 38th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'11)~-- Part~{II}},
acronym =             {{ICALP}'11},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {6756},
pages =               {416-427},
year =                {2011},
month =               jul,
}

[BDG+98] Béatrice Bérard, Volker Diekert, Paul Gastin, and Antoine Petit. Characterization of the Expressive Power of Silent Transitions in Timed Automata. Fundamenta Informaticae 36(2-3):145-182. IOS Press, November 1998.
@article{fundi36(2-3)-BDGP,
author =              {B{\'e}rard, B{\'e}atrice and Diekert, Volker and
Gastin, Paul and Petit, Antoine},
title =               {Characterization of the Expressive Power of Silent
Transitions in Timed Automata},
publisher =           {IOS Press},
journal =             {Fundamenta Informaticae},
volume =              {36},
number =              {2-3},
pages =               {145-182},
year =                {1998},
month =               nov,
}

[BDH+06] Dietmar Berwanger, Anuj Dawar, Paul Hunter, and Stephan Kreutzer. 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},
}

[BDJ+16] Thomas Brihaye, Benoît Delahaye, Loïg Jezequel, Nicolas Markey, and Jiří Srba (eds.) Proceedings of the Cassting Workshop on Games for the Synthesis of Complex Systems (Cassting'16) and of the 3rd International Workshop on Synthesis of Complex Parameters (SynCoP'16). Electronic Proceedings in Theoretical Computer Science 220. July 2016.
@proceedings{cassting-syncop2016-DJMS,
title =               {{P}roceedings of the {C}assting Workshop on {G}ames
for the {S}ynthesis of {C}omplex {S}ystems
({C}assting'16) and of the 3rd {I}nternational
{W}orkshop on {S}ynthesis of {C}omplex {P}arameters
({S}yn{C}o{P}'16)},
editor =              {Brihaye, {\relax Th}omas and Delahaye, Beno{\^\i}t
and Jezequel, Lo{\"\i}g and Markey, Nicolas and
Srba, Ji{ r}{\'\i}},
booktitle =           {{P}roceedings of the {C}assting Workshop on {G}ames
for the {S}ynthesis of {C}omplex {S}ystems
({C}assting'16) and of the 3rd {I}nternational
{W}orkshop on {S}ynthesis of {C}omplex {P}arameters
({S}yn{C}o{P}'16)},
acronym =             {{C}assting{{\slash}}{S}yn{C}o{P}'16},
series =              {Electronic Proceedings in Theoretical Computer
Science},
volume =              {220},
year =                {2016},
month =               jul,
confyear =            {2016},
confmonth =           {4},
doi =                 {10.4204/EPTCS.220},
url =                 {http://eptcs.web.cse.unsw.edu.au/
content.cgi?CASSTINGSynCoP2016},
}

[BDL12] Benedikt Bollig, Normann Decker, and Martin Leucker. Frequency Linear-time Temporal Logic. In TASE'12, pages 85-92. IEEE Comp. Soc. Press, July 2012.
@inproceedings{tase2012-BDL,
author =              {Bollig, Benedikt and Decker, Normann and Leucker,
Martin},
title =               {Frequency Linear-time Temporal Logic},
editor =              {Margaria, Tiziana and Qiu, Zongyang and Yang,
Hongli},
booktitle =           {{P}roceedings of the 6th {I}nternational {S}ymposium
on {T}heoretical {A}spects of {S}oftware
{E}ngineering ({TASE}'12)},
acronym =             {{TASE}'12},
publisher =           {IEEE Comp. Soc. Press},
pages =               {85-92},
year =                {2012},
month =               jul,
doi =                 {10.1109/TASE.2012.43},
}

[BDL+06] Gerd Behrmann, Alexandre David, Kim Guldstrand Larsen, John Håkansson, Paul Pettersson, Wang Yi, and Martijn Hendriks. UPPAAL 4.0. In QEST'06, pages 125-126. IEEE Comp. Soc. Press, September 2006.
@inproceedings{qest2006-BDLHPYH,
author =              {Behrmann, Gerd and David, Alexandre and Larsen, Kim
Guldstrand and H{\aa}kansson, John and Pettersson,
Paul and Yi, Wang and Hendriks, Martijn},
title =               {UPPAAL~4.0},
booktitle =           {{P}roceedings of the 3rd {I}nternational
{C}onference on {Q}uantitative {E}valuation of
{S}ystems ({QEST}'06)},
acronym =             {{QEST}'06},
publisher =           {IEEE Comp. Soc. Press},
pages =               {125-126},
year =                {2006},
month =               sep,
doi =                 {10.1109/QEST.2006.59},
}

[BDL+14] Peter Bulychev, Alexandre David, Kim Guldstrand Larsen, and Guangyuan Li. Efficient Controller Synthesis for a fragment of MTL0,&infin. Acta Informatica 51(3-4):165-192. Springer-Verlag, June 2014.
@article{acta51(3-4)-BDLL,
author =              {Bulychev, Peter and David, Alexandre and Larsen, Kim
Guldstrand and Li, Guangyuan},
title =               {Efficient Controller Synthesis for a fragment of
{{$$\textsf{MTL}_{0,\infty}$$}}},
publisher =           {Springer-Verlag},
journal =             {Acta Informatica},
volume =              {51},
number =              {3-4},
pages =               {165-192},
year =                {2014},
month =               jun,
doi =                 {10.1007/s00236-013-0189-z},
}

[BDL+12] Peter Bulychev, Alexandre David, Kim Guldstrand Larsen, Axel Legay, Guangyuan Li, Danny Bøgsted Poulsen, and Amélie Stainer. 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] Peter Bulychev, Alexandre David, Kim Guldstrand Larsen, Axel Legay, Marius Mikučionis, and Danny Bøgsted Poulsen. Checking and Distributing Statistical Model Checking. In NFM'12, Lecture Notes in Computer Science 7226, pages 449-463. Springer-Verlag, April 2012.
@inproceedings{nasaFM2012-BDLLMP,
author =              {Bulychev, Peter and David, Alexandre and Larsen, Kim
Guldstrand and Legay, Axel and Miku{{c}}ionis,
Marius and Poulsen, Danny B{\o}gsted},
title =               {Checking and Distributing Statistical Model
Checking},
editor =              {Goodloe, Alwyn and Person, Suzette},
booktitle =           {{P}roceedings of the 4th {NASA} {F}ormal {M}ethods
{S}ymposium ({NFM}'12)},
acronym =             {{NFM}'12},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {7226},
pages =               {449-463},
year =                {2012},
month =               apr,
}

[BDL+09] Thomas Brihaye, Arnaud Da Costa, François Laroussinie, and Nicolas Markey. ATL with Strategy Contexts and Bounded Memory. In LFCS'09, Lecture Notes in Computer Science 5407, pages 92-106. Springer-Verlag, January 2009.
Abstract

We extend the alternating-time temporal logics ATL and ATL* with strategy contexts and memory constraints: the first extension make strategy quantifiers to not "forget" the strategies being executed by the other players. The second extension allows strategy quantifiers to restrict to memoryless or bounded-memory strategies.

We first consider expressiveness issues. We show that our logics can express important properties such as equilibria, and we formally compare them with other similar formalisms (ATL, ATL*, Game Logic, Strategy Logic, ...). We then address the problem of model-checking for our logics, providing a PSPACE algoritm for the sublogics involving only memoryless strategies and an EXPSPACE algorithm for the bounded-memory case.

@inproceedings{lfcs2009-BDLM,
author =              {Brihaye, {\relax Th}omas and Da{~}Costa, Arnaud and
Laroussinie, Fran{\c c}ois and Markey, Nicolas},
title =               {{ATL} with Strategy Contexts and Bounded Memory},
editor =              {Artemov, Sergei N. and Nerode, Anil},
booktitle =           {{P}roceedings of the {I}nternational {S}ymposium
{L}ogical {F}oundations of {C}omputer {S}cience
({LFCS}'09)},
acronym =             {{LFCS}'09},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {5407},
pages =               {92-106},
year =                {2009},
month =               jan,
doi =                 {10.1007/978-3-540-92687-0_7},
abstract =            {We extend the alternating-time temporal logics ATL
and ATL\textsuperscript{*} with \emph{strategy
contexts} and \emph{memory constraints}: the first
extension make strategy quantifiers to not
{"}forget{"} the strategies being executed by the
other players. The second extension allows strategy
quantifiers to restrict to memoryless or
bounded-memory strategies.\par We first consider
expressiveness issues. We show that our logics can
express important properties such as equilibria, and
we formally compare them with other similar
formalisms (ATL, ATL\textsuperscript{*}, Game Logic,
Strategy Logic,~...). We~then address the problem of
model-checking for our logics, providing a PSPACE
algoritm for the sublogics involving only memoryless
strategies and an EXPSPACE algorithm for the
bounded-memory case.},
}

[BDL+97] Joshua Berman, Arthur Drisko, François Lemieux, Cristopher Moore, and Denis Thé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] Gerd Behrmann, Alexandre David, Kim Guldstrand Larsen, Paul Pettersson, and Wang Yi. 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] Patricia Bouyer, Deepak D'Souza, Parthasarathy Madhusudan, and Antoine Petit. Timed Control with Partial Observability. In CAV'03, Lecture Notes in Computer Science 2725, pages 180-192. Springer-Verlag, July 2003.
@inproceedings{cav2003-BDMP,
author =              {Bouyer, Patricia and D'Souza, Deepak and Madhusudan,
Parthasarathy and Petit, Antoine},
title =               {Timed Control with Partial Observability},
editor =              {Hunt, Jr, Warren A. and Somenzi, Fabio},
booktitle =           {{P}roceedings of the 15th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'03)},
acronym =             {{CAV}'03},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {2725},
pages =               {180-192},
year =                {2003},
month =               jul,
}

[BDM+09] Patricia Bouyer, Marie Duflot, Nicolas Markey, and Gabriel Renault. Measuring Permissivity in Finite Games. In CONCUR'09, Lecture Notes in Computer Science 5710, pages 196-210. Springer-Verlag, September 2009.
Abstract

In this paper, we extend the classical notion of strategies in turn-based finite games by allowing several moves to be selected. We define and study a quantitative measure for permissivity of such strategies by assigning penalties when blocking transitions. We prove that for reachability objectives, most permissive strategies exist, can be chosen memoryless, and can be computed in polynomial time, while it is in NP∩coNP for discounted and mean penalties.

@inproceedings{concur2009-BDMR,
author =              {Bouyer, Patricia and Duflot, Marie and Markey,
Nicolas and Renault, Gabriel},
title =               {Measuring Permissivity in Finite Games},
editor =              {Bravetti, Mario and Zavattaro, Gianluigi},
booktitle =           {{P}roceedings of the 20th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'09)},
acronym =             {{CONCUR}'09},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {5710},
pages =               {196-210},
year =                {2009},
month =               sep,
doi =                 {10.1007/978-3-642-04081-8_14},
abstract =            {In this paper, we extend the classical notion of
strategies in turn-based finite games by allowing
several moves to be selected. We~define and study a
quantitative measure for permissivity of such
strategies by assigning penalties when blocking
transitions. We~prove that for reachability
objectives, most permissive strategies exist, can be
chosen memoryless, and can be computed in polynomial
time, while it is in
$$\textsf{NP}\cap\textsf{coNP}$$ for discounted and
mean penalties.},
}

[BDR03] Véronique Bruyère, Emmanuel Dall'Olio, and Jean-François Raskin. 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
title =               {Durations, Parametric Model Checking in Timed
Automata with {P}resburger Arithmetic},
editor =              {Alt, Helmut and Habib, Michel},
booktitle =           {{P}roceedings of the 20th {S}ymposium on
{T}heoretical {A}spects of {C}omputer {S}cience
({STACS}'03)},
acronym =             {{STACS}'03},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {2607},
pages =               {687-698},
year =                {2003},
month =               feb,
}

[BDS+09] Hans Bherer, Jules Desharnais, and Richard St-Denis. Control of Parameterized Discrete Event Systems. Discrete Event Dynamic Systems 19(2):213-165. Kluwer Academic, June 2009.
@article{deds19(2)-BDSD,
author =              {Bherer, Hans and Desharnais, Jules and St-Denis,
Richard},
title =               {Control of Parameterized Discrete Event Systems},
journal =             {Discrete Event Dynamic Systems},
volume =              {19},
number =              {2},
pages =               {213-165},
year =                {2009},
month =               jun,
doi =                 {10.1007/s10626-008-0040-9},
}

[Bea03] Danièle Beauquier. On probabilistic timed automata. Theoretical Computer Science 292(1):65-84. Elsevier, January 2003.
@article{tcs292(1)-Bea,
author =              {Beauquier, Dani{\e}le},
title =               {On~probabilistic timed automata},
publisher =           {Elsevier},
journal =             {Theoretical Computer Science},
volume =              {292},
number =              {1},
pages =               {65-84},
year =                {2003},
month =               jan,
doi =                 {10.1016/S0304-3975(01)00215-8},
}

[Bed01] Nicolas Bedon. 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},
journal =             {Journal of Computer and System Sciences},
volume =              {63},
number =              {3},
pages =               {394-431},
year =                {2001},
month =               nov,
}

[BEG+15] Endre Boros, Khaled Elbassioni, Vladimir Gurvich, and Kazuhisa Makino. Markov Decision Processes and Stochastic Games with Total Effective Payoff. In STACS'15, Leibniz International Proceedings in Informatics 30, pages 103-115. Leibniz-Zentrum für Informatik, March 2015.
@inproceedings{stacs2015-BEGM,
author =              {Boros, Endre and Elbassioni, Khaled and Gurvich,
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] Richard Beigel. 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},
}

[Bel57] Richard Bellman. Dynamic Programming. Princeton University, 1957.
@book{DP-Bel,
author =              {Bellman, Richard},
title =               {Dynamic Programming},
publisher =           {Princeton University},
year =                {1957},
}

[Bel58] Richard Bellman. On a Routing Problem. Quarterly of Applied Mathematics 16(1):87-90. 1958.
@article{qam16(1)-Bel,
author =              {Bellman, Richard},
title =               {On a Routing Problem},
journal =             {Quarterly of Applied Mathematics},
volume =              {16},
number =              {1},
pages =               {87-90},
year =                {1958},
}

[BEM96] Julian C. Bradfield, Javier Esparza, and Angelika Mader. 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,
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érard Berry. The foundations of Esterel. In Gordon D. Plotkin, Colin Stirling, and Mads Tofte (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,
booktitle =           {Proof, Language, and Interaction~-- Essays in Honour
of {R}obin {M}ilner},
publisher =           {MIT Press},
pages =               {425-454},
year =                {2000},
}

[Bey01] Dirk Beyer. 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] Patricia Bouyer and Vojtěch Forejt. Reachability in Stochastic Timed Games. In ICALP'09, Lecture Notes in Computer Science 5556, pages 103-114. Springer-Verlag, July 2009.
@inproceedings{icalp2009-BF,
author =              {Bouyer, Patricia and Forejt, Vojt{{e}}ch},
title =               {Reachability in Stochastic Timed Games},
editor =              {Albers, Susanne and Marchetti{-}Spaccamela Alberto
and Matias, Yossi and Nikoletseas, Sotiris and
Thomas, Wolfgang},
booktitle =           {{P}roceedings of the 36th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'09)~-- Part~{II}},
acronym =             {{ICALP}'09},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {5556},
pages =               {103-114},
year =                {2009},
month =               jul,
}

[BFD02] Alexander Bolotov, Michael J. Fischer, and Clare Dixon. On the Relationship between ω-Automata and Temporal Logic Normal Forms. Journal of Logic and Computation 12(4):561-581. Oxford University Press, August 2002.
@article{jlc12(4)-BFD,
author =              {Bolotov, Alexander and Fischer, Michael J. and
Dixon, Clare},
title =               {On the Relationship between {$$\omega$$}-Automata
and Temporal Logic Normal Forms},
publisher =           {Oxford University Press},
journal =             {Journal of Logic and Computation},
volume =              {12},
number =              {4},
pages =               {561-581},
year =                {2002},
month =               aug,
}

[BFH09] Felix Brandt, Felix Fischer, and Markus Holzer. Symmetries and the complexity of pure Nash equilibrium. Journal of Computer and System Sciences 75(3):163-177. Elsevier, May 2009.
@article{jcss75(3)-BFH,
author =              {Brandt, Felix and Fischer, Felix and Holzer, Markus},
title =               {Symmetries and the complexity of pure {N}ash
equilibrium},
publisher =           {Elsevier},
journal =             {Journal of Computer and System Sciences},
volume =              {75},
number =              {3},
pages =               {163-177},
year =                {2009},
month =               may,
}

[BFH+03] Albert Benveniste, Éric Fabre, Stefan Haar, and Claude Jard. 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] Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim Guldstrand Larsen, Paul Pettersson, and Judi Romijn. Efficient Guiding Towards Cost-Optimality in UPPAAL. In TACAS'01, Lecture Notes in Computer Science 2031, pages 174-188. Springer-Verlag, April 2001.
@inproceedings{tacas2001-BFHLPR,
author =              {Behrmann, Gerd and Fehnker, Ansgar and Hune, Thomas
and Larsen, Kim Guldstrand and Pettersson, Paul and
Romijn, Judi},
title =               {Efficient Guiding Towards Cost-Optimality in UPPAAL},
editor =              {Margaria, Tiziana and Yi, Wang},
booktitle =           {{P}roceedings of the 7th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'01)},
acronym =             {{TACAS}'01},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {2031},
pages =               {174-188},
year =                {2001},
month =               apr,
}

[BFH+01] Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim Guldstrand Larsen, Paul Pettersson, Judi Romijn, and Frits Vaandrager. Minimum-Cost Reachability for Priced Timed Automata. In HSCC'01, Lecture Notes in Computer Science 2034, pages 147-161. Springer-Verlag, March 2001.
@inproceedings{hscc2001-BFHLPRV,
author =              {Behrmann, Gerd and Fehnker, Ansgar and Hune, Thomas
and Larsen, Kim Guldstrand and Pettersson, Paul and
Romijn, Judi and Vaandrager, Frits},
title =               {Minimum-Cost Reachability for Priced Timed Automata},
editor =              {Di{~}Benedetto, Maria Domenica and
Sangiovani{-}Vincentelli, Alberto L.},
booktitle =           {{P}roceedings of the 4th {I}nternational {W}orkshop
on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
({HSCC}'01)},
acronym =             {{HSCC}'01},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {2034},
pages =               {147-161},
year =                {2001},
month =               mar,
doi =                 {10.1007/3-540-45351-2_15},
}

[BFL+10] Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, and Nicolas Markey. Timed Automata with Observers under Energy Constraints. In HSCC'10, pages 61-70. ACM Press, April 2010.
Abstract

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).},
}

[BFL+11] Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, and Nicolas Markey. Quantitative analysis of real-time systems using priced timed automata. Communications of the ACM 54(9):78-87. ACM Press, September 2011.
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.

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

[BFL+18] Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, Joël Ouaknine, and James Worrell. Model Checking Real-Time Systems. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (eds.), Handbook of Model Checking. Springer-Verlag, May 2018.
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).

@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).},
}

[BFL+08] Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, and Jiří Srba. Infinite Runs in Weighted Timed Automata with Energy Constraints. In FORMATS'08, Lecture Notes in Computer Science 5215, pages 33-47. Springer-Verlag, September 2008.
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 (e.g. energy). We ask the question whether there exists an infinite path for which the accumulated weight for any finite prefix satisfies certain constraints (e.g. remains between 0 and some given upper-bound). We also consider a game version of the above, where certain transitions may be uncontrollable.

@inproceedings{formats2008-BFLMS,
author =              {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim
Guldstrand and Markey, Nicolas and Srba, Ji{
r}{\'\i}},
title =               {Infinite Runs in Weighted Timed Automata with Energy
Constraints},
editor =              {Cassez, Franck and Jard, Claude},
booktitle =           {{P}roceedings of the 6th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'08)},
acronym =             {{FORMATS}'08},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {5215},
pages =               {33-47},
year =                {2008},
month =               sep,
doi =                 {10.1007/978-3-540-85778-5_4},
abstract =            {We~study the problems of existence and construction
of infinite schedules for finite weighted automata
and one-clock weighted timed automata, subject to
boundary constraints on the accumulated weight. More
specifically, we~consider automata equipped with
positive and negative weights on transitions and
locations, corresponding to the production and
consumption of some resource (\emph{e.g.}~energy).
We~ask the question whether there exists an infinite
path for which the accumulated weight for any finite
prefix satisfies certain constraints
(\emph{e.g.}~remains between~$$0$$ and some given
upper-bound). We~also consider a game version of the
above, where certain transitions may be
uncontrollable.},
}

[BFM15] Patricia Bouyer, Erwin Fang, and Nicolas Markey. Permissive strategies in timed automata and games. In AVOCS'15, Electronic Communications of the EASST 72. European Association of Software Science and Technology, September 2015.
Abstract

Timed automata are a convenient framework for modelling and reasoning about real-time systems. While these models are now very well-understood, they do not offer a convenient way of taking timing imprecisions into account. Several solutions (e.g. parametric guard enlargement) have recently been proposed over the last ten years to take such imprecisions into account. In this paper, we propose a new approach for handling robust reachability, based on permissive strategies. While classical strategies propose to play an action at an exact point in time, permissive strategies return an interval of possible dates when to play the selected action. With such a permissive strategy, we associate a penalty, which is the inverse of the length of the proposed interval, and accumulates along the run. We show that in that setting, optimal strategies can be computed in polynomial time for one-clock timed automata.

@inproceedings{avocs2015-BFM,
author =              {Bouyer, Patricia and Fang, Erwin and Markey,
Nicolas},
title =               {Permissive strategies in timed automata and games},
editor =              {Grov, Gudmund and Ireland, Andrew},
booktitle =           {{P}roceedings of the 15th {I}nternational {W}orkshop
on {A}utomated {V}erification of {C}ritical
{S}ystems ({AVOCS}'15)},
acronym =             {{AVOCS}'15},
publisher =           {European Association of Software Science and
Technology},
series =              {Electronic Communications of the EASST},
volume =              {72},
year =                {2015},
month =               sep,
doi =                 {10.14279/tuj.eceasst.72.1015},
abstract =            {Timed automata are a convenient framework for
modelling and reasoning about real-time systems.
While these models are now very well-understood,
they do not offer a convenient way of taking timing
imprecisions into account. Several solutions (e.g.
parametric guard enlargement) have recently been
proposed over the last ten years to take such
imprecisions into account. In this paper, we propose
a new approach for handling robust reachability,
based on permissive strategies. While classical
strategies propose to play an action at an exact
point in time, permissive strategies return an
interval of possible dates when to play the selected
action. With such a permissive strategy, we
associate a penalty, which is the inverse of the
length of the proposed interval, and accumulates
along the run. We show that in that setting, optimal
strategies can be computed in polynomial time for
one-clock timed automata.},
}

[BFP+73] Manuel Blum, Robert W. Floyd, Vaughan R. Pratt, Ronald L. Rivest, and Robert Endre Tarjan. 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},
journal =             {Journal of Computer and System Sciences},
volume =              {7},
number =              {4},
pages =               {448-461},
year =                {1973},
month =               aug,
}

[BFS14] Nathalie Bertrand, Paulin Fournier, and Arnaud Sangnier. Playing with Probabilities in Reconfigurable Broadcast Networks. In FoSSaCS'14, Lecture Notes in Computer Science 8412, pages 134-148. Springer-Verlag, April 2014.
@inproceedings{fossacs2014-BFS,
author =              {Bertrand, Nathalie and Fournier, Paulin and
Sangnier, Arnaud},
title =               {Playing with Probabilities in Reconfigurable
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] Nathalie Bertrand, Paulin Fournier, and Arnaud Sangnier. 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 Yuri Gurevich. The Decision Problem for Linear Temporal Logic. Notre Dame Journal of Formal Logic 26(2):115-128. April 1985.
@article{ndjfl26(2)-BG,
author =              {Burgess,John P. and Gurevich, Yuri},
title =               {The Decision Problem for Linear Temporal Logic},
journal =             {Notre Dame Journal of Formal Logic},
volume =              {26},
number =              {2},
pages =               {115-128},
year =                {1985},
month =               apr,
}

[BG93] Orna Bernholtz and Orna Grumberg. Branching Time Temporal Logic and A m o r p H O u s Tree Automata. In CONCUR'93, Lecture Notes in Computer Science 715, pages 262-277. Springer-Verlag, August 1993.
@inproceedings{concur1993-BG,
author =              {Bernholtz, Orna and Grumberg, Orna},
title =               {Branching Time Temporal Logic and {{$$\mathcal{A} \textup{m} \textbf{o} r \textsc{p} \mathcal{H} \texttt{O} u \textbf{s}$$}} Tree Automata},
editor =              {Best, Eike},
booktitle =           {{P}roceedings of the 4th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'93)},
acronym =             {{CONCUR}'93},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {715},
pages =               {262-277},
year =                {1993},
month =               aug,
}

[BG99] Glenn Bruns and Patrice Godefroid. 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] Glenn Bruns and Patrice Godefroid. 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] Robert Baumgartner and Georg Gottlob. 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égis Barbanchon and Étienne Grandjean. 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] Dietmar Berwanger and Erich Grä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] Dietmar Berwanger and Erich Grädel. Entanglement –-mdash; A Measure for the Complexity of Directed Graphs with Applications to Logic and Games. In LPAR'04, Lecture Notes in Computer Science 3452, pages 209-223. Springer-Verlag, March 2005.
@inproceedings{lpar2004-BG,
author =              {Berwanger, Dietmar and Gr{\"a}del, Erich},
title =               {Entanglement~--- {A} Measure for the Complexity of
Directed Graphs with Applications to Logic and
Games},
editor =              {Baader, Franz and Voronkov, Andrei},
booktitle =           {{P}roceedings of the 11th {I}nternational
{C}onference {L}ogic {P}rogramming and {A}utomated
{R}easoning ({LPAR}'04)},
acronym =             {{LPAR}'04},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {3452},
pages =               {209-223},
year =                {2005},
month =               mar,
}

[BG13] Nils Bulling and Valentin Goranko. 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
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},
}

[BGH13] Olivier Bournez, Daniel S. Graça, and Emmanuel Hainry. Computation with perturbed dynamical systems. Journal of Computer and System Sciences 79(5):714-724. Elsevier, August 2013.
@article{jcss79(5)-BGH,
author =              {Bournez, Olivier and Gra{\c c}a, Daniel S. and
Hainry, Emmanuel},
title =               {Computation with perturbed dynamical systems},
publisher =           {Elsevier},
journal =             {Journal of Computer and System Sciences},
volume =              {79},
number =              {5},
pages =               {714-724},
year =                {2013},
month =               aug,
}

[BGH+09] Roderick Bloem, Karin Greimel, Thomas A. Henzinger, and Barbara Jobstmann. 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
publisher =           {IEEE Comp. Soc. Press},
pages =               {85-92},
year =                {2009},
month =               nov,
}

[BGH+15] Thomas Brihaye, Gilles Geeraerts, Axel Haddad, Engel Lefaucheux, and Benjamin Monmege. 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
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] Thomas Brihaye, Gilles Geeraerts, Axel Haddad, and Benjamin Monmege. 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
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] Boaz Barak, Oded Goldreich, Rusell Impagliazzo, Steven Rudich, Amit Sahai, Salil Vadhan, and Ke Yang. 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
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] Boaz Barak, Oded Goldreich, Rusell Impagliazzo, Steven Rudich, Amit Sahai, Salil Vadhan, and Ke Yang. 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
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] Johan Bengtsson, W. O. David Griffioen, Kåre J. Kristoffersen, Kim Guldstrand Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. 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
and Yi, Wang},
title =               {Verification of an Audio Protocol with Bus Collision
Using {\scshape {U}ppaal}},
editor =              {Alur, Rajeev and Henzinger, Thomas A.},
booktitle =           {{P}roceedings of the 8th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'96)},
acronym =             {{CAV}'96},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {1102},
pages =               {244-256},
year =                {1996},
month =               jul,
}

[BGM14] Patricia Bouyer, Patrick Gardy, and Nicolas Markey. Quantitative verification of weighted Kripke structures. In ATVA'14, Lecture Notes in Computer Science 8837, pages 64-80. Springer-Verlag, November 2014.
Abstract

Extending formal verification techniques to handle quantitative aspects, both for the models and for the properties to be checked, has become a central research topic over the last twenty years. Following several recent works, we study model checking for (one-dimensional) weighted Kripke structures with positive and negative weights, and temporal logics constraining the total and/or average weight. We prove decidability when only accumulated weight is constrained, while allowing average-weight constraints alone already is undecidable.

@inproceedings{atva2014-BGM,
author =              {Bouyer, Patricia and Gardy, Patrick and Markey,
Nicolas},
title =               {Quantitative verification of weighted {K}ripke
structures},
editor =              {Cassez, Franck and Raskin, Jean-Fran{\c c}ois},
booktitle =           {{P}roceedings of the 12th {I}nternational
{S}ymposium on {A}utomated {T}echnology for
{V}erification and {A}nalysis ({ATVA}'14)},
acronym =             {{ATVA}'14},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {8837},
pages =               {64-80},
year =                {2014},
month =               nov,
doi =                 {10.1007/978-3-319-11936-6_6},
abstract =            {Extending formal verification techniques to handle
quantitative aspects, both for the models and for
the properties to be checked, has become a central
research topic over the last twenty years. Following
several recent works, we study model checking for
(one-dimensional) weighted Kripke structures with
positive and negative weights, and temporal logics
constraining the total and/or average weight. We
prove decidability when only accumulated weight is
constrained, while allowing average-weight
}

[BGM15] Patricia Bouyer, Patrick Gardy, and Nicolas Markey. Weighted strategy logic with boolean goals over one-counter games. In FSTTCS'15, Leibniz International Proceedings in Informatics 45, pages 69-83. Leibniz-Zentrum für Informatik, December 2015.
Abstract

Strategy Logic is a powerful specification language for expressing non-zero-sum properties of multi-player games. SL conveniently extends the logic ATL with explicit quantification and assignment of strategies. In this paper, we consider games over one-counter automata, and a quantitative extension 1cSL of SL with assertions over the value of the counter. We prove two results: we first show that, if decidable, model checking the so-called Boolean-goal fragment of 1cSL has non-elementary complexity; we actually prove the result for the Boolean-goal fragment of SL over finite-state games, which was an open question in (Mogavero et al. Reasoning about strategies: On the model-checking problem. 2014). As a first step towards proving decidability, we then show that the Boolean-goal fragment of 1cSL over one-counter games enjoys a nice periodicity property.

@inproceedings{fsttcs2015-BGM,
author =              {Bouyer, Patricia and Gardy, Patrick and Markey,
Nicolas},
title =               {Weighted strategy logic with boolean goals over
one-counter games},
editor =              {Harsha, Prahladh and Ramalingam, G.},
booktitle =           {{P}roceedings of the 35th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience ({FSTTCS}'15)},
acronym =             {{FSTTCS}'15},
publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
series =              {Leibniz International Proceedings in Informatics},
volume =              {45},
pages =               {69-83},
year =                {2015},
month =               dec,
doi =                 {10.4230/LIPIcs.FSTTCS.2015.69},
abstract =            {Strategy Logic is a powerful specification language
for expressing non-zero-sum properties of
multi-player games. SL conveniently extends the
logic ATL with explicit quantification and
assignment of strategies. In this paper, we consider
games over one-counter automata, and a quantitative
extension 1cSL of SL with assertions over the value
of the counter. We prove two results: we first show
that, if decidable, model checking the so-called
Boolean-goal fragment of 1cSL has non-elementary
complexity; we actually prove the result for the
Boolean-goal fragment of SL over finite-state games,
which was an open question in (Mogavero
\emph{et~al.} Reasoning about strategies: On the
model-checking problem. 2014). As a first step
towards proving decidability, we then show that the
Boolean-goal fragment of 1cSL over one-counter games
enjoys a nice periodicity property.},
}

[BGM16] Patricia Bouyer, Patrick Gardy, and Nicolas Markey. On the semantics of Strategy Logic. Information Processing Letters 116(2):75-79. Elsevier, February 2016.
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.

@article{ipl116(2)-BGM,
author =              {Bouyer, Patricia and Gardy, Patrick and Markey,
Nicolas},
title =               {On the semantics of Strategy Logic},
publisher =           {Elsevier},
journal =             {Information Processing Letters},
volume =              {116},
number =              {2},
pages =               {75-79},
year =                {2016},
month =               feb,
doi =                 {10.1016/j.ipl.2015.10.004},
abstract =            {We define and study a slight variation on the
semantics of Strategy Logic: while in the classical
semantics, all strategies are shifted during the
evaluation of temporal modalities, we propose to
only shift the strategies that have been assigned to
a player, thus matching the intuition that we can
assign the very same strategy to the players at
different points in time. We prove that
surprisingly, this renders the model-checking
problem undecidable.},
}

[BGM+08] Thomas Brihaye, Mohamed Ghannem, Nicolas Markey, and Lionel Rieg. Good friends are hard to find!. In TIME'08, pages 32-40. IEEE Comp. Soc. Press, June 2008.
Abstract

We focus on the problem of finding (the size of) a minimal winning coalition in a multi-player game. More precisely, we prove that deciding whether there is a winning coalition of size at most k is NP-complete, while deciding whether k is the optimal size is DP-complete. We also study different variants of our original problem: the function problem, where the aim is to effectively compute the coalition; more succinct encoding of the game; and richer families of winning objectives.

@inproceedings{time2008-BGMR,
author =              {Brihaye, {\relax Th}omas and Ghannem, Mohamed and
Markey, Nicolas and Rieg, Lionel},
title =               {Good friends are hard to find!},
booktitle =           {{P}roceedings of the 15th {I}nternational
{S}ymposium on {T}emporal {R}epresentation and
{R}easoning ({TIME}'08)},
acronym =             {{TIME}'08},
publisher =           {IEEE Comp. Soc. Press},
pages =               {32-40},
year =                {2008},
month =               jun,
doi =                 {10.1109/TIME.2008.10},
abstract =            {We focus on the problem of finding (the~size of)
a~minimal winning coalition in a multi-player game.
More precisely, we~prove that deciding whether there
is a winning coalition of size at most~$$k$$ is
NP-complete, while deciding whether $$k$$ is the
optimal size is DP-complete. We~also study different
variants of our original problem: the function
problem, where the aim is to effectively compute the
coalition; more succinct encoding of the game; and
richer families of winning objectives.},
}

[BGM+18] Damien Busatto-Gaston, Benjamin Monmege, and Pierre-Alain Reynier. Symbolic Approximation of Weighted Timed Games. In FSTTCS'18, Leibniz International Proceedings in Informatics, pages 28:1-28:16. Leibniz-Zentrum für Informatik, December 2018.
@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},
pages =               {28:1-28:16},
year =                {2018},
month =               dec,
doi =                 {10.4230/LIPIcs.FSTTCS.2018.28},
}

[BGM+18] Patricia Bouyer, Mauricio González, Nicolas Markey, and Mickael Randour. Multi-weighted Markov Decision Processes with Reachability Objectives. In GandALF'18, Electronic Proceedings in Theoretical Computer Science 277, pages 250-264. September 2018.
Abstract

In this paper, we are interested in the synthesis of schedulers in double-weighted Markov decision processes, which satisfy both a percentile constraint over a weighted reachability condition, and a quantitative constraint on the expected value of a random variable defined using a weighted reachability condition. This problem is inspired by the modelization of an electric-vehicle charging problem. We study the cartography of the problem, when one parameter varies, and show how a partial cartography can be obtained via two sequences of opimization problems. We discuss completeness and feasability of the method.

@inproceedings{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.},
}

[BGN+14] Thomas Brihaye, Gilles Geeraerts, Shankara Narayanan Krishna, Lakshmi Manasa, Benjamin Monmege, and Ashutosh Trivedi. Adding negative prices to priced timed games. In CONCUR'14, Lecture Notes in Computer Science 8704, pages 560-575. Springer-Verlag, September 2014.
@inproceedings{concur2014-BGKMMT,
author =              {Brihaye, {\relax Th}omas and Geeraerts, Gilles and
Narayanan Krishna, Shankara and Manasa, Lakshmi and
Monmege, Benjamin and Trivedi, Ashutosh},
title =               {Adding negative prices to priced timed games},
editor =              {Baldan, Paolo and Gorla, Daniele},
booktitle =           {{P}roceedings of the 25th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'14)},
acronym =             {{CONCUR}'14},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {8704},
pages =               {560-575},
year =                {2014},
month =               sep,
doi =                 {10.1007/978-3-662-44584-6_38},
}

[BGP96] Béatrice Bérard, Paul Gastin, and Antoine Petit. Timed Automata with non Observable Actions: Expressive power and refinement. In STACS'96, Lecture Notes in Computer Science 1046, pages 257-268. Springer-Verlag, February 1996.
@inproceedings{stacs1996-BGP,
author =              {B{\'e}rard, B{\'e}atrice and Gastin, Paul and Petit,
Antoine},
title =               {Timed Automata with non Observable Actions:
Expressive power and refinement},
editor =              {Puech, Claude and Reischuk, R{\"u}diger},
booktitle =           {{P}roceedings of the 13th {S}ymposium on
{T}heoretical {A}spects of {C}omputer {S}cience
({STACS}'96)},
acronym =             {{STACS}'96},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {1046},
pages =               {257-268},
year =                {1996},
month =               feb,
}

[BGS92] José Balcázar, Joaquim Gabarró, and Miklós Sántha. Deciding bisimilarity is P-complete. Formal Aspects of Computing 4(1 supplement):638-648. Springer-Verlag, November 1992.
@article{fac4(1sup)-BGSC,
author =              {Balc{\'a}zar, Jos{\'e} and Gabarr{\'o}, Joaquim and
S{\'a}ntha, Mikl{\'o}s},
title =               {Deciding bisimilarity is {P}-complete},
publisher =           {Springer-Verlag},
journal =             {Formal Aspects of Computing},
volume =              {4},
number =              {1 supplement},
pages =               {638-648},
year =                {1992},
month =               nov,
}

[BGS14] Benedikt Bollig, Paul Gastin, and Jana Schubert. 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] Nikita Borisov, Ian Goldberg, 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] Manuel Blum and Carl Hewitt. 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] Anne Bergeron and Sylvie Hamel. From Cascade Decompositions to Bit-Vector Algotithms. Theoretical Computer Science 313(1):3-16. Elsevier, February 2004.
@article{tcs313(1)-BH,
author =              {Bergeron, Anne and Hamel, Sylvie},
title =               {From Cascade Decompositions to Bit-Vector
Algotithms},
publisher =           {Elsevier},
journal =             {Theoretical Computer Science},
volume =              {313},
number =              {1},
pages =               {3-16},
year =                {2004},
month =               feb,
}

[BH05] Dragan Bosnacki 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
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] Bernard Boigelot and Frédéric Herbreteau. 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},
}

[Bhe09] Hans Bherer. Controller Synthesis for Parameterized Discrete Event Systems. PhD thesis, Université Laval, Québec, Canada, 2009.
@phdthesis{bherer09,
author =              {Bherer, Hans},
title =               {Controller Synthesis for Parameterized Discrete
Event Systems},
year =                {2009},
school =              {Universit{\'e} Laval, Qu\'ebec, Canada},
}

[BHJ03] Bernard Boigelot, Frédéric Herbreteau, and Sébastien Jodogne. 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] Bernard Boigelot, Frédéric Herbreteau, and Sébastien Jodogne. Hybrid Acceleration using Real Vector Automata. Technical Report 2003.18, Centre Fédéré en Vérification, Bruxelles, Belgium, 2003.
@techreport{TR-cfv0318,
author =              {Boigelot, Bernard and Herbreteau, Fr{\'e}d{\'e}ric
and Jodogne, S{\'e}bastien},
title =               {Hybrid Acceleration using Real Vector Automata},
number =              {2003.18},
year =                {2003},
institution =         {Centre F\'ed\'er\'e en V\'erification, Bruxelles,
Belgium},
type =                {Technical Report},
}

[BHK00] Steven Bradley, William Henderson, and David Kendall. Using Timed Automata for Response Time Analysis and Distributer Real-Time Systems. In WRTP'99, pages 143-148. Pergamon Press, January 2000.
@inproceedings{wrtp1999-BHK,
author =              {Bradley, Steven and Henderson, William and Kendall,
David},
title =               {Using Timed Automata for Response Time Analysis and
Distributer Real-Time Systems},
editor =              {Frigeri, Alceu Heinke and Halang, Wolfgang A. and
Son, Sang H.},
booktitle =           {{P}roceedings of the 24th {IFAC}/{IFIP} {W}orkshop
on {R}eal-{T}ime {P}rogramming ({WRTP}'99)},
acronym =             {{WRTP}'99},
publisher =           {Pergamon Press},
pages =               {143-148},
year =                {2000},
month =               jan,
confyear =            {1999},
confmonth =           {5},
}

[BHL14] Nathalie Bertrand, Serge Haddad, and Engel Lefaucheux. Foundation of Diagnosis and Predictability in Probabilistic Systems. In FSTTCS'14, Leibniz International Proceedings in Informatics 29, pages 417-429. Leibniz-Zentrum für Informatik, December 2014.
@inproceedings{fsttcs2014-BHL,
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},
}

[BHM08] Aske Wiid Brekling, Michael R. Hansen, and Jan Madsen. 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
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] Bernard Boigelot, Frédéric Herbreteau, and Isabelle Mainz. 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éatrice Bérard, Loïc Hélouët, and John Mullins. 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},
}

[BHM+17] Patricia Bouyer, Piotr Hofman, Nicolas Markey, Mickael Randour, and Martin Zimmermann. Bounding Average-energy Games. In FoSSaCS'17, Lecture Notes in Computer Science 10203, pages 179-195. Springer-Verlag, April 2017.
Abstract

We consider average-energy games, where the goal is to minimize the long-run average of the accumulated energy. Decidability of average-energy games with a lower-bound constraint on the energy level (but no upper bound) is an open problem; in particular, there is no known upper bound on the memory that is required for winning strategies.

By reducing average-energy games with lower-bounded energy to infinite-state mean-payoff games and analyzing the frequency of low-energy configurations, we show an almost tight doubly-exponential upper bound on the necessary memory, and that the winner of average-energy games with lower-bounded energy can be determined in doubly-exponential time. We also prove EXPSPACE-hardness of this problem.

Finally, we consider multi-dimensional extensions of all types of average-energy games: without bounds, with only a lower bound, and with both a lower and an upper bound on the energy. We show that the fully-bounded version is the only case to remain decidable in multiple dimensions.

@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] Thomas Brihaye, Thomas A. Henzinger, Vinayak S. Prabhu, and Jean-François Raskin. 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] Patricia Bouyer, Serge Haddad, and Pierre-Alain Reynier. 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,
Pierre-Alain},
title =               {Timed Unfoldings for Networks of Timed Automata},
editor =              {Graf, Susanne and Zhang, Wenhui},
booktitle =           {{P}roceedings of the 4th {I}nternational {S}ymposium
on {A}utomated {T}echnology for {V}erification and
{A}nalysis ({ATVA}'06)},
acronym =             {{ATVA}'06},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {4218},
pages =               {292-306},
year =                {2006},
month =               oct,
doi =                 {10.1007/11901914_23},
}

[BHR09] Patricia Bouyer, Serge Haddad, and Pierre-Alain Reynier. Undecidability Results for Timed Automata with Silent Transitions. Fundamenta Informaticae 92(1-2):1-25. IOS Press, 2009.
@article{fundi92(1-2)-BHR,
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èle Beauquier, Yoram Hirshfeld, Alexander Rabinovich, and Anatol Slissenko. 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] Dirk Beyer, Thomas A. Henzinger, and Grégory Thé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] Marius Bozga, Radu Iosif, and Yassine Lakhnech. 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] Marius Bozga, Radu Iosif, and Yassine Lakhnech. 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,
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. Mix Barrington, Neil Immerman, and Howard Straubing. 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$$}}},
journal =             {Journal of Computer and System Sciences},
volume =              {41},
number =              {3},
pages =               {274-306},
year =                {1990},
month =               dec,
}

[BJ10] Nils Bulling and Wojciech Jamroga. Model Checking Agents with Memory Is Harder than It Seemed. In AAMAS'10, pages 633-640. International Foundation for Autonomous Agents and Multiagent Systems, May 2010.
@inproceedings{aamas2010-BJ,
author =              {Bulling, Nils and Jamroga, Wojciech},
title =               {Model Checking Agents with Memory Is Harder than It
Seemed},
editor =              {van der Hoek, Wiebe and Kaminka, Gal A. and
Lesp{\'e}rance, Yves and Luck, Michael and Sen,
Sandeep},
booktitle =           {{P}roceedings of the 9th {I}nternational
{C}onference on {A}utonomous {A}gents and
{M}ultiagent {S}ystems ({AAMAS}'10)},
acronym =             {{AAMAS}'10},
publisher =           {International Foundation for Autonomous Agents and
Multiagent Systems},
pages =               {633-640},
year =                {2010},
month =               may,
}

[BJK10] Tomáš Brázdil, Petr Jančar, and Antonín Kučera. Reachability Games on Extended Vector Addition Systems with States. In ICALP'10, Lecture Notes in Computer Science 6199, pages 478-489. Springer-Verlag, July 2010.
@inproceedings{icalp2010-BJK,
author =              {Br{\'a}zdil, Tom{\'a}{ s} and Jan{ c}ar, Petr
and Ku{ c}era, Anton{\'\i}n},
title =               {Reachability Games on Extended Vector Addition
Systems with States},
editor =              {Abramsky, Samson and Gavoille, Cyril and Kirchner,
Claude and Meyer auf der Heide, Friedhelm and
Spirakis, Paul G.},
booktitle =           {{P}roceedings of the 37th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'10)~-- Part~{II}},
acronym =             {{ICALP}'10},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {6199},
pages =               {478-489},
year =                {2010},
month =               jul,
doi =                 {10.1007/978-3-642-14162-1_40},
}

[BJK+05] Manfred Broy, Bengt Jonsson, Joost-Pieter Katoen, Martin Leucker, and Alexander Pretschner. Model-Based Testing of Reactive Systems – Advanced lectures. Lecture Notes in Computer Science 3472. Springer-Verlag, 2005.
@book{mbt-bjklp,
author =              {Broy, Manfred and Jonsson, Bengt and Katoen,
Joost-Pieter and Leucker, Martin and Pretschner,
Alexander},
title =               {Model-Based Testing of Reactive Systems~-- Advanced
lectures},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {3472},
year =                {2005},
}

[BJL+10] Thomas Brihaye, Marc Jungers, Samson Lasaulce, Nicolas Markey, and Ghassan Oreiby. Using Model Checking for Analyzing Distributed Power Control Problems. EURASIP Journal on Wireless Communications and Networking 2010(861472). Hindawi Publishing Corp., June 2010.
Abstract

Model checking (MC) is a formal verification technique which has been known and still knows a resounding success in the computer science community. Realizing that the distributed power control (PC) problem can be modeled by a timed game between a given transmitter and its environment, the authors wanted to know whether this approach can be applied to distributed PC. It turns out that it can be applied successfully and allows one to analyze realistic scenarios including the case of discrete transmit powers and games with incomplete information. The proposed methodology is as follows. We state some objectives a transmitter-receiver pair would like to reach. The network is modeled by a game where transmitters are considered as timed automata interacting with each other. The objectives are then translated into timed alternating-time temporal logic formulae and MC is exploited to know whether the desired properties are verified and determine a winning strategy.

@article{jwcn2010(861472)-BJLMO,
author =              {Brihaye, {\relax Th}omas and Jungers, Marc and
Lasaulce, Samson and Markey, Nicolas and Oreiby,
Ghassan},
title =               {Using Model Checking for Analyzing Distributed Power
Control Problems},
publisher =           {Hindawi Publishing Corp.},
journal =             {EURASIP Journal on Wireless Communications and
Networking},
volume =              {2010},
number =              {861472},
year =                {2010},
month =               jun,
doi =                 {10.1155/2010/861472},
abstract =            {Model checking~(MC) is a formal verification
technique which has been known and still knows a
resounding success in the computer science
community. Realizing that the distributed power
control~(PC) problem can be modeled by a timed game
between a given transmitter and its environment, the
authors wanted to know whether this approach can be
applied to distributed~PC. It~turns out that it can
be applied successfully and allows one to analyze
realistic scenarios including the case of discrete
transmit powers and games with incomplete
information. The proposed methodology is as follows.
We state some objectives a transmitter-receiver pair
would like to reach. The network is modeled by a
game where transmitters are considered as timed
automata interacting with each other. The objectives
are then translated into timed alternating-time
temporal logic formulae and MC is exploited to know
whether the desired properties are verified and
determine a winning strategy.},
}

[BJL+98] Johan Bengtsson, Bengt Jonsson, Johan Lilius, and Wang Yi. Partial-Order Reductions for Timed Systems. In CONCUR'98, Lecture Notes in Computer Science 1466, pages 485-500. Springer-Verlag, September 1998.
@inproceedings{concur1998-BJLY,
author =              {Bengtsson, Johan and Jonsson, Bengt and Lilius,
Johan and Yi, Wang},
title =               {Partial-Order Reductions for Timed Systems},
editor =              {Sangiorgi, Davide and de Simone, Robert},
booktitle =           {{P}roceedings of the 9th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'98)},
acronym =             {{CONCUR}'98},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {1466},
pages =               {485-500},
year =                {1998},
month =               sep,
doi =                 {10.1007/BFb0055643},
}

[BJM15] Patricia Bouyer, Samy Jaziri, and Nicolas Markey. On the Value Problem in Weighted Timed Games. In CONCUR'15, Leibniz International Proceedings in Informatics 42, pages 311-324. Leibniz-Zentrum für Informatik, September 2015.
Abstract

A weighted timed game is a timed game with extra quantitative information representing e.g. energy consumption. Optimizing the cost for reaching a target is a natural question, which has been investigated for ten years. Existence of optimal strategies is known to be undecidable in general, and only very restricted classes of games have been described for which optimal cost and almost-optimal strategies can be computed.

In this paper, we show that the value problem is undecidable in general weighted timed games. The undecidability proof relies on that for the existence of optimal strategies and on a diagonalization construction recently designed in the context of quantitative temporal logics. We then provide an algorithm to compute arbitrary approximations of the value in a game, and almost-optimal strategies. The algorithm applies in a large subclass of weighted timed games, and is the first approximation scheme which is designed in the current context.

@inproceedings{concur2015-BJM,
author =              {Bouyer, Patricia and Jaziri, Samy and Markey,
Nicolas},
title =               {On~the Value Problem in Weighted Timed Games},
editor =              {Aceto, Luca and de Frutos{-}Escrig, David},
booktitle =           {{P}roceedings of the 26th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'15)},
acronym =             {{CONCUR}'15},
publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
series =              {Leibniz International Proceedings in Informatics},
volume =              {42},
pages =               {311-324},
year =                {2015},
month =               sep,
doi =                 {10.4230/LIPIcs.CONCUR.2015.311},
abstract =            {A~weighted timed game is a timed game with extra
quantitative information representing e.g. energy
consumption. Optimizing the cost for reaching a
target is a natural question, which has been
investigated for ten years. Existence of optimal
strategies is known to be undecidable in general,
and only very restricted classes of games have been
described for which optimal cost and almost-optimal
strategies can be computed.\par In this paper, we
show that the value problem is undecidable in
general weighted timed games. The undecidability
proof relies on that for the existence of optimal
strategies and on a diagonalization construction
recently designed in the context of quantitative
temporal logics. We then provide an algorithm to
compute arbitrary approximations of the value in a
game, and almost-optimal strategies. The algorithm
applies in a large subclass of weighted timed games,
and is the first approximation scheme which is
designed in the current context.},
}

[BJM17] Patricia Bouyer, Samy Jaziri, and Nicolas Markey. On the determinization of timed systems. In FORMATS'17, Lecture Notes in Computer Science 10419, pages 25-41. Springer-Verlag, September 2017.
Abstract

We introduce a new formalism called automata over a timed domain which provides an adequate framework for the determinization of timed systems. In this formalism, determinization w.r.t. timed language is always possible at the cost of changing the timed domain. We give a condition for determinizability of automata over a timed domain without changing the timed domain, which allows us to recover several known determinizable classes of timed systems, such as strongly-non-zeno timed automata, integer-reset timed automata, perturbed timed automata, etc. Moreover in the case of timed automata this condition encompasses most determinizability conditions from the literature.

@inproceedings{formats2017-BJM,
author =              {Bouyer, Patricia and Jaziri, Samy and Markey,
Nicolas},
title =               {On the determinization of timed systems},
editor =              {Abate, Alessandro and Geeraerts, Gilles},
booktitle =           {{P}roceedings of the 15th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'17)},
acronym =             {{FORMATS}'17},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {10419},
pages =               {25-41},
year =                {2017},
month =               sep,
doi =                 {10.1007/978-3-319-65765-3 2},
abstract =            {We introduce a new formalism called \emph{automata
over a timed domain} which provides an adequate
framework for the determinization of timed systems.
In~this formalism, determinization w.r.t. timed
language is always possible at the cost of changing
the timed domain. We~give a condition for
determinizability of automata over a timed domain
without changing the timed domain, which allows us
to recover several known determinizable classes of
timed systems, such as strongly-non-zeno timed
automata, integer-reset timed automata, perturbed
timed automata, etc. Moreover in the case of timed
automata this condition encompasses most
determinizability conditions from the literature.},
}

[BJM17] Patricia Bouyer, Vincent Jugé, and Nicolas Markey. Courcelle's Theorem Made Dynamic. Technical Report 1702.05183, arXiv, February 2017.
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.

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

[BJM18] Patricia Bouyer, Samy Jaziri, and Nicolas Markey. Efficient timed diagnosis using automata with timed domains. In RV'18, Lecture Notes in Computer Science 11237, pages 205-221. Springer-Verlag, November 2018.
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].

@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] Marius Bozga, Hou Jianmin, Oded Maler, and Sergio Yovine. 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] Joakim Byg, Kenneth Yrke Jørgensen, and Jiří Srba. TAPAAL: Editor, Simulator and Verifier of Timed-Arc Petri Nets. In ATVA'09, Lecture Notes in Computer Science 5799, pages 84-89. Springer-Verlag, October 2009.
@inproceedings{atva2009-BJS,
author =              {Byg, Joakim and J{\o}rgensen, Kenneth Yrke and Srba,
Ji{ r}{\'\i}},
title =               {{TAPAAL}: Editor, Simulator and Verifier of
Timed-Arc {P}etri Nets},
editor =              {Liu, Zhiming and Ravn, Anders P.},
booktitle =           {{P}roceedings of the 7th {I}nternational {S}ymposium
on {A}utomated {T}echnology for {V}erification and
{A}nalysis ({ATVA}'09)},
acronym =             {{ATVA}'09},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {5799},
pages =               {84-89},
year =                {2009},
month =               oct,
doi =                 {10.1007/978-3-642-04761-9_7},
}

[BJS+12] Nathalie Bertrand, Thierry Jéron, Amélie Stainer, and Moez Krichen. 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] Jasper Berendsen, David N. Jansen, and Frits Vaandrager. 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] Julien Bernet, David Janin, and Igor Walukiewicz. Permissive strategies: from parity games to safety games. RAIRO – Theoretical Informatics and Applications 36(3):261-275. EDP Sciences, 2002.
@article{rairo-tia36(3)-BJW,
author =              {Bernet, Julien and Janin, David and Walukiewicz,
Igor},
title =               {Permissive strategies: from parity games to safety
games},
publisher =           {EDP Sciences},
journal =             {RAIRO~-- Theoretical Informatics and Applications},
volume =              {36},
number =              {3},
pages =               {261-275},
year =                {2002},
}

[BK08] Christel Baier and Joost-Pieter Katoen. Principles of Model-Checking. MIT Press, May 2008.
@book{PoMC2008-BK,
author =              {Baier, {\relax Ch}ristel and Katoen, Joost-Pieter},
title =               {Principles of Model-Checking},
publisher =           {MIT Press},
year =                {2008},
month =               may,
}

[BKK11] Christel Baier, Joachim Klein, and Sascha Klü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, David Klaška, Antonín Kučera, and Petr Novotný. Minimizing Running Costs in Consumption Systems. In CAV'14, Lecture Notes in Computer Science 8559, pages 457-472. Springer-Verlag, July 2014.
@inproceedings{cav2014-BKKN,
author =              {Br{\'a}zdil, Tom{\'a}{ s} and Kla{{s}}ka, David
and Ku{ c}era, Anton{\'\i}n and Novotn{\'y}, Petr},
title =               {Minimizing Running Costs in Consumption Systems},
editor =              {Biere, Armin and Bloem, Roderick},
booktitle =           {{P}roceedings of the 26th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'14)},
acronym =             {{CAV}'14},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {8559},
pages =               {457-472},
year =                {2014},
month =               jul,
}

[BKM+06] Jeremy W. Bryans, Maciej Koutny, Laurent Mazaré, 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] Thomas Bøgholm, Henrik Kargh-hansen, Petur Olsen, Bent Thomsen, and Kim Guldstrand Larsen. 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] Howard Barringer, Ruurd Kuiper, and Amir Pnueli. 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] Dietmar Berwanger, łukasz Kaiser, and Bernd Puchala. A Perfect-Information Construction for Coordination in Games. In FSTTCS'11, Leibniz International Proceedings in Informatics 13, pages 387-398. Leibniz-Zentrum für Informatik, December 2011.
@inproceedings{fsttcs2011-BKP,
author =              {Berwanger, Dietmar and Kaiser, {\L}ukasz and
Puchala, Bernd},
title =               {A~Perfect-Information Construction for Coordination
in Games},
editor =              {Chakraborty, Supratik and Kumar, Amit},
booktitle =           {{P}roceedings of the 31st {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience ({FSTTCS}'11)},
acronym =             {{FSTTCS}'11},
publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
series =              {Leibniz International Proceedings in Informatics},
volume =              {13},
pages =               {387-398},
year =                {2011},
month =               dec,
}

[BL69] Julius R. Büchi and Lawrence H. Landweber. Solving Sequential Conditions by Finite-State Strategies. Transactions of the American Mathematical Society 138:295-311. American Mathematical Society, April 1969.
@article{TAMS138-BL,
author =              {B{\"u}chi, Julius R. and Landweber, Lawrence H.},
title =               {Solving Sequential Conditions by Finite-State
Strategies},
publisher =           {American Mathematical Society},
journal =             {Transactions of the American Mathematical Society},
volume =              {138},
pages =               {295-311},
year =                {1969},
month =               apr,
}

[BL95] Ahmed Bouajjani and Yassine Lakhnech. 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łaj Bojańczyk and Sławomir Lasota. A Machine-Independent Characterization of Timed Languages. In ICALP'12, Lecture Notes in Computer Science 7392, pages 92-103. Springer-Verlag, July 2012.
@inproceedings{icalp2012-BL,
author =              {Boja{\'n}czyk, Miko{\l}aj and Lasota, S{\l}awomir},
title =               {A~Machine-Independent Characterization of Timed
Languages},
editor =              {Czumaj, Artur and Mehlhorn, Kurt and Pitts, Andrew
and Wattenhofer, Roger},
booktitle =           {{P}roceedings of the 39th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'12)~-- Part~{II}},
acronym =             {{ICALP}'12},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {7392},
pages =               {92-103},
year =                {2012},
month =               jul,
doi =                 {10.1007/978-3-642-31585-5_12},
}

[Bla00] Patrick Blackburn. Representations, Reasoning and Relational Structures: a Hybrid Logic Manifesto. Logic Journal of the IGPL 8(3):339-365. Oxford University Press, May 2000.
@article{jigpl8(3)-Bla,
author =              {Blackburn, Patrick},
title =               {Representations, Reasoning and Relational
Structures: a Hybrid Logic Manifesto},
publisher =           {Oxford University Press},
journal =             {Logic Journal of the IGPL},
volume =              {8},
number =              {3},
pages =               {339-365},
year =                {2000},
month =               may,
}

[BLM07] Patricia Bouyer, Kim Guldstrand Larsen, and Nicolas Markey. Model Checking One-clock Priced Timed Automata. In FoSSaCS'07, Lecture Notes in Computer Science 4423, pages 108-122. Springer-Verlag, March 2007.
Abstract

We consider the model of priced (a.k.a. weighted) timed automata, an extension of timed automata with cost information on both locations and transitions. We prove that model-checking this class of models against the logic WCTL, CTL with cost-constrained modalities, is PSPACE-complete under the "single-clock" assumption. In contrast, it has been recently proved that the model-checking problem is undecidable for this model as soon as the system has three clocks. We also prove that the model-checking of WCTL becomes undecidable, even under this "single-clock" assumption.

@inproceedings{fossacs2007-BLM,
author =              {Bouyer, Patricia and Larsen, Kim Guldstrand and
Markey, Nicolas},
title =               {Model Checking One-clock Priced Timed Automata},
editor =              {Seidl, Helmut},
booktitle =           {{P}roceedings of the 10th {I}nternational
{C}onference on {F}oundations of {S}oftware
{S}cience and {C}omputation {S}tructure
({FoSSaCS}'07)},
acronym =             {{FoSSaCS}'07},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {4423},
pages =               {108-122},
year =                {2007},
month =               mar,
doi =                 {10.1007/978-3-540-71389-0_9},
abstract =            {We consider the model of priced (a.k.a.~weighted)
timed automata, an extension of timed automata with
cost information on both locations and transitions.
We prove that model-checking this class of models
against the logic~WCTL, CTL~with cost-constrained
modalities, is PSPACE-complete under the
{"}single-clock{"} assumption. In~contrast, it~has
been recently proved that the model-checking problem
is undecidable for this model as soon as the system
has three clocks. We also prove that the
model-checking of~WCTL becomes undecidable, even
under this {"}single-clock{"} assumption.},
}

[BLM08] Patricia Bouyer, Kim Guldstrand Larsen, and Nicolas Markey. Model Checking One-clock Priced Timed Automata. Logical Methods in Computer Science 4(2). May 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 (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\}$$).},
}

[BLM12] Patricia Bouyer, Kim Guldstrand Larsen, and Nicolas Markey. Lower-Bound Constrained Runs in Weighted Timed Automata. In QEST'12, pages 128-137. IEEE Comp. Soc. Press, September 2012.
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 et al., "Infinite runs in weighted timed automata with energy constraints", FORMATS'08], we show that the existence of an infinite lower-bound-constrained run is–-mdash;for us somewhat unexpectedly–-mdash;undecidable for weighted timed automata with four or more clocks.

This undecidability result assumes a fixed and know initial credit. We show that the related problem of existence of an initial credit for which there ex- ist a feasible run is decidable in PSPACE. We also investigate the variant of these problems where only bounded-duration runs are considered, showing that this restriction makes our original problem decidable in NEXPTIME. Finally, we prove that the universal versions of all those problems (i.e, checking that all the considered runs satisfy the lower-bound constraint) are decidable in PSPACE.

@inproceedings{qest2012-BLM,
author =              {Bouyer, Patricia and Larsen, Kim Guldstrand and
Markey, Nicolas},
title =               {Lower-Bound Constrained Runs in Weighted Timed
Automata},
booktitle =           {{P}roceedings of the 9th {I}nternational
{C}onference on {Q}uantitative {E}valuation of
{S}ystems ({QEST}'12)},
acronym =             {{QEST}'12},
publisher =           {IEEE Comp. Soc. Press},
pages =               {128-137},
year =                {2012},
month =               sep,
doi =                 {10.1109/QEST.2012.28},
abstract =            {We investigate a number of problems related to
infinite runs of weighted timed automata, subject to
lower-bound constraints on the accumulated weight.
Closing an open problem from [Bouyer
\textit{et~al.}, {"}Infinite runs in weighted timed
automata with energy constraints{"}, FORMATS'08], we
show that the existence of an infinite
lower-bound-constrained run is---for us somewhat
unexpectedly---undecidable for weighted timed
automata with four or more clocks.\par This
undecidability result assumes a fixed and know
initial credit. We show that the related problem of
existence of an initial credit for which there ex-
ist a feasible run is decidable in PSPACE. We also
investigate the variant of these problems where only
bounded-duration runs are considered, showing that
this restriction makes our original problem
decidable in NEXPTIME. Finally, we prove that the
universal versions of all those problems (i.e,
checking that all the considered runs satisfy the
lower-bound constraint) are decidable in PSPACE.},
}

[BLM14] Patricia Bouyer, Kim Guldstrand Larsen, and Nicolas Markey. Lower-Bound Constrained Runs in Weighted Timed Automata. Performance Evaluation 73:91-109. Elsevier, March 2014.
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.

This undecidability result assumes a fixed and known initial credit. We show that the related problem of existence of an initial credit for which there exists a feasible run is decidable in PSPACE. We also investigate the variant of these problems where only bounded-duration runs are considered, showing that this restriction makes our original problem decidable in NEXPTIME. We prove that the universal versions of all those problems (i.e, checking that all the considered runs satisfy the lower-bound constraint) are decidable in PSPACE.

Finally, we extend this study to multi-weighted timed automata: the existence of a feasible run becomes undecidable even for bounded duration, but the existence of initial credits remains decidable (in PSPACE).

@article{peva73()-BLM,
author =              {Bouyer, Patricia and Larsen, Kim Guldstrand and
Markey, Nicolas},
title =               {Lower-Bound Constrained Runs in Weighted Timed
Automata},
publisher =           {Elsevier},
journal =             {Performance Evaluation},
volume =              {73},
pages =               {91-109},
year =                {2014},
month =               mar,
doi =                 {10.1016/j.peva.2013.11.002},
abstract =            {We investigate a number of problems related to
infinite runs of weighted timed automata (with a
single weight variable), subject to lower-bound
constraints on the accumulated weight. Closing an
open problem from an earlier paper, we show that the
existence of an infinite lower-bound-constrained run
is--for us somewhat unexpectedly--undecidable for
weighted timed automata with four or more
clocks.\par This undecidability result assumes a
fixed and known initial credit. We show that the
related problem of existence of an initial credit
for which there exists a feasible run is decidable
in PSPACE. We also investigate the variant of these
problems where only bounded-duration runs are
considered, showing that this restriction makes our
original problem decidable in NEXPTIME. We prove
that the universal versions of all those problems
(i.e, checking that all the considered runs satisfy
the lower-bound constraint) are decidable in
PSPACE.\par Finally, we extend this study to
multi-weighted timed automata: the existence of a
feasible run becomes undecidable even for bounded
duration, but the existence of initial credits
remains decidable (in~PSPACE).},
}

[BLM+07] Thomas Brihaye, François Laroussinie, Nicolas Markey, and Ghassan Oreiby. Timed Concurrent Game Structures. In CONCUR'07, Lecture Notes in Computer Science 4703, pages 445-459. Springer-Verlag, September 2007.
Abstract

We propose a new model for timed games, based on concurrent game structures (CGSs). Compared to the classical timed game automata of Asarin et al., our timed CGSs are "more concurrent", in the sense that they always allow all the agents to act on the system, independently of the delay they want to elapse before their action. Timed CGSs weaken the "element of surprise" of timed game automata reported by de Alfaro et al.

We prove that our model has nice properties, in particular that model-checking timed CGSs against timed ATL is decidable via region abstraction, and in particular that strategies are "region-stable" if winning objectives are. We also propose a new extension of TATL, containing ATL*, which we call TALTL. We prove that model-checking this logic remains decidable on timed CGSs. Last, we explain how our algorithms can be adapted in order to rule out Zeno (co-)strategies, based on the ideas of Henzinger et al.

@inproceedings{concur2007-BLMO,
author =              {Brihaye, {\relax Th}omas and Laroussinie, Fran{\c
c}ois and Markey, Nicolas and Oreiby, Ghassan},
title =               {Timed Concurrent Game Structures},
editor =              {Caires, Lu{\'\i}s and Vasconcelos, Vasco T.},
booktitle =           {{P}roceedings of the 18th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'07)},
acronym =             {{CONCUR}'07},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {4703},
pages =               {445-459},
year =                {2007},
month =               sep,
doi =                 {10.1007/978-3-540-74407-8_30},
abstract =            {We propose a new model for timed games, based on
concurrent game structures~(CGSs). Compared to the
classical \emph{timed game automata} of~Asarin
\emph{et~al.}, our timed~CGSs are {"}more
concurrent{"}, in the sense that they always allow
all the agents to act on the system, independently
of the delay they want to elapse before their
action. Timed CGSs weaken the {"}element of
surprise{"} of timed game automata reported by
de~Alfaro \emph{et~al.}\par We prove that our model
has nice properties, in particular that
model-checking timed CGSs against timed
$$\textsf{ATL}$$ is decidable \emph{via} region
abstraction, and in particular that strategies are
{"}region-stable{"} if winning objectives are. We
also propose a new extension of $$\textsf{TATL}$$,
containing~$$\textsf{ATL}^{*}$$, which we
call~$$\textsf{TALTL}$$. We~prove that
model-checking this logic remains decidable on timed
CGSs. Last, we explain how our algorithms can be
adapted in order to rule out Zeno (co-)strategies,
based on the ideas of Henzinger \emph{et~al.}},
}

[BLM+17] Patricia Bouyer, François Laroussinie, Nicolas Markey, Joël Ouaknine, and James Worrell. Timed temporal logics. In Luca Aceto, Giorgio Bacci, Giovanni Bacci, Anna Ingólfsdóttir, Axel Legay, and Radu Mardare (eds.), Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday, Lecture Notes in Computer Science 10460, pages 211-230. Springer-Verlag, August 2017.
Abstract

Since the early 1990's, classical temporal logics have been extended with timing constraints. While temporal logics only express contraints on the order of events, their timed extensions can add quantitative constraints on delays between those events. We survey expressiveness and algorithmic results on those logics, and discuss semantic choices that may look unimportant but do have an impact on the questions we consider.

@incollection{kimfest2017-BLMOW,
author =              {Bouyer, Patricia and Laroussinie, Fran{\c c}ois and
Markey, Nicolas and Ouaknine, Jo{\"e}l and Worrell,
James},
title =               {Timed temporal logics},
editor =              {Aceto, Luca and Bacci, Giorgio and Bacci, Giovanni
and Ing{\'o}lfsd{\'o}ttir, Anna and Legay, Axel and
booktitle =           {Models, Algorithms, Logics and Tools: Essays
Dedicated to Kim Guldstrand Larsen on the Occasion
of His 60th Birthday},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {10460},
pages =               {211-230},
year =                {2017},
month =               aug,
doi =                 {10.1007/978-3-319-65764-6_11},
abstract =            {Since the early 1990's, classical temporal logics
have been extended with timing constraints. While
temporal logics only express contraints on the order
of events, their timed extensions can add
quantitative constraints on delays between those
events. We survey expressiveness and algorithmic
results on those logics, and discuss semantic
choices that may look unimportant but do have an
impact on the questions we consider.},
}

[BLM+06] Patricia Bouyer, Kim Guldstrand Larsen, Nicolas Markey, and Jacob Illum Rasmussen. Almost Optimal Strategies in One-Clock Priced Timed Automata. In FSTTCS'06, Lecture Notes in Computer Science 4337, pages 345-356. Springer-Verlag, December 2006.
Abstract

We consider timed games extended with cost information, and prove computability of the optimal cost and of ε-optimal memoryless strategies in timed games with one clock. In contrast, this problem has recently been proved undecidable for timed games with three clocks.

@inproceedings{fsttcs2006-BLMR,
author =              {Bouyer, Patricia and Larsen, Kim Guldstrand and
Markey, Nicolas and Rasmussen, Jacob Illum},
title =               {Almost Optimal Strategies in One-Clock Priced Timed
Automata},
editor =              {Arun-Kumar, S. and Garg, Naveen},
booktitle =           {{P}roceedings of the 26th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience ({FSTTCS}'06)},
acronym =             {{FSTTCS}'06},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {4337},
pages =               {345-356},
year =                {2006},
month =               dec,
doi =                 {10.1007/11944836_32},
abstract =            {We consider timed games extended with cost
information, and prove computability of the optimal
cost and of $$\epsilon$$-optimal memoryless
strategies in timed games with one~clock.
In~contrast, this problem has recently been proved
undecidable for timed games with three clocks.},
}

[BLM+97] David A. Mix Barrington, Chi-Jen Lu, Peter Bro Miltersen, and Sven Skyum. On Uniformity Within NC1. Research Report 97-044, Electronic Colloquium on Computational Complexity, September 1997.
@techreport{eccc1997-BLMS,
author =              {Barrington, David A. Mix and Lu, Chi-Jen and
Miltersen, Peter Bro and Skyum, Sven},
title =               {On Uniformity Within {{$$\mathit{NC}^1$$}}},
number =              {97-044},
year =                {1997},
month =               sep,
institution =         {Electronic Colloquium on Computational Complexity},
type =                {Research Report},
}

[BLM+11] Patricia Bouyer, Kim Guldstrand Larsen, Nicolas Markey, Ocan Sankur, and Claus Thrane. Timed automata can always be made implementable. In CONCUR'11, Lecture Notes in Computer Science 6901, pages 76-91. Springer-Verlag, September 2011.
Abstract

Timed automata follow a mathematical semantics, which assumes perfect precision and synchrony of clocks. Since this hypothesis does not hold in digital systems, properties proven formally on a timed automaton may be lost at implementation. In order to ensure implementability, several approaches have been considered, corresponding to different hypotheses on the implementation platform. We address two of these: a timed automaton is samplable if its semantics is preserved under a discretization of time; it is robust if its semantics is preserved when all timing constraints are relaxed by some small positive parameter. We propose a construction which makes timed automata implementable in the above sense: From any timed automaton A, we build a timed automaton A' that exhibits the same behaviour as A, and moreover is both robust and samplable by construction.

@inproceedings{concur2011-BLMST,
author =              {Bouyer, Patricia and Larsen, Kim Guldstrand and
Markey, Nicolas and Sankur, Ocan and Thrane, Claus},
title =               {Timed automata can always be made implementable},
editor =              {Katoen, Joost-Pieter and K{\"o}nig, Barbara},
booktitle =           {{P}roceedings of the 22nd {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'11)},
acronym =             {{CONCUR}'11},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {6901},
pages =               {76-91},
year =                {2011},
month =               sep,
doi =                 {10.1007/978-3-642-23217-6_6},
abstract =            {Timed automata follow a mathematical semantics,
which assumes perfect precision and synchrony of
clocks. Since this hypothesis does not hold in
digital systems, properties proven formally on a
timed automaton may be lost at implementation. In
order to ensure implementability, several approaches
have been considered, corresponding to different
hypotheses on the implementation platform. We
address two of these: a~timed automaton is samplable
if its semantics is preserved under a discretization
of time; it is robust if its semantics is preserved
when all timing constraints are relaxed by some
small positive parameter. We propose a construction
which makes timed automata implementable in the
above sense: From any timed
automaton~$$\mathcal{A}$$, we build a timed
automaton~$$\mathcal{A}'$$ that exhibits the same
behaviour as~$$\mathcal{A}$$, and moreover is both
robust and samplable by construction.},
}

[BLN03] Dirk Beyer, Claus Lewerentz, and Andreas Noack. 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] Johannes Blö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
}

[BLP03] Gerd Behrmann, Kim Guldstrand Larsen, and Radek Pelá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
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] Gerd Behrmann, Kim Guldstrand Larsen, Justin Pearson, Carsten Weise, and Wang Yi. 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] Gerd Behrmann, Kim Guldstrand Larsen, Justin Pearson, Carsten Weise, and Wang Yi. 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] Patricia Bouyer, François Laroussinie, and Pierre-Alain Reynier. Diagonal Constraints in Timed Automata: Forward Analysis of Timed Systems. In FORMATS'05, Lecture Notes in Computer Science 3829, pages 112-126. Springer-Verlag, September 2005.
@inproceedings{formats2005-BLR,
author =              {Bouyer, Patricia and Laroussinie, Fran{\c c}ois and
Reynier, Pierre-Alain},
title =               {Diagonal Constraints in Timed Automata: Forward
Analysis of Timed Systems},
editor =              {Pettersson, Paul and Yi, Wang},
booktitle =           {{P}roceedings of the 3rd {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'05)},
acronym =             {{FORMATS}'05},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {3829},
pages =               {112-126},
year =                {2005},
month =               sep,
doi =                 {10.1007/11603009_10},
}

[BLR05] Gerd Behrmann, Kim Guldstrand Larsen, and Jacob Illum Rasmussen. Optimal scheduling using priced timed automata. SIGMETRICS Performance Evaluation Review 32(4):34-40. March 2005.
@article{SIGper32(4)-BLR,
author =              {Behrmann, Gerd and Larsen, Kim Guldstrand and
Rasmussen, Jacob Illum},
title =               {Optimal scheduling using priced timed automata},
journal =             {SIGMETRICS Performance Evaluation Review},
volume =              {32},
number =              {4},
pages =               {34-40},
year =                {2005},
month =               mar,
}

[BLW01] Benedikt Bollig, Martin Leucker, and Michael Weber. 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] Bernard Berthomieu and Miguel Menasche. 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] Ed Brinksma and Angelika Mader. Verification and Optimization of a PLC Control Schedule. In SPIN'00, Lecture Notes in Computer Science 1885, pages 73-92. Springer-Verlag, August 2000.
@inproceedings{spin2000-BM,
author =              {Brinksma, Ed and Mader, Angelika},
title =               {Verification and Optimization of a {PLC} Control
Schedule},
editor =              {Havelund, Klaus and Penix, John and Viser, Willem},
booktitle =           {{P}roceedings of the 7th {I}nternational {SPIN}
{W}orkshop ({SPIN}'00)},
acronym =             {{SPIN}'00},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {1885},
pages =               {73-92},
year =                {2000},
month =               aug,
}

[BM07] Patricia Bouyer and Nicolas Markey. Costs are Expensive!. In FORMATS'07, Lecture Notes in Computer Science 4763, pages 53-68. Springer-Verlag, October 2007.
Abstract

We study the model-checking problem for WMTL, a cost-extension of the linear-time timed temporal logic MTL, that is interpreted over weighted timed automata. We draw a complete picture of the decidability for that problem: it is decidable only for the class of one-clock weighted timed automata with a restricted stopwatch cost, and any slight extension of this model leads to undecidability. We finally give some consequences on the undecidability of linear hybrid automata.

@inproceedings{formats2007-BM,
author =              {Bouyer, Patricia and Markey, Nicolas},
title =               {Costs are Expensive!},
editor =              {Raskin, Jean-Fran{\c c}ois and Thiagarajan, P. S.},
booktitle =           {{P}roceedings of the 5th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'07)},
acronym =             {{FORMATS}'07},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {4763},
pages =               {53-68},
year =                {2007},
month =               oct,
doi =                 {10.1007/978-3-540-75454-1_6},
abstract =            {We study the model-checking problem for WMTL,
a~cost-extension of the linear-time timed temporal
logic MTL, that is interpreted over weighted timed
automata. We~draw a complete picture of the
decidability for that problem: it~is decidable only
for the class of one-clock weighted timed automata
with a restricted stopwatch cost, and any slight
extension of this model leads to undecidability.
We~finally give some consequences on the
undecidability of linear hybrid automata.},
}

[BMF02] Ed Brinksma, Angelika Mader, and Ansgar Fehnker. 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] Patricia Bouyer, Nicolas Markey, and Raj Mohan Matteplackel. Averaging in LTL. In CONCUR'14, Lecture Notes in Computer Science 8704, pages 266-280. Springer-Verlag, September 2014.
Abstract

For the accurate analysis of computerized systems, powerful quantitative formalisms have been designed, together with efficient verification algorithms. However, verification has mostly remained boolean–-mdash;either a property is true, or it is false. We believe that this is too crude in a context where quantitative information and constraints are crucial: correctness should be quantified!

In a recent line of works, several authors have proposed quantitative semantics for temporal logics, using e.g. discounting modalities (which give less importance to distant events). In the present paper, we define and study a quantitative semantics of LTL with averaging modalities, either on the long run or within an until modality. This, in a way, relaxes the classical Boolean semantics of LTL, and provides a measure of certain properties of a model. We prove that computing and even approximating the value of a formula in this logic is undecidable.

@inproceedings{concur2014-BMM,
author =              {Bouyer, Patricia and Markey, Nicolas and
Matteplackel, Raj~Mohan},
title =               {Averaging in~{LTL}},
editor =              {Baldan, Paolo and Gorla, Daniele},
booktitle =           {{P}roceedings of the 25th {I}nternational
{C}onference on {C}oncurrency {T}heory
({CONCUR}'14)},
acronym =             {{CONCUR}'14},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {8704},
pages =               {266-280},
year =                {2014},
month =               sep,
doi =                 {10.1007/978-3-662-44584-6_19},
abstract =            {For the accurate analysis of computerized systems,
powerful quantitative formalisms have been designed,
together with efficient verification algorithms.
However, verification has mostly remained
boolean---either a property is~true, or it~is false.
We~believe that this is too crude in a context where
quantitative information and constraints are
crucial: correctness should be quantified!\par In a
recent line of works, several authors have proposed
quantitative semantics for temporal logics, using
e.g. \emph{discounting} modalities (which give less
importance to distant events). In~the present paper,
we define and study a quantitative semantics of~LTL
with \emph{averaging} modalities, either on the long
run or within an until modality. This, in a way,
relaxes the classical Boolean semantics of~LTL, and
provides a measure of certain properties of a model.
We~prove that computing and even approximating the
value of a formula in this logic is undecidable.},
}

[BMM+00] Jean-Camille Birget, Stuart W. Margolis, John C. Meakin, and Pascal Weil. 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,
}

[BMO+08] Patricia Bouyer, Nicolas Markey, Joël Ouaknine, Philippe Schnoebelen, and James Worrell. On Termination for Faulty Channel Machines. In STACS'08, Leibniz International Proceedings in Informatics 1, pages 121-132. Leibniz-Zentrum für Informatik, February 2008.
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 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
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.},
}

[BMO+12] Patricia Bouyer, Nicolas Markey, Joël Ouaknine, Philippe Schnoebelen, and James Worrell. On Termination and Invariance for Faulty Channel Systems. Formal Aspects of Computing 24(4-6):595-607. Springer-Verlag, July 2012.
Abstract

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
channel and write messages to the tail of a channel.
In this paper we focus on channel machines with
\emph{insertion errors}, i.e., machines in whose
channels messages can spontaneously appear. We
consider the invariance problem: does a given
insertion channel machine have an infinite
computation all of whose configurations satisfy a
given predicate? We show that this problem is
primitive-recursive if the predicate is closed under
message losses. We also give a non-elementary lower
bound for the invariance problem under this
restriction. Finally, using the previous result, we
show that the satisfiability problem for the safety
fragment of Metric Temporal Logic is
non-elementary.},
}

[BMO+11] Patricia Bouyer, Nicolas Markey, Jörg Olschewski, and Michael Ummels. Measuring Permissiveness in Parity Games: Mean-Payoff Parity Games Revisited. In ATVA'11, Lecture Notes in Computer Science 6996, pages 135-149. Springer-Verlag, October 2011.
Abstract

We study nondeterministic strategies in parity games with the aim of computing a most permissive winning strategy. Following earlier work, we measure permissiveness in terms of the average number/weight of transitions blocked by a strategy. Using a translation into mean-payoff parity games, we prove that deciding (the permissiveness of) a most permissive winning strategy is in NP∩coNP. Along the way, we provide a new study of mean-payoff parity games. In particular, we give a new algorithm for solving these games, which beats all previously known algorithms for this problem.

@inproceedings{atva2011-BMOU,
author =              {Bouyer, Patricia and Markey, Nicolas and Olschewski,
J{\"o}rg and Ummels, Michael},
title =               {Measuring Permissiveness in Parity Games:
Mean-Payoff Parity Games Revisited},
editor =              {Bultan, Tevfik and Hsiung, Pao-Ann},
booktitle =           {{P}roceedings of the 9th {I}nternational {S}ymposium
on {A}utomated {T}echnology for {V}erification and
{A}nalysis ({ATVA}'11)},
acronym =             {{ATVA}'11},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {6996},
pages =               {135-149},
year =                {2011},
month =               oct,
doi =                 {10.1007/978-3-642-24372-1_11},
abstract =            {We study nondeterministic strategies in parity games
with the aim of computing a most permissive winning
strategy. Following earlier work, we measure
permissiveness in terms of the average
number{\slash}weight of transitions blocked by a
strategy. Using a translation into mean-payoff
parity games, we prove that deciding (the
permissiveness~of) a~most permissive winning
strategy is in $$\textsf{NP}\cap\textsf{coNP}$$.
Along the way, we~provide a new study of mean-payoff
parity games. In particular, we give a new algorithm
for solving these games, which beats all previously
known algorithms for this problem.},
}

[BMO+07] Patricia Bouyer, Nicolas Markey, Joël Ouaknine, and James Worrell. The Cost of Punctuality. In LICS'07, pages 109-118. IEEE Comp. Soc. Press, July 2007.
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.

Until recently, it was widely believed that admitting even the simplest punctual specifications in any linear-time temporal logic would automatically lead to undecidability. Although this was recently disproved, until now no punctual fragment of MTL was known to have even primitive recursive complexity (with certain decidable fragments having provably non-primitive recursive complexity).

In this paper we identify a co-flat' subset of MTL that is capable of expressing a large class of punctual specifications and for which model checking (although not satisfiability) has no complexity cost over MITL. Our logic is moreover qualitatively different from MITL in that it can express properties that are not timed-regular. Correspondingly, our decision procedures do not involve translating formulas into finite-state automata, but rather into certain kinds of reversal-bounded Turing machines. Using this translation we show that the model checking problem for our logic is EXPSPACE-Complete, and is even PSPACE-Complete if timing constraints are encoded in unary.

@inproceedings{lics2007-BMOW,
author =              {Bouyer, Patricia and Markey, Nicolas and Ouaknine,
Jo{\"e}l and Worrell, James},
title =               {The Cost of Punctuality},
booktitle =           {{P}roceedings of the 22nd {A}nnual {S}ymposium on
{L}ogic in {C}omputer {S}cience ({LICS}'07)},
acronym =             {{LICS}'07},
publisher =           {IEEE Comp. Soc. Press},
pages =               {109-118},
year =                {2007},
month =               jul,
doi =                 {10.1109/LICS.2007.49},
abstract =            {In an influential paper titled {"}The Benefits of
Relaxing Punctuality{"}, Alur, Feder, and~Henzinger
introduced Metric Interval Temporal Logic~(MITL) as
a fragment of the real-time logic Metric Temporal
Logic~(MTL) in which exact or punctual timing
constraints are banned. Their main result showed
that model checking and satisfiability for~MITL are
both EXPSPACE-Complete.\par Until recently, it was
widely believed that admitting even the simplest
punctual specifications in any linear-time temporal
logic would automatically lead to undecidability.
Although this was recently disproved, until now no
punctual fragment of~MTL was known to have even
primitive recursive complexity (with certain
decidable fragments having provably non-primitive
recursive complexity).\par In this paper we identify
a co-flat' subset of~MTL that is capable of
expressing a large class of punctual specifications
and for which model checking (although not
satisfiability) has no complexity cost over~MITL.
Our logic is moreover qualitatively different
from~MITL in that it can express properties that are
not timed-regular. Correspondingly, our decision
procedures do not involve translating formulas into
finite-state automata, but rather into certain kinds
of reversal-bounded Turing machines. Using this
translation we show that the model checking problem
for our logic is EXPSPACE-Complete, and is even
PSPACE-Complete if timing constraints are encoded in
unary.},
}

[BMO+08] Patricia Bouyer, Nicolas Markey, Joël Ouaknine, and James Worrell. On Expressiveness and Complexity in Real-time Model Checking. In ICALP'08, Lecture Notes in Computer Science 5126, pages 124-135. Springer-Verlag, July 2008.
Abstract

Metric Interval Temporal Logic (MITL) is a popular formalism for expressing real-time specifications. This logic achieves decidability by restricting the precision of timing constraints, in particular, by banning so-called punctual specifications. In this paper we introduce a significantly more expressive logic that can express a wide variety of punctual specifications, but whose model-checking problem has the same complexity as that of MITL. We conclude that for model checking the most commonly occurring specifications, such as invariance and bounded response, punctuality can be accommodated at no cost.

@inproceedings{icalp2008-BMOW,
author =              {Bouyer, Patricia and Markey, Nicolas and Ouaknine,
Jo{\"e}l and Worrell, James},
title =               {On Expressiveness and Complexity in Real-time Model
Checking},
editor =              {Aceto, Luca and Damg{\aa}rd, Ivan and Goldberg,
Leslie Ann and Halld{\'o}rsson, Magn{\'u}s M. and
Ing{\'o}lfsd{\'o}ttir, Anna and Walukiewicz, Igor},
booktitle =           {{P}roceedings of the 35th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'08)~-- Part~{II}},
acronym =             {{ICALP}'08},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {5126},
pages =               {124-135},
year =                {2008},
month =               jul,
doi =                 {10.1007/978-3-540-70583-3_11},
abstract =            {Metric Interval Temporal Logic (MITL) is a popular
formalism for expressing real-time specifications.
This logic achieves decidability by restricting the
precision of timing constraints, in particular, by
banning so-called \emph{punctual} specifications.
In~this paper we~introduce a significantly more
expressive logic that can express a wide variety of
punctual specifications, but whose model-checking
problem has the same complexity as that of~MITL.
We~conclude that for model checking the most
commonly occurring specifications, such as
invariance and bounded response, punctuality can be
accommodated at no cost.},
}

[BMP10] Laura Bozzelli, Aniello Murano, and Adriano Peron. 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,
title =               {Pushdown module checking},
publisher =           {Springer-Verlag},
journal =             {Formal Methods in System Design},
volume =              {36},
number =              {1},
pages =               {65-95},
year =                {2010},
month =               feb,
}

[BMP+15] Patricia Bouyer, Nicolas Markey, Nicolas Perrin, and Philipp Schlehuber-Caissier. Timed automata abstraction of switched dynamical systems using control funnels. In FORMATS'15, Lecture Notes in Computer Science 9268, pages 60-75. Springer-Verlag, September 2015.
Abstract

The development of formal methods for control design is an important challenge with potential applications in a wide range of safety-critical cyber-physical systems. Focusing on switched dynamical systems, we propose a new abstraction, based on time-varying regions of invariance (the control funnels), that models behaviors of systems as timed automata. The main advantage of this method is that it allows automated verification of formal specifications and reactive controller synthesis without discretizing the evolution of the state of the system. Efficient constructions are possible in the case of linear dynamics. We demonstrate the potential of our approach with two examples.

@inproceedings{formats2015-BMPS,
author =              {Bouyer, Patricia and Markey, Nicolas and Perrin,
Nicolas and Schlehuber{-}Caissier, Philipp},
title =               {Timed automata abstraction of switched dynamical
systems using control funnels},
editor =              {Sankaranarayanan, Sriram and Vicario, Enrico},
booktitle =           {{P}roceedings of the 13th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'15)},
acronym =             {{FORMATS}'15},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {9268},
pages =               {60-75},
year =                {2015},
month =               sep,
doi =                 {10.1007/978-3-319-22975-1_5},
abstract =            {The~development of formal methods for control design
is an important challenge with potential
applications in a wide range of safety-critical
cyber-physical systems. Focusing on switched
dynamical systems, we~propose a new abstraction,
based on time-varying regions of invariance
(the~\emph{control funnels}), that models behaviors
of systems as timed automata. The main advantage of
this method is that it allows automated verification
of formal specifications and reactive controller
synthesis without discretizing the evolution of the
state of the system. Efficient constructions are
possible in the case of linear dynamics.
We~demonstrate the potential of our approach with
two examples.},
}

[BMP+17] Patricia Bouyer, Nicolas Markey, Nicolas Perrin, and Philipp Schlehuber-Caissier. Timed automata abstraction of switched dynamical systems using control funnels. Real-Time Systems 53(3):327-353. Kluwer Academic, May 2017.
Abstract

The development of formal methods for control design is an important challenge with potential applications in a wide range of safety-critical cyber-physical systems. Focusing on switched dynamical systems, we propose a new abstraction, based on time-varying regions of invariance (control funnels), that models behaviors of systems as timed automata. The main advantage of this method is that it allows for the automated verification and reactive controller synthesis without discretizing the evolution of the state of the system. Efficient and analytic constructions are possible in the case of linear dynamics whereas bounding funnels with conjectured properties based on numerical simulations can be used for general nonlinear dynamics. We demonstrate the potential of our approach with three examples.

@article{rts53(3)-BMPS,
author =              {Bouyer, Patricia and Markey, Nicolas and Perrin,
Nicolas and Schlehuber{-}Caissier, Philipp},
title =               {Timed automata abstraction of switched dynamical
systems using control funnels},
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] Martin Beaudry, Pierre McKenzie, Pierre Péladeau, and Denis Thé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
title =               {Finite Monoids: From Word to Circuit Evaluation},
publisher =           {Society for Industrial and Applied Math.},
journal =             {SIAM Journal on Computing},
volume =              {26},
number =              {1},
pages =               {138-152},
year =                {1997},
month =               feb,
}

[BMR06] Patricia Bouyer, Nicolas Markey, and Pierre-Alain Reynier. Robust Model-Checking of Linear-Time Properties in Timed Automata. In LATIN'06, Lecture Notes in Computer Science 3887, pages 238-249. Springer-Verlag, March 2006.
Abstract

Formal verification of timed systems is well understood, but their implementation is still challenging. Recent works by Raskin et al. have brought out a model of parameterized timed automata that can be used to prove implementability of timed systems for safety properties. We define here a more general notion of robust model-checking for linear-time properties, which consists in verifying whether a property still holds even if the transitions are slightly delayed or expedited. We provide PSPACE algorithms for the robust model-checking of Büchi-like and LTL properties. We also verify bounded-response-time properties.

@inproceedings{latin2006-BMR,
author =              {Bouyer, Patricia and Markey, Nicolas and Reynier,
Pierre-Alain},
title =               {Robust Model-Checking of Linear-Time Properties in
Timed Automata},
editor =              {Correa, Jos{\'e} R. and Hevia, Alejandro and Kiwi,
Marcos},
booktitle =           {{P}roceedings of the 7th {L}atin {A}merican
{S}ymposium on {T}heoretical {IN}formatics
({LATIN}'06)},
acronym =             {{LATIN}'06},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {3887},
pages =               {238-249},
year =                {2006},
month =               mar,
doi =                 {10.1007/11682462_25},
abstract =            {Formal verification of timed systems is well
understood, but their \emph{implementation} is still
challenging. Recent works by Raskin \emph{et al.}
have brought out a model of parameterized timed
automata that can be used to prove
\emph{implementability} of timed systems for safety
properties. We define here a more general notion of
robust model-checking for linear-time properties,
which consists in verifying whether a property still
holds even if the transitions are slightly delayed
or expedited. We provide PSPACE algorithms for the
robust model-checking of B{\"u}chi-like and LTL
properties. We also verify bounded-response-time
properties.},
}

[BMR08] Patricia Bouyer, Nicolas Markey, and Pierre-Alain Reynier. Robust Analysis of Timed Automata via Channel Machines. In FoSSaCS'08, Lecture Notes in Computer Science 4962, pages 157-171. Springer-Verlag, March 2008.
Abstract

Whereas formal verification of timed systems has become a very active field of research, the idealised mathematical semantics of timed automata cannot be faithfully implemented. Several works have thus focused on a modified semantics of timed automata which ensures implementability, and robust model-checking algorithms for safety, and later LTL properties have been designed. Recently, a new approach has been proposed, which reduces (standard) model-checking of timed automata to other verification problems on channel machines. Thanks to a new encoding of the modified semantics as a network of timed systems, we propose an original combination of both approaches, and prove that robust model-checking for coFlat-MTL, a large fragment of MTL, is EXPSPACE-Complete.

@inproceedings{fossacs2008-BMR,
author =              {Bouyer, Patricia and Markey, Nicolas and Reynier,
Pierre-Alain},
title =               {Robust Analysis of Timed Automata via Channel
Machines},
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éronique Bruyère, Noëmie Meunier, and Jean-François Raskin. Secure Equilibria in Weighted Games. In CSL/ LICS'14. ACM Press, July 2014.
@inproceedings{csllics2014-BMR,
author =              {Bruy{\e}re, V{\'e}ronique and Meunier, No{\"e}mie
title =               {Secure Equilibria in Weighted Games},
booktitle =           {{P}roceedings of the Joint Meeting of the 23rd
{EACSL} {A}nnual {C}onference on {C}omputer
{S}cience {L}ogic and the 29th {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer
{S}cience ({CSL\slash LICS}'14)},
acronym =             {{CSL\slash LICS}'14},
publisher =           {ACM Press},
chapter =             {26},
year =                {2014},
month =               jul,
doi =                 {10.1145/2603088.2603109},
}

[BMR+15] Patricia Bouyer, Nicolas Markey, Mickael Randour, Kim Guldstrand Larsen, and Simon Laursen. Average-energy games. In GandALF'15, Electronic Proceedings in Theoretical Computer Science 193, pages 1-15. September 2015.
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 NPcoNP 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.},
}

[BMR+18] Patricia Bouyer, Nicolas Markey, Mickael Randour, Kim Guldstrand Larsen, and Simon Laursen. Average-energy games. Acta Informatica 55(2). Springer-Verlag, March 2018.
Abstract

Two-player quantitative zero-sum games provide a natural framework to synthesize controllers with performance guarantees for reactive systems within an uncontrollable environment. Classical settings include mean-payoff games, where the objective is to optimize the long-run average gain per action, and energy games, where the system has to avoid running out of energy. We study average-energy games, where the goal is to optimize the long-run average of the accumulated energy. We show that this objective arises naturally in several applications, and that it yields interesting connections with previous concepts in the literature. We prove that deciding the winner in such games is in NP∩coNP and at least as hard as solving mean-payoff games, and we establish that memoryless strategies suffice to win. We also consider the case where the system has to minimize the average-energy while maintaining the accumulated energy within predefined bounds at all times: this corresponds to operating with a finite-capacity storage for energy. We give results for one-player and two-player games, and establish complexity bounds and memory requirements.

@article{acta55(2)-BMRLL,
author =              {Bouyer, Patricia and Markey, Nicolas and Randour,
Mickael and Larsen, Kim Guldstrand and Laursen,
Simon},
title =               {Average-energy games},
publisher =           {Springer-Verlag},
journal =             {Acta Informatica},
volume =              {55},
number =              {2},
year =                {2018},
month =               mar,
doi =                 {10.1007/s00236-016-0274-1},
abstract =            {Two-player quantitative zero-sum games provide a
natural framework to synthesize controllers with
performance guarantees for reactive systems within
an uncontrollable environment. Classical settings
include mean-payoff games, where the objective is to
optimize the long-run average gain per action, and
energy games, where the system has to avoid running
out of energy. We study average-energy games, where
the goal is to optimize the long-run average of the
accumulated energy. We show that this objective
arises naturally in several applications, and that
it yields interesting connections with previous
concepts in the literature. We prove that deciding
the winner in such games is in
$$\textsf{NP}\cap\textsf{coNP}$$ and at least as
hard as solving mean-payoff games, and we establish
that memoryless strategies suffice to win. We also
consider the case where the system has to minimize
the average-energy while maintaining the accumulated
energy within predefined bounds at all times: this
corresponds to operating with a finite-capacity
storage for energy. We give results for one-player
and two-player games, and establish complexity
bounds and memory requirements.},
}

[BMR+16] Patricia Bouyer, Nicolas Markey, Mickael Randour, Arnaud Sangnier, and Daniel Stan. Reachability in Networks of Register Protocols under Stochastic Schedulers. In ICALP'16, Leibniz International Proceedings in Informatics 55, pages 106:1-106:14. Leibniz-Zentrum für Informatik, July 2016.
Abstract

We study the almost-sure reachability problem in a distributed system obtained as the asynchronous composition of N copies (called processes) of the same automaton (called protocol), that can communicate via a shared register with finite domain. The automaton has two types of transitions: write-transitions update the value of the register, while read-transitions move to a new state depending on the content of the register. Non-determinism is resolved by a stochastic scheduler. Given a protocol, we focus on almost-sure reachability of a target state by one of the processes. The answer to this problem naturally depends on the number N of processes. However, we prove that our setting has a cut-off property : the answer to the almost-sure reachability problem is constant when N is large enough; we then develop an EXPSPACE algorithm deciding whether this constant answer is positive or negative.

@inproceedings{icalp2016-BMRSS,
author =              {Bouyer, Patricia and Markey, Nicolas and Randour,
Mickael and Sangnier, Arnaud and Stan, Daniel},
title =               {Reachability in Networks of Register Protocols under
Stochastic Schedulers},
editor =              {Chatzigiannakis, Ioannis and Mitzenmacher, Michael
and Rabani, Yuval and Sangiorgi, Davide},
booktitle =           {{P}roceedings of the 43rd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'16)~-- Part~{II}},
acronym =             {{ICALP}'16},
publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
series =              {Leibniz International Proceedings in Informatics},
volume =              {55},
pages =               {106:1-106:14},
year =                {2016},
month =               jul,
doi =                 {10.4230/LIPIcs.ICALP.2016.106},
abstract =            {We study the almost-sure reachability problem in a
distributed system obtained as the asynchronous
composition of~$$N$$ copies (called
\emph{processes}) of the same automaton (called
\emph{protocol}), that can communicate via a shared
register with finite domain. The automaton has two
types of transitions: write-transitions update the
value of the register, while read-transitions move
to a new state depending on the content of the
register. Non-determinism is resolved by a
stochastic scheduler. Given a protocol, we focus on
almost-sure reachability of a target state by one of
the processes. The answer to this problem naturally
depends on the number~$$N$$ of processes. However,
we prove that our setting has a cut-off property :
the answer to the almost-sure reachability problem
is constant when $$N$$ is large enough; we~then
develop an EXPSPACE algorithm deciding whether this
constant answer is positive or negative.},
}

[BMS11] Patricia Bouyer, Nicolas Markey, and Ocan Sankur. Robust Model-Checking of Timed Automata via Pumping in Channel Machines. In FORMATS'11, Lecture Notes in Computer Science 6919, pages 97-112. Springer-Verlag, September 2011.
Abstract

Timed automata are governed by a mathematical semantics which assumes perfectly continuous and precise clocks. This requirement is not satised by digital hardware on which the models are implemented. In fact, it was shown that the presence of imprecisions, however small they may be, may yield extra behaviours. Therefore correctness proven on the formal model does not imply correctness of the real system.

The problem of robust model-checking was then dened to circumvent this inconsistency. It consists in computing a bound on the imprecision under which the system will be correct.

In this work, we show that robust model-checking against ω-regular properties for timed automata can be reduced to standard model-checking of timed automata, by computing an adequate bound on the imprecision. This yields a new algorithm for robust model-checking of ω-regular properties, which is both optimal and valid for general timed automata.

@inproceedings{formats2011-BMS,
author =              {Bouyer, Patricia and Markey, Nicolas and Sankur,
Ocan},
title =               {Robust Model-Checking of Timed Automata via Pumping
in Channel Machines},
editor =              {Fahrenberg, Uli and Tripakis, Stavros},
booktitle =           {{P}roceedings of the 9th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'11)},
acronym =             {{FORMATS}'11},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {6919},
pages =               {97-112},
year =                {2011},
month =               sep,
doi =                 {10.1007/978-3-642-24310-3_8},
abstract =            {Timed automata are governed by a mathematical
semantics which assumes perfectly continuous and
precise clocks. This requirement is not satised by
digital hardware on which the models are
implemented. In~fact, it~was shown that the presence
of imprecisions, however small they may be, may
yield extra behaviours. Therefore correctness proven
on the formal model does not imply correctness of
the real system.\par The problem of robust
model-checking was then dened to circumvent this
inconsistency. It consists in computing a bound on
the imprecision under which the system will be
correct.\par In this work, we show that robust
model-checking against $$\omega$$-regular properties
for timed automata can be reduced to standard
model-checking of timed automata, by computing an
adequate bound on the imprecision. This yields a new
algorithm for robust model-checking of
$$\omega$$-regular properties, which is both optimal
and valid for general timed automata.},
}

[BMS12] Patricia Bouyer, Nicolas Markey, and Ocan Sankur. Robust reachability in timed automata: a game-based approach. In ICALP'12, Lecture Notes in Computer Science 7392, pages 128-140. Springer-Verlag, July 2012.
Abstract

Reachability checking is one of the most basic problems in verification. By solving this problem, one synthesizes a strategy that dictates the actions to be performed for ensuring that the target location is reached. In this work, we are interested in synthesizing "robust" strategies for ensuring reachability of a location in a timed automaton; with "robust", we mean that it must still ensure reachability even when the delays are perturbed by the environment. We model this perturbed semantics as a game between the controller and its environment, and solve the parameterized robust reachability problem: we show that the existence of an upper bound on the perturbations under which there is a strategy reaching a target location is EXPTIME-complete.

@inproceedings{icalp2012-BMS,
author =              {Bouyer, Patricia and Markey, Nicolas and Sankur,
Ocan},
title =               {Robust reachability in timed automata: a~game-based
approach},
editor =              {Czumaj, Artur and Mehlhorn, Kurt and Pitts, Andrew
and Wattenhofer, Roger},
booktitle =           {{P}roceedings of the 39th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'12)~-- Part~{II}},
acronym =             {{ICALP}'12},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {7392},
pages =               {128-140},
year =                {2012},
month =               jul,
doi =                 {10.1007/978-3-642-31585-5_15},
abstract =            {Reachability checking is one of the most basic
problems in verification. By solving this problem,
one synthesizes a strategy that dictates the actions
to be performed for ensuring that the target
location is reached. In this work, we are interested
in synthesizing {"}robust{"} strategies for ensuring
reachability of a location in a timed automaton;
with {"}robust{"}, we mean that it must still ensure
reachability even when the delays are perturbed by
the environment. We model this perturbed semantics
as a game between the controller and its
environment, and solve the parameterized robust
reachability problem: we show that the existence of
an upper bound on the perturbations under which
there is a strategy reaching a target location is
EXPTIME-complete.},
}

[BMS13] Patricia Bouyer, Nicolas Markey, and Ocan Sankur. Robustness in timed automata. In RP'13, Lecture Notes in Computer Science 8169, pages 1-18. Springer-Verlag, September 2013.
Abstract

In this paper we survey several approaches to the robustness of timed automata, that is, the ability of a system to resist to slight perturbations or errors. We will concentrate on robustness against timing errors which can be due to measuring errors, imprecise clocks, and unexpected runtime behaviors such as execution times that are longer or shorter than expected.

We consider the perturbation model of guard enlargement and formulate several robust verification problems that have been studied recently, including robustness analysis, robust implementation, and robust control.

@inproceedings{rp2013-BMS,
author =              {Bouyer, Patricia and Markey, Nicolas and Sankur,
Ocan},
title =               {Robustness in timed automata},
editor =              {Abdulla, Parosh Aziz and Potapov, Igor},
booktitle =           {{P}roceedings of the 7th {W}orkshop on
{R}eachability {P}roblems in {C}omputational
{M}odels ({RP}'13)},
acronym =             {{RP}'13},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {8169},
pages =               {1-18},
year =                {2013},
month =               sep,
doi =                 {10.1007/978-3-642-41036-9_1},
abstract =            {In this paper we survey several approaches to the
robustness of timed automata, that~is, the ability
of a system to resist to slight perturbations or
errors. We will concentrate on robustness against
timing errors which can be due to measuring errors,
imprecise clocks, and unexpected runtime behaviors
such as execution times that are longer or shorter
than expected.\par We consider the perturbation
model of guard enlargement and formulate several
robust verification problems that have been studied
recently, including robustness analysis, robust
implementation, and robust control.},
}

[BMS13] Patricia Bouyer, Nicolas Markey, and Ocan Sankur. Robust Weighted Timed Automata and Games. In FORMATS'13, Lecture Notes in Computer Science 8053, pages 31-46. Springer-Verlag, August 2013.
Abstract

Weighted timed automata extend timed automata with cost variables that can be used to model the evolution of various quantities. Although cost-optimal reachability is decidable (in polynomial space) on this model, it becomes undecidable on weighted timed games. This paper studies cost-optimal reachability problems on weighted timed automata and games under robust semantics. More precisely, we consider two perturbation game semantics that introduce imprecisions in the standard semantics, and bring robustness properties w.r.t. timing imprecisions to controllers. We give a polynomial-space algorithm for weighted timed automata, and prove the undecidability of cost-optimal reachability on weighted timed games, showing that the problem is robustly undecidable.

@inproceedings{formats2013-BMS,
author =              {Bouyer, Patricia and Markey, Nicolas and Sankur,
Ocan},
title =               {Robust Weighted Timed Automata and Games},
editor =              {Braberman, V{\'\i}ctor and Fribourg, Laurent},
booktitle =           {{P}roceedings of the 11th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'13)},
acronym =             {{FORMATS}'13},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {8053},
pages =               {31-46},
year =                {2013},
month =               aug,
doi =                 {10.1007/978-3-642-40229-6_3},
abstract =            {Weighted timed automata extend timed automata with
cost variables that can be used to model the
evolution of various quantities. Although
cost-optimal reachability is decidable (in
polynomial space) on this model, it becomes
undecidable on weighted timed games. This paper
studies cost-optimal reachability problems on
weighted timed automata and games under robust
semantics. More precisely, we consider two
perturbation game semantics that introduce
imprecisions in the standard semantics, and bring
robustness properties w.r.t. timing imprecisions to
controllers. We give a polynomial-space algorithm
for weighted timed automata, and prove the
undecidability of cost-optimal reachability on
weighted timed games, showing that the problem is
robustly undecidable.},
}

[BMS14] Patricia Bouyer, Nicolas Markey, and Daniel Stan. Mixed Nash Equilibria in Concurrent Games. In FSTTCS'14, Leibniz International Proceedings in Informatics 29, pages 351-363. Leibniz-Zentrum für Informatik, December 2014.
Abstract

We study mixed-strategy Nash equilibria in multiplayer deterministic concurrent games played on graphs, with terminal-reward payoffs (that is, absorbing states with a value for each player). We show undecidability of the existence of a constrained Nash equilibrium (the constraint requiring that one player should have maximal payoff), with only three players and 0/1-rewards (i.e., reachability objectives). This has to be compared with the undecidability result by Ummels and Wojtczak for turn-based games which requires 14 players and general rewards. Our proof has various interesting consequences: (i) the undecidability of the existence of a Nash equilibrium with a constraint on the social welfare; (ii) the undecidability of the existence of an (unconstrained) Nash equilibrium in concurrent games with terminal-reward payoffs.

@inproceedings{fsttcs2014-BMS,
author =              {Bouyer, Patricia and Markey, Nicolas and Stan,
Daniel},
title =               {Mixed {N}ash Equilibria in Concurrent Games},
editor =              {Raman, Venkatesh and Suresh, S. P.},
booktitle =           {{P}roceedings of the 34th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience ({FSTTCS}'14)},
acronym =             {{FSTTCS}'14},
publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
series =              {Leibniz International Proceedings in Informatics},
volume =              {29},
pages =               {351-363},
year =                {2014},
month =               dec,
doi =                 {10.4230/LIPIcs.FSTTCS.2014.351},
abstract =            {We study mixed-strategy Nash equilibria in
multiplayer deterministic concurrent games played on
graphs, with terminal-reward payoffs (that is,
absorbing states with a value for each player). We
show undecidability of the existence of a
constrained Nash equilibrium (the constraint
requiring that one player should have maximal
payoff), with only three players and 0/1-rewards
(i.e., reachability objectives). This has to be
compared with the undecidability result by Ummels
and Wojtczak for turn-based games which requires 14
players and general rewards. Our proof has various
interesting consequences: (i)~the~undecidability of
the existence of a Nash equilibrium with a
constraint on the social welfare;
(ii)~the~undecidability of the existence of an
(unconstrained) Nash equilibrium in concurrent games
with terminal-reward payoffs.},
}

[BMS15] Patricia Bouyer, Nicolas Markey, and Ocan Sankur. Robust Reachability in Timed Automata and Games: A Game-based Approach. Theoretical Computer Science 563:43-74. Elsevier, January 2015.
Abstract

Reachability checking is one of the most basic problems in verification. By solving this problem in a game, one can synthesize a strategy that dictates the actions to be performed for ensuring that the target location is reached. In this work, we are interested in synthesizing "robust" strategies for ensuring reachability of a location in timed automata. By robust, we mean that it must still ensure reachability even when the delays are perturbed by the environment. We model this perturbed semantics as a game between the controller and its environment, and solve the parameterized robust reachability problem: we show that the existence of an upper bound on the perturbations under which there is a strategy reaching a target location is EXPTIME-complete. We also extend our algorithm, with the same complexity, to turn-based timed games, where the successor state is entirely determined by the environment in some locations.

@article{tcs563()-BMS,
author =              {Bouyer, Patricia and Markey, Nicolas and Sankur,
Ocan},
title =               {Robust Reachability in Timed Automata and Games:
A~Game-based Approach},
publisher =           {Elsevier},
journal =             {Theoretical Computer Science},
volume =              {563},
pages =               {43-74},
year =                {2015},
month =               jan,
doi =                 {10.1016/j.tcs.2014.08.014},
abstract =            {Reachability checking is one of the most basic
problems in verification. By solving this problem in
a game, one can synthesize a strategy that dictates
the actions to be performed for ensuring that the
target location is reached. In this work, we are
interested in synthesizing {"}robust{"} strategies
for ensuring reachability of a location in timed
automata. By robust, we mean that it must still
ensure reachability even when the delays are
perturbed by the environment. We model this
perturbed semantics as a game between the controller
and its environment, and solve the parameterized
robust reachability problem: we show that the
existence of an upper bound on the perturbations
under which there is a strategy reaching a target
location is EXPTIME-complete. We also extend our
algorithm, with the same complexity, to turn-based
timed games, where the successor state is entirely
determined by the environment in some locations.},
}

[BMS16] Patricia Bouyer, Nicolas Markey, and Daniel Stan. Stochastic Equilibria under Imprecise Deviations in Terminal-Reward Concurrent Games. In GandALF'16, Electronic Proceedings in Theoretical Computer Science 226, pages 61-75. September 2016.
Abstract

We study the existence of mixed-strategy equilibria in concurrent games played on graphs. While existence is guaranteed with safety objectives for each player, Nash equilibria need not exist when players are given arbitrary terminal-reward objectives, and their existence is undecidable with qualitative reachability objectives (and only three players). However, these results rely on the fact that the players can enforce infinite plays while trying to improve their payoffs. In this paper, we introduce a relaxed notion of equilibria, where deviations are imprecise. We prove that contrary to Nash equilibria, such (stationary) equilibria always exist, and we develop a PSPACE algorithm to compute one.

@inproceedings{gandalf2016-BMS,
author =              {Bouyer, Patricia and Markey, Nicolas and Stan,
Daniel},
title =               {Stochastic Equilibria under Imprecise Deviations in
Terminal-Reward Concurrent Games},
editor =              {Cantone, Domenico and Delzanno, Giorgio},
booktitle =           {{P}roceedings of the 7th {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics and {F}ormal
{V}erification ({GandALF}'16)},
acronym =             {{GandALF}'16},
series =              {Electronic Proceedings in Theoretical Computer
Science},
volume =              {226},
pages =               {61-75},
year =                {2016},
month =               sep,
doi =                 {10.4204/EPTCS.226.5},
abstract =            {We study the existence of mixed-strategy equilibria
in concurrent games played on graphs. While
existence is guaranteed with safety objectives for
each player, Nash equilibria need not exist when
players are given arbitrary terminal-reward
objectives, and their existence is undecidable with
qualitative reachability objectives (and~only three
players). However, these results rely on the fact
that the players can enforce infinite plays while
trying to improve their payoffs. In this paper, we
introduce a relaxed notion of equilibria, where
deviations are imprecise. We prove that contrary to
Nash equilibria, such (stationary) equilibria always
exist, and we develop a PSPACE algorithm to compute
one.},
}

[BMT99] Augustin Baziramwabo, Pierre McKenzie, and Denis Thérien. Modular Temporal Logic. In LICS'99, pages 344-351. IEEE Comp. Soc. Press, July 1999.
@inproceedings{lics1999-BMT,
author =              {Baziramwabo, Augustin and McKenzie, Pierre and
Th{\'e}rien, Denis},
title =               {Modular Temporal Logic},
booktitle =           {{P}roceedings of the 14th {A}nnual {S}ymposium on
{L}ogic in {C}omputer {S}cience ({LICS}'99)},
acronym =             {{LICS}'99},
publisher =           {IEEE Comp. Soc. Press},
pages =               {344-351},
year =                {1999},
month =               jul,
}

[BMV14] Patricia Bouyer, Nicolas Markey, and Steen Vester. Nash Equilibria in Symmetric Games with Partial Observation. In SR'14, Electronic Proceedings in Theoretical Computer Science 146, pages 49-55. March 2014.
Abstract

We investigate a model for representing large multiplayer games, which satisfy strong symmetry properties. This model is made of multiple copies of an arena; each player plays in his own arena, and can partially observe what the other players do. Therefore, this game has partial information and symmetry constraints, which make the computation of Nash equilibria difficult. We show several undecidability results, and for bounded-memory strategies, we precisely characterize the complexity of computing pure Nash equilibria (for qualitative objectives) in this game model.

@inproceedings{sr2014-BMV,
author =              {Bouyer, Patricia and Markey, Nicolas and Vester,
Steen},
title =               {Nash Equilibria in Symmetric Games with Partial
Observation},
booktitle =           {{P}roceedings of the 2nd {I}nternational {W}orkshop
on {S}trategic {R}easoning ({SR}'14)},
acronym =             {{SR}'14},
series =              {Electronic Proceedings in Theoretical Computer
Science},
volume =              {146},
pages =               {49-55},
year =                {2014},
month =               mar,
doi =                 {10.4204/EPTCS.146.7},
abstract =            {We investigate a model for representing large
multiplayer games, which satisfy strong symmetry
properties. This model is made of multiple copies of
an arena; each player plays in his own arena, and
can partially observe what the other players do.
Therefore, this game has partial information and
symmetry constraints, which make the computation of
Nash equilibria difficult. We show several
undecidability results, and for bounded-memory
strategies, we precisely characterize the complexity
of computing pure Nash equilibria (for qualitative
objectives) in this game model.},
}

[BMV15] Dietmar Berwanger, Anup Basil Mathew, and Marie Van den Bogaard. Hierarchical Information Patterns and Distributed Strategy Synthesis. In ATVA'15, Lecture Notes in Computer Science 9364, pages 378-393. Springer-Verlag, October 2015.
@inproceedings{atva2015-BMV,
author =              {Berwanger, Dietmar and Mathew, Anup Basil and
Van{~}den{ }Bogaard, Marie},
title =               {Hierarchical Information Patterns and Distributed
Strategy Synthesis},
editor =              {Finkbeiner, Bernd and Pu, Geguang and Zhang, Lijun},
booktitle =           {{P}roceedings of the 13th {I}nternational
{S}ymposium on {A}utomated {T}echnology for
{V}erification and {A}nalysis ({ATVA}'15)},
acronym =             {{ATVA}'15},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {9364},
pages =               {378-393},
year =                {2015},
month =               oct,
}

[BMV17] Patricia Bouyer, Nicolas Markey, and Steen Vester. Nash Equilibria in Symmetric Graph Games with Partial Observation. Information and Computation 254(2):238-258. Elsevier, June 2017.
Abstract

We investigate a model for representing large multiplayer games, which satisfy strong symmetry properties. This model is made of multiple copies of an arena; each player plays in his own arena, and can partially observe what the other players do. Therefore, this game has partial information and symmetry constraints, which make the computation of Nash equilibria difficult. We show several undecidability results, and for bounded-memory strategies, we precisely characterize the complexity of computing pure Nash equilibria (for qualitative objectives) in this game model.

@article{icomp254()-BMV,
author =              {Bouyer, Patricia and Markey, Nicolas and Vester,
Steen},
title =               {{N}ash Equilibria in Symmetric Graph Games with
Partial Observation},
publisher =           {Elsevier},
journal =             {Information and Computation},
volume =              {254},
number =              {2},
pages =               {238-258},
year =                {2017},
month =               jun,
doi =                 {10.1016/j.ic.2016.10.010},
abstract =            {We investigate a model for representing large
multiplayer games, which satisfy strong symmetry
properties. This model is made of multiple copies of
an arena; each player plays in his own arena, and
can partially observe what the other players do.
Therefore, this game has partial information and
symmetry constraints, which make the computation of
Nash equilibria difficult. We show several
undecidability results, and for bounded-memory
strategies, we precisely characterize the complexity
of computing pure Nash equilibria (for qualitative
objectives) in this game model.},
}

[BO04] Stephen J. Bellantoni and Isabel Oitavem. Separating NC along the δ axis. Theoretical Computer Science 318(1-2):57-78. Elsevier, June 2004.
@article{tcs318(1-2)-BO,
author =              {Bellantoni, Stephen J. and Oitavem, Isabel},
title =               {Separating {{$$\mathrm{NC}$$}} along the
{{$$\delta$$}} axis},
publisher =           {Elsevier},
journal =             {Theoretical Computer Science},
volume =              {318},
number =              {1-2},
pages =               {57-78},
year =                {2004},
month =               jun,
doi =                 {10.1016/j.tcs.2003.10.021},
}

[Bod88] Hans L. Bodlaender. Dynamic Programming on Graphs with Bounded Treewidth. In ICALP'88, Lecture Notes in Computer Science 317, pages 105-118. Springer-Verlag, July 1988.
@inproceedings{icalp1988-Bod,
author =              {Bodlaender, Hans L.},
title =               {Dynamic Programming on Graphs with Bounded
Treewidth},
editor =              {Lepist{\"o}, Timo and Salomaa, Arto},
booktitle =           {{P}roceedings of the 15th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'88)},
acronym =             {{ICALP}'88},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {317},
pages =               {105-118},
year =                {1988},
month =               jul,
doi =                 {10.1007/3-540-19488-6_110},
}

[Bod93] Hans L. Bodlaender. A Tourist Guide through Treewidth. Acta Cybernetica 11(1-2):1-21. Institute of Informatics, University of Szeged, 1993.
@article{actacyb11(1-2)-Bod,
author =              {Bodlaender, Hans L.},
title =               {A~Tourist Guide through Treewidth},
publisher =           {Institute of Informatics, University of Szeged},
journal =             {Acta Cybernetica},
volume =              {11},
number =              {1-2},
pages =               {1-21},
year =                {1993},
}

[Bod96] Hans L. Bodlaender. A linear-time algorithm for finding tree-decompositions of small treewidth. SIAM Journal on Computing 25(6):1305-1317. Society for Industrial and Applied Math., December 1996.
@article{siamcomp25(6)-Bod,
author =              {Bodlaender, Hans L.},
title =               {A~linear-time algorithm for finding
tree-decompositions of small treewidth},
publisher =           {Society for Industrial and Applied Math.},
journal =             {SIAM Journal on Computing},
volume =              {25},
number =              {6},
pages =               {1305-1317},
year =                {1996},
month =               dec,
doi =                 {10.1137/S0097539793251219},
}

[Boj08] Mikołaj Bojań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}},
booktitle =           {{P}roceedings of the 11th {I}nternational
{C}onference on {F}oundations of {S}oftware
{S}cience and {C}omputation {S}tructure
({FoSSaCS}'08)},
acronym =             {{FoSSaCS}'08},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {4962},
pages =               {172-185},
year =                {2008},
month =               mar,
}

[Bou02] Patricia Bouyer. Timed Automata May Cause some Troubles. Research Report LSV-02-09, Lab. Spécification & Vérification, ENS Cachan, France, July 2002.
@techreport{LSV0209-Bou,
author =              {Bouyer, Patricia},
title =               {Timed Automata May Cause some Troubles},
number =              {LSV-02-09},
year =                {2002},
month =               jul,
institution =         {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
France},
type =                {Research Report},
}

[Bou03] Patricia Bouyer. Untameable Timed Automata!. In STACS'03, Lecture Notes in Computer Science 2607, pages 620-631. Springer-Verlag, February 2003.
@inproceedings{stacs2003-Bou,
author =              {Bouyer, Patricia},
title =               {Untameable Timed Automata!},
editor =              {Alt, Helmut and Habib, Michel},
booktitle =           {{P}roceedings of the 20th {S}ymposium on
{T}heoretical {A}spects of {C}omputer {S}cience
({STACS}'03)},
acronym =             {{STACS}'03},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {2607},
pages =               {620-631},
year =                {2003},
month =               feb,
doi =                 {10.1007/3-540-36494-3_54},
}

[Bou04] Patricia Bouyer. Forward Analysis of Updatable Timed Automata. Formal Methods in System Design 24(3):281-320. Kluwer Academic, May 2004.
@article{fmsd24(3)-Bou,
author =              {Bouyer, Patricia},
title =               {Forward Analysis of Updatable Timed Automata},
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] Laura Bozzelli. 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},
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] Bruno Blanchet and Andreas Podelski. 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] Mordechai Ben-Ari, Amir Pnueli, and Zohar Manna. The Temporal Logic of Branching Time. In POPL'81, pages 164-176. ACM Press, January 1981.
@inproceedings{popl1981-BPM,
author =              {Ben{-}Ari, Mordechai and Pnueli, Amir and Manna,
Zohar},
title =               {The Temporal Logic of Branching Time},
booktitle =           {Conference Record of the 8th {ACM} {S}ymposium on
{P}rinciples of {P}rogramming {L}anguages
({POPL}'81)},
acronym =             {{POPL}'81},
publisher =           {ACM Press},
pages =               {164-176},
year =                {1981},
month =               jan,
}

[BPM83] Mordechai Ben-Ari, Amir Pnueli, and Zohar Manna. The Temporal Logic of Branching Time. Acta Informatica 20:207-226. Springer-Verlag, 1983.
@article{acta20()-BPM,
author =              {Ben{-}Ari, Mordechai and Pnueli, Amir and Manna,
Zohar},
title =               {The Temporal Logic of Branching Time},
publisher =           {Springer-Verlag},
journal =             {Acta Informatica},
volume =              {20},
pages =               {207-226},
year =                {1983},
}

[BPR+16] Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin, and Mathieu Sassolas. 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] Thomas Ball and Sriram Rajamani. 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èle Beauquier and Alexander Rabinovich. 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éronique Bruyère and Jean-François Raskin. 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,
title =               {The Modal Mu-Calculus Alternation Hierarchy is
Strict},
publisher =           {Elsevier},
journal =             {Theoretical Computer Science},
volume =              {195},
number =              {2},
pages =               {133-153},
year =                {1998},
month =               mar,
}

[BRB90] Karl S. Brace, Richard L. Ruddel, and Randal E. Bryant. Efficient Implementation of a BDD package. In DAC'90, pages 40-45. IEEE Comp. Soc. Press, June 1990.
@inproceedings{dac1990-BRB,
author =              {Brace, Karl S. and Ruddel, Richard L. and Bryant,
Randal E.},
title =               {Efficient Implementation of a {BDD} package},
booktitle =           {{P}roceedings of the 27th {D}esign {A}utomation
{C}onference ({DAC}'90)},
acronym =             {{DAC}'90},
publisher =           {IEEE Comp. Soc. Press},
pages =               {40-45},
year =                {1990},
month =               jun,
}

[Bre12] Romain Brenguier. Nash Equilibria in Concurrent Games –Application to Timed Games. Thèse de doctorat, Lab. Spécification & Vérification, ENS Cachan, France, November 2012.
@phdthesis{phd-brenguier,
author =              {Brenguier, Romain},
title =               {Nash Equilibria in Concurrent Games~--Application to
Timed Games},
year =                {2012},
month =               nov,
school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
France},
type =                {Th\ese de doctorat},
}

[Bre16] Romain Brenguier. Optimal Assumptions for Synthesis. In CONCUR'16, Leibniz International Proceedings in Informatics 59, pages 8:1-8:15. Leibniz-Zentrum für Informatik, August 2016.
@inproceedings{concur2016-Bre,
author =              {Brenguier, Romain},
title =               {Optimal Assumptions for Synthesis},
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 Maria Bersani, Matteo Rossi, and Pierluigi San 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] Romain Brenguier, Jean-François Raskin, and Mathieu Sassolas. 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},
}

[BRS17] Romain Brenguier, Jean-François Raskin, and Ocan Sankur. Assume-admissible synthesis. Acta Informatica 54(1):41-83. Springer-Verlag, February 2017.
@article{acta54(1)-BRS,
author =              {Brenguier, Romain and Raskin, Jean-Fran{\c c}ois and
Sankur, Ocan},
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] Benedikt Brü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] Patrick Blackburn and Jerry Seligman. 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},
journal =             {Journal of Logic, Language and Information},
volume =              {4},
number =              {3},
pages =               {251-272},
year =                {1995},
}

[BS98] Patrick Blackburn and Jerry Seligman. 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 Colin Stirling. Modal Logics and Mu-Calculi: An Introduction. In Jan A. Bergstra, Alban Ponse, 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] Nathalie Bertrand and Sven Schewe. Playing Optimally on Timed Automata with Random Delays. In FORMATS'12, Lecture Notes in Computer Science 7595, pages 43-58. Springer-Verlag, September 2012.
@inproceedings{formats2012-BS,
author =              {Bertrand, Nathalie and Schewe, Sven},
title =               {Playing Optimally on Timed Automata with Random
Delays},
editor =              {Jurdzi{\'n}ski, Marcin and Nickovic, Dejan},
booktitle =           {{P}roceedings of the 10th {I}nternational
{C}onferences on {F}ormal {M}odelling and {A}nalysis
of {T}imed {S}ystems ({FORMATS}'12)},
acronym =             {{FORMATS}'12},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {7595},
pages =               {43-58},
year =                {2012},
month =               sep,
doi =                 {10.1007/978-3-642-33365-1_5},
}

[BSJ+15] Nathalie Bertrand, Amélie Stainer, Thierry Jéron, and Moez Krichen. A game approach to determinize timed automata. Formal Methods in System Design 46(1):42-80. Springer-Verlag, February 2015.
@article{fmsd46(1)-BSJK,
author =              {Bertrand, Nathalie and Stainer, Am{\'e}lie and
J{\'e}ron, Thierry and Krichen, Moez},
title =               {A~game approach to determinize timed automata},
publisher =           {Springer-Verlag},
journal =             {Formal Methods in System Design},
volume =              {46},
number =              {1},
pages =               {42-80},
year =                {2015},
month =               feb,
doi =                 {10.1007/s10703-014-0220-1},
}

[BST98] Sébastien Bornot, Joseph Sifakis, and Stavros Tripakis. 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] Paul Beame, Michael Saks, and Jayram S. Thathachar. Time-Space Tradeoffs for Branching Programs. Research Report 98-053, Electronic Colloquium on Computational Complexity, September 1998.
@techreport{eccc1998-BST,
author =              {Beame, Paul and Saks, Michael and Thathachar, Jayram
S.},
title =               {Time-Space Tradeoffs for Branching Programs},
number =              {98-053},
year =                {1998},
month =               sep,
institution =         {Electronic Colloquium on Computational Complexity},
type =                {Research Report},
}

[BSV04] Henrik Björklund, Sven Sandberg, and Sergei Vorobyov. Memoryless Determinacy of Parity and Mean Payoff Games: A Simple Proof. Theoretical Computer Science 310(1-3):365-378. Elsevier, January 2004.
@article{tcs310(1-3)-BSV,
author =              {Bj{\"o}rklund, Henrik and Sandberg, Sven and
Vorobyov, Sergei},
title =               {Memoryless Determinacy of Parity and Mean Payoff
Games: A~Simple Proof},
publisher =           {Elsevier},
journal =             {Theoretical Computer Science},
volume =              {310},
number =              {1-3},
pages =               {365-378},
year =                {2004},
month =               jan,
doi =                 {10.1016/S0304-3975(03)00427-4},
}

[BT96] Dimitri P. Bertsekas and John N. Tsitsiklis. Neuro-Dynamic Programming. Anthropological Field Studies 3. Athena Scientific, 1996.
@book{NDP-BT,
author =              {Bertsekas, Dimitri P. and Tsitsiklis, John N.},
title =               {Neuro-Dynamic Programming},
publisher =           {Athena Scientific},
series =              {Anthropological Field Studies},
volume =              {3},
year =                {1996},
}

[BT99] Patrick Blackburn and Miroslava Tzakova. 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] Harry Buhrman and Leen Torenvliet. 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écile Bui Thanh, Hanna Klaudel, and Franck Pommereau. 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] Ahmed Bouajjani, Stavros Tripakis, and Sergio Yovine. On-the-Fly Symbolic Model Checking for Real-Time Systems. In RTSS'97, pages 25-35. IEEE Comp. Soc. Press, December 1997.
@inproceedings{rts1997-BTY,
author =              {Bouajjani, Ahmed and Tripakis, Stavros and Yovine,
Sergio},
title =               {On-the-Fly Symbolic Model Checking for Real-Time
Systems},
booktitle =           {{P}roceedings of the 18th {S}ymposium on {R}eal-Time
{S}ystems ({RTSS}'97)},
acronym =             {{RTSS}'97},
publisher =           {IEEE Comp. Soc. Press},
pages =               {25-35},
year =                {1997},
month =               dec,
}

[Buc62] Julius R. Büchi. On a Decision Method in Restricted Second Order Arithmetic. In LMPS'60, pages 1-11. Stanford University Press, June 1962.
@inproceedings{lmps60-Buc,
author =              {B{\"u}chi, Julius R.},
title =               {On a Decision Method in Restricted Second Order
Arithmetic},
editor =              {Nagel, Ernest and Suppes, Patrick and Tarski,
Alfred},
booktitle =           {{P}roceedings of the 1960 {I}nternational {C}ongress
on {L}ogic, {M}ethodology and {P}hilosophy of
{S}cience ({LMPS}'60)},
acronym =             {{LMPS}'60},
publisher =           {Stanford University Press},
pages =               {1-11},
year =                {1962},
month =               jun,
confyear =            {1960},
}

[Bur79] John P. Burgess. Logic and Time. Journal of Symbolic Logic 44(4):566-582. Association for Symbolic Logic, December 1979.
@article{jsl44(4)-Bur,
author =              {Burgess,John P.},
title =               {Logic and Time},
publisher =           {Association for Symbolic Logic},
journal =             {Journal of Symbolic Logic},
volume =              {44},
number =              {4},
pages =               {566-582},
year =                {1979},
month =               dec,
}

[Bur80] John P. Burgess. Decidability for Branching Time. Studia Logica 39(2-3):203-218. Kluwer Academic, 1980.
@article{studlog39(2-3)-Bur,
author =              {Burgess,John P.},
title =               {Decidability for Branching Time},
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 Peter Clote and Jan Krajíček (eds.), Proof Theory, Complexity, and Arithmetic. Oxford University Press, 1993.
@incollection{PTCA-Bus,
author =              {Buss, Samuel R.},
title =               {Algorithms for Boolean Formula Evaluation and for
Tree Contraction},
editor =              {Clote, Peter and Kraj{\'\i}{ c}ek, Jan},
booktitle =           {Proof Theory, Complexity, and Arithmetic},
publisher =           {Oxford University Press},
pages =               {96-115},
year =                {1993},
}

[Bus97] Samuel R. Buss. ALOGTIME Algorithm for Tree Isomorphism, Comparison, and Canonization. In KGC'97, Lecture Notes in Computer Science 1289, pages 18-33. Springer-Verlag, August 1997.
@inproceedings{kgc1997-Bus,
author =              {Buss, Samuel R.},
title =               {{ALOGTIME} Algorithm for Tree Isomorphism,
Comparison, and Canonization},
editor =              {Gottlob, Georg and Leitsch, Alexander and Mundici,
Daniele},
booktitle =           {{P}roceedings of the 5th {K}urt {G}{\"o}del
{C}olloquium ({KGC}'97)},
acronym =             {{KGC}'97},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {1289},
pages =               {18-33},
year =                {1997},
month =               aug,
}

[BV07] Henrik Björklund and Sergei Vorobyov. A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games. Discrete Applied Mathematics 155(2):210-229. Elsevier, January 2007.
@article{dam155(2)-BV,
author =              {Bj{\"o}rklund, Henrik and Vorobyov, Sergei},
title =               {A combinatorial strongly subexponential strategy
improvement algorithm for mean payoff games},
publisher =           {Elsevier},
journal =             {Discrete Applied Mathematics},
volume =              {155},
number =              {2},
pages =               {210-229},
year =                {2007},
month =               jan,
doi =                 {10.1016/j.dam.2006.04.029},
}

[BVW94] Orna Bernholtz, Moshe Y. Vardi, and Pierre Wolper. An Automata-Theoretic Approach to Branching-Time Model Checking (Extended Abstract). In CAV'94, Lecture Notes in Computer Science 818, pages 142-155. Springer-Verlag, June 1994.
@inproceedings{cav1994-BVW,
author =              {Bernholtz, Orna and Vardi, Moshe Y. and Wolper,
Pierre},
title =               {An Automata-Theoretic Approach to Branching-Time
Model Checking (Extended Abstract)},
editor =              {Dill, David L.},
booktitle =           {{P}roceedings of the 6th {I}nternational
{C}onference on {C}omputer {A}ided {V}erification
({CAV}'94)},
acronym =             {{CAV}'94},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {818},
pages =               {142-155},
year =                {1994},
month =               jun,
}

[BW94] Bertil A. Brandin and W. Murray Wonham. Supervisory Control of Timed Discrete-Event Systems. IEEE Transactions on Automatic Control 39(2):329-342. IEEE Comp. Soc. Press, February 1994.
@article{tac39(2)-BW,
author =              {Brandin, Bertil A. and Wonham, W. Murray},
title =               {Supervisory Control of Timed Discrete-Event Systems},
publisher =           {IEEE Comp. Soc. Press},
journal =             {IEEE Transactions on Automatic Control},
volume =              {39},
number =              {2},
pages =               {329-342},
year =                {1994},
month =               feb,
}

[BW17] Julian C. Bradfield and Igor Walukiewicz. The mu-calculus and model-checking. In Edmund M. Clarke, Thomas A. Henzinger, and Helmut Veith (eds.), Handbook of Model Checking. Springer-Verlag, 2017. To appear.
@incollection{HMC-BW,
author =              {Bradfield, Julian C. and Walukiewicz, Igor},
title =               {The mu-calculus and model-checking},
editor =              {Clarke, Edmund M. and Henzinger, Thomas A. and
Veith, Helmut},
booktitle =           {Handbook of Model Checking},
publisher =           {Springer-Verlag},
year =                {2017},
note =                {To~appear},
}

[BY03] Johan Bengtsson and Wang Yi. On Clock Difference Constraints and Termination in Reachability Analysis of Timed Automata. In ICFEM'03. Springer-Verlag, November 2003.
@incollection{icfem2003-BY,
author =              {Bengtsson, Johan and Yi, Wang},
title =               {On Clock Difference Constraints and Termination in
Reachability Analysis of Timed Automata},
booktitle =           {{P}roceedings of the 5th {I}nternational
{C}onference on {F}ormal {E}ngineering {M}ethods
({ICFEM}'03)},
acronym =             {{ICFEM}'03},
publisher =           {Springer-Verlag},
pages =               {491-503},
year =                {2003},
month =               nov,
}

[BY04] Johan Bengtsson and Wang Yi. Timed Automata: Semantics, Algorithms and Tools. In Jörg Desel, Wolfgang Reisig, and Grzegorz Rozenberg (eds.), Lectures on Concurrency and Petri Nets, Lecture Notes in Computer Science 2098, pages 87-124. Springer-Verlag, 2004.
@incollection{lncs3098-BY,
author =              {Bengtsson, Johan and Yi, Wang},
title =               {Timed Automata: Semantics, Algorithms and Tools},
editor =              {Desel, J{\"o}rg and Reisig, Wolfgang and Rozenberg,
Grzegorz},
booktitle =           {Lectures on Concurrency and {P}etri Nets},
publisher =           {Springer-Verlag},
series =              {Lecture Notes in Computer Science},
volume =              {2098},
pages =               {87-124},
year =                {2004},
doi =                 {10.1007/b98282},
}