@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}, futureseries = {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}, year = 2019, note = {To appear}, 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).} }

*This file was generated by
bibtex2html 1.98.*