Nicolas Markey

Abstract

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

@inproceedings{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.},
}

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 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.},
}

Abstract

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.},
}

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.

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.},
}

@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,
}

@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,
}

@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},
}

@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},
}

@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},
}

@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,
}

@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},
}

@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},
}

@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},
}

@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},
}

@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},
}

@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},
}

@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,
}

@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,
}

@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},
}

@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},
}

@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},
}

@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,
}

@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,
}

@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,
}

@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},
}

@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},
}

@phdthesis{phd-ehlers,
  author =              {Ehlers, R{\"u}diger},
  title =               {Symmetric and Efficient Synthesis},
  year =                {2013},
  month =               oct,
  school =              {Saarland University, Germany},
}

@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},
}

@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},
}

@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},
}

@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},
}

@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},
}

@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},
}

@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,
}

@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},
}

@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},
}

@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},
}

@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},
}

@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},
}

@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},
}

@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},
}

@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},
}

@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,
}

@book{KR13-CN,
  author =              {Kurose, Jim and Ross, Keith},
  title =               {Computer Networks~-- A~top-down approach},
  publisher =           {Pearson},
  year =                {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,
}

@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},
}

@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},
}

@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},
}

@book{Sip13-ITC,
  author =              {Sipser, Michael},
  title =               {Introduction to the theory of computation},
  publisher =           {Cengage Learning},
  year =                {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},
}

@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},
}

@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},
}

@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},
}