Nicolas Markey

Résumé

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

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

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

Résumé

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

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

@incollection{ces2009-CM,
  author =              {Cassez, Franck and Markey, Nicolas},
  title =               {Control of Timed Systems},
  editor =              {Jard, Claude and Roux, Olivier H.},
  booktitle =           {Communicating Embedded Systems~-- Software and
                         Design},
  publisher =           {Wiley-ISTE},
  pages =               {83-120},
  chapter =             {3},
  year =                {2009},
  month =               oct,
  url =                 {http://www.iste.co.uk/index.php?f=x&ACTION=View&id=288},
}

@book{AB09-CCMA,
  author =              {Arora, Sanjeev and Barak, Boaz},
  title =               {Computational Complexity: A~Modern Approach},
  publisher =           {Cambridge University Press},
  year =                {2009},
}

@inproceedings{fossacs2009-AD,
  author =              {Antonopoulos, Timos and Dawar, Anuj},
  title =               {Separating Graph Logic from~{MSO}},
  editor =              {de Alfaro, Luca},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'09)},
  acronym =             {{FoSSaCS}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5504},
  pages =               {63-77},
  year =                {2009},
  month =               mar,
}

@inproceedings{fossacs2009-ADMW,
  author =              {Alur, Rajeev and Degorre, Aldric and Maler, Oded and
                         Weiss, Gera},
  title =               {On Omega-Languages Defined by Mean-Payoff
                         Conditions},
  editor =              {de Alfaro, Luca},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'09)},
  acronym =             {{FoSSaCS}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5504},
  year =                {2009},
  month =               mar,
  doi =                 {10.1007/978-3-642-00596-1_24},
}

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

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

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

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

@inproceedings{fmcad2009-BGHJ,
  author =              {Bloem, Roderick and Greimel, Karin and Henzinger,
                         Thomas A. and Jobstmann, Barbara},
  title =               {Synthesizing robust systems},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference on {F}ormal {M}ethods in
                         {C}omputer-{A}ided {D}esign ({FMCAD}'09)},
  acronym =             {{FMCAD}'09},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {85-92},
  year =                {2009},
  month =               nov,
}

@phdthesis{bherer09,
  author =              {Bherer, Hans},
  title =               {Controller Synthesis for Parameterized Discrete
                         Event Systems},
  year =                {2009},
  school =              {Universit{\'e} Laval, Qu\'ebec, Canada},
}

@article{fundi92(1-2)-BHR,
  author =              {Bouyer, Patricia and Haddad, Serge and Reynier,
                         Pierre-Alain},
  title =               {Undecidability Results for Timed Automata with
                         Silent Transitions},
  publisher =           {IOS Press},
  journal =             {Fundamenta Informaticae},
  volume =              {92},
  number =              {1-2},
  pages =               {1-25},
  year =                {2009},
}

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

@article{tcs410(36)-BMI,
  author =              {Busch, Costas and Magdon{-}Ismail, Malik},
  title =               {Atomic routing games on maximum congestion},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {410},
  number =              {36},
  pages =               {3337-3347},
  year =                {2009},
  month =               aug,
  doi =                 {10.1016/j.tcs.2009.04.015},
}

@inproceedings{cdc2009-Cas,
  author =              {Cassez, Franck},
  title =               {A~note on fault diagnosis algorithms},
  booktitle =           {{P}roceedings of the 48th {IEEE} {C}onference on
                         {D}ecision and {C}ontrol ({CDC}'09)},
  acronym =             {{CDC}'09},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {6941-6946},
  year =                {2009},
  month =               dec,
  doi =                 {10.1109/CDC.2009.5399968},
}

@article{cacm52(11)-CES,
  author =              {Clarke, Edmund M. and Emerson, E. Allen and Sifakis,
                         Joseph},
  title =               {Model checking: algorithmic verification and
                         debugging},
  publisher =           {ACM Press},
  journal =             {Communications of the ACM},
  volume =              {52},
  number =              {11},
  pages =               {74-84},
  year =                {2009},
  month =               nov,
  doi =                 {10.1145/1592761.1592781},
}

@phdthesis{phd-chamuczynski09,
  author =              {Patryk Chamuczy{\'n}ski},
  title =               {Algorithms and data structures for parametric
                         analysis of real time systems},
  year =                {2009},
  school =              {University of G{\"o}ttingen, Germany},
  type =                {Th\`ese de doctorat},
}

@inproceedings{hscc2009-CJLRR,
  author =              {Cassez, Franck and Jensen, Jan J. and Larsen, Kim
                         Guldstrand and Raskin, Jean-Fran{\c c}ois and
                         Reynier, Pierre-Alain},
  title =               {Automatic Synthesis of Robust and Optimal
                         Controllers~-- An~Industrial Case Study},
  editor =              {Majumdar, Rupak and Tabuada, Paulo},
  booktitle =           {{P}roceedings of the 12th {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
                         ({HSCC}'09)},
  acronym =             {{HSCC}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5469},
  pages =               {90-104},
  year =                {2009},
  month =               apr,
  doi =                 {10.1007/978-3-642-00602-9_7},
}

@article{jlc19(6)-DG,
  author =              {Demri, St{\'e}phane and Gascon, R{\'e}gis},
  title =               {The Effects of Bounding Syntactic Resources on
                         {P}resburger~{LTL}},
  publisher =           {Oxford University Press},
  journal =             {Journal of Logic and Computation},
  volume =              {19},
  number =              {6},
  pages =               {1541-1575},
  year =                {2009},
  month =               dec,
  doi =                 {10.1093/logcom/exp037},
}

@article{siamcomp39(1)-DGP,
  author =              {Daskalakis, Constantinos and Goldberg, Paul W. and
                         Papadimitriou, {\relax Ch}ristos H.},
  title =               {The complexity of computing a {N}ash equilibrium},
  publisher =           {Society for Industrial and Applied Math.},
  journal =             {SIAM Journal on Computing},
  volume =              {39},
  number =              {1},
  pages =               {195-259},
  year =                {2009},
}

@techreport{CFV-2009-121-DGR,
  author =              {Doyen, Laurent and Gentilini, Raffaella and Raskin,
                         Jean-Fran{\c c}ois},
  title =               {Faster Pseudo-Polynomial Algorithms for Mean-Payoff
                         Games},
  number =              {2009-121},
  year =                {2009},
  institution =         {CFV},
  type =                {Technical Report},
}

@inproceedings{formats2009-DGRR,
  author =              {Doyen, Laurent and Geeraerts, Gilles and Raskin,
                         Jean-Fran{\c c}ois and Reichert, Julien},
  title =               {Realizability of Real-Time Logics},
  editor =              {Ouaknine, Jo{\"e}l and Vaandrager, Frits},
  booktitle =           {{P}roceedings of the 7th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'09)},
  acronym =             {{FORMATS}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5813},
  pages =               {133-148},
  year =                {2009},
  month =               sep,
}

@inproceedings{icalp2009-DKL,
  author =              {Dax, Christian and Klaedtke, Felix and Lange,
                         Martin},
  title =               {On Regular Temporal Logics with Past},
  editor =              {Albers, Susanne and Marchetti{-}Spaccamela Alberto
                         and Matias, Yossi and Nikoletseas, Sotiris and
                         Thomas, Wolfgang},
  booktitle =           {{P}roceedings of the 36th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'09)~-- Part~{II}},
  acronym =             {{ICALP}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5556},
  pages =               {175-187},
  year =                {2009},
  month =               jul,
  doi =                 {10.1007/978-3-642-02930-1_15},
}

@book{hwa-DKV,
  title =               {Handbook of Weighted Automata},
  editor =              {Droste, Manfred and Kuich, Werner and Vogler,
                         Walter},
  booktitle =           {Handbook of Weighted Automata},
  publisher =           {Springer-Verlag},
  year =                {2009},
}

@incollection{mbdes2009-DLRS,
  author =              {David, Alexandre and Larsen, Kim Guldstrand and
                         Rasmussen, Jacob Illum and Skou, Arne},
  title =               {Model-based framework for schedulability analysis
                         using UPPAAL~4.1},
  editor =              {Nicolescu, Gabriela and Mosterman, Pieter J.},
  booktitle =           {Model-Based Design for Embedded Systems},
  publisher =           {CRC Press},
  series =              {Computational Analysis, Synthesis, and Design of
                         Dynamic Systems},
  pages =               {93-119},
  year =                {2009},
}

@article{tcs410(4-5)-ER,
  author =              {Ehrenfeucht, Andrzej and Rozenberg, Grzegorz},
  title =               {Introducing Time in Reaction Systems},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {410},
  number =              {4-5},
  year =                {2009},
  month =               feb,
  doi =                 {10.1016/j.tcs.2008.09.043},
}

@inproceedings{cav2009-FJR,
  author =              {Filiot, Emmanuel and Jin, Naiyong and Raskin,
                         Jean-Fran{\c c}ois},
  title =               {An Antichain Algorithm for {LTL} Realizability},
  editor =              {Bouajjani, Ahmed and Maler, Oded},
  booktitle =           {{P}roceedings of the 21st {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'09)},
  acronym =             {{CAV}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5643},
  pages =               {263-277},
  year =                {2009},
  month =               jun,
}

@article{tcs410(36)-FKKMS,
  author =              {Fotakis, Dimitris and Kontogiannis, Spyros and
                         Koutsoupias, Elias and Mavronicolas, Marios and
                         Spirakis, Paul G.},
  title =               {The~structure and complexity of Nash equilibria for
                         a selfish routing game},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {410},
  number =              {36},
  pages =               {3305-3326},
  year =                {2009},
  month =               aug,
  doi =                 {10.1016/j.tcs.2008.01.004},
}

@inproceedings{atva2009-FL,
  author =              {Friedmann, Oliver and Lange, Martin},
  title =               {Solving Parity Games in Practice},
  editor =              {Liu, Zhiming and Ravn, Anders P.},
  booktitle =           {{P}roceedings of the 7th {I}nternational {S}ymposium
                         on {A}utomated {T}echnology for {V}erification and
                         {A}nalysis ({ATVA}'09)},
  acronym =             {{ATVA}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5799},
  pages =               {182-196},
  year =                {2009},
  month =               oct,
  doi =                 {10.1007/978-3-642-04761-9_15},
}

@inproceedings{infinity2008-FL,
  author =              {Fahrenberg, Uli and Larsen, Kim Guldstrand},
  title =               {Discount-optimal infinite Runs in Proced Timed
                         Automata},
  editor =              {Habermehl, Peter and Vojnar, Tom{\'a}{\v s}},
  booktitle =           {{J}oint {P}roceedings of the 8th, 9th, and 10th
                         {I}nternational {W}orkshops on {V}erification of
                         {I}nfinite-{S}tate {S}ystems {(INFINITY}'06-08)},
  acronym =             {{INFINITY}'06-08},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {239},
  pages =               {179-191},
  year =                {2009},
  month =               jul,
}

@inproceedings{memics2209-FLT,
  author =              {Fahrenberg, Uli and Larsen, Kim Guldstrand and
                         Thrane, Claus},
  title =               {A Quantitative Characterization of Weighted {K}ripke
                         Structures in Temporal Logics},
  editor =              {Hlin{\v{e}}n{\'y}, Petr and Maty{\'a}{\v{s}}, Vashek
                         and Vojnar, Tom{\'a}{\v s}},
  booktitle =           {{P}roceedings of the 5th {A}nnual {D}octoral
                         {W}orkshop on {M}athematical and {E}ngineering
                         {M}ethods in {C}omputer {S}cience ({MEMICS}'09)},
  acronym =             {{MEMICS}'09},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {OpenAccess Series in Informatics},
  volume =              {13},
  year =                {2009},
  month =               sep,
}

@article{cacm52(9)-For,
  author =              {Fortnow, Lance},
  title =               {The Status of the {P} versus {NP} Problem},
  publisher =           {ACM Press},
  journal =             {Communications of the ACM},
  volume =              {52},
  number =              {9},
  pages =               {78-86},
  year =                {2009},
  month =               sep,
}

@article{Automatica45(2)-GL,
  author =              {Genc, Sahika and Lafortune, St{\'e}phane},
  title =               {Predictability of event occurrences in
                         partially-observed discrete-event systems},
  publisher =           {Elsevier},
  journal =             {Automatica},
  volume =              {45},
  number =              {2},
  pages =               {301-311},
  year =                {2009},
  month =               feb,
  doi =                 {10.1016/j.automatica.2008.06.022},
}

@inproceedings{cav2009-GS,
  author =              {Gawlitza, Thomas and Seidl, Helmut},
  title =               {Games through Nested Fixpoints},
  editor =              {Bouajjani, Ahmed and Maler, Oded},
  booktitle =           {{P}roceedings of the 21st {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'09)},
  acronym =             {{CAV}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5643},
  pages =               {291-305},
  year =                {2009},
  month =               jun,
  doi =                 {10.1007/978-3-642-02658-4_24},
}

@article{fmsd34(3)-GSZ,
  author =              {Gastin, Paul and Sznajder, Tali and Zeitoun, Marc},
  title =               {Distributed synthesis for well-connected
                         architectures},
  publisher =           {Springer-Verlag},
  journal =             {Formal Methods in System Design},
  volume =              {34},
  number =              {3},
  pages =               {215-237},
  year =                {2009},
  month =               jun,
}

@inproceedings{concur2009-HKOW,
  author =              {Haase, Christoph and Kreutzer, Stephan and Ouaknine,
                         Jo{\"e}l and Worrell, James},
  title =               {Reachability in Succinct and Parametric One-Counter
                         Automata},
  editor =              {Bravetti, Mario and Zavattaro, Gianluigi},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'09)},
  acronym =             {{CONCUR}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5710},
  pages =               {369-383},
  year =                {2009},
  month =               sep,
  doi =                 {10.1007/978-3-642-04081-8_25},
}

@article{jlap78(5)-JBCS,
  author =              {Jaghoori, Mohammad Mahdi and de~Boer, Frank S. and
                         Chothia, Tom and Sirjani, Marjan},
  title =               {Schedulability of asynchronous real-time concurrent
                         objects},
  publisher =           {Elsevier},
  journal =             {Journal of Logic and Algebraic Programming},
  volume =              {78},
  number =              {5},
  pages =               {402-416},
  year =                {2009},
  month =               may,
}

@inproceedings{icalp2009-KF,
  author =              {Kuhtz, Lars and Finkbeiner, Bernd},
  title =               {{LTL} Path Checking is Efficiently Parallelizable},
  editor =              {Albers, Susanne and Marchetti{-}Spaccamela Alberto
                         and Matias, Yossi and Nikoletseas, Sotiris and
                         Thomas, Wolfgang},
  booktitle =           {{P}roceedings of the 36th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'09)~-- Part~{II}},
  acronym =             {{ICALP}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5556},
  pages =               {235-246},
  year =                {2009},
  month =               jul,
}

@article{ejor199(2)-KFS,
  author =              {Kuipers, Jeroen and Flesch, Janos and Schoenmakers,
                         Gijs and Vrieze, Koos},
  title =               {Pure subgame-perfect equilibria in free transition
                         games},
  publisher =           {Elsevier},
  journal =             {European Journal of Operational Research},
  volume =              {199},
  number =              {2},
  pages =               {442-447},
  year =                {2009},
  month =               dec,
}

@article{KP-csr09,
  author =              {Koutsoupias, Elias and Papadimitriou, {\relax
                         Ch}ristos H.},
  title =               {Worst-case equilibria},
  journal =             {Computer Science Review},
  volume =              {3},
  number =              {2},
  pages =               {65-69},
  year =                {2009},
  month =               may,
  doi =                 {10.1016/j.cosrev.2009.04.003},
}

@inproceedings{fsen2009-KRT,
  author =              {Klein, Dominik and Radmacher, Frank G. and Thomas,
                         Wolfgang},
  title =               {The Complexity of Reachability in Randomized
                         Sabotage Games},
  editor =              {Arbab, Farhad and Sirjani, Marjan},
  booktitle =           {{R}evised {S}elected {P}apers of the 3rd
                         {I}nternational {C}onference on {F}undamentals of
                         {S}oftware {E}ngineering ({FSEN}'09)},
  acronym =             {{FSEN}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5961},
  pages =               {162-177},
  year =                {2009},
  month =               apr,
}

@article{fmsd34(3)-KT,
  author =              {Krichen, Moez and Tripakis, Stavros},
  title =               {Conformance testing for real-time systems},
  publisher =           {Springer-Verlag},
  journal =             {Formal Methods in System Design},
  volume =              {34},
  number =              {3},
  pages =               {238-304},
  year =                {2009},
  month =               jun,
  doi =                 {10.1007/s10703-009-0065-1},
}

@inproceedings{emsoft2009-LPT,
  author =              {Lampka, Kai and Perathoner, Simon and Thiele,
                         Lothar},
  title =               {Analytic Real-time Analysis and Timed Automata:
                         A~Hybrid Method for Analyzing Embedded Real-time
                         Systems},
  editor =              {Chakraborty, Samarjit and Halbwachs, Nicolas},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference on {E}mbedded {S}oftware ({EMSOFT}'09)},
  acronym =             {{EMSOFT}'09},
  publisher =           {ACM Press},
  pages =               {107-116},
  year =                {2009},
  month =               oct,
  doi =                 {10.1145/1629335.1629351},
}

@article{jlap78(5)-LS,
  author =              {Leucker, Martin and Schallart, Christian},
  title =               {A brief account of runtime verification},
  publisher =           {Elsevier},
  journal =             {Journal of Logic and Algebraic Programming},
  volume =              {78},
  number =              {5},
  pages =               {293-303},
  year =                {2009},
  month =               may,
  doi =                 {10.1016/j.jlap.2008.08.004},
}

@inproceedings{concur2009-ORW,
  author =              {Ouaknine, Jo{\"e}l and Rabinovich, Alexander and
                         Worrell, James},
  title =               {Time-Bounded Verification},
  editor =              {Bravetti, Mario and Zavattaro, Gianluigi},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'09)},
  acronym =             {{CONCUR}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5710},
  pages =               {496-510},
  year =                {2009},
  month =               sep,
}

@article{moor34(3)-PPT,
  author =              {Penn, Michal and Polukarov, Maria and Tennenholtz,
                         Moshe},
  title =               {Random Order Congestion Games},
  publisher =           {Informs},
  journal =             {Mathematics of Operations Research},
  volume =              {34},
  number =              {3},
  pages =               {706-725},
  year =                {2009},
  month =               aug,
  doi =                 {10.1287/moor.1090.0394},
}

@incollection{hwa-ch12-Rah,
  author =              {Rahonis, George},
  title =               {Fuzzy Languages},
  editor =              {Droste, Manfred and Kuich, Werner and Vogler,
                         Walter},
  booktitle =           {Handbook of Weighted Automata},
  publisher =           {Springer-Verlag},
  pages =               {481-517},
  chapter =             {12},
  year =                {2009},
  doi =                 {10.1007/978-3-642-01492-5 12},
}

@book{mas-SL09,
  author =              {Shoham, Yoav and Leyton-Brown, Kevin},
  title =               {Multiagent Systems~-- Algorithmic, Game-Theoretic,
                         and Logical Foundations},
  publisher =           {Cambridge University Press},
  year =                {2009},
}

@inproceedings{concur2009-SRS,
  author =              {Singh, Anu and Ramakrishnan, C. R. and Smolka, Scott
                         A.},
  title =               {Query-Based Model Checking of Ad~Hoc Network
                         Protocols},
  editor =              {Bravetti, Mario and Zavattaro, Gianluigi},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'09)},
  acronym =             {{CONCUR}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5710},
  pages =               {603-619},
  year =                {2009},
  month =               sep,
  doi =                 {10.1007/978-3-642-04081-8_40},
}

@inproceedings{qfm2009-SZHV,
  author =              {Schuts, Mathijs and Zhu, Yunshan and Heidarian,
                         Faranak and Vaandrager, Frits},
  title =               {Modelling Clock Synchronization in the Chess g{MAC}
                         {WSN} Protocol},
  editor =              {Andova, Suzana and McIver, Annabelle K. and
                         D{'}Argenio, Pedro R. and Cuijpers, Pieter J. L. and
                         Markovski, Jasen and Morgan, Carroll C. and
                         N{\'u}{\~n}ez, Manuel},
  booktitle =           {{P}roceedings of the 1st {W}orkshop on
                         {Q}uantitative {F}ormal {M}ethods: {T}heory and
                         {A}pplications ({QFM}'09)},
  acronym =             {{QFM}'09},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {13},
  pages =               {41-54},
  year =                {2009},
  month =               nov,
}

@article{ipl109(13)-TD,
  author =              {Tian, Cong and Duan, Zhenhua},
  title =               {A~Note on Stutter-Invariant {PLTL}},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {109},
  number =              {13},
  pages =               {663-667},
  year =                {2009},
  month =               jun,
}

@article{tocl10(3)-Tri,
  author =              {Tripakis, Stavros},
  title =               {Checking Timed B{\"{u}}chi Automata Emptiness on
                         Simulation Graphs},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {10},
  number =              {3},
  year =                {2009},
  month =               apr,
  doi =                 {10.1145/1507244.1507245},
}

@inproceedings{csl2009-UW,
  author =              {Ummels, Michael and Wojtczak, Dominik},
  title =               {Decision Problems for {N}ash Equilibria in
                         Stochastic Games},
  editor =              {Gr{\"a}del, Erich and Kahle, Reinhard},
  booktitle =           {{P}roceedings of the 23rd {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'09)},
  acronym =             {{CSL}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5771},
  pages =               {51-530},
  year =                {2009},
  month =               sep,
}

@inproceedings{icalp2009-UW,
  author =              {Ummels, Michael and Wojtczak, Dominik},
  title =               {The Complexity of {N}ash Equilibria in Simple
                         Stochastic Multiplayer Games},
  editor =              {Albers, Susanne and Marchetti{-}Spaccamela Alberto
                         and Matias, Yossi and Nikoletseas, Sotiris and
                         Thomas, Wolfgang},
  booktitle =           {{P}roceedings of the 36th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'09)~-- Part~{II}},
  acronym =             {{ICALP}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5556},
  pages =               {297-308},
  year =                {2009},
  month =               jul,
}

@inproceedings{csl2009-Web,
  author =              {Weber, Michael},
  title =               {On the Complexity of Branching-Time Logics},
  editor =              {Gr{\"a}del, Erich and Kahle, Reinhard},
  booktitle =           {{P}roceedings of the 23rd {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'09)},
  acronym =             {{CSL}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5771},
  pages =               {530-545},
  year =                {2009},
  month =               sep,
}