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

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

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

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

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

@inproceedings{concur2009-BDMR,
  author =              {Bouyer, Patricia and Duflot, Marie and Markey,
                         Nicolas and Renault, Gabriel},
  title =               {Measuring Permissivity in Finite Games},
  editor =              {Bravetti, Mario and Zavattaro, Gianluigi},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'09)},
  acronym =             {{CONCUR}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5710},
  pages =               {196-210},
  year =                {2009},
  month =               sep,
  doi =                 {10.1007/978-3-642-04081-8_14},
  abstract =            {In this paper, we extend the classical notion of
                         strategies in turn-based finite games by allowing
                         several moves to be selected. We~define and study a
                         quantitative measure for permissivity of such
                         strategies by assigning penalties when blocking
                         transitions. We~prove that for reachability
                         objectives, most permissive strategies exist, can be
                         chosen memoryless, and can be computed in polynomial
                         time, while it is in
                         \(\textsf{NP}\cap\textsf{coNP}\) for discounted and
                         mean penalties.},
}
[CM09] Franck Cassez and Nicolas Markey. Control of Timed Systems. In Claude Jard and Olivier H. Roux (eds.), Communicating Embedded Systems – Software and Design. Wiley-ISTE, October 2009. 
@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},
}
[AB09] Sanjeev Arora and Boaz Barak. Computational Complexity: A Modern Approach. Cambridge University Press, 2009. 
@book{AB09-CCMA,
  author =              {Arora, Sanjeev and Barak, Boaz},
  title =               {Computational Complexity: A~Modern Approach},
  publisher =           {Cambridge University Press},
  year =                {2009},
}
[AD09] Timos Antonopoulos and Anuj Dawar. Separating Graph Logic from MSO. In FoSSaCS'09, Lecture Notes in Computer Science 5504, pages 63-77. Springer-Verlag, March 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,
}
[ADM+09] Rajeev Alur, Aldric Degorre, Oded Maler, and Gera Weiss. On Omega-Languages Defined by Mean-Payoff Conditions. In FoSSaCS'09, Lecture Notes in Computer Science 5504. Springer-Verlag, March 2009. 
@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},
}
[BBB+09] Christel Baier, Nathalie Bertrand, Patricia Bouyer, and Thomas Brihaye. When are timed automata determinizable?. In ICALP'09, Lecture Notes in Computer Science 5556, pages 43-54. Springer-Verlag, July 2009. 
@inproceedings{icalp2009-BBBB,
  author =              {Baier, {\relax Ch}ristel and Bertrand, Nathalie and
                         Bouyer, Patricia and Brihaye, {\relax Th}omas},
  title =               {When are timed automata determinizable?},
  editor =              {Albers, Susanne and Marchetti{-}Spaccamela Alberto
                         and Matias, Yossi and Nikoletseas, Sotiris and
                         Thomas, Wolfgang},
  booktitle =           {{P}roceedings of the 36th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'09)~-- Part~{II}},
  acronym =             {{ICALP}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5556},
  pages =               {43-54},
  year =                {2009},
  month =               jul,
  doi =                 {10.1007/978-3-642-02930-1_4},
}
[BDS+09] Hans Bherer, Jules Desharnais, and Richard St-Denis. Control of Parameterized Discrete Event Systems. Discrete Event Dynamic Systems 19(2):213-165. Kluwer Academic, June 2009. 
@article{deds19(2)-BDSD,
  author =              {Bherer, Hans and Desharnais, Jules and St-Denis,
                         Richard},
  title =               {Control of Parameterized Discrete Event Systems},
  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},
}
[BF09] Patricia Bouyer and Vojtěch Forejt. Reachability in Stochastic Timed Games. In ICALP'09, Lecture Notes in Computer Science 5556, pages 103-114. Springer-Verlag, July 2009. 
@inproceedings{icalp2009-BF,
  author =              {Bouyer, Patricia and Forejt, Vojt{\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,
}
[BFH09] Felix Brandt, Felix Fischer, and Markus Holzer. Symmetries and the complexity of pure Nash equilibrium. Journal of Computer and System Sciences 75(3):163-177. Elsevier, May 2009. 
@article{jcss75(3)-BFH,
  author =              {Brandt, Felix and Fischer, Felix and Holzer, Markus},
  title =               {Symmetries and the complexity of pure {N}ash
                         equilibrium},
  publisher =           {Elsevier},
  journal =             {Journal of Computer and System Sciences},
  volume =              {75},
  number =              {3},
  pages =               {163-177},
  year =                {2009},
  month =               may,
}
[BGH+09] Roderick Bloem, Karin Greimel, Thomas A. Henzinger, and Barbara Jobstmann. Synthesizing robust systems. In FMCAD'09, pages 85-92. IEEE Comp. Soc. Press, November 2009. 
@inproceedings{fmcad2009-BGHJ,
  author =              {Bloem, Roderick and Greimel, Karin and Henzinger,
                         Thomas A. and Jobstmann, Barbara},
  title =               {Synthesizing robust systems},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference on {F}ormal {M}ethods in
                         {C}omputer-{A}ided {D}esign ({FMCAD}'09)},
  acronym =             {{FMCAD}'09},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {85-92},
  year =                {2009},
  month =               nov,
}
[Bhe09] Hans Bherer. Controller Synthesis for Parameterized Discrete Event Systems. PhD thesis, Université Laval, Québec, Canada, 2009. 
@phdthesis{bherer09,
  author =              {Bherer, Hans},
  title =               {Controller Synthesis for Parameterized Discrete
                         Event Systems},
  year =                {2009},
  school =              {Universit{\'e} Laval, Qu\'ebec, Canada},
}
[BHR09] Patricia Bouyer, Serge Haddad, and Pierre-Alain Reynier. Undecidability Results for Timed Automata with Silent Transitions. Fundamenta Informaticae 92(1-2):1-25. IOS Press, 2009. 
@article{fundi92(1-2)-BHR,
  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},
}
[BJS09] Joakim Byg, Kenneth Yrke Jørgensen, and Jiří Srba. TAPAAL: Editor, Simulator and Verifier of Timed-Arc Petri Nets. In ATVA'09, Lecture Notes in Computer Science 5799, pages 84-89. Springer-Verlag, October 2009. 
@inproceedings{atva2009-BJS,
  author =              {Byg, Joakim and J{\o}rgensen, Kenneth Yrke and Srba,
                         Ji{\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},
}
[BM09] Costas Busch and Malik Magdon-Ismail. Atomic routing games on maximum congestion. Theoretical Computer Science 410(36):3337-3347. Elsevier, August 2009. 
@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},
}
[Cas09] Franck Cassez. A note on fault diagnosis algorithms. In CDC'09, pages 6941-6946. IEEE Comp. Soc. Press, December 2009. 
@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},
}
[CES09] Edmund M. Clarke, E. Allen Emerson, and Joseph Sifakis. Model checking: algorithmic verification and debugging. Communications of the ACM 52(11):74-84. ACM Press, November 2009. 
@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},
}
[Cha09] Patryk Chamuczyński. Algorithms and data structures for parametric analysis of real time systems. Thèse de doctorat, University of Göttingen, Germany, 2009. 
@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},
}
[CJL+09] Franck Cassez, Jan J. Jensen, Kim Guldstrand Larsen, Jean-François Raskin, and Pierre-Alain Reynier. Automatic Synthesis of Robust and Optimal Controllers – An Industrial Case Study. In HSCC'09, Lecture Notes in Computer Science 5469, pages 90-104. Springer-Verlag, April 2009. 
@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},
}
[DG09] Stéphane Demri and Régis Gascon. The Effects of Bounding Syntactic Resources on Presburger LTL. Journal of Logic and Computation 19(6):1541-1575. Oxford University Press, December 2009. 
@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},
}
[DGP09] Constantinos Daskalakis, Paul W. Goldberg, and Christos H. Papadimitriou. The complexity of computing a Nash equilibrium. SIAM Journal on Computing 39(1):195-259. Society for Industrial and Applied Math., 2009. 
@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},
}
[DGR09] Laurent Doyen, Raffaella Gentilini, and Jean-François Raskin. Faster Pseudo-Polynomial Algorithms for Mean-Payoff Games. Technical Report 2009-121, CFV, 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},
}
[DGR+09] Laurent Doyen, Gilles Geeraerts, Jean-François Raskin, and Julien Reichert. Realizability of Real-Time Logics. In FORMATS'09, Lecture Notes in Computer Science 5813, pages 133-148. Springer-Verlag, September 2009. 
@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,
}
[DKL09] Christian Dax, Felix Klaedtke, and Martin Lange. On Regular Temporal Logics with Past. In ICALP'09, Lecture Notes in Computer Science 5556, pages 175-187. Springer-Verlag, July 2009. 
@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},
}
[DKV09] Manfred Droste, Werner Kuich, and Walter Vogler. Handbook of Weighted Automata. Springer-Verlag, 2009. 
@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},
}
[DLR+09] Alexandre David, Kim Guldstrand Larsen, Jacob Illum Rasmussen, and Arne Skou. Model-based framework for schedulability analysis using UPPAAL 4.1. In Gabriela Nicolescu and Pieter J. Mosterman (eds.), Model-Based Design for Embedded Systems, Computational Analysis, Synthesis, and Design of Dynamic Systems, pages 93-119. CRC Press, 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},
}
[ER09] Andrzej Ehrenfeucht and Grzegorz Rozenberg. Introducing Time in Reaction Systems. Theoretical Computer Science 410(4-5). Elsevier, February 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},
}
[FJR09] Emmanuel Filiot, Naiyong Jin, and Jean-François Raskin. An Antichain Algorithm for LTL Realizability. In CAV'09, Lecture Notes in Computer Science 5643, pages 263-277. Springer-Verlag, June 2009. 
@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,
}
[FKK+09] Dimitris Fotakis, Spyros Kontogiannis, Elias Koutsoupias, Marios Mavronicolas, and Paul G. Spirakis. The structure and complexity of Nash equilibria for a selfish routing game. Theoretical Computer Science 410(36):3305-3326. Elsevier, August 2009. 
@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},
}
[FL09] Oliver Friedmann and Martin Lange. Solving Parity Games in Practice. In ATVA'09, Lecture Notes in Computer Science 5799, pages 182-196. Springer-Verlag, October 2009. 
@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},
}
[FL09] Uli Fahrenberg and Kim Guldstrand Larsen. Discount-optimal infinite Runs in Proced Timed Automata. In INFINITY'06-08, Electronic Notes in Theoretical Computer Science 239, pages 179-191. Elsevier, July 2009. 
@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,
}
[FLT09] Uli Fahrenberg, Kim Guldstrand Larsen, and Claus Thrane. A Quantitative Characterization of Weighted Kripke Structures in Temporal Logics. In MEMICS'09, OpenAccess Series in Informatics 13. Leibniz-Zentrum für Informatik, September 2009. 
@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,
}
[For09] Lance Fortnow. The Status of the P versus NP Problem. Communications of the ACM 52(9):78-86. ACM Press, September 2009. 
@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,
}
[GL09] Sahika Genc and Stéphane Lafortune. Predictability of event occurrences in partially-observed discrete-event systems. Automatica 45(2):301-311. Elsevier, February 2009. 
@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},
}
[GS09] Thomas Gawlitza and Helmut Seidl. Games through Nested Fixpoints. In CAV'09, Lecture Notes in Computer Science 5643, pages 291-305. Springer-Verlag, June 2009. 
@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},
}
[GSZ09] Paul Gastin, Tali Sznajder, and Marc Zeitoun. Distributed synthesis for well-connected architectures. Formal Methods in System Design 34(3):215-237. Springer-Verlag, June 2009. 
@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,
}
[HKO+09] Christoph Haase, Stephan Kreutzer, Joël Ouaknine, and James Worrell. Reachability in Succinct and Parametric One-Counter Automata. In CONCUR'09, Lecture Notes in Computer Science 5710, pages 369-383. Springer-Verlag, September 2009. 
@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},
}
[JdB+09] Mohammad Mahdi Jaghoori, Frank S. de Boer, Tom Chothia, and Marjan Sirjani. Schedulability of asynchronous real-time concurrent objects. Journal of Logic and Algebraic Programming 78(5):402-416. Elsevier, May 2009. 
@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,
}
[KF09] Lars Kuhtz and Bernd Finkbeiner. LTL Path Checking is Efficiently Parallelizable. In ICALP'09, Lecture Notes in Computer Science 5556, pages 235-246. Springer-Verlag, July 2009. 
@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,
}
[KFS+09] Jeroen Kuipers, Janos Flesch, Gijs Schoenmakers, and Koos Vrieze. Pure subgame-perfect equilibria in free transition games. European Journal of Operational Research 199(2):442-447. Elsevier, December 2009. 
@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,
}
[KP09] Elias Koutsoupias and Christos H. Papadimitriou. Worst-case equilibria. Computer Science Review 3(2):65-69. May 2009. 
@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},
}
[KRT09] Dominik Klein, Frank G. Radmacher, and Wolfgang Thomas. The Complexity of Reachability in Randomized Sabotage Games. In FSEN'09, Lecture Notes in Computer Science 5961, pages 162-177. Springer-Verlag, April 2009. 
@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,
}
[KT09] Moez Krichen and Stavros Tripakis. Conformance testing for real-time systems. Formal Methods in System Design 34(3):238-304. Springer-Verlag, June 2009. 
@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},
}
[LPT09] Kai Lampka, Simon Perathoner, and Lothar Thiele. Analytic Real-time Analysis and Timed Automata: A Hybrid Method for Analyzing Embedded Real-time Systems. In EMSOFT'09, pages 107-116. ACM Press, October 2009. 
@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},
}
[LS09] Martin Leucker and Christian Schallart. A brief account of runtime verification. Journal of Logic and Algebraic Programming 78(5):293-303. Elsevier, May 2009. 
@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},
}
[ORW09] Joël Ouaknine, Alexander Rabinovich, and James Worrell. Time-Bounded Verification. In CONCUR'09, Lecture Notes in Computer Science 5710, pages 496-510. Springer-Verlag, September 2009. 
@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,
}
[PPT09] Michal Penn, Maria Polukarov, and Moshe Tennenholtz. Random Order Congestion Games. Mathematics of Operations Research 34(3):706-725. Informs, August 2009. 
@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},
}
[Rah09] George Rahonis. Fuzzy Languages. In Manfred Droste, Werner Kuich, and Walter Vogler (eds.), Handbook of Weighted Automata. Springer-Verlag, 2009. 
@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},
}
[SLB09] Yoav Shoham and Kevin Leyton-Brown. Multiagent Systems – Algorithmic, Game-Theoretic, and Logical Foundations. Cambridge University Press, 2009. 
@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},
}
[SRS09] Anu Singh, C. R. Ramakrishnan, and Scott A. Smolka. Query-Based Model Checking of Ad Hoc Network Protocols. In CONCUR'09, Lecture Notes in Computer Science 5710, pages 603-619. Springer-Verlag, September 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},
}
[SZH+09] Mathijs Schuts, Yunshan Zhu, Faranak Heidarian, and Frits Vaandrager. Modelling Clock Synchronization in the Chess gMAC WSN Protocol. In QFM'09, Electronic Proceedings in Theoretical Computer Science 13, pages 41-54. November 2009. 
@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,
}
[TD09] Cong Tian and Zhenhua Duan. A Note on Stutter-Invariant PLTL. Information Processing Letters 109(13):663-667. Elsevier, June 2009. 
@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,
}
[Tri09] Stavros Tripakis. Checking Timed Büchi Automata Emptiness on Simulation Graphs. ACM Transactions on Computational Logic 10(3). ACM Press, April 2009. 
@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},
}
[UW09] Michael Ummels and Dominik Wojtczak. Decision Problems for Nash Equilibria in Stochastic Games. In CSL'09, Lecture Notes in Computer Science 5771, pages 51-530. Springer-Verlag, September 2009. 
@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,
}
[UW09] Michael Ummels and Dominik Wojtczak. The Complexity of Nash Equilibria in Simple Stochastic Multiplayer Games. In ICALP'09, Lecture Notes in Computer Science 5556, pages 297-308. Springer-Verlag, July 2009. 
@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,
}
[Web09] Michael Weber. On the Complexity of Branching-Time Logics. In CSL'09, Lecture Notes in Computer Science 5771, pages 530-545. Springer-Verlag, September 2009. 
@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,
}
List of authors