2013
[BMS13] Patricia Bouyer, Nicolas Markey et Ocan Sankur. Robust Weighted Timed Automata and Games. In FORMATS'13, Lecture Notes in Computer Science 8053, pages 31-46. Springer-Verlag, août 2013.
Résumé

Weighted timed automata extend timed automata with cost variables that can be used to model the evolution of various quantities. Although cost-optimal reachability is decidable (in polynomial space) on this model, it becomes undecidable on weighted timed games. This paper studies cost-optimal reachability problems on weighted timed automata and games under robust semantics. More precisely, we consider two perturbation game semantics that introduce imprecisions in the standard semantics, and bring robustness properties w.r.t. timing imprecisions to controllers. We give a polynomial-space algorithm for weighted timed automata, and prove the undecidability of cost-optimal reachability on weighted timed games, showing that the problem is robustly undecidable.

@inproceedings{formats2013-BMS,
  author =              {Bouyer, Patricia and Markey, Nicolas and Sankur,
                         Ocan},
  title =               {Robust Weighted Timed Automata and Games},
  editor =              {Braberman, V{\'\i}ctor and Fribourg, Laurent},
  booktitle =           {{P}roceedings of the 11th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'13)},
  acronym =             {{FORMATS}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8053},
  pages =               {31-46},
  year =                {2013},
  month =               aug,
  doi =                 {10.1007/978-3-642-40229-6_3},
  abstract =            {Weighted timed automata extend timed automata with
                         cost variables that can be used to model the
                         evolution of various quantities. Although
                         cost-optimal reachability is decidable (in
                         polynomial space) on this model, it becomes
                         undecidable on weighted timed games. This paper
                         studies cost-optimal reachability problems on
                         weighted timed automata and games under robust
                         semantics. More precisely, we consider two
                         perturbation game semantics that introduce
                         imprecisions in the standard semantics, and bring
                         robustness properties w.r.t. timing imprecisions to
                         controllers. We give a polynomial-space algorithm
                         for weighted timed automata, and prove the
                         undecidability of cost-optimal reachability on
                         weighted timed games, showing that the problem is
                         robustly undecidable.},
}
[LM13] François Laroussinie et Nicolas Markey. Satisfiability of ATL with strategy contexts. In GandALF'13, Electronic Proceedings in Theoretical Computer Science 119, pages 208-223. Août 2013.
Résumé

Various extensions of the temporal logic ATL have recently been introduced to express rich properties of multi-agent systems. Among these, ATLsc extends ATL with strategy contexts, while Strategy Logic has first-order quantification over strategies. There is a price to pay for the rich expressiveness of these logics: model-checking is non-elementary, and satisfiability is undecidable.

We prove in this paper that satisfiability is decidable in several special cases. The most important one is when restricting to turn-based games. We prove that decidability also holds for concurrent games if the number of moves available to the agents is bounded. Finally, we prove that restricting strategy quantification to memoryless strategies brings back undecidability.

@inproceedings{gandalf2013-LM,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas},
  title =               {Satisfiability of {ATL} with strategy contexts},
  editor =              {Puppis, Gabriele and Villa, Tiziano},
  booktitle =           {{P}roceedings of the 4th {I}nternational {S}ymposium
                         on {G}ames, {A}utomata, {L}ogics and {F}ormal
                         {V}erification ({GandALF}'13)},
  acronym =             {{GandALF}'13},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {119},
  pages =               {208-223},
  year =                {2013},
  month =               aug,
  doi =                 {10.4204/EPTCS.119.18},
  abstract =            {Various extensions of the temporal logic ATL have
                         recently been introduced to express rich properties
                         of multi-agent systems. Among these, ATLsc extends
                         ATL with \emph{strategy contexts}, while Strategy
                         Logic has \emph{first-order quantification} over
                         strategies. There is a price to pay for the rich
                         expressiveness of these logics: model-checking is
                         non-elementary, and satisfiability is
                         undecidable.\par We prove in this paper that
                         satisfiability is decidable in several special
                         cases. The most important one is when restricting to
                         \emph{turn-based} games. We~prove that decidability
                         also holds for concurrent games if the number of
                         moves available to the agents is bounded. Finally,
                         we~prove that restricting strategy quantification to
                         memoryless strategies brings back undecidability.},
}
[SBM+13] Ocan Sankur, Patricia Bouyer, Nicolas Markey et Pierre-Alain Reynier. Robust Controller Synthesis in Timed Automata. In CONCUR'13, Lecture Notes in Computer Science 8052, pages 546-560. Springer-Verlag, août 2013.
Résumé

We consider the fundamental problem of Büchi acceptance in timed automata in a robust setting. The problem is formalised in terms of controller synthesis: timed automata are equipped with a parametrised game-based semantics that models the possible perturbations of the decisions taken by the controller. We characterise timed automata that are robustly controllable for some parameter, with a simple graph theoretic condition, by showing the equivalence with the existence of an aperiodic lasso that satisfies the winning condition (aperiodicity was defined and used earlier in different contexts to characterise convergence phenomena in timed automata). We then show decidability and PSPACE-completeness of our problem.

@inproceedings{concur2013-SBMR,
  author =              {Sankur, Ocan and Bouyer, Patricia and Markey,
                         Nicolas and Reynier, Pierre-Alain},
  title =               {Robust Controller Synthesis in Timed Automata},
  editor =              {D{'}Argenio, Pedro R. and Melgratt, Hern{\'a}n C.},
  booktitle =           {{P}roceedings of the 24th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'13)},
  acronym =             {{CONCUR}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8052},
  pages =               {546-560},
  year =                {2013},
  month =               aug,
  doi =                 {10.1007/978-3-642-40184-8_38},
  abstract =            {We consider the fundamental problem of B{\"u}chi
                         acceptance in timed automata in a robust setting.
                         The problem is formalised in terms of controller
                         synthesis: timed automata are equipped with a
                         parametrised game-based semantics that models the
                         possible perturbations of the decisions taken by the
                         controller. We characterise timed automata that are
                         robustly controllable for some parameter, with a
                         simple graph theoretic condition, by showing the
                         equivalence with the existence of an aperiodic lasso
                         that satisfies the winning condition (aperiodicity
                         was defined and used earlier in different contexts
                         to characterise convergence phenomena in timed
                         automata). We then show decidability and
                         PSPACE-completeness of our problem.},
}
[BMS13] Patricia Bouyer, Nicolas Markey et Ocan Sankur. Robustness in timed automata. In RP'13, Lecture Notes in Computer Science 8169, pages 1-18. Springer-Verlag, septembre 2013.
Résumé

In this paper we survey several approaches to the robustness of timed automata, that is, the ability of a system to resist to slight perturbations or errors. We will concentrate on robustness against timing errors which can be due to measuring errors, imprecise clocks, and unexpected runtime behaviors such as execution times that are longer or shorter than expected.

We consider the perturbation model of guard enlargement and formulate several robust verification problems that have been studied recently, including robustness analysis, robust implementation, and robust control.

@inproceedings{rp2013-BMS,
  author =              {Bouyer, Patricia and Markey, Nicolas and Sankur,
                         Ocan},
  title =               {Robustness in timed automata},
  editor =              {Abdulla, Parosh Aziz and Potapov, Igor},
  booktitle =           {{P}roceedings of the 7th {W}orkshop on
                         {R}eachability {P}roblems in {C}omputational
                         {M}odels ({RP}'13)},
  acronym =             {{RP}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8169},
  pages =               {1-18},
  year =                {2013},
  month =               sep,
  doi =                 {10.1007/978-3-642-41036-9_1},
  abstract =            {In this paper we survey several approaches to the
                         robustness of timed automata, that~is, the ability
                         of a system to resist to slight perturbations or
                         errors. We will concentrate on robustness against
                         timing errors which can be due to measuring errors,
                         imprecise clocks, and unexpected runtime behaviors
                         such as execution times that are longer or shorter
                         than expected.\par We consider the perturbation
                         model of guard enlargement and formulate several
                         robust verification problems that have been studied
                         recently, including robustness analysis, robust
                         implementation, and robust control.},
}
[ABK13] Shaull Almagor, Udi Boker et Orna Kupferman. Formalizing and Reasoning about Quality. In ICALP'13, Lecture Notes in Computer Science 7966, pages 15-27. Springer-Verlag, juillet 2013. 
@inproceedings{icalp2013-ABK,
  author =              {Almagor, Shaull and Boker, Udi and Kupferman, Orna},
  title =               {Formalizing and Reasoning about Quality},
  editor =              {Fomin, Fedor V. and Freivalds, Rusins and
                         Kwiatkowska, Marta and Peleg, David},
  booktitle =           {{P}roceedings of the 40th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'13)~-- Part~{II}},
  acronym =             {{ICALP}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7966},
  pages =               {15-27},
  year =                {2013},
  month =               jul,
}
[BBF+13] Aaron Bohy, Véronique Bruyère, Emmanuel Filiot et Jean-François Raskin. Synthesis from LTL Specifications with Mean-Payoff Objectives. In TACAS'13, Lecture Notes in Computer Science 7795, pages 169-184. Springer-Verlag, mars 2013. 
@inproceedings{tacas2013-BBFR,
  author =              {Bohy, Aaron and Bruy{\`e}re, V{\'e}ronique and
                         Filiot, Emmanuel and Raskin, Jean-Fran{\c c}ois},
  title =               {Synthesis from {LTL} Specifications with Mean-Payoff
                         Objectives},
  editor =              {Piterman, Nir and Smolka, Scott A.},
  booktitle =           {{P}roceedings of the 19th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'13)},
  acronym =             {{TACAS}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7795},
  pages =               {169-184},
  year =                {2013},
  month =               mar,
}
[BBL+13] Giorgio Bacci, Giovanni Bacci, Kim Guldstrand Larsen et Radu Mardare. Computing Behavioral Distances, Compositionally. In MFCS'13, Lecture Notes in Computer Science 8087, pages 74-85. Springer-Verlag, août 2013. 
@inproceedings{mfcs2013-BBLM,
  author =              {Bacci, Giorgio and Bacci, Giovanni and Larsen, Kim
                         Guldstrand and Mardare, Radu},
  title =               {Computing Behavioral Distances, Compositionally},
  editor =              {Chatterjee, Krishnendu and Sgall, Ji{\v r}{\'\i}},
  booktitle =           {{P}roceedings of the 38th {I}nternational
                         {S}ymposium on {M}athematical {F}oundations of
                         {C}omputer {S}cience ({MFCS}'13)},
  acronym =             {{MFCS}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8087},
  pages =               {74-85},
  year =                {2013},
  month =               aug,
  doi =                 {10.1007/978-3-642-40313-2_9},
}
[BBL+13] Giorgio Bacci, Giovanni Bacci, Kim Guldstrand Larsen et Radu Mardare. The BisimDist Library: Efficient Computation of Bisimilarity Distances for Markovian Models. In QEST'13, pages 278-281. IEEE Comp. Soc. Press, août 2013. 
@inproceedings{qest2013-BBLM,
  author =              {Bacci, Giorgio and Bacci, Giovanni and Larsen, Kim
                         Guldstrand and Mardare, Radu},
  title =               {The BisimDist Library: Efficient Computation of
                         Bisimilarity Distances for {M}arkovian Models},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {C}onference on {Q}uantitative {E}valuation of
                         {S}ystems ({QEST}'13)},
  acronym =             {{QEST}'13},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {278-281},
  year =                {2013},
  month =               aug,
  doi =                 {10.1007/978-3-642-40196-1_23},
}
[BG13] Nils Bulling et Valentin Goranko. How to Be Both Rich and Happy: Combining Quantitative and Qualitative Strategic Reasoning about Multi-Player Games (Extended Abstract). In SR'13, Electronic Proceedings in Theoretical Computer Science 112, pages 33-41. Mars 2013. 
@inproceedings{sr2013-BG,
  author =              {Bulling, Nils and Goranko, Valentin},
  title =               {How to Be Both Rich and Happy: Combining
                         Quantitative and Qualitative Strategic Reasoning
                         about Multi-Player Games (Extended Abstract)},
  booktitle =           {{P}roceedings of the 1st {I}nternational {W}orkshop
                         on {S}trategic {R}easoning ({SR}'13)},
  acronym =             {{SR}'13},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {112},
  pages =               {33-41},
  year =                {2013},
  month =               mar,
  doi =                 {10.4204/EPTCS.112.8},
}
[BGH13] Olivier Bournez, Daniel S. Graça et Emmanuel Hainry. Computation with perturbed dynamical systems. Journal of Computer and System Sciences 79(5):714-724. Elsevier, août 2013. 
@article{jcss79(5)-BGH,
  author =              {Bournez, Olivier and Gra{\c c}a, Daniel S. and
                         Hainry, Emmanuel},
  title =               {Computation with perturbed dynamical systems},
  publisher =           {Elsevier},
  journal =             {Journal of Computer and System Sciences},
  volume =              {79},
  number =              {5},
  pages =               {714-724},
  year =                {2013},
  month =               aug,
}
[BKK+13] Udi Boker, Denis Kuperberg, Orna Kupferman et Michal Skrzypczak. Nondeterminism in the Presence of a Diverse or Unknown Future. In ICALP'13, Lecture Notes in Computer Science 7966, pages 89-100. Springer-Verlag, juillet 2013. 
@inproceedings{icalp2013-BKKS,
  author =              {Boker, Udi and Kuperberg, Denis and Kupferman, Orna
                         and Skrzypczak, Michal},
  title =               {Nondeterminism in the Presence of a Diverse or
                         Unknown Future},
  editor =              {Fomin, Fedor V. and Freivalds, Rusins and
                         Kwiatkowska, Marta and Peleg, David},
  booktitle =           {{P}roceedings of the 40th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'13)~-- Part~{II}},
  acronym =             {{ICALP}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7966},
  pages =               {89-100},
  year =                {2013},
  month =               jul,
  doi =                 {10.1007/978-3-642-39212-2_11},
}
[BRS13] Marcello Maria Bersani, Matteo Rossi et Pierluigi San Pietro. Deciding the Satisfiability of MITL Specifications. In GandALF'13, Electronic Proceedings in Theoretical Computer Science 119, pages 64-78. Août 2013. 
@inproceedings{gandalf2013-BRS,
  author =              {Bersani, Marcello Maria and Rossi, Matteo and
                         San{~}Pietro, Pierluigi},
  title =               {Deciding the Satisfiability of {MITL}
                         Specifications},
  editor =              {Puppis, Gabriele and Villa, Tiziano},
  booktitle =           {{P}roceedings of the 4th {I}nternational {S}ymposium
                         on {G}ames, {A}utomata, {L}ogics and {F}ormal
                         {V}erification ({GandALF}'13)},
  acronym =             {{GandALF}'13},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {119},
  pages =               {64-78},
  year =                {2013},
  month =               aug,
  doi =                 {10.4204/EPTCS.119.8},
}
[Bru13] Benedikt Brütsch. Synthesizing structured reactive programs via deterministic tree automata. In SR'13, Electronic Proceedings in Theoretical Computer Science 112, pages 107-113. Mars 2013. 
@inproceedings{sr2013-Bru,
  author =              {Br{\"u}tsch, Benedikt},
  title =               {Synthesizing structured reactive programs via
                         deterministic tree automata},
  booktitle =           {{P}roceedings of the 1st {I}nternational {W}orkshop
                         on {S}trategic {R}easoning ({SR}'13)},
  acronym =             {{SR}'13},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {112},
  pages =               {107-113},
  year =                {2013},
  month =               mar,
  doi =                 {10.4204/EPTCS.112.16},
}
[CB13] Franck Cassez et Jean-Luc Béchennec. Timing Analysis of Binary Programs with UPPAAL. In ACSD'13, pages 41-50. IEEE Comp. Soc. Press, juillet 2013. 
@inproceedings{acsd2013-CB,
  author =              {Cassez, Franck and B{\'e}chennec, Jean-Luc},
  title =               {Timing Analysis of Binary Programs with {UPPAAL}},
  editor =              {Carmona, Josep and Lazarescu, Mihai T. and
                         Pietkiewicz-Koutny, Marta},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {A}pplication of {C}oncurrency to
                         {S}ystem {D}esign ({ACSD}'13)},
  acronym =             {{ACSD}'13},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {41-50},
  year =                {2013},
  month =               jul,
  doi =                 {10.1109/ACSD.2013.7},
}
[CBC13] Christophe Chareton, Julien Brunel et David Chemouil. Towards an Updatable Strategy Logic. In SR'13, Electronic Proceedings in Theoretical Computer Science 112, pages 91-98. Mars 2013. 
@inproceedings{sr2013-BCC,
  author =              {Chareton, Christophe and Brunel, Julien and
                         Chemouil, David},
  title =               {Towards an Updatable Strategy Logic},
  booktitle =           {{P}roceedings of the 1st {I}nternational {W}orkshop
                         on {S}trategic {R}easoning ({SR}'13)},
  acronym =             {{SR}'13},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {112},
  pages =               {91-98},
  year =                {2013},
  month =               mar,
  doi =                 {10.4204/EPTCS.112.14},
}
[CBK+13] Maximilien Colange, Souheib Baarir, Fabrice Kordon et Yann Thierry-Mieg. Towards Distributed Software Model-Checking using Decision Diagrams. In CAV'13, Lecture Notes in Computer Science 8044, pages 830-845. Springer-Verlag, juillet 2013. 
@inproceedings{cav2013-CBKT,
  author =              {Colange, Maximilien and Baarir, Souheib and Kordon,
                         Fabrice and Thierry{-}Mieg, Yann},
  title =               {Towards Distributed Software Model-Checking using
                         Decision Diagrams},
  editor =              {Sharygina, Natasha and Veith, Helmut},
  booktitle =           {{P}roceedings of the 25th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'13)},
  acronym =             {{CAV}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8044},
  pages =               {830-845},
  year =                {2013},
  month =               jul,
  doi =                 {10.1007/978-3-642-39799-8_58},
}
[CDR+13] Krishnendu Chatterjee, Laurent Doyen, Mickael Randour et Jean-François Raskin. Looking at Mean-Payoff and Total-Payoff through Windows. In ATVA'13, Lecture Notes in Computer Science 8172, pages 118-132. Springer-Verlag, octobre 2013. 
@inproceedings{atva2013-CDRR,
  author =              {Chatterjee, Krishnendu and Doyen, Laurent and
                         Randour, Mickael and Raskin, Jean-Fran{\c c}ois},
  title =               {Looking at Mean-Payoff and Total-Payoff through
                         Windows},
  editor =              {Hung, Dang Van and Ogawa, Mizuhito},
  booktitle =           {{P}roceedings of the 11th {I}nternational
                         {S}ymposium on {A}utomated {T}echnology for
                         {V}erification and {A}nalysis ({ATVA}'13)},
  acronym =             {{ATVA}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8172},
  pages =               {118-132},
  year =                {2013},
  month =               oct,
}
[CHO+13] Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop et Andreas Pavlogiannis. Distributed synthesis for LTL fragments. In FMCAD'13, pages 18-25. IEEE Comp. Soc. Press, octobre 2013. 
@inproceedings{fmcad2013-CHOP,
  author =              {Chatterjee, Krishnendu and Henzinger, Thomas A. and
                         Otop, Jan and Pavlogiannis, Andreas},
  title =               {Distributed synthesis for {LTL} fragments},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {F}ormal {M}ethods in
                         {C}omputer-{A}ided {D}esign ({FMCAD}'13)},
  acronym =             {{FMCAD}'13},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {18-25},
  year =                {2013},
  month =               oct,
}
[CHR13] Pavol Černý, Thomas A. Henzinger et Arjun Radhakrishna. Quantitative abstraction refinement. In POPL'13, pages 115-128. ACM Press, janvier 2013. 
@inproceedings{popl2013-CHR,
  author =              {{\v{C}}ern{\'y}, Pavol and Henzinger, Thomas A. and
                         Radhakrishna, Arjun},
  title =               {Quantitative abstraction refinement},
  editor =              {Giacobazzi, Roberto and Cousot, Radhia},
  booktitle =           {Conference Record of the 40th {ACM}
                         {SIGPLAN}-{SIGACT} {S}ymposium on {P}rinciples of
                         {P}rogramming {L}anguages ({POPL}'13)},
  acronym =             {{POPL}'13},
  publisher =           {ACM Press},
  pages =               {115-128},
  year =                {2013},
  month =               jan,
  doi =                 {10.1145/2429069.2429085},
}
[DDL+13] Alexandre David, Dehui Du, Kim Guldstrand Larsen, Axel Legay et Marius Mikučionis. Optimizing Control Strategy Using Statistical Model Checking. In NFM'13, Lecture Notes in Computer Science 7871, pages 352-367. Springer-Verlag, mai 2013. 
@inproceedings{nasafm2013-DDLLM,
  author =              {David, Alexandre and Du, Dehui and Larsen, Kim
                         Guldstrand and Legay, Axel and Miku{\v{c}}ionis,
                         Marius},
  title =               {Optimizing Control Strategy Using Statistical Model
                         Checking},
  editor =              {Brat, Guillaume and Rungta, Neha and Venet, Arnaud},
  booktitle =           {{P}roceedings of the th {NASA} {F}ormal {M}ethods
                         {S}ymposium ({NFM}'13)},
  acronym =             {{NFM}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7871},
  pages =               {352-367},
  year =                {2013},
  month =               may,
  doi =                 {10.1007/978-3-642-38088-4_24},
}
[DJL+13] Stéphane Demri, Marcin Jurdziński, Oded Lachish et Ranko Lazić. The covering and boundedness problems for branching vector addition systems. Journal of Computer and System Sciences 79(1):23-38. Elsevier, février 2013. 
@article{jcss79(1)-DJLL,
  author =              {Demri, St{\'e}phane and Jurdzi{\'n}ski, Marcin and
                         Lachish, Oded and Lazi{\'c}, Ranko},
  title =               {The covering and boundedness problems for branching
                         vector addition systems},
  publisher =           {Elsevier},
  journal =             {Journal of Computer and System Sciences},
  volume =              {79},
  number =              {1},
  pages =               {23-38},
  year =                {2013},
  month =               feb,
  doi =                 {10.1016/j.jcss.2012.04.002},
}
[DLL+13] Alexandre David, Kim Guldstrand Larsen, Axel Legay et Danny Bøgsted Poulsen. Statistical Model Checking of Dynamic Networks of Stochastic Hybrid Automata. In AVOCS'13, Electronic Communications of the EASST 10. European Association of Software Science and Technology, septembre 2013. 
@inproceedings{avocs2013-DLLP,
  author =              {David, Alexandre and Larsen, Kim Guldstrand and
                         Legay, Axel and Poulsen, Danny B{\o}gsted},
  title =               {Statistical Model Checking of Dynamic Networks of
                         Stochastic Hybrid Automata},
  editor =              {Schneider, Steve and Treharne, Helen},
  booktitle =           {{P}roceedings of the 13th {I}nternational {W}orkshop
                         on {A}utomated {V}erification of {C}ritical
                         {S}ystems ({AVOCS}'13)},
  acronym =             {{AVOCS}'13},
  publisher =           {European Association of Software Science and
                         Technology},
  series =              {Electronic Communications of the EASST},
  volume =              {10},
  year =                {2013},
  month =               sep,
}
[DLM+13] Peter H. Dalsgaard, Thibault Le Guilly, Daniel Middelhede, Petur Olsen, Thomas Pedersen, Anders P. Ravn et Arne Skou. A Toolchain for Home Automation Controller Development. In SEAA'13, pages 122-129. Septembre 2013. 
@inproceedings{HLMOPRS-seaa2013,
  author =              {Dalsgaard, Peter H. and Le{~}Guilly, Thibault and
                         Middelhede, Daniel and Olsen, Petur and Pedersen,
                         Thomas and Ravn, Anders P. and Skou, Arne},
  title =               {A Toolchain for Home Automation Controller
                         Development},
  editor =              {Demir{\"o}rs, Onur and T{\"u}retken, Oktay},
  booktitle =           {{P}roceedings of the 39th {E}uromicro {C}onference
                         on {S}oftware {E}ngineering and {A}dvanced
                         {A}pplications ({SEAA}'13)},
  acronym =             {{SEAA}'13},
  pages =               {122-129},
  year =                {2013},
  month =               sep,
}
[DV13] Giuseppe De Giacomo et Moshe Y. Vardi. Linear Temporal Logic and Linear Dynamic Logic on Finite Traces. In IJCAI'13, pages 854-860. IJCAI organization, août 2013. 
@inproceedings{ijcai2013-DGV,
  author =              {De{~}Giacomo, Giuseppe and Vardi, Moshe Y.},
  title =               {Linear Temporal Logic and Linear Dynamic Logic on
                         Finite Traces},
  editor =              {Rossi, Francesca},
  booktitle =           {{P}roceedings of the 23rd {I}nternational {J}oint
                         {C}onference on {A}rtificial {I}ntelligence
                         ({IJCAI}'13)},
  acronym =             {{IJCAI}'13},
  publisher =           {IJCAI organization},
  pages =               {854-860},
  year =                {2013},
  month =               aug,
}
[EF13] Daniel Ejsing-Dunn et Lisa Fontani. Infinite Runs in Recharge Automata. Master's thesis, Computer Science Department, Aalborg University, Denmark, Juin 2013. 
@mastersthesis{master13-EF,
  author =              {Ejsing{-}Dunn, Daniel and Fontani, Lisa},
  title =               {Infinite Runs in Recharge Automata},
  year =                {2013},
  month =               jun,
  school =              {Computer Science Department, Aalborg University,
                         Denmark},
}
[EGM13] Javier Esparza, Pierre Ganty et Rupak Majumdar. Parameterized verification of asynchronous shared-memory systems. In CAV'13, Lecture Notes in Computer Science 8044, pages 124-140. Springer-Verlag, juillet 2013. 
@inproceedings{cav2013-EGM,
  author =              {Esparza, Javier and Ganty, Pierre and Majumdar,
                         Rupak},
  title =               {Parameterized verification of asynchronous
                         shared-memory systems},
  editor =              {Sharygina, Natasha and Veith, Helmut},
  booktitle =           {{P}roceedings of the 25th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'13)},
  acronym =             {{CAV}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8044},
  pages =               {124-140},
  year =                {2013},
  month =               jul,
  doi =                 {10.1007/978-3-642-39799-8_8},
}
[Ehl13] Rüdiger Ehlers. Symmetric and Efficient Synthesis. PhD thesis, Saarland University, Germany, Octobre 2013. 
@phdthesis{phd-ehlers,
  author =              {Ehlers, R{\"u}diger},
  title =               {Symmetric and Efficient Synthesis},
  year =                {2013},
  month =               oct,
  school =              {Saarland University, Germany},
}
[FJ13] John Fearnley et Marcin Jurdziński. Reachability in two-clock timed automata is PSPACE-complete. In ICALP'13, Lecture Notes in Computer Science 7966, pages 212-223. Springer-Verlag, juillet 2013. 
@inproceedings{icalp2013-FJ,
  author =              {Fearnley, John and Jurdzi{\'n}ski, Marcin},
  title =               {Reachability in two-clock timed automata is
                         {PSPACE}-complete},
  editor =              {Fomin, Fedor V. and Freivalds, Rusins and
                         Kwiatkowska, Marta and Peleg, David},
  booktitle =           {{P}roceedings of the 40th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'13)~-- Part~{II}},
  acronym =             {{ICALP}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7966},
  pages =               {212-223},
  year =                {2013},
  month =               jul,
  doi =                 {10.1007/978-3-642-39212-2_21},
}
[FLL13] Oliver Friedmann, Martin Lange et Markus Latte. Satisfiability Games for Branching-Time Logics. Logical Methods in Computer Science 9(4). Octobre 2013. 
@article{lmcs9(4)-FLL,
  author =              {Friedmann, Oliver and Lange, Martin and Latte,
                         Markus},
  title =               {Satisfiability Games for Branching-Time Logics},
  journal =             {Logical Methods in Computer Science},
  volume =              {9},
  number =              {4},
  year =                {2013},
  month =               oct,
  doi =                 {10.2168/LMCS-9(4:5)2013},
}
[FPS13] Nathanaël Fijalkow, Sophie Pinchinat et Olivier Serre. Emptiness Of Alternating Tree Automata Using Games With Imperfect Information. In FSTTCS'13, Leibniz International Proceedings in Informatics 24, pages 299-311. Leibniz-Zentrum für Informatik, décembre 2013. 
@inproceedings{fsttcs2013-FPS,
  author =              {Fijalkow, Nathana{\"e}l and Pinchinat, Sophie and
                         Serre, Olivier},
  title =               {Emptiness Of Alternating Tree Automata Using Games
                         With Imperfect Information},
  editor =              {Seth, Anil and Vishnoi, Nisheeth K.},
  booktitle =           {{P}roceedings of the 33rd {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'13)},
  acronym =             {{FSTTCS}'13},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {24},
  pages =               {299-311},
  year =                {2013},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2013.299},
}
[Gel13] Marcus Gelderie. Strategy Composition in Compositional Games. In ICALP'13, Lecture Notes in Computer Science 7966, pages 263-274. Springer-Verlag, juillet 2013. 
@inproceedings{icalp2013-Gel,
  author =              {Gelderie, Marcus},
  title =               {Strategy Composition in Compositional Games},
  editor =              {Fomin, Fedor V. and Freivalds, Rusins and
                         Kwiatkowska, Marta and Peleg, David},
  booktitle =           {{P}roceedings of the 40th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'13)~-- Part~{II}},
  acronym =             {{ICALP}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7966},
  pages =               {263-274},
  year =                {2013},
  month =               jul,
  doi =                 {10.1007/978-3-642-39212-2_25},
}
[GL13] Stefan Göller et Markus Lohrey. Branching-time model checking of one-counter processes and timed automata. SIAM Journal on Computing 42(3):884-923. Society for Industrial and Applied Math., 2013. 
@article{siamcomp42(3)-GL,
  author =              {G{\"o}ller, Stefan and Lohrey, Markus},
  title =               {Branching-time model checking of one-counter
                         processes and timed automata},
  publisher =           {Society for Industrial and Applied Math.},
  journal =             {SIAM Journal on Computing},
  volume =              {42},
  number =              {3},
  pages =               {884-923},
  year =                {2013},
  doi =                 {10.1137/120876435},
}
[Hen13] Thomas A. Henzinger. Quantitative reactive modeling and verification. Computer Science – Research and Development 28(4):331-344. Novembre 2013. 
@article{csrd28(4)-Hen,
  author =              {Henzinger, Thomas A.},
  title =               {Quantitative reactive modeling and verification},
  journal =             {Computer Science~-- Research and Development},
  volume =              {28},
  number =              {4},
  pages =               {331-344},
  year =                {2013},
  month =               nov,
  doi =                 {10.1007/s00450-013-0251-7},
}
[HIM13] Thomas Dueholm Hansen, Rasmus Ibsen-Jensen et Peter Bro Miltersen. A Faster Algorithm for Solving One-Clock Priced Timed Games. In CONCUR'13, Lecture Notes in Computer Science 8052, pages 531-545. Springer-Verlag, août 2013. 
@inproceedings{concur2013-HIM,
  author =              {Hansen, Thomas Dueholm and Ibsen{-}Jensen, Rasmus
                         and Miltersen, Peter Bro},
  title =               {A~Faster Algorithm for Solving One-Clock Priced
                         Timed Games},
  editor =              {D{'}Argenio, Pedro R. and Melgratt, Hern{\'a}n C.},
  booktitle =           {{P}roceedings of the 24th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'13)},
  acronym =             {{CONCUR}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8052},
  pages =               {531-545},
  year =                {2013},
  month =               aug,
}
[HLW13] Andreas Herzig, Emiliano Lorini et Dirk Walther. Reasoning about Actions Meets Strategic Logics. In LORI'13, Lecture Notes in Computer Science 8196, pages 162-175. Springer-Verlag, octobre 2013. 
@inproceedings{lori2013-HLW,
  author =              {Herzig, Andreas and Lorini, Emiliano and Walther,
                         Dirk},
  title =               {Reasoning about Actions Meets Strategic Logics},
  editor =              {Grossi, Davide and Roy, Olivier and Huang, Huaxin},
  booktitle =           {{P}roceedings of the 4th {W}orkshop on {L}ogic,
                         {R}ationality, and {I}nteraction ({LORI}'13)},
  acronym =             {{LORI}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8196},
  pages =               {162-175},
  year =                {2013},
  month =               oct,
  doi =                 {10.1007/978-3-642-40948-6_13},
}
[HO13] Thomas A. Henzinger et Jan Otop. From Model Checking to Model Measuring. In CONCUR'13, Lecture Notes in Computer Science 8052, pages 273-287. Springer-Verlag, août 2013. 
@inproceedings{concur2013-HO,
  author =              {Henzinger, Thomas A. and Otop, Jan},
  title =               {From Model Checking to Model Measuring},
  editor =              {D{'}Argenio, Pedro R. and Melgratt, Hern{\'a}n C.},
  booktitle =           {{P}roceedings of the 24th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'13)},
  acronym =             {{CONCUR}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8052},
  pages =               {273-287},
  year =                {2013},
  month =               aug,
  doi =                 {10.1007/978-3-642-40184-8_20},
}
[HOW13] Paul Hunter, Joël Ouaknine et James Worrell. Expressive Completeness for Metric Temporal Logic. In LICS'13, pages 349-357. IEEE Comp. Soc. Press, juin 2013. 
@inproceedings{lics2013-HOW,
  author =              {Hunter, Paul and Ouaknine, Jo{\"e}l and Worrell,
                         James},
  title =               {Expressive Completeness for Metric Temporal Logic},
  booktitle =           {{P}roceedings of the 28th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'13)},
  acronym =             {{LICS}'13},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {349-357},
  year =                {2013},
  month =               jun,
  doi =                 {10.1109/LICS.2013.41},
}
[HSW13] Frédéric Herbreteau, B. Srivathsan et Igor Walukiewicz. Lazy Abstractions for Timed Automata. In CAV'13, Lecture Notes in Computer Science 8044, pages 990-1005. Springer-Verlag, juillet 2013. 
@inproceedings{cav2013-HSW,
  author =              {Herbreteau, Fr{\'e}d{\'e}ric and Srivathsan, B. and
                         Walukiewicz, Igor},
  title =               {Lazy Abstractions for Timed Automata},
  editor =              {Sharygina, Natasha and Veith, Helmut},
  booktitle =           {{P}roceedings of the 25th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'13)},
  acronym =             {{CAV}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8044},
  pages =               {990-1005},
  year =                {2013},
  month =               jul,
  doi =                 {10.1007/978-3-642-39799-8_71},
}
[HSW13] Chung-Hao Huang, Sven Schewe et Farn Wang. Model Checking Iterated Games. In TACAS'13, Lecture Notes in Computer Science 7795, pages 154-168. Springer-Verlag, mars 2013. 
@inproceedings{tacas2013-HSW,
  author =              {Huang, Chung-Hao and Schewe, Sven and Wang, Farn},
  title =               {Model Checking Iterated Games},
  editor =              {Piterman, Nir and Smolka, Scott A.},
  booktitle =           {{P}roceedings of the 19th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'13)},
  acronym =             {{TACAS}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7795},
  pages =               {154-168},
  year =                {2013},
  month =               mar,
  doi =                 {10.1007/978-3-642-36742-7_11},
}
[Hun13] Paul Hunter. When is Metric Temporal Logic Expressively Complete?. In CSL'13, Leibniz International Proceedings in Informatics 23, pages 380-394. Leibniz-Zentrum für Informatik, septembre 2013. 
@inproceedings{csl2013-Hun,
  author =              {Hunter, Paul},
  title =               {When is Metric Temporal Logic Expressively
                         Complete?},
  editor =              {Ronchi{ }Della{~}Rocca, Simona},
  booktitle =           {{P}roceedings of the 27th {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'13)},
  acronym =             {{CSL}'13},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {23},
  pages =               {380-394},
  year =                {2013},
  month =               sep,
  doi =                 {10.4230/LIPIcs.CSL.2013.380},
}
[JLR13] Line Juhl, Kim Guldstrand Larsen et Jean-François Raskin. Optimal Bounds for Multiweighted and Parametrised Energy Games. In Theories of Programming and Formal Methods – Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday, Lecture Notes in Computer Science 8051, pages 244-255. Springer-Verlag, 2013. 
@inproceedings{tpfm2013-JLR,
  author =              {Juhl, Line and Larsen, Kim Guldstrand and Raskin,
                         Jean-Fran{\c c}ois},
  title =               {Optimal Bounds for Multiweighted and Parametrised
                         Energy Games},
  editor =              {Liu, Zhiming and Woodcock, Jim and Zhu, Yunshan},
  booktitle =           {Theories of Programming and Formal Methods~-- Essays
                         Dedicated to Jifeng He on the Occasion of His 70th
                         Birthday},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8051},
  pages =               {244-255},
  year =                {2013},
  doi =                 {10.1007/978-3-642-39698-4_15},
}
[JLS+13] Jonas Finnemann Jensen, Kim Guldstrand Larsen, Jiří Srba et Lars Kærlund Østergaard. Local Model Checking of Weighted CTL with Upper-Bound Constraints. In SPIN'13, Lecture Notes in Computer Science 7976, pages 178-195. Springer-Verlag, juillet 2013. 
@inproceedings{spin2013-JLSO,
  author =              {Jensen, Jonas Finnemann and Larsen, Kim Guldstrand
                         and Srba, Ji{\v r}{\'\i} and {\O}stergaard, Lars
                         K{\ae}rlund},
  title =               {Local Model Checking of Weighted {CTL} with
                         Upper-Bound Constraints},
  editor =              {Bartocci, Ezio and Ramakrishnan, C. R.},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {S}ymposium on {M}odel-{C}herking {S}oftware
                         ({SPIN}'13)},
  acronym =             {{SPIN}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7976},
  pages =               {178-195},
  year =                {2013},
  month =               jul,
  doi =                 {10.1007/978-3-642-39176-7_12},
}
[KBM13] Jean-François Kempf, Marius Bozga et Oded Maler. As soon as probable: Optimal scheduling under stochastic uncertainty. In TACAS'13, Lecture Notes in Computer Science 7795, pages 385-400. Springer-Verlag, mars 2013. 
@inproceedings{tacas2013-KBM,
  author =              {Kempf, Jean-Fran{\c c}ois and Bozga, Marius and
                         Maler, Oded},
  title =               {As soon as probable: Optimal scheduling under
                         stochastic uncertainty},
  editor =              {Piterman, Nir and Smolka, Scott A.},
  booktitle =           {{P}roceedings of the 19th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'13)},
  acronym =             {{TACAS}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7795},
  pages =               {385-400},
  year =                {2013},
  month =               mar,
}
[KR13] Jim Kurose et Keith Ross. Computer Networks – A top-down approach. Pearson, 2013. 
@book{KR13-CN,
  author =              {Kurose, Jim and Ross, Keith},
  title =               {Computer Networks~-- A~top-down approach},
  publisher =           {Pearson},
  year =                {2013},
}
[MMS13] Fabio Mogavero, Aniello Murano et Luigi Sauro. On the Boundary of Behavioral Strategies. In LICS'13, pages 263-272. IEEE Comp. Soc. Press, juin 2013. 
@inproceedings{lics2013-MMS,
  author =              {Mogavero, Fabio and Murano, Aniello and Sauro,
                         Luigi},
  title =               {On the Boundary of Behavioral Strategies},
  booktitle =           {{P}roceedings of the 28th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'13)},
  acronym =             {{LICS}'13},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {263-272},
  year =                {2013},
  month =               jun,
}
[Rei13] Julien Reichert. On The Complexity of Counter Reachability Games. In RP'13, Lecture Notes in Computer Science 8169, pages 196-208. Springer-Verlag, septembre 2013. 
@inproceedings{rp2013-Rei,
  author =              {Reichert, Julien},
  title =               {On The Complexity of Counter Reachability Games},
  editor =              {Abdulla, Parosh Aziz and Potapov, Igor},
  booktitle =           {{P}roceedings of the 7th {W}orkshop on
                         {R}eachability {P}roblems in {C}omputational
                         {M}odels ({RP}'13)},
  acronym =             {{RP}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8169},
  pages =               {196-208},
  year =                {2013},
  month =               sep,
  doi =                 {10.1007/978-3-642-41036-9_18},
}
[San13] Ocan Sankur. Robustness in Timed Automata: Analysis, Synthesis, Implementation. Thèse de doctorat, Lab. Spécification & Vérification, ENS Cachan, France, Mai 2013. 
@phdthesis{phd-sankur,
  author =              {Sankur, Ocan},
  title =               {Robustness in Timed Automata: Analysis, Synthesis,
                         Implementation},
  year =                {2013},
  month =               may,
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {Th\`ese de doctorat},
}
[Sch13] Sylvain Schmitz. Complexity Hierarchies Beyond Elementary. Research Report cs.CC/1312.5686, arXiv, décembre 2013. 
@techreport{arxiv-cs.CC/1312.5686,
  author =              {Schmitz, Sylvain},
  title =               {Complexity Hierarchies Beyond Elementary},
  number =              {cs.CC/1312.5686},
  year =                {2013},
  month =               dec,
  institution =         {arXiv},
  type =                {Research Report},
}
[Sip13] Michael Sipser. Introduction to the theory of computation. Cengage Learning, 2013. 
@book{Sip13-ITC,
  author =              {Sipser, Michael},
  title =               {Introduction to the theory of computation},
  publisher =           {Cengage Learning},
  year =                {2013},
}
[SW13] Chrstoffer Sloth et Rafael Wisniewski. Complete abstractions of dynamical systems by timed automata. Nonlinear Analysis: Hybrid Systems 7(1):80-100. Février 2013. 
@article{nahs7(1)-SW,
  author =              {Sloth, Chrstoffer and Wisniewski, Rafael},
  title =               {Complete abstractions of dynamical systems by timed
                         automata},
  journal =             {Nonlinear Analysis: Hybrid Systems},
  volume =              {7},
  number =              {1},
  pages =               {80-100},
  year =                {2013},
  month =               feb,
  doi =                 {10.1007/s10703-011-0118-0},
}
[UB13] Michael Ummels et Christel Baier. Computing Quantiles in Markov Reward Models. In FoSSaCS'13, Lecture Notes in Computer Science 7794, pages 353-368. Springer-Verlag, mars 2013. 
@inproceedings{UB-fossacs13,
  author =              {Ummels, Michael and Baier, {\relax Ch}ristel},
  title =               {Computing Quantiles in {M}arkov Reward Models},
  editor =              {Pfenning, Frank},
  booktitle =           {{P}roceedings of the 16th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'13)},
  acronym =             {{FoSSaCS}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7794},
  pages =               {353-368},
  year =                {2013},
  month =               mar,
  doi =                 {10.1007/978-3-642-37075-5_23},
}
[Wan13] Farn Wang. Efficient Model-Checking of Dense-Time Systems with Time-Convexity Analysis. Theoretical Computer Science 467:89-108. Elsevier, janvier 2013. 
@article{tcs467-Wan,
  author =              {Wang, Farn},
  title =               {Efficient Model-Checking of Dense-Time Systems with
                         Time-Convexity Analysis},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {467},
  pages =               {89-108},
  year =                {2013},
  month =               jan,
  doi =                 {10.1016/j.tcs.2012.09.019},
}
[ZL13] Janan Zaytoon et Stéphane Lafortune. Overview of fault diagnosis methods for Discrete Event Systems. Annual Reviews in Control 37(2):308-320. Elsevier, 2013. 
@article{aric37(2)-ZL,
  author =              {Zaytoon, Janan and Lafortune, St{\'e}phane},
  title =               {Overview of fault diagnosis methods for Discrete
                         Event Systems},
  publisher =           {Elsevier},
  journal =             {Annual Reviews in Control},
  volume =              {37},
  number =              {2},
  pages =               {308-320},
  year =                {2013},
  doi =                 {10.1016/j.arcontrol.2013.09.009},
}
Liste des auteurs