Nicolas Markey

Résumé

The problems of time-dependent behavior in general, and dynamic resource allocation in particular, pervade many aspects of modern life. Prominent examples range from reliability and efficient use of communication resources in a telecommunication network to the allocation of tracks in a continental railway network, from scheduling the usage of computational resources on a chip for durations of nano-seconds to the weekly, monthly, or longer-range reactive planning in a factory or a supply chain.

@article{cacm54(9)-BFLM,
  author =              {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim
                         Guldstrand and Markey, Nicolas},
  title =               {Quantitative analysis of real-time systems using
                         priced timed automata},
  publisher =           {ACM Press},
  journal =             {Communications of the ACM},
  volume =              {54},
  number =              {9},
  pages =               {78-87},
  year =                {2011},
  month =               sep,
  doi =                 {10.1145/1995376.1995396},
  abstract =            {The problems of time-dependent behavior in general,
                         and dynamic resource allocation in particular,
                         pervade many aspects of modern life. Prominent
                         examples range from reliability and efficient use of
                         communication resources in a telecommunication
                         network to the allocation of tracks in a continental
                         railway network, from scheduling the usage of
                         computational resources on a chip for durations of
                         nano-seconds to the weekly, monthly, or longer-range
                         reactive planning in a factory or a supply chain.},
}

Résumé

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

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

Résumé

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

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

Résumé

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

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

Résumé

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

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

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

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

Résumé

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 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{fsttcs2011-SBM,
  author =              {Sankur, Ocan and Bouyer, Patricia and Markey,
                         Nicolas},
  title =               {Shrinking Timed Automata},
  editor =              {Chakraborty, Supratik and Kumar, Amit},
  booktitle =           {{P}roceedings of the 31st {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'11)},
  acronym =             {{FSTTCS}'11},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {13},
  pages =               {90-102},
  year =                {2011},
  month =               dec,
  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.},
}

Résumé

We review several aspects of robustness of real-time systems, and present recent results on the robust verification of timed automata.

@inproceedings{sies2011-Mar,
  author =              {Markey, Nicolas},
  title =               {Robustness in Real-time Systems},
  booktitle =           {{P}roceedings of the 6th {IEEE} {I}nternational
                         {S}ymposium on {I}ndustrial {E}mbedded {S}ystems
                         ({SIES}'11)},
  acronym =             {{SIES}'11},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {28-34},
  year =                {2011},
  month =               jun,
  doi =                 {10.1109/SIES.2011.5953652},
  abstract =            {We~review several aspects of robustness of real-time
                         systems, and present recent results on the robust
                         verification of timed automata.},
}

@phdthesis{hdr2011-Mar,
  author =              {Markey, Nicolas},
  title =               {Verification of Embedded Systems -- Algorithms and
                         Complexity},
  year =                {2011},
  month =               apr,
  school =              {{\'E}cole Normale Sup{\'e}rieure de Cachan, France},
  type =                {M\'emoire d'habilitation},
}

@book{AG-gt4cs11,
  author =              {Apt, Krzysztof and Gr{\"a}del, Erich},
  title =               {Lectures in Game Theory for Computer Scientists},
  publisher =           {Cambridge University Press},
  year =                {2011},
}

@inproceedings{atva2011-BBDDR,
  author =              {Brihaye, {\relax Th}omas and Bruy{\`e}re,
                         V{\'e}ronique and Doyen, Laurent and Ducobu, Marc
                         and Raskin, Jean-Fran{\c c}ois},
  title =               {Antichain-based {QBF} Solving},
  editor =              {Bultan, Tevfik and Hsiung, Pao-Ann},
  booktitle =           {{P}roceedings of the 9th {I}nternational {S}ymposium
                         on {A}utomated {T}echnology for {V}erification and
                         {A}nalysis ({ATVA}'11)},
  acronym =             {{ATVA}'11},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6996},
  pages =               {183-197},
  year =                {2011},
  month =               oct,
}

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

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

@inproceedings{icalp2011(2)-BDGORW,
  author =              {Brihaye, {\relax Th}omas and Doyen, Laurent and
                         Geeraerts, Gilles and Ouaknine, Jo{\"e}l and Raskin,
                         Jean-Fran{\c c}ois and Worrell, James},
  title =               {On Reachability for Hybrid Automata over Bounded
                         Time},
  editor =              {Aceto, Luca and Henzinger, Monika and Sgall, Ji{\v
                         r}{\'\i}},
  booktitle =           {{P}roceedings of the 38th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'11)~-- Part~{II}},
  acronym =             {{ICALP}'11},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6756},
  pages =               {416-427},
  year =                {2011},
  month =               jul,
}

@article{spe41(2)-ADGPY,
  author =              {Behrmann, Gerd and David, Alexandre and Larsen, Kim
                         Guldstrand and Pettersson, Paul and Yi, Wang},
  title =               {Developing {UPPAAL} over 15~years},
  publisher =           {IEEE Comp. Soc. Press},
  journal =             {Software~-- Practice and Experience},
  volume =              {41},
  number =              {2},
  pages =               {133-142},
  year =                {2011},
  month =               feb,
}

@article{alga61(2)-BFFM,
  author =              {Bil{\`o}, Vittorio and Fanelli, Angelo and Flammini,
                         Michele and Moscardelli, Luca},
  title =               {Graphical congestion games},
  publisher =           {Springer-Verlag},
  journal =             {Algorithmica},
  volume =              {61},
  number =              {2},
  pages =               {274-297},
  year =                {2011},
  month =               oct,
  doi =                 {10.1007/s00453-010-9417-x},
}

@inproceedings{fsttcs2011-BG,
  author =              {Bertrand, Nathalie and Genest, Blaise},
  title =               {Minimal Disclosure in {P}artially {O}bservable
                         {M}arkov {D}ecision {P}rocesses},
  editor =              {Chakraborty, Supratik and Kumar, Amit},
  booktitle =           {{P}roceedings of the 31st {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'11)},
  acronym =             {{FSTTCS}'11},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {13},
  pages =               {411-422},
  year =                {2011},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2011.411},
}

@inproceedings{concur2011-BKK,
  author =              {Baier, {\relax Ch}ristel and Klein, Joachim and
                         Kl{\"u}ppelholz, Sascha},
  title =               {A Compositional Framework for Controller Synthesis},
  editor =              {Katoen, Joost-Pieter and K{\"o}nig, Barbara},
  booktitle =           {{P}roceedings of the 22nd {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'11)},
  acronym =             {{CONCUR}'11},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6901},
  pages =               {512-527},
  year =                {2011},
  month =               sep,
}

@inproceedings{fsttcs2011-BKP,
  author =              {Berwanger, Dietmar and Kaiser, {\L}ukasz and
                         Puchala, Bernd},
  title =               {A~Perfect-Information Construction for Coordination
                         in Games},
  editor =              {Chakraborty, Supratik and Kumar, Amit},
  booktitle =           {{P}roceedings of the 31st {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'11)},
  acronym =             {{FSTTCS}'11},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {13},
  pages =               {387-398},
  year =                {2011},
  month =               dec,
}

@book{mso-CE11,
  author =              {Courcelle, Bruno and Engelfriet, Joost},
  title =               {Graph Structure and Monadic Second-Order Logic, a
                         Language Theoretic Approach},
  publisher =           {Cambridge University Press},
  year =                {2011},
}

@article{lmcs7(4)-CHP,
  author =              {Chatterjee, Krishnendu and Henzinger, Thomas A. and
                         Prabhu, Vinayak S.},
  title =               {Timed Parity Games: Complexity and Robustness},
  journal =             {Logical Methods in Computer Science},
  volume =              {7},
  number =              {4},
  year =                {2011},
  month =               dec,
  doi =                 {10.2168/LMCS-7(4:8)2011},
}

@inproceedings{lics2011-CHS,
  author =              {Carayol, Arnaud and Haddad, Axel and Serre, Olivier},
  title =               {Qualitative Tree Languages},
  booktitle =           {{P}roceedings of the 26th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'11)},
  acronym =             {{LICS}'11},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {13-22},
  year =                {2011},
  month =               jun,
  doi =                 {10.1109/LICS.2011.28},
}

@inproceedings{adaeurope2011-CLPV,
  author =              {Carnevali, Laura and Lipari, Giuseppe and Pinzuti,
                         Alessandro and Vicario, Enrico},
  title =               {A Formal Approach to Design and Verification of
                         Two-Level Hierarchical Scheduling Systems},
  editor =              {Romanovsky, Alexander and Vardanega, Tullio},
  booktitle =           {Proceedings of the 16th {A}da-{E}urope
                         {I}nternational {C}onference on {R}eliable
                         {S}oftware {T}echnologies ({ADA-EUROPE}'11)},
  acronym =             {{ADA-EUROPE}'11},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6652},
  pages =               {118-131},
  year =                {2011},
  confyear =            {2011},
  confmonth =           {6},
}

@phdthesis{phd-dacosta,
  author =              {Da{~}Costa, Arnaud},
  title =               {Propri{\'e}t{\'e}s de jeux multi-agents},
  year =                {2011},
  month =               sep,
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {Th\`ese de doctorat},
}

@inproceedings{formats2011-DLLMPVW,
  author =              {David, Alexandre and Larsen, Kim Guldstrand and
                         Legay, Axel and Miku{\v{c}}ionis, Marius and
                         Poulsen, Danny B{\o}gsted and van Vliet, Jonas and
                         Wang, Zheng},
  title =               {Statistical Model Checking for Networks of Priced
                         Timed Automata},
  editor =              {Fahrenberg, Uli and Tripakis, Stavros},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'11)},
  acronym =             {{FORMATS}'11},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6919},
  pages =               {80-96},
  year =                {2011},
  month =               sep,
}

@inproceedings{cav2011-DLLMW,
  author =              {David, Alexandre and Larsen, Kim Guldstrand and
                         Legay, Axel and Miku{\v{c}}ionis, Marius and Wang,
                         Zheng},
  title =               {Time for Statistical Model Checking of Real-Time
                         Systems},
  editor =              {Gopalakrishnan, Ganesh and Qadeer, Shaz},
  booktitle =           {{P}roceedings of the 23rd {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'11)},
  acronym =             {{CAV}'11},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6806},
  pages =               {349-355},
  year =                {2011},
  month =               jul,
  doi =                 {10.1007/978-3-642-22110-1_27},
}

@inproceedings{mfcs2011-DMS,
  author =              {Doyen, Laurent and Massart, {\relax Th}ierry and
                         Shirmohammadi, Mahsa},
  title =               {Infinite Synchronizing Words for Probabilistic
                         Automata},
  editor =              {Murlak, Filip and Sankovski, Piotr},
  booktitle =           {{P}roceedings of the 36th {I}nternational
                         {S}ymposium on {M}athematical {F}oundations of
                         {C}omputer {S}cience ({MFCS}'13)},
  acronym =             {{MFCS}'11},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6907},
  pages =               {278-289},
  year =                {2011},
  month =               aug,
  doi =                 {10.1007/978-3-642-22993-0_27},
}

@techreport{arxiv11-DT,
  author =              {Dima, C{\u a}t{\u a}lin and {\c T}iplea, Ferucio
                         Lauren{\c t}iu},
  title =               {Model-checking {ATL} under Imperfect Information and
                         Perfect Recall Semantics is Undecidable},
  number =              {1102.4225},
  year =                {2011},
  month =               feb,
  institution =         {arXiv},
  type =                {Research Report},
}

@article{sttt13(5)-Fil,
  author =              {Filli{\^a}tre, Jean-Christophe},
  title =               {Deductive software verification},
  publisher =           {Springer-Verlag},
  journal =             {International Journal on Software Tools for
                         Technology Transfer},
  volume =              {13},
  number =              {5},
  pages =               {397-403},
  year =                {2011},
  month =               oct,
  doi =                 {10.1007/s10009-011-0211-0},
}

@inproceedings{ictac2011-FJLS,
  author =              {Fahrenberg, Uli and Juhl, Line and Larsen, Kim
                         Guldstrand and Srba, Ji{\v r}{\'\i}},
  title =               {Energy Games in Multiweighted Automata},
  editor =              {Cerone, Antonio and Pihlajasaari, Pekka},
  booktitle =           {{P}roceedings of the 8th {I}nternational
                         {C}olloquium on {T}heoretical {A}spects of
                         {C}omputing ({ICTAC}'11)},
  acronym =             {{ICTAC}'11},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6916},
  pages =               {95-115},
  year =                {2011},
  month =               aug,
  doi =                 {10.1007/978-3-642-23283-1_9},
}

@inproceedings{fsttcs2011-FLT,
  author =              {Fahrenberg, Uli and Legay, Axel and Thrane, Claus},
  title =               {The Quantitative Linear-Time--Branching-Time
                         Spectrum},
  editor =              {Chakraborty, Supratik and Kumar, Amit},
  booktitle =           {{P}roceedings of the 31st {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'11)},
  acronym =             {{FSTTCS}'11},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {13},
  year =                {2011},
  month =               dec,
}

@inproceedings{csl2011-FLZ,
  author =              {Fridman, Wladimir and L{\"o}ding, Christof and
                         Zimmermann, Martin},
  title =               {Degrees of Lookahead in Context-free Infinite Games},
  editor =              {Bezem, Marc},
  booktitle =           {{P}roceedings of the 25th {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'11)},
  acronym =             {{CSL}'11},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {12},
  pages =               {264-276},
  year =                {2011},
  month =               sep,
}

@inproceedings{formats2011-GRS,
  author =              {Geeraerts, Gilles and Raskin, Jean-Fran{\c c}ois and
                         Sznajder, Tali},
  title =               {Event-clock automata: form theory to practice},
  editor =              {Fahrenberg, Uli and Tripakis, Stavros},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'11)},
  acronym =             {{FORMATS}'11},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6919},
  pages =               {209-224},
  year =                {2011},
  month =               sep,
  doi =                 {10.1007/978-3-642-24310-3_15},
}

@inproceedings{gandalf2011-GRT,
  author =              {Gr{\"u}ner, Sten and Radmacher, Frank G. and Thomas,
                         Wolfgang},
  title =               {Connectivity Games over Dynamic Networks},
  editor =              {D{'}Agostino, Giovanna and La{~}Torre, Salvatore},
  booktitle =           {{P}roceedings of the 2nd {I}nternational {S}ymposium
                         on {G}ames, {A}utomata, {L}ogics and {F}ormal
                         {V}erification ({GandALF}'11)},
  acronym =             {{GandALF}'11},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {54},
  pages =               {131-145},
  year =                {2011},
  month =               jun,
}

@inproceedings{fsttcs11-Hag,
  author =              {Hague, Matthew},
  title =               {Parameterised Pushdown Systems with Non-Atomic
                         Writes},
  editor =              {Chakraborty, Supratik and Kumar, Amit},
  booktitle =           {{P}roceedings of the 31st {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'11)},
  acronym =             {{FSTTCS}'11},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {13},
  pages =               {457-468},
  year =                {2011},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2011.457},
}

@inproceedings{fsttcs2011-HKSW,
  author =              {Herbreteau, Fr{\'e}d{\'e}ric and Kini, Dileep and
                         Srivathsan, B. and Walukiewicz, Igor},
  title =               {Using non-convex approximations for efficient
                         analysis of timed automata},
  editor =              {Chakraborty, Supratik and Kumar, Amit},
  booktitle =           {{P}roceedings of the 31st {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'11)},
  acronym =             {{FSTTCS}'11},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {13},
  pages =               {78-89},
  year =                {2011},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2011.78},
}

@article{tcs412(39)-HMRT,
  author =              {Hoefer, Martin and Mirrokni, Vahab S. and
                         R{\"{o}}glin, Heiko and Teng, Shang-Hua},
  title =               {Competitive routing over time},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {412},
  number =              {39},
  pages =               {5420-5432},
  year =                {2011},
  month =               sep,
  doi =                 {10.1016/j.tcs.2011.05.055},
}

@inproceedings{fossacs2011-JR,
  author =              {Jaubert, R{\'e}mi and Reynier, Pierre-Alain},
  title =               {Quantitative Robustness Analysis of Flat Timed
                         Automata},
  editor =              {Hofmann, Martin},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'11)},
  acronym =             {{FoSSaCS}'11},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6604},
  pages =               {229-244},
  year =                {2011},
  month =               mar,
}

@article{tocsys49(1)-ks,
  author =              {Koch, Ronald and Skutella, Martin},
  title =               {{N}ash equilibria and the price of anarchy for flows
                         over time},
  publisher =           {Springer-Verlag},
  journal =             {Theory of Computing Systems},
  volume =              {49},
  number =              {1},
  pages =               {71-97},
  year =                {2011},
  month =               jul,
  doi =                 {10.1007/s00224-010-9299-y},
}

@inproceedings{csl2011-Mad,
  author =              {Madhusudan, Parthasarathy},
  title =               {Synthesizing Reactive Programs},
  editor =              {Bezem, Marc},
  booktitle =           {{P}roceedings of the 25th {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'11)},
  acronym =             {{CSL}'11},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {12},
  pages =               {428-442},
  year =                {2011},
  month =               sep,
}

@inproceedings{fase2011-PHP,
  author =              {Post, Amalinda and Hoenicke, Jochen and Podelski,
                         Andreas},
  title =               {RT-Inconsistency: A~New Property for Real-Time
                         Requirements},
  editor =              {Giannakopoulou, Dimitra and Orejas, Fernando},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onference on {F}undamental {A}pproaches to
                         {S}oftware {E}ngineering ({FASE}'11)},
  acronym =             {{FASE}'11},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6603},
  pages =               {34-49},
  year =                {2011},
  month =               mar,
  doi =                 {978-3-642-19811-3_4},
}

@inproceedings{concur2011-PS,
  author =              {Pandya, Paritosh K. and Shah, Simoni S.},
  title =               {On Expressive Powers of Timed Logics: Comparing
                         Boundedness, Non-punctuality, and Deterministic
                         Freezing},
  editor =              {Katoen, Joost-Pieter and K{\"o}nig, Barbara},
  booktitle =           {{P}roceedings of the 22nd {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'11)},
  acronym =             {{CONCUR}'11},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6901},
  pages =               {60-75},
  year =                {2011},
  month =               sep,
  doi =                 {10.1007/978-3-642-23217-6_5},
}

@article{fmsd38(3)-quaas,
  author =              {Quaas, Karin},
  title =               {{MSO} logics for weighted timed automata},
  publisher =           {Springer-Verlag},
  journal =             {Formal Methods in System Design},
  volume =              {38},
  number =              {3},
  pages =               {193-222},
  year =                {2011},
  month =               jun,
  doi =                 {10.1007/s10703-011-0112-6},
}

@inproceedings{lata2011-quaas,
  author =              {Quaas, Karin},
  title =               {On the Interval-Bound Problem for Weighted Timed
                         Automata},
  editor =              {Dediu, Adrian Horia and Inenaga, Shunsuke and
                         Mart{\'\i}n-Vide, Carlos},
  booktitle =           {{P}roceedings of the 5th {I}nternational
                         {C}onference on {L}anguage and {A}utomata {T}heory
                         and {A}pplications ({LATA}'11)},
  acronym =             {{LATA}'11},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6638},
  pages =               {452-464},
  year =                {2011},
  month =               may,
}

@inproceedings{qapl2011-Rut,
  author =              {Rutkowski, Micha{\l}},
  title =               {Two-Player Reachability-Price Games on Single-Clock
                         Timed Automata},
  booktitle =           {{P}roceedings of the 9th {W}orkshop on
                         {Q}uantitative {A}spects of {P}rogramming
                         {L}anguages ({QAPL}'11)},
  acronym =             {{QAPL}'11},
  publisher =           {Massink, Mieke and Norman, Gethin},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {57},
  pages =               {31-46},
  year =                {2011},
  month =               apr,
}

@inproceedings{fmcad2011-SB,
  author =              {Somenzi, Fabio and Bradley, Steven},
  title =               {{IC3:} where monolithic and incremental meet},
  booktitle =           {{P}roceedings of the 11th {I}nternational
                         {C}onference on {F}ormal {M}ethods in
                         {C}omputer-{A}ided {D}esign ({FMCAD}'11)},
  acronym =             {{FMCAD}'11},
  pages =               {3-8},
  year =                {2011},
  month =               oct,
}

@inproceedings{concur2011-WHY,
  author =              {Wang, Farn and Huang, Chung-Hao and Yu, Fang},
  title =               {A~Temporal Logic for the Interaction of Strategies},
  editor =              {Katoen, Joost-Pieter and K{\"o}nig, Barbara},
  booktitle =           {{P}roceedings of the 22nd {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'11)},
  acronym =             {{CONCUR}'11},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6901},
  pages =               {466-481},
  year =                {2011},
  month =               sep,
}

@inproceedings{formats2011-WLT,
  author =              {Woehrle, Matthias and Lampka, Kai and Thiele,
                         Lothar},
  title =               {Segmented State Space Traversal for Conformance
                         Testing of Cyber-Physical Systems},
  editor =              {Fahrenberg, Uli and Tripakis, Stavros},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'11)},
  acronym =             {{FORMATS}'11},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6919},
  pages =               {193-208},
  year =                {2011},
  month =               sep,
}

@article{rts47(4)-WYY,
  author =              {Wang, Farn and Yao, Li-Wei and Yang, Ya-Lan},
  title =               {Efficient verification of distributed real-time
                         systems with broadcasting behaviors},
  publisher =           {Kluwer Academic},
  journal =             {Real-Time Systems},
  volume =              {47},
  number =              {4},
  pages =               {285-318},
  year =                {2011},
  month =               jul,
}