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

Finally, we consider multi-dimensional extensions of all types of average-energy games: without bounds, with only a lower bound, and with both a lower and an upper bound on the energy. We show that the fully-bounded version is the only case to remain decidable in multiple dimensions.}
}
@article{BMPS-rts16,
  publisher = {Kluwer Academic Publishers},
  journal = {Real-Time Systems},
  author = {Bouyer, Patricia and Markey, Nicolas and Perrin,
                         Nicolas and Schlehuber{-}Caissier, Philipp},
  title = {Timed automata abstraction of switched dynamical
                         systems using control funnels},
  volume = {53},
  number = {3},
  year = {2017},
  pages = {327-353},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMPS-rts16.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMPS-rts16.pdf},
  doi = {10.1007/s11241-016-9262-3},
  abstract = {The development of formal methods for control design
                         is an important challenge with potential
                         applications in a wide range of safety-critical
                         cyber-physical systems. Focusing on switched
                         dynamical systems, we propose a new abstraction,
                         based on time-varying regions of invariance (control
                         funnels), that models behaviors of systems as timed
                         automata. The~main advantage of this method is that
                         it allows for the automated verification and
                         reactive controller synthesis without discretizing
                         the evolution of the state of the system. Efficient
                         and analytic constructions are possible in the case
                         of linear dynamics whereas bounding funnels with
                         conjectured properties based on numerical
                         simulations can be used for general nonlinear
                         dynamics. We~demonstrate the potential of our
                         approach with three examples.}
}
@incollection{BFLMOW-hmc18,
  author = {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim G.
                  and Markey, Nicolas and Ouaknine, Jo{\"e}l and
                  Worrell, James},
  title = {Model Checking Real-Time Systems},
  booktitle = {Handbook of Model Checking},
  editor = {Clarke, Ed and Henzinger, Tom and Veith, Helmut},
  publisher = {Springer},
  year = 2018,
  pages = {1001-1046},
  nochapter = {29},
  doi = {10.1007/978-3-319-10575-8_29},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLMOW-hmc17.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLMOW-hmc17.pdf},
  isbn = {978-3-319-10574-1},
  abstract = {This chapter surveys timed automata as a formalism for
    model checking real-time systems. We begin with introducing the
    model, as an extension of finite-state automata with real-valued
    variables for measuring time. We then present the main
    model-checking results in this framework, and give a hint about some
    recent extensions (namely weighted timed automata and timed
    games).}
}
@inproceedings{BMS-gandalf16,
  address = {Catania, Italy},
  month = sep,
  year = 2016,
  volume = {226},
  series = {Electronic Proceedings in Theoretical Computer Science},
  editor = {Cantone, Domenico and Delzanno, Giorgio},
  acronym = {{GandALF}'16},
  booktitle = {{P}roceedings of the 7th {I}nternational {S}ymposium
                on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification
                  ({GandALF}'16)},
  author = {Bouyer, Patricia and Markey, Nicolas and Stan, Daniel},
  title = {Stochastic Equilibria under Imprecise Deviations in
                  Terminal-Reward Concurrent Games},
  pages = {61-75},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-gandalf16.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-gandalf16.pdf},
  doi = {10.4204/EPTCS.226.5},
  abstract = {We study the existence of mixed-strategy equilibria in
    concurrent games played on graphs. While existence is guaranteed
    with safety objectives for each player, Nash equilibria need not
    exist when players are given arbitrary terminal-reward objectives,
    and their existence is undecidable with qualitative reachability
    objectives (and~only three players). However, these results rely on
    the fact that the players can enforce infinite plays while trying to
    improve their payoffs. In this paper, we introduce a relaxed notion
    of equilibria, where deviations are imprecise. We prove that
    contrary to Nash equilibria, such (stationary) equilibria always
    exist, and we develop a PSPACE algorithm to compute one.}
}
@article{BMRLL-acta16,
  publisher = {Springer},
  journal = {Acta Informatica},
  author = {Bouyer, Patricia and Markey, Nicolas and Randour, Mickael
                  and Larsen, Kim G. and Laursen, Simon},
  title = {Average-energy games},
  volume = {55},
  number = {2},
  year = 2018,
  month = jul,
  pages = {91-127},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMRLL-acta16.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMRLL-acta16.pdf},
  doi = {10.1007/s00236-016-0274-1},
  abstract = {Two-player quantitative zero-sum games provide a natural
    framework to synthesize controllers with performance guarantees for
    reactive systems within an uncontrollable environment. Classical
    settings include mean-payoff games, where the objective is to
    optimize the long-run average gain per action, and energy games,
    where the system has to avoid running out of energy. We study
    average-energy games, where the goal is to optimize the long-run
    average of the accumulated energy. We show that this objective
    arises naturally in several applications, and that it yields
    interesting connections with previous concepts in the literature. We
    prove that deciding the winner in such games is in NP coNP and at
    least as hard as solving mean-payoff games, and we establish that
    memoryless strategies suffice to win. We also consider the case
    where the system has to minimize the average-energy while
    maintaining the accumulated energy within predefined bounds at all
    times: this corresponds to operating with a finite-capacity storage
    for energy. We give results for one-player and two-player games, and
    establish complexity bounds and memory requirements.}
}
@inproceedings{Bouyer-mfcs16,
  address = {Krakow, Poland},
  month = aug,
  year = 2016,
  volume = {58},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
  acronym = {{MFCS}'16},
  booktitle = {{P}roceedings of the 41st
               {I}nternational {S}ymposium on
               {M}athematical {F}oundations of 
               {C}omputer {S}cience
               ({MFCS}'16)},
  author = {Bouyer, Patricia},
  title = {Optimal Reachability in Weighted Timed Automata and Games},
  pages = {3:1-3:3},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/bouyer-mfcs16.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bouyer-mfcs16.pdf},
  doi = {10.4230/LIPIcs.MFCS.2016.3},
  abstract = {This is an overview of the invited talk delivered at the 41st International Symposium on Math- ematical Foundations of Computer Science (MFCS-2016).}
}
@inproceedings{ABKMT-mfcs16,
  address = {Krakow, Poland},
  month = aug,
  year = 2016,
  volume = {58},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
  acronym = {{MFCS}'16},
  booktitle = {{P}roceedings of the 41st
               {I}nternational {S}ymposium on
               {M}athematical {F}oundations of 
               {C}omputer {S}cience
               ({MFCS}'16)},
  author = {Akshay, S. and Bouyer, Patricia and Krishna, Shankara Narayanan and
                  Manasa, Lakshmi and Trivedi, Ashutosh },
  title = {Stochastic Timed Games Revisited},
  pages = {8:1-8:14},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABKMT-mfcs16.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABKMT-mfcs16.pdf},
  doi = {10.4230/LIPIcs.MFCS.2016.8},
  abstract = {Stochastic timed games (STGs), introduced by Bouyer and Forejt,
    naturally generalize both continuous-time Markov chains and timed automata
    by providing a partition of the locations between those controlled by two
    players (Player Box and Player Diamond) with competing objectives and
    those governed by stochastic laws. Depending on the number of
    players---2,~1, or~0---subclasses of stochastic timed games are often
    classified as \(2\frac{1}{2}\)-player, \(1\frac{1}{2}\)-player, and
    \(\frac{1}{2}\)-player games where the \(\frac{1}{2}\) symbolizes the
    presence of the stochastic {"}nature{"} player. For STGs with reachability
    objectives it is known that \(1\frac{1}{2}\)-player one-clock STGs are
    decidable for qualitative objectives, and that \(2\frac{1}{2}\)-player
    three-clock STGs are undecidable for quantitative reachability objectives.
    This paper further refines the gap in this decidability spectrum. We show
    that quantitative reachability objectives are already undecidable for
    \(1\frac{1}{2}\)-player four-clock STGs, and even under the time-bounded
    restriction for \(2\frac{1}{2}\)-player five-clock~STGs. We~also obtain a
    class of \(1\frac{1}{2}\), \(2\frac{1}{2}\)-player STGs for which the
    quantitative reachability problem is decidable.}
}
@inproceedings{BBCM-csr16,
  address = {St~Petersburg, Russia},
  month = jun,
  year = 2016,
  volume = {9691},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Gerhard J. Woeginger},
  acronym = {{CSR}'16},
  booktitle = {{P}roceedings of the 11th {I}nternational {C}omputer {S}cience
                  {S}ymposium in {R}ussia ({CSR}'16)},
  author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and Carlier,
                  Pierre 
                  and Menet, Quentin},
  title = {Compositional Design of Stochastic Timed Automata},
  pages = {117-130},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBCM-csr16.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBCM-csr16.pdf},
  doi = {10.1007/978-3-319-34171-2_9},
  abstract = {In this paper, we study the model of stochastic timed automata
     and we target the definition of adequate composition operators that will
     allow a compositional approach to the design of stochastic systems with
     hard real-time constraints. This paper achieves the first step towards
     that goal. Firstly, we define a parallel composition operator that
     (we~prove) corresponds to the interleaving semantics for that model; we
     give conditions over probability distributions, which ensure that the
     operator is well-defined; and we exhibit problematic behaviours when this
     condition is not satisfied. We furthermore identify a large and natural
     subclass which is closed under parallel composition. Secondly, we define
     a bisimulation notion which naturally extends that for continuous-time
     Markov chains. Finally, we importantly show that the defined bisimulation
     is a congruence w.r.t. the parallel composition, which is an expected
     property for a proper modular approach to system design.}
}
@inproceedings{BBBC-icalp16,
  address = {Rome, Italy},
  month = jul,
  year = 2016,
  volume = {55},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Chatzigiannakis, Ioannis and Mitzenmacher,
                  Michael and Rabani, Yuval and Sangiorgi, Davide},
  acronym = {{ICALP}'16},
  booktitle = {{P}roceedings of the 43rd {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming ({ICALP}'16)},
  author = {Bertrand, Nathalie and Bouyer, Patricia and Brihaye,
                  {\relax Th}omas
                  and Carlier, Pierre},
  title = {Analysing Decisive Stochastic Processes},
  pages = {101:1-101:14},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBC-icalp16.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBC-icalp16.pdf},
  doi = {10.4230/LIPIcs.ICALP.2016.101},
  abstract = {In~2007, Abdulla \textit{et~al.} introduced the elegant concept
    of decisive Markov chain. Intuitively, decisiveness allows one to lift the
    good properties of finite Markov chains to infinite Markov chains. For
    instance, the approximate quantitative reachability problem can be solved
    for decisive Markov chains (enjoying reasonable effectiveness assumptions)
    including probabilistic lossy channel systems and probabilistic vector
    addition systems with states. In this paper, we extend the concept of
    decisiveness to more general stochastic processes. This extension is non
    trivial as we consider stochastic processes with a potentially continuous
    set of states and uncountable branching (common features of real-time
    stochastic processes). This allows us to obtain decidability results for
    both qualitative and quantitative verification problems on some classes of
    real-time stochastic processes, including generalized semi-Markov
    processes and stochastic timed automata.}
}
@article{BMV-ic16,
  publisher = {Elsevier Science Publishers},
  journal = {Information and Computation},
  author = {Bouyer, Patricia and Markey, Nicolas and Vester, Steen},
  title = {{N}ash Equilibria in Symmetric Graph Games with Partial Observation},
  volume = {254},
  number = {2},
  month = jun,
  year = 2017,
  pages = {238-258},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMV-ic16.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMV-ic16.pdf},
  doi = {10.1016/j.ic.2016.10.010},
  abstract = {We investigate a model for representing large multiplayer games,
    which satisfy strong symmetry properties. This model is made of multiple
    copies of an arena; each player plays in his own arena, and can partially
    observe what the other players do. Therefore, this game has partial
    information and symmetry constraints, which make the computation of Nash
    equilibria difficult. We show several undecidability results, and for
    bounded-memory strategies, we precisely characterize the complexity of
    computing pure Nash equilibria (for qualitative objectives) in this game
    model.}
}
@inproceedings{BCM-cav16,
  address = {Toronto, Canada},
  month = jul,
  year = 2016,
  volume = 9779,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Chaudhuri, Swarat and Farzan, Azadeh},
  acronym = {{CAV}'16},
  booktitle = {{P}roceedings of the 28th
               {I}nternational {C}onference on 
               {C}omputer {A}ided {V}erification
               ({CAV}'16)~-- {P}art~{I}},
  author = {Bouyer, Patricia and Colange, Maximilien and Markey, Nicolas},
  title = {Symbolic Optimal Reachability in Weighted Timed Automata},
  pages = {513-530},
  url = {http://arxiv.org/abs/1602.00481},
  doi = {10.1007/978-3-319-41528-4_28},
  abstract = {Weighted timed automata have been defined in the early 2000's
   for modelling resource-consumption or -allocation problems in real-time
   systems. Optimal reachability is decidable in weighted timed automata, and
   a symbolic forward algorithm has been developed to solve that problem. This
   algorithm uses so-called priced zones, an extension of standard zones with
   cost functions. In order to ensure termination, the algorithm requires
   clocks to be bounded. For unpriced timed automata, much work has been done
   to develop sound abstractions adapted to the forward exploration of timed
   automata, ensuring termination of the model-checking algorithm without
   bounding the clocks. In this paper, we take advantage of recent
   developments on abstractions for timed automata, and propose an algorithm
   allowing for symbolic analysis of all weighted timed automata, without
   requiring bounded clocks.}
}
@inproceedings{BMRSS-icalp16,
  address = {Rome, Italy},
  month = jul,
  year = 2016,
  volume = {55},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Chatzigiannakis, Ioannis and Mitzenmacher,
                  Michael and Rabani, Yuval and Sangiorgi, Davide},
  acronym = {{ICALP}'16},
  booktitle = {{P}roceedings of the 43rd {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming ({ICALP}'16)},
  author = {Bouyer, Patricia and Markey, Nicolas and Randour,
                  Mickael and Sangnier, Arnaud and Stan, Daniel},
  title = {Reachability in Networks of Register Protocols under
                  Stochastic Schedulers},
  pages = {106:1-106:14},
  url = {http://arxiv.org/abs/1602.05928},
  doi = {10.4230/LIPIcs.ICALP.2016.106},
  abstract = {We study the almost-sure reachability problem in a distributed
    system obtained as the asynchronous composition of~\(N\) copies (called
    \emph{processes}) of the same automaton (called \emph{protocol}), that can
    communicate via a shared register with finite domain. The automaton has
    two types of transitions: write-transitions update the value of the
    register, while read-transitions move to a new state depending on the
    content of the register. Non-determinism is resolved by a stochastic
    scheduler. Given a protocol, we focus on almost-sure reachability of a
    target state by one of the processes. The answer to this problem naturally
    depends on the number~\(N\) of processes. However, we prove that our
    setting has a cut-off property : the answer to the almost-sure
    reachability problem is constant when \(N\) is large enough; we~then
    develop an EXPSPACE algorithm deciding whether this constant answer is
    positive or negative.}
}
@comment{{B-arxiv16,
  author =		Bollig, Benedikt, 
  affiliation = 	aff-LSVmexico,
  title =    		One-Counter Automata with Counter Visibility, 
  institution = 	Computing Research Repository, 
  number =    		1602.05940, 
  month = 		feb, 
  nmonth =     		2,
  year = 		2016, 
  type = 		RR, 
  axeLSV = 		mexico,
  NOcontrat = 		"",
  
  url =			http://arxiv.org/abs/1602.05940, 
  PDF =			"http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf",
  lsvdate-new =  	20160222,
  lsvdate-upd =  	20160222,
  lsvdate-pub =  	20160222,
  lsv-category = 	"rapl",
  wwwpublic =    	"public and ccsb",
  note = 		18~pages, 

  abstract = "In a one-counter automaton (OCA), one can read a letter
    from some finite alphabet, increment and decrement the counter by
    one, or test it for zero. It is well-known that universality and
    language inclusion for OCAs are undecidable. We consider here OCAs
    with counter visibility: Whenever the automaton produces a letter,
    it outputs the current counter value along with~it. Hence, its
    language is now a set of words over an infinite alphabet. We show
    that universality and inclusion for that model are in PSPACE, thus
    no harder than the corresponding problems for finite automata, which
    can actually be considered as a special case. In fact, we show that
    OCAs with counter visibility are effectively determinizable and
    closed under all boolean operations. As~a~strict generalization, we
    subsequently extend our model by registers. The general nonemptiness
    problem being undecidable, we impose a bound on the number of
    register comparisons and show that the corresponding nonemptiness
    problem is NP-complete.",
}}
@techreport{BJM-arxiv16,
  author = {Bouyer, Patricia and Markey, Nicolas and Jug{\'e}, Vincent},
  title = {Dynamic Complexity of Parity Games with Bounded Tree-Width},
  institution = {Computing Research Repository},
  number = {1610.00571},
  year = {2016},
  url = {https://arxiv.org/abs/1610.00571},
  pdf = {https://arxiv.org/abs/1610.00571},
  month = oct,
  type = {Research Report},
  note = {33~pages}
}
@inproceedings{GBM-stacs18,
  address = {Caen, France},
  month = feb,
  volume = {96},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Niedermeier, Rolf and Vall{\'e}e, Brigitte},
  acronym = {{STACS}'18},
  booktitle = {{P}roceedings of the 35th {A}nnual
               {S}ymposium on {T}heoretical {A}spects of
               {C}omputer {S}cience
               ({STACS}'18)},
  author = {Gardy, Patrick and Bouyer, Patricia and Markey, Nicolas},
  title = {Dependences in Strategy Logic},
  pages = {34:1-34:15},
  year = {2018},
  doi = {10.4230/LIPIcs.STACS.2018.34},
  pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/8532/pdf/LIPIcs-STACS-2018-34.pdf},
  url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=8532},
  abstract = {Strategy Logic (SL) is a very expressive logic for specifying and verifying properties of multi-agent systems: in SL, one can quantify over strategies, assign them to agents, and express properties of the resulting plays. Such a powerful framework has two drawbacks: first, model checking SL has non-elementary complexity; second, the exact semantics of SL is rather intricate, and may not correspond to what is expected. In this paper, we focus on strategy dependences in SL, by tracking how existentially-quantified strategies in a formula may (or may not) depend on other strategies selected in the formula. We study different kinds of dependences, refining the approach of [Mogavero et al., Reasoning about strategies: On the model-checking problem, 2014], and prove that they give rise to different satisfaction relations. In the setting where strategies may only depend on what they have observed, we identify a large fragment of SL for which we prove model checking can be performed in 2-EXPTIME.}
}
@inproceedings{GBBLM-gretsi17,
  address = {Juan-les-Pins, France},
  month = sep,
  year = 2017,
  publisher = {},
  editor = {},
  acronym = {{GRETSI}'17},
  booktitle = {Actes du XXVI$^{\text{\`eme}}$ colloque GRETSI},
  author = {Mauricio Gonz{\'a}lez and Olivier Beaude and
                  Patricia Bouyer and Samson Lasaulce and Nicolas
                  Markey},
  title = {Strat{\'e}gies d'ordonnancement de consommation
                  d'{\'e}nergie en pr{\'e}sence d'information
                  imparfaite de pr{\'e}vision},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/GBBLM-gretsi17.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GBBLM-gretsi17.pdf}
}
@techreport{BJM-arxiv17,
  author = {Bouyer, Patricia and Markey, Nicolas and
                   Jug{\'e}, Vincent},
  institution = {Computing Research Repository},
  month = feb,
  note = {14~pages},
  number = {1702.05183},
  type = {Research Report},
  title = {Courcelle's Theorem Made Dynamic},
  year = {2017},
  url = {https://arxiv.org/abs/1702.05183},
  pdf = {https://arxiv.org/abs/1702.05183}
}
@inproceedings{BHJ-concur17,
  address = {Berlin, Germany},
  month = sep,
  year = 2017,
  volume = {85},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Meyer, Roland and Nestmann, Uwe},
  acronym = {{CONCUR}'17},
  booktitle = {{P}roceedings of the 28th
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'17)},
  author = {Bouyer, Patricia and Haddad, Serge and Jug{\'e}, Vincent},
  title = {Unbounded product-form {P}etri nets},
  pages = {31:1--31:16},
  url = {http://drops.dagstuhl.de/opus/volltexte/2017/7795},
  pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/7795/pdf/LIPIcs-CONCUR-2017-31.pdf},
  doi = {10.4230/LIPIcs.CONCUR.2017.31},
  abstract = {Computing steady-state distributions in infinite-state stochastic systems is in general a very difficult task. Product-form Petri nets are those Petri nets for which the steady-state distribution can be described as a natural product corresponding, up to a normalising constant, to an exponentiation of the markings. However, even though some classes of nets are known to have a product-form distribution, computing the normalising constant can be hard. The class of (closed) \(\Pi^3\)-nets has been proposed in an earlier work, for which it is shown that one can compute the steady-state distribution efficiently. However these nets are bounded. In this paper, we generalise queuing Markovian networks and closed \(\Pi^3\)-nets to obtain the class of open \(\Pi^3\)-nets, that generate infinite-state systems. We show interesting properties of these nets: (1) we prove that liveness can be decided in polynomial time, and that reachability in live \(\Pi^3\)-nets can be decided in polynomial time; (2) we show that we can decide ergodicity of such nets in polynomial time as well; (3) we provide a pseudo-polynomial time algorithm to compute the normalising constant.}
}
@inproceedings{BJM-formats17,
  address = {Berlin, Germany},
  month = sep,
  year = 2017,
  volume = {10419},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Abate, Alessandro and Geeraerts, Gilles},
  acronym = {{FORMATS}'17},
  booktitle = {{P}roceedings of the 15th {I}nternational {C}onference
           on {F}ormal {M}odelling and {A}nalysis of {T}imed
           {S}ystems ({FORMATS}'17)},
  author = {Bouyer, Patricia and Jaziri, Samy and Markey, Nicolas},
  title = {On the Determinization of Timed Systems},
  pages = {25-41},
  url = {https://hal.archives-ouvertes.fr/hal-01566436/},
  doi = {10.1007/978-3-319-65765-3_2},
  abstract = {We introduce a new formalism called automata over a timed domain which provides an adequate framework for the determinization of timed systems. In this formalism, determinization w.r.t. timed language is always possible at the cost of changing the timed domain. We give a condition for determinizability of automata over a timed domain without changing the timed domain, which allows us to recover several known determinizable classes of timed systems, such as strongly-non-zeno timed automata, integer-reset timed automata, perturbed timed automata, etc. Moreover in the case of timed automata this condition encompasses most determinizability conditions from the literature.}
}
@incollection{BLMOW-kimfest17,
  author = {Bouyer, Patricia and Laroussinie, Fran{\c{c}}ois and
                         Markey, Nicolas and Ouaknine, Jo{\"e}l and Worrell,
                         James},
  title = {Timed temporal logics},
  editor = {Aceto, Luca and Bacci, Giorgio and Bacci, Giovani
                         and Ing{\'o}lfsd{\'o}ttir, Anna and Legay, Axel and
                         Mardare, Radu},
  booktitle = {Models, Algorithms, Logics and Tools: Essays
                         Dedicated to Kim Guldstrand Larsen on the Occasion
                         of His 60th Birthday},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {10460},
  year = {2017},
  pages = {211-230},
  month = aug,
  doi = {10.1007/978-3-319-65764-6_11},
  abstract = {Since the early 1990's, classical temporal logics
                         have been extended with timing constraints. While
                         temporal logics only express contraints on the order
                         of events, their timed extensions can add
                         quantitative constraints on delays between those
                         events. We survey expressiveness and algorithmic
                         results on those logics, and discuss semantic
                         choices that may look unimportant but do have an
                         impact on the questions we consider.},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BLMOW-kimfest17.pdf},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BLMOW-kimfest17.pdf}
}
@inproceedings{BGMR-gandalf18,
  address = {Saarbr{\"u}cken, Germany},
  month = sep,
  volume = {277},
  series = {Electronic Proceedings in Theoretical Computer Science},
  editor = {Andrea Orlandini and Martin Zimmermann},
  acronym = {{GandALF}'18},
  booktitle = {{P}roceedings of the 9th {I}nternational {S}ymposium
                on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification
                  ({GandALF}'18)},
  author = {Bouyer, Patricia and Gonz{\'a}lez, Mauricio and Markey, Nicolas and Randour, Mickael},
  title = {Multi-weighted Markov Decision Processes with Reachability Objectives},
  pages = {250-264},
  year = {2018},
  doi = {10.4204/EPTCS.277.18},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMR-gandalf18.pdf},
  url = {http://arxiv.org/abs/1809.03107},
  abstract = {In this paper, we are interested in the synthesis of schedulers in double-weighted Markov decision processes, which satisfy both a percentile constraint over a weighted reachability condition, and a quantitative constraint on the expected value of a random variable defined using a weighted reachability condition. This problem is inspired by the modelization of an electric-vehicle charging problem. We study the cartography of the problem, when one parameter varies, and show how a partial cartography can be obtained via two sequences of opimization problems. We discuss completeness and feasability of the method.}
}
@inproceedings{BJM-rv18,
  address = {Limassol, Cyprus},
  month = nov,
  volume = 11237,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Colombo, Christian and Leucker, Martin},
  acronym = {{RV}'18},
  booktitle = {{P}roceedings of the 18th {W}orkshop on {R}untime {V}erification ({RV}'18)},
  author = {Bouyer, Patricia and Jaziri, Samy and Markey, Nicolas},
  title = {Efficient Timed Diagnosis Using Automata with Timed Domains},
  pages = {205-221},
  year = {2018},
  doi = {10.1007/978-3-030-03769-7_12},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BJM-rv18.pdf},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BJM-rv18.pdf},
  abstract = {We consider the problems of efficiently diagnosing and predicting what did (or will) happen in a partially-observable one-clock timed automaton. We introduce timed sets as a formalism to keep track of the evolution of the reachable configurations over time, and use our previous work on automata over timed domains to build a candidate diagnoser for our timed automaton. We report on our implementation of this approach compared to the approach of [Tripakis, Fault diagnosis for timed automata, 2002].}
}
@inproceedings{BBJ-csl18,
  address = {Birmingham, UK},
  month = sep,
  year = 2018,
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Ghica, Dan R. and Jung, Achim},
  acronym = {{CSL}'18},
  booktitle = {{P}roceedings of the 27th {A}nnual {EACSL} {C}onference on
                  {C}omputer {S}cience {L}ogic ({CSL}'18)},
  author = {B{\'e}rard, B{\'e}atrice and Bouyer, Patricia and Jug{\'e}, Vincent},
  title = {Finite bisimulations for dynamical systems with overlapping trajectories},
  url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9693},
  pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/9693/pdf/LIPIcs-CSL-2018-26.pdf},
  doi = {10.4230/LIPIcs.CSL.2018.26},
  abstract = {Having a finite bisimulation is a good feature for a dynamical system, since it can lead to the decidability of the verification of reachability properties. We investigate a new class of o-minimal dynamical systems with very general flows, where the classical restrictions on trajectory intersections are partly lifted. We identify conditions, that we call Finite and Uniform Crossing: When Finite Crossing holds, the time-abstract bisimulation is computable and, under the stronger Uniform Crossing assumption, this bisimulation is finite and definable.}
}
@inproceedings{BBFLMR-fm18,
  address = {Oxford, UK},
  month = jul,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Roscoe, {Bill W.} and Peleska, Jan},
  acronym = {{FM}'18},
  booktitle = {{P}roceedings of the 22nd {I}nternational {S}ymposium on {F}ormal
                  {M}ethods ({FM}'18)},
  author = {Bacci, Giovanni and Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim G. and Markey, Nicolas and Reynier, Pierre-Alain},
  title = {Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty},
  pages = {203-221},
  year = {2018},
  doi = {10.1007/978-3-319-95582-7_12},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBFLMR-fm18.pdf},
  url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBFLMR-fm18.pdf},
  note = {Best paper award},
  abstract = {In this paper, we propose a novel framework for the synthesis of robust and optimal energy-aware controllers. The framework is based on energy timed automata, allowing for easy expression of timing-constraints and variable energy-rates. We prove decidability of the energy-constrained infinite-run problem in settings with both certainty and uncertainty of the energy-rates. We also consider the optimization problem of identifying the minimal upper bound that will permit existence of energy-constrained infinite runs. Our algorithms are based on quantifier elimination for linear real arithmetic. Using Mathematica and Mjollnir, we illustrate our framework through a real industrial example of a hydraulic oil pump. Compared with previous approaches our method is completely automated and provides improved results.}
}
@article{BBBC-jlamp18,
  publisher = {Elsevier Science Publishers},
  journal = {Journal of Logic and Algebraic Methods in Programming},
  author = {Bertrand, Nathalie and Bouyer, Patricia and Brihaye, Thomas and Carlier, Pierre},
  title = {When are Stochastic Transition Systems Tameable?},
  volume = {99},
  pages = {41-96},
  year = {2018},
  month = oct,
  doi = {10.1016/j.jlamp.2018.03.004},
  pdf = {https://arxiv.org/pdf/1703.04806.pdf},
  url = {https://doi.org/10.1016/j.jlamp.2018.03.004},
  abstract = {A decade ago, Abdulla, Ben Henda and Mayr introduced the elegant concept of decisiveness for denumerable Markov chains [1]. Roughly speaking, decisiveness allows one to lift most good properties from finite Markov chains to denumerable ones, and therefore to adapt existing verification algorithms to infinite-state models. Decisive Markov chains however do not encompass stochastic real-time systems, and general stochastic transition systems (STSs for short) are needed. In this article, we provide a framework to perform both the qualitative and the quantitative analysis of STSs. First, we define various notions of decisiveness (inherited from [1]), notions of fairness and of attractors for STSs, and make explicit the relationships between them. Then, we define a notion of abstraction, together with natural concepts of soundness and completeness, and we give general transfer properties, which will be central to several verification algorithms on STSs. We further design a generic construction which will be useful for the analysis of ω-regular properties, when a finite attractor exists, either in the system (if it is denumerable), or in a sound denumerable abstraction of the system. We next provide algorithms for qualitative model-checking, and generic approximation procedures for quantitative model-checking. Finally, we instantiate our framework with stochastic timed automata (STA), generalized semi-Markov processes (GSMPs) and stochastic time Petri nets (STPNs), three models combining dense-time and probabilities. This allows us to derive decidability and approximability results for the verification of these models. Some of these results were known from the literature, but our generic approach permits to view them in a unified framework, and to obtain them with less effort. We also derive interesting new approximability results for STA, GSMPs and STPNs.}
}
@inproceedings{B-fossacs18,
  address = {Thessaloniki, Greece},
  month = apr,
  year = 2018,
  volume = {10803},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Baier, Christel and {Dal Lago}, Ugo},
  acronym = {{FoSSaCS}'18},
  booktitle = {{P}roceedings of the 21st {I}nternational
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'18)},
  author = {Bouyer, Patricia},
  title = {Games on graphs with a public signal monitoring},
  pages = {530-547},
  url = {https://arxiv.org/abs/1710.07163},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/B-fossacs18.pdf},
  doi = {10.1007/978-3-319-89366-2_29},
  abstract = {We study Nash equilibria in games on graphs with an imperfect monitoring based on a public signal. In such games, deviations and players responsible for those deviations can be hard to detect and track. We propose a generic epistemic game abstraction, which conveniently allows to represent the knowledge of the players about these deviations, and give a characterization of Nash equilibria in terms of winning strategies in the abstraction. We then use the abstraction to develop algorithms for some payoff functions.}
}
@inproceedings{BBM-fsttcs19,
  address = {Bombay, India},
  month = dec,
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Arkadev Chattopadhyay and Paul Gastin},
  acronym = {{FSTTCS}'19},
  booktitle = {{P}roceedings of the 39th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'19)},
  author = {Nathalie Bertrand and Patricia Bouyer and Anirban Majumdar},
  title = {Concurrent parameterized games},
  pages = {31:1-31:15},
  year = 2019,
  doi = {10.4230/LIPIcs.FSTTCS.2019.31},
  pdf = {https://drops.dagstuhl.de/opus/volltexte/2019/11593/pdf/LIPIcs-FSTTCS-2019-31.pdf},
  url = {https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11593},
  abstract = {Traditional concurrent games on graphs involve a fixed number of players, who take decisions simultaneously, determining the next state of the game. In this paper, we introduce a parameterized variant of concurrent games on graphs, where the parameter is precisely the number of players. Parameterized concurrent games are described by finite graphs, in which the transitions bear regular languages to describe the possible move combinations that lead from one vertex to another. We consider the problem of determining whether the first player, say Eve, has a strategy to ensure a reachability objective against any strategy profile of her opponents as a coalition. In particular Eve's strategy should be independent of the number of opponents she actually has. Technically, this paper focuses on an a priori simpler setting where the languages labeling transitions only constrain the number of opponents (but not their precise action choices). These constraints are described as semilinear sets, finite unions of intervals, or intervals. We establish the precise complexities of the parameterized reachability game problem, ranging from PTIME-complete to PSPACE-complete, in a variety of situations depending on the contraints (semilinear predicates, unions of intervals, or intervals) and on the presence or not of non-determinism.}
}
@inproceedings{BT-mfcs19,
  address = {Aachen, Germany},
  month = aug,
  volume = {138},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Pinar Heggernes and Joost-Pieter Katoen and Peter Rossmanith},
  acronym = {{MFCS}'19},
  booktitle = {{P}roceedings of the 42nd
               {I}nternational {S}ymposium on
               {M}athematical {F}oundations of 
               {C}omputer {S}cience
               ({MFCS}'19)},
  author = {Patricia Bouyer and Nathan Thomasset},
  title = {Nash equilibria in games over graphs equipped with a communication mechanism},
  pages = {9:1-9:14},
  year = 2019,
  doi = {10.4230/LIPIcs.MFCS.2019.9},
  pdf = {http://drops.dagstuhl.de/opus/volltexte/2019/10953/pdf/LIPIcs-MFCS-2019-9.pdf},
  url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=10953}
}
@inproceedings{BBM-concur19,
  address = {Amsterdam, The Netherlands},
  month = aug,
  volume = {140},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Wan Fokkink and Rob {van Glabbeek}},
  acronym = {{CONCUR}'19},
  booktitle = {{P}roceedings of the 30th
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'19)},
  author = {Nathalie Bertrand and Patricia Bouyer and Anirban Majumdar},
  title = {Reconfiguration and message losses in parameterized broadcast networks},
  pages = {32:1-32:15},
  year = 2019,
  doi = {10.4230/LIPIcs.CONCUR.2019.32},
  pdf = {http://drops.dagstuhl.de/opus/volltexte/2019/10934/pdf/LIPIcs-CONCUR-2019-32.pdf},
  url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=10934}
}
@article{GBM-tocsys19,
  publisher = {Springer},
  journal = {Theory of Computing Systems},
  author = {Gardy, Patrick and Bouyer, Patricia and Markey, Nicolas},
  title = {Dependences in Strategy Logic},
  volume = {64},
  number = {3},
  year = 2020,
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GBM-tocsys19.pdf},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GBM-tocsys19.pdf}
}
@inproceedings{BKMMMP-ijcai19,
  futureaddress = {},
  month = jul,
  publisher = {IJCAI organization},
  editor = {Kraus, Sarit},
  acronym = {{IJCAI}'19},
  booktitle = {{P}roceedings of the 28th {I}nternational {J}oint 
               {C}onference on {A}rtificial {I}ntelligence
               ({IJCAI}'19)},
  author = {Bouyer, Patricia and Kupferman, Orna and Markey, Nicolas and Maubert, Bastien and Murano, Aniello and Perelli, Giuseppe},
  title = {Reasoning about Quality and Fuzziness of Strategic Behaviours},
  pages = {1588-1594},
  year = 2019,
  doi = {10.24963/ijcai.2019/220},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKMMMP-ijcai19.pdf},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKMMMP-ijcai19.pdf}
}
@inproceedings{BBR-fossacs19,
  address = {Prague, Czech Republic},
  month = apr,
  year = 2019,
  volume = {11425},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Boja{\'n}czyk, Mikolaj and Simpson, Alex},
  acronym = {{FoSSaCS}'19},
  booktitle = {{P}roceedings of the 22nd {I}nternational
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'19)},
  author = {Benedikt Bollig and Patricia Bouyer and Fabian Reiter},
  title = {Identifiers in Registers - Describing Network Algorithms with Logic},
  pages = {115-132},
  url = {https://arxiv.org/abs/1811.08197},
  pdf = {https://arxiv.org/pdf/1811.08197.pdf},
  doi = {10.1007/978-3-030-17127-8},
  abstract = {We propose a formal model of distributed computing based on register automata
that captures a broad class of synchronous network algorithms. The local memory
of each process is represented by a finite-state controller and a fixed number
of registers, each of which can store the unique identifier of some process in
the network. To underline the naturalness of our model, we show that it has the
same expressive power as a certain extension of first-order logic on graphs
whose nodes are equipped with a total order. Said extension lets us define new
functions on the set of nodes by means of a so-called partial fixpoint
operator. In spirit, our result bears close resemblance to a classical theorem
of descriptive complexity theory that characterizes the complexity class PSPACE
in terms of partial fixpoint logic (a proper superclass of the logic we
consider here).}
}
@inproceedings{BBBFS-gandalf20,
  address = {Brussels, Belgium},
  month = sep,
  series = {Electronic Proceedings in Theoretical Computer Science},
  editor = {Bresolin, Davide and Raskin, Jean-Fran\c{c}ois},
  acronym = {{GandALF}'20},
  booktitle = {{P}roceedings of the 11th {I}nternational {S}ymposium
                on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification
                  ({GandALF}'20)},
  author = {B{\'e}atrice B{\'e}rard and
               Benedikt Bollig and
               Patricia Bouyer and
               Matthias F{\"u}gger and
               Nathalie Sznajder},
  title = {Synthesis in Presence of Dynamic Links},
  year = {2020},
  note = {To appear}
}
@inproceedings{BLORV-concur20,
  address = {Vienna, Austria},
  month = sep,
  volume = {171},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Igor Konnov and Laura Kovacs},
  acronym = {{CONCUR}'20},
  booktitle = {{P}roceedings of the 31st
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'20)},
  author = {Bouyer, Patricia and Le Roux, St{\'e}phane and Oualhadj, Youssouf and Randour, Mickael and Vandenhove, Pierre},
  title = {Games Where You Can Play Optimally with Arena-Independent Finite Memory},
  optpages = {},
  nolsvdate-upd = 20200630,
  year = 2020,
  note = {To appear},
  abstract = {}
}
@inproceedings{B-atva19,
  address = {Taipei, Taiwan},
  month = oct,
  volume = {11781},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Yu{-}Fang Chen and Chih{-}Hong Cheng and Javier Esparza},
  acronym = {{ATVA}'19},
  booktitle = {{P}roceedings of the 17th {I}nternational
               {S}ymposium on {A}utomated {T}echnology
               for {V}erification and {A}nalysis
               ({ATVA}'19)},
  author = {Patricia Bouyer},
  title = {{A Note on Game Theory and Verification (Invited Talk)}},
  pages = {3-22},
  doi = {10.1007/978-3-030-31784-3_1},
  year = 2019
}
@inproceedings{B-time19,
  address = {M{\'{a}}laga, Spain},
  month = oct,
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Johann Gamper and Sophie Pinchinat and Guido Sciavicco},
  acronym = {{TIME}'19},
  booktitle = {{P}roceedings of the 26th {I}nternational {S}ymposium on 
	       {T}emporal {R}epresentation and {R}easoning
	       ({TIME}'19)},
  author = {Patricia Bouyer},
  title = {{On the Computation of Nash Equilibria in Games on Graphs (Invited Talk)}},
  pages = {3:1-3:3},
  doi = {10.4230/LIPIcs.TIME.2019.3},
  year = 2019
}

This file was generated by bibtex2html 1.98.