Nicolas Markey

@article{jpl35(2)-Cat,
  author =              {ten Cate, Balder},
  title =               {Expressivity of Second Order Propositional Modal
                         Logic},
  publisher =           {Springer-Verlag},
  journal =             {Journal of Philosophical Logic},
  volume =              {35},
  number =              {2},
  pages =               {209-223},
  year =                {2006},
  month =               sep,
}

@phdthesis{phd-cachat,
  author =              {Cachat, Thierry},
  title =               {Games on Pushdown Graphs and Extensions},
  year =                {2003},
  month =               dec,
  school =              {RWTH Aachen, Germany},
  type =                {Th\`ese de doctorat},
}

@inproceedings{fsttcs2006-Cac,
  author =              {Cachat, Thierry},
  title =               {Tree Automata Make Ordinal Theory Easy},
  editor =              {Arun-Kumar, S. and Garg, Naveen},
  booktitle =           {{P}roceedings of the 26th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'06)},
  acronym =             {{FSTTCS}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4337},
  pages =               {285-296},
  year =                {2006},
  month =               dec,
}

@inproceedings{soda2006-CdAH,
  author =              {Chatterjee, Krishnendu and de Alfaro, Luca and
                         Henzinger, Thomas A.},
  title =               {The Complexity of Quantitative Concurrent Parity
                         Games},
  booktitle =           {{P}roceedings of the 17th {A}nnual {ACM}-{SIAM}
                         {S}ymposium on {D}iscrete {A}lgorithms ({SODA}'06)},
  acronym =             {{SODA}'06},
  publisher =           {Society for Industrial and Applied Math.},
  pages =               {678-687},
  year =                {2006},
  month =               jan,
  doi =                 {10.1145/1109557.1109631},
}

@inproceedings{qest2006-CdAH,
  author =              {Chatterjee, Krishnendu and de Alfaro, Luca and
                         Henzinger, Thomas A.},
  title =               {Strategy Improvement for Concurrent Reachability
                         Games},
  booktitle =           {{P}roceedings of the 3rd {I}nternational
                         {C}onference on {Q}uantitative {E}valuation of
                         {S}ystems ({QEST}'06)},
  acronym =             {{QEST}'06},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {291-300},
  year =                {2006},
  month =               sep,
  doi =                 {10.1109/QEST.2006.48},
}

@inproceedings{emsoft2003-CdAHS,
  author =              {Chakrabarti, Arindam and de Alfaro, Luca and
                         Henzinger, Thomas A. and Stoelinga, Mari{\"e}lle},
  title =               {Resource Interfaces},
  editor =              {Alur, Rajeev and Lee, Insup},
  booktitle =           {{P}roceedings of the 3rd {I}nternational
                         {C}onference on {E}mbedded {S}oftware ({EMSOFT}'03)},
  acronym =             {{EMSOFT}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2855},
  pages =               {117-133},
  year =                {2003},
  month =               oct,
  doi =                 {10.1007/978-3-540-45212-6_9},
}

@techreport{AR-s4-2003,
  author =              {Caillaud, Beno{\^\i}t},
  title =               {Project-Team {S4}},
  year =                {2003},
  institution =         {IRISA, Rennes, France},
  type =                {Activity Report},
}

@inproceedings{formats2004-CAMN,
  author =              {Cotton, Scott and Asarin, Eugene and Maler, Oded and
                         Niebert, Peter},
  title =               {Some Progress in Satisfiability Checking for
                         Difference Logic},
  editor =              {Lakhnech, Yassine and Yovine, Sergio},
  booktitle =           {{P}roceedings of the {J}oint {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'04) and {F}ormal
                         {T}echniques in {R}eal-Time and {F}ault-Tolerant
                         {S}ystems ({FTRTFT}'04)},
  acronym =             {{FORMATS-FTRTFT}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3253},
  pages =               {263-276},
  year =                {2004},
  month =               sep,
}

@article{jcss34(2-3)-Cas,
  author =              {Castellani, Ilaria},
  title =               {Bisimulations and abstraction homomorphisms},
  publisher =           {Academic Press},
  journal =             {Journal of Computer and System Sciences},
  volume =              {34},
  number =              {2-3},
  pages =               {210-235},
  year =                {1987},
  month =               apr,
}

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

@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{popl1977-CC,
  author =              {Cousot, Patrick and Cousot, Radhia},
  title =               {Abstract Interpretation: A~Unified Lattice Model for
                         Static Analysis of Programs by Construction or
                         Approximation of Fixpoints},
  booktitle =           {Conference Record of the 4th {ACM} {S}ymposium on
                         {P}rinciples of {P}rogramming {L}anguages
                         ({POPL}'77)},
  acronym =             {{POPL}'77},
  publisher =           {ACM Press},
  pages =               {238-252},
  year =                {1977},
  month =               jan,
  doi =                 {10.1145/512950.512973},
}

@article{pjm82(1)-CC,
  author =              {Cousot, Patrick and Cousot, Radhia},
  title =               {Constructive Versions of {T}arski's Fixed Point
                         Theorems},
  journal =             {Pacific Journal of Mathematics},
  volume =              {82},
  number =              {1},
  pages =               {43-57},
  year =                {1979},
}

@techreport{TR-CMU-CS-94-146,
  author =              {Campos, S{\'e}rgio Vale Aguiar and Clarke, Edmund
                         M.},
  title =               {Real-Time Symbolic Model Checking for Discrete Time
                         Models},
  number =              {CMU-CS-94-146},
  year =                {1994},
  month =               may,
  institution =         {Computer Science Deparment, Carnegie Mellon
                         University, Pittsburgh, Pennsylvania, USA},
  type =                {Technical Report},
}

@incollection{tertsd1995-CC,
  author =              {Campos, S{\'e}rgio Vale Aguiar and Clarke, Edmund
                         M.},
  title =               {Real-time symbolic model checking for discrete time
                         models},
  editor =              {Rus, Teodor and Rattray, Charles},
  booktitle =           {Real-time symbolic model checking for discrete time
                         models},
  publisher =           {World Scientific},
  series =              {AMAST Series in Computing},
  volume =              {2},
  pages =               {129-145},
  year =                {1995},
  month =               jan,
}

@article{sttt2(3)-CC,
  author =              {Campos, S{\'e}rgio Vale Aguiar and Clarke, Edmund
                         M.},
  title =               {Analysis and verification of real-time systems using
                         quantitative symbolic algorithms},
  publisher =           {Springer-Verlag},
  journal =             {International Journal on Software Tools for
                         Technology Transfer},
  volume =              {2},
  number =              {3},
  pages =               {260-269},
  year =                {1999},
  month =               nov,
  doi =                 {10.1007/s100090050033},
}

@inproceedings{csl2000-CC,
  author =              {Comon, Hubert and Cortier, V{\'e}ronique},
  title =               {Flatness is not Weakness},
  editor =              {Clote, Peter and Schwichtenberg, Helmut},
  booktitle =           {{P}roceedings of the 14th {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'00)},
  acronym =             {{CSL}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1862},
  pages =               {262-276},
  year =                {2000},
  month =               aug,
}

@article{tcs253(1)-CC,
  author =              {Campos, S{\'e}rgio Vale Aguiar and Clarke, Edmund
                         M.},
  title =               {The {V}erus Language: Representing Time Efficiently
                         with {BDD}s},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {253},
  number =              {1},
  pages =               {95-118},
  year =                {2001},
  month =               feb,
}

@article{eatcs-bull77()-CC,
  author =              {Calude, Cristian S. and Calude, Elena},
  title =               {The Bridge Crossing Problem},
  publisher =           {EATCS},
  journal =             {EATCS Bulletin},
  volume =              {77},
  pages =               {180-190},
  year =                {2002},
  month =               jun,
}

@inproceedings{cav2002-CCGGPRST,
  author =              {Cimatti, Alessandro and Clarke, Edmund M. and
                         Giunchiglia, Enrico and Giunchiglia, Fausto and
                         Pistore, Marco and Roveri, Marco and Sebastiani,
                         Roberto and Tacchella, Armando},
  title =               {{NuSMV2}: An OpenSource Tool for Symbolic Model
                         Checking},
  editor =              {Brinksma, Ed and Larsen, Kim Guldstrand},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'02)},
  acronym =             {{CAV}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2404},
  pages =               {359-364},
  year =                {2002},
  month =               jul,
}

@inproceedings{cav1999-CCGR,
  author =              {Cimatti, Alessandro and Clarke, Edmund M. and
                         Giunchiglia, Fausto and Roveri, Marco},
  title =               {{NuSMV}: A New Symbolic Model Verifier},
  editor =              {Halbwachs, Nicolas and Peled, Doron A.},
  booktitle =           {{P}roceedings of the 11th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'99)},
  acronym =             {{CAV}'99},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1633},
  pages =               {495-499},
  year =                {1999},
  month =               jul,
}

@article{sttt2(4)-CCGR,
  author =              {Cimatti, Alessandro and Clarke, Edmund M. and
                         Giunchiglia, Fausto and Roveri, Marco},
  title =               {{NuSMV}: A New Symbolic Model Checker},
  publisher =           {Springer-Verlag},
  journal =             {International Journal on Software Tools for
                         Technology Transfer},
  volume =              {2},
  number =              {4},
  pages =               {410-425},
  year =                {2000},
  month =               mar,
}

@inproceedings{atva2006-CCJ,
  author =              {Cassez, Franck and Chatain, {\relax Th}omas and
                         Jard, Claude},
  title =               {Symbolic Unfoldings for Networks of Timed Automata},
  editor =              {Graf, Susanne and Zhang, Wenhui},
  booktitle =           {{P}roceedings of the 4th {I}nternational {S}ymposium
                         on {A}utomated {T}echnology for {V}erification and
                         {A}nalysis ({ATVA}'06)},
  acronym =             {{ATVA}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4218},
  pages =               {307-321},
  year =                {2006},
  month =               oct,
  doi =                 {10.1007/11901914_24},
}

@inproceedings{iccd1995-CCMM,
  author =              {Campos, S{\'e}rgio Vale Aguiar and Clarke, Edmund M.
                         and Marrero, Wilfredo R. and Minea, Marius},
  title =               {Verifying the performance of the PCI local bus using
                         symbolic techniques},
  booktitle =           {{P}roceedings of the 5th {I}nternational
                         {C}onference on {C}omputer {D}esign ({ICCD}'95)},
  acronym =             {{ICCD}'95},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {72-78},
  year =                {1995},
  month =               oct,
}

@techreport{TR-CMU-CS-94-147,
  author =              {Campos, S{\'e}rgio Vale Aguiar and Clarke, Edmund M.
                         and Marrero, Wilfredo R. and Minea, Marius and
                         Hiraishi, Hiromi},
  title =               {Computing Quantitative Characteristics of
                         Finite-State Real-Time Systems},
  number =              {CMU-CS-94-147},
  year =                {1994},
  month =               may,
  institution =         {Computer Science Deparment, Carnegie Mellon
                         University, Pittsburgh, Pennsylvania, USA},
  type =                {Technical Report},
}

@article{or68(2)-CCMS,
  author =              {Colini{-}Baldeschi, Riccardo and Cominetti, Roberto
                         and Mertikopoulos, Panayotis and Scarsini, Marco},
  title =               {When is selfish routing bad? {T}he~price of anarchy
                         in light and heavy traffic},
  publisher =           {Informs},
  journal =             {Operations Research},
  volume =              {68},
  number =              {2},
  pages =               {411-434},
  year =                {2020},
  month =               apr,
  doi =                 {10.1287/opre.2019.1894},
}

@inproceedings{rex1988-CD,
  author =              {Clarke, Edmund M. and Draghicescu, I. A.},
  title =               {Expressibility Results for Linear-Time and
                         Branching-Time Logics},
  editor =              {de~Bakker, Jaco W. and de Roever, Willem-Paul and
                         Rozenberg, Grzegorz},
  booktitle =           {{L}inear {T}ime, {B}ranching {T}ime and {P}artial
                         {O}rder in {L}ogics and {M}odels for
                         {C}oncurrency~--- {P}roceedings of {REX}
                         {S}chool{\slash}{W}orkshop~1988 ({REX}'88)},
  acronym =             {{REX}'88},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {354},
  pages =               {428-437},
  year =                {1988},
  month =               may,
}

@inproceedings{icalp2010-CD,
  author =              {Chatterjee, Krishnendu and Doyen, Laurent},
  title =               {Energy Parity Games},
  editor =              {Abramsky, Samson and Gavoille, Cyril and Kirchner,
                         Claude and Meyer auf der Heide, Friedhelm and
                         Spirakis, Paul G.},
  booktitle =           {{P}roceedings of the 37th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'10)~-- Part~{II}},
  acronym =             {{ICALP}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6199},
  pages =               {599-610},
  year =                {2010},
  month =               jul,
}

@article{tcs458-CD,
  author =              {Chatterjee, Krishnendu and Doyen, Laurent},
  title =               {Energy Parity Games},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {458},
  pages =               {49-60},
  year =                {2012},
  month =               nov,
  doi =                 {10.1016/j.tcs.2012.07.038},
}

@inproceedings{icalp2016-CD,
  author =              {Chatterjee, Krishnendu and Doyen, Laurent},
  title =               {Computation Tree Logic for Synchronization
                         Properties},
  editor =              {Chatzigiannakis, Ioannis and Mitzenmacher, Michael
                         and Rabani, Yuval and Sangiorgi, Davide},
  booktitle =           {{P}roceedings of the 43rd {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'16)~-- Part~{II}},
  acronym =             {{ICALP}'16},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {55},
  pages =               {98:1-98:14},
  year =                {2016},
  month =               jul,
  doi =                 {10.4230/LIPIcs.ICALP.2016.98},
}

@article{ipl91(5)-CDC,
  author =              {Chatterjee, Krishnendu and Dasgupta, Pallab and
                         Chakrabarti, P. P.},
  title =               {The power of first-order quantification over states
                         in branching and linear time temporal logics},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {91},
  number =              {5},
  pages =               {201-210},
  year =                {2004},
  month =               sep,
}

@inproceedings{concur2005-CDFLL,
  author =              {Cassez, Franck and David, Alexandre and Fleury,
                         Emmanuel and Larsen, Kim Guldstrand and Lime,
                         Didier},
  title =               {Efficient On-the-fly Algorithms for the Analysis of
                         Timed Games},
  editor =              {Abadi, Mart{\'\i}n and de Alfaro, Luca},
  booktitle =           {{P}roceedings of the 16th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'05)},
  acronym =             {{CONCUR}'05},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3653},
  pages =               {66-80},
  year =                {2005},
  month =               aug,
  doi =                 {10.1007/11539452_9},
}

@inproceedings{vmcai2014-CDFR,
  author =              {Chatterjee, Krishnendu and Doyen, Laurent and
                         Filiot, Emmanuel and Raskin, Jean-Fran{\c c}ois},
  title =               {Doomsday Equilibria for Omega-Regular Games},
  editor =              {McMillan, Kenneth L. and Rival, Xavier},
  booktitle =           {{P}roceedings of the 15th {I}nternational {W}orkshop
                         on {V}erification, {M}odel {C}hecking, and
                         {A}bstract {I}nterpretation ({VMCAI}'14)},
  acronym =             {{VMCAI}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8318},
  pages =               {78-97},
  year =                {2014},
  month =               jan,
  doi =                 {10.1007/978-3-642-54013-4_5},
}

@inproceedings{vmcai2014-CDFR,
  author =              {Chatterjee, Krishnendu and Doyen, Laurent and
                         Filiot, Emmanuel and Raskin, Jean-Fran{\c c}ois},
  title =               {Doomsday Equilibria for Omega-Regular Games},
  editor =              {McMillan, Kenneth L. and Rival, Xavier},
  booktitle =           {{P}roceedings of the 15th {I}nternational {W}orkshop
                         on {V}erification, {M}odel {C}hecking, and
                         {A}bstract {I}nterpretation ({VMCAI}'14)},
  acronym =             {{VMCAI}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8318},
  pages =               {78-97},
  year =                {2014},
  month =               jan,
  doi =                 {10.1007/978-3-642-54013-4_5},
}

@inproceedings{csl2008-CDH,
  author =              {Chatterjee, Krishnendu and Doyen, Laurent and
                         Henzinger, Thomas A.},
  title =               {Quantitative Languages},
  editor =              {Kaminski, Michael and Martini, Simone},
  booktitle =           {{P}roceedings of the 22nd {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'08)},
  acronym =             {{CSL}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5213},
  pages =               {385-400},
  year =                {2008},
  month =               sep,
  doi =                 {10.1007/978-3-540-87531-4_28},
}

@article{tocl11(4)-CDH,
  author =              {Chatterjee, Krishnendu and Doyen, Laurent and
                         Henzinger, Thomas A.},
  title =               {Quantitative Languages},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {11},
  number =              {4},
  year =                {2010},
  month =               jul,
  doi =                 {10.1145/1805950.1805953},
}

@inproceedings{kimfest2017-CDH,
  author =              {Chatterjee, Krishnendu and Doyen, Laurent and
                         Henzinger, Thomas A.},
  title =               {The Cost of Exactness in Quantitative Reachability},
  editor =              {Aceto, Luca and Bacci, Giorgio and Bacci, Giovanni
                         and Ing{\'o}lfsd{\'o}ttir, Anna and Legay, Axel and
                         Mardare, Radu},
  booktitle =           {Models, Algorithms, Logics and Tools: Essays
                         Dedicated to Kim Guldstrand Larsen on the Occasion
                         of His 60th Birthday},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {10460},
  pages =               {367-381},
  year =                {2017},
  month =               aug,
  doi =                 {10.1007/978-3-319-63121-9_18},
}

@inproceedings{csl2006-CDHR,
  author =              {Chatterjee, Krishnendu and Doyen, Laurent and
                         Henzinger, Thomas A. and Raskin, Jean-Fran{\c c}ois},
  title =               {Algorithms for Omega-Regular Games with Imperfect
                         Information},
  editor =              {{\'E}sik, Zolt{\'a}n},
  booktitle =           {{P}roceedings of the 20th {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'06)},
  acronym =             {{CSL}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4207},
  pages =               {287-302},
  year =                {2006},
  month =               sep,
}

@inproceedings{fsttcs2010-CDHR,
  author =              {Chatterjee, Krishnendu and Doyen, Laurent and
                         Henzinger, Thomas A. and Raskin, Jean-Fran{\c c}ois},
  title =               {Generalized Mean-payoff and Energy Games},
  editor =              {Lodaya, Kamal and Mahajan, Meena},
  booktitle =           {{P}roceedings of the 30th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'10)},
  acronym =             {{FSTTCS}'10},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {8},
  pages =               {505-516},
  year =                {2010},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2010.505},
}

@inproceedings{atva2007-CDLLR,
  author =              {Cassez, Franck and David, Alexandre and Larsen, Kim
                         Guldstrand and Lime, Didier and Raskin, Jean-Fran{\c
                         c}ois},
  title =               {Timed Control with Observation Based and Stuttering
                         Invariant Strategies},
  editor =              {Namjoshi, Kedar and Yoneda, Tomohiro and Higashino,
                         Teruo and Okamura, Yoshio},
  booktitle =           {{P}roceedings of the 5th {I}nternational {S}ymposium
                         on {A}utomated {T}echnology for {V}erification and
                         {A}nalysis ({ATVA}'07)},
  acronym =             {{ATVA}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4762},
  pages =               {192-206},
  year =                {2007},
  month =               oct,
  doi =                 {10.1007/978-3-540-75596-8_15},
}

@article{fmsd40(1)-CDM,
  author =              {Cassez, Franck and Dubreil, J{\'e}r{\'e}my and
                         Marchand, Herv{\'e}},
  title =               {Synthesis of opaque systems with static and dynamic
                         masks},
  publisher =           {Springer-Verlag},
  journal =             {Formal Methods in System Design},
  volume =              {40},
  number =              {1},
  pages =               {88-115},
  year =                {2012},
  month =               feb,
  doi =                 {10.1007/s10703-012-0141-9},
}

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

@article{icomp242()-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},
  publisher =           {Elsevier},
  journal =             {Information and Computation},
  volume =              {242},
  pages =               {25-52},
  year =                {2015},
  month =               jun,
  doi =                 {10.1016/j.ic.2015.03.010},
}

@article{mathprog-CDS,
  author =              {Cominetti, Roberto and Dose, Valerio and Scarsini,
                         Marco},
  title =               {The~price of anarchy in routing games as a function
                         of the demand},
  journal =             {Mathematical Programming},
  year =                {2023},
  doi =                 {10.1007/s10107-021-01701-7},
  note =                {To~appear},
}

@inproceedings{kr2002-CDV,
  author =              {Calvanese, Diego and De{~}Giacomo, Giuseppe and
                         Vardi, Moshe Y.},
  title =               {Reasoning about Actions and Planning in {LTL} Action
                         Theories},
  editor =              {Giunchiglia, Fausto},
  booktitle =           {{P}roceedings of the 8th {I}nternational
                         {C}onference on {P}rinciples of {K}nowledge
                         {R}epresentation and {R}easoning ({KR}'02)},
  acronym =             {{KR}'02},
  publisher =           {Morgan Kaufmann Publishers},
  pages =               {593-602},
  year =                {2002},
  month =               apr,
}

@inproceedings{icalp1980-CE,
  author =              {Clarke, Edmund M. and Emerson, E. Allen},
  title =               {Characterizing properties of parallel programs as
                         fixpoints},
  editor =              {de~Bakker, Jaco W. and van Leeuwen, Jan},
  booktitle =           {{P}roceedings of the 7th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'80)},
  acronym =             {{ICALP}'80},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {85},
  pages =               {169-181},
  year =                {1980},
  month =               jul,
}

@inproceedings{lop1981-CE,
  author =              {Clarke, Edmund M. and Emerson, E. Allen},
  title =               {Design and Synthesis of Synchronization Skeletons
                         using Branching-Time Temporal Logic},
  editor =              {Kozen, Dexter C.},
  booktitle =           {{P}roceedings of the 3rd {W}orkshop on {L}ogics of
                         {P}rograms ({LOP}'81)},
  acronym =             {{LOP}'81},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {131},
  pages =               {52-71},
  year =                {1982},
  confyear =            {1981},
  confmonth =           {5},
  doi =                 {10.1007/BFb0025774},
}

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

@inproceedings{cav1998-CEJS,
  author =              {Clarke, Edmund M. and Emerson, E. Allen and Jha,
                         Somesh and Sistla, A. Prasad},
  title =               {Symmetry Reductions in Model Checking},
  editor =              {Hu, Alan J. and Vardi, Moshe Y.},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'98)},
  acronym =             {{CAV}'98},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1427},
  pages =               {147-158},
  year =                {1998},
  month =               jun,
  doi =                 {10.1007/BFb0028741},
}

@article{mfc14(3)-Cer,
  author =              {{\v{C}}ern{\'y}, J{\'a}n},
  title =               {Pozn{\'a}mka k homog{\'e}nnym experimentom s
                         kone{\v{c}}n{\'y}mi automatmi},
  journal =             {Matematicko-fyzik{\'a}lny {\v{c}}asopis},
  volume =              {14},
  number =              {3},
  pages =               {208-216},
  year =                {1964},
}

@inproceedings{cav1992-Cer,
  author =              {{\v{C}}er{\={a}}ns, K{\={a}}rlis},
  title =               {Decidability of Bisimulation Equivalences for
                         Parallel Timer Processes},
  editor =              {von Bochmann, Gregor and Probst, David K.},
  booktitle =           {{P}roceedings of the 4th {I}nternational {W}orkshop
                         on {C}omputer {A}ided {V}erification ({CAV}'92)},
  acronym =             {{CAV}'92},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {663},
  pages =               {302-315},
  year =                {1993},
  confyear =            {1992},
  confmonth =           {6-7},
}

@article{jcss46-CER93,
  author =              {Courcelle, Bruno and Engelfriet, Joost and
                         Rozenberg, Grzegorz},
  title =               {Handle-rewriting hypergraph grammars},
  publisher =           {Academic Press},
  journal =             {Journal of Computer and System Sciences},
  volume =              {46},
  number =              {2},
  year =                {1993},
  month =               apr,
  doi =                 {10.1016/0022-0000(93)90004-G},
}

@mastersthesis{master14-Cer,
  author =              {{\v{C}}erm{\'a}k, Petr},
  title =               {A~Model Checker for Strategy Logic},
  year =                {2014},
  month =               jun,
  school =              {Dept. of Computing, Imperial College London, UK},
}

@inproceedings{popl1983-CES,
  author =              {Clarke, Edmund M. and Emerson, E. Allen and Sistla,
                         A. Prasad},
  title =               {Automatic Verification of Finite-State Concurrent
                         Systems using Temporal Logic Specifications: A
                         Practical Approach},
  booktitle =           {Conference Record of the 10th {ACM} {S}ymposium on
                         {P}rinciples of {P}rogramming {L}anguages
                         ({POPL}'83)},
  acronym =             {{POPL}'83},
  publisher =           {ACM Press},
  pages =               {117-126},
  year =                {1983},
  month =               jan,
}

@article{toplas8(2)-CES,
  author =              {Clarke, Edmund M. and Emerson, E. Allen and Sistla,
                         A. Prasad},
  title =               {Automatic Verification of Finite-State Concurrent
                         Systems Using Temporal Logic Specifications},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Programming Languages and
                         Systems},
  volume =              {8},
  number =              {2},
  pages =               {244-263},
  year =                {1986},
  month =               apr,
}

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

@inproceedings{icalp2016-CFGR,
  author =              {Condurache, Rodica and Filiot, Emmanuel and
                         Gentilini, Raffaella and Raskin, Jean-Fran{\c c}ois},
  title =               {The Complexity of Rational Synthesis},
  editor =              {Chatzigiannakis, Ioannis and Mitzenmacher, Michael
                         and Rabani, Yuval and Sangiorgi, Davide},
  booktitle =           {{P}roceedings of the 43rd {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'16)~-- Part~{II}},
  acronym =             {{ICALP}'16},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {55},
  pages =               {121:1-121:15},
  year =                {2016},
  month =               jul,
  doi =                 {10.4230/LIPIcs.ICALP.2016.121},
}

@article{ijfcs14(4)-CFHKOST,
  author =              {Clarke, Edmund M. and Fehnker, Ansgar and Han, Zhi
                         and Krogh, Bruce H. and Ouaknine, Jo{\"e}l and
                         Stursberg, Olaf and Theobald, Michael},
  title =               {Abstraction and Countrexample-Guided Refinement in
                         Model Checking of Hybrid Systems},
  journal =             {International Journal of Foundations of Computer
                         Science},
  volume =              {14},
  number =              {4},
  pages =               {583-604},
  year =                {2003},
  month =               aug,
  doi =                 {10.1142/S012905410300190X},
}

@inproceedings{CFKPS-tacas2012,
  author =              {Chen, Taolue and Forejt, Vojt{\v{e}}ch and
                         Kwiatkowska, Marta and Parker, David and Simaitis,
                         Aistis},
  title =               {Automatic Verification of Competitive Stochastic
                         Systems},
  editor =              {Flanagan, Cormac and K{\"o}nig, Barbara},
  booktitle =           {{P}roceedings of the 18th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'12)},
  acronym =             {{TACAS}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7214},
  pages =               {315-330},
  year =                {2012},
  month =               mar,
}

@inproceedings{CFKSTU-concur2012,
  author =              {Chen, Taolue and Forejt, Vojt{\v{e}}ch and
                         Kwiatkowska, Marta and Simaitis, Aistis and Trivedi,
                         Ashutosh and Ummels, Michael},
  title =               {Playing Stochastic Games Precisely},
  editor =              {Koutny, Maciej and Ulidowski, Irek},
  booktitle =           {{P}roceedings of the 23rd {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'12)},
  acronym =             {{CONCUR}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7454},
  pages =               {348-363},
  year =                {2012},
  month =               sep,
}

@article{icomp124(1)-CFP,
  author =              {C{\'e}c{\'e}, G{\'e}rard and Finkel, Alain and
                         Purushothaman Iyer, S.},
  title =               {Unreliable Channels are Easier to Verify Than
                         Perfect Channels},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {124},
  number =              {1},
  pages =               {20-31},
  year =                {1996},
  month =               jan,
}

@article{arcs2()-CG,
  author =              {Clarke, Edmund M. and Grumberg, Orna},
  title =               {Research on Automatic Verification of Finite-State
                         Concurrent Systems},
  publisher =           {Annual Reviews Inc.},
  journal =             {Annual Review of Computer Science},
  volume =              {2},
  pages =               {269-290},
  year =                {1987},
}

@inproceedings{esa1996-CG,
  author =              {Cherkassky, Boris V. and Goldberg, Andrew V.},
  title =               {Negative-Cycle Detection Algorithm},
  editor =              {D{\'\i}az, Josep and Serna, Maria J.},
  booktitle =           {{P}roceedings of the 4th {A}nnual {E}uropean
                         {S}ymposium on {A}lgorithms ({ESA}'96)},
  acronym =             {{ESA}'96},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1136},
  pages =               {349-363},
  year =                {1996},
  month =               sep,
}

@techreport{arxiv1402.3199,
  author =              {Chaturvedi, Namit and Gelderie, Marcus},
  title =               {Weak {{\(\omega\)}}-Regular Trace Languages},
  number =              {1402.3199},
  year =                {2014},
  month =               feb,
  institution =         {arXiv},
  type =                {Research Report},
}

@article{fmsd10(1)-CGH,
  author =              {Clarke, Edmund M. and Grumberg, Orna and Hamaguchi,
                         Kiyoharu},
  title =               {Another Look at {LTL} Model Checking},
  publisher =           {Kluwer Academic},
  journal =             {Formal Methods in System Design},
  volume =              {10},
  number =              {1},
  pages =               {47-71},
  year =                {1997},
  month =               feb,
}

@inproceedings{cav2000-CGJLV,
  author =              {Clarke, Edmund M. and Grumberg, Orna and Jha, Somesh
                         and Lu, Yuan and Veith, Helmut},
  title =               {Counterexample-Guided Abstraction Refinement},
  editor =              {Emerson, E. Allen and Sistla, A. Prasad},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'00)},
  acronym =             {{CAV}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1855},
  pages =               {154-169},
  year =                {2000},
  month =               jul,
  doi =                 {10.1007/10722167_15},
}

@incollection{lncs2000-CGJLV,
  author =              {Clarke, Edmund M. and Grumberg, Orna and Jha, Somesh
                         and Lu, Yuan and Veith, Helmut},
  title =               {Progress on the State Explosion Problem in Model
                         Checking},
  editor =              {Wilhelm, Reinhard},
  booktitle =           {Informatics~-- 10~Years Back. 10~Years Ahead},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2000},
  pages =               {176-194},
  year =                {2001},
}

@article{jacm50(5)-CGJLV,
  author =              {Clarke, Edmund M. and Grumberg, Orna and Jha, Somesh
                         and Lu, Yuan and Veith, Helmut},
  title =               {Counterexample-Guided Abstraction Refinement for
                         Symbolic Model Checking},
  publisher =           {ACM Press},
  journal =             {Journal of the~ACM},
  volume =              {50},
  number =              {5},
  pages =               {752-794},
  year =                {2003},
  month =               sep,
  doi =                 {10.1145/876638.876643},
}

@inproceedings{cav1993-CGL,
  author =              {{\v{C}}er{\={a}}ns, K{\={a}}rlis and Godskesen, Jens
                         Christian and Larsen, Kim Guldstrand},
  title =               {Timed Modal Specification - Theory and Tools},
  editor =              {Courcoubetis, Costas},
  booktitle =           {{P}roceedings of the 5th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'93)},
  acronym =             {{CAV}'93},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {697},
  pages =               {253-267},
  year =                {1993},
  month =               jun,
}

@article{toplas16(5)-CGL,
  author =              {Clarke, Edmund M. and Grumberg, Orna and Long, David
                         E.},
  title =               {Model Checking},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Programming Languages and
                         Systems},
  volume =              {16},
  number =              {5},
  pages =               {1-45},
  year =                {1994},
  month =               sep,
}

@inproceedings{dac1995-CGMZ,
  author =              {Clarke, Edmund M. and Grumberg, Orna and McMillan,
                         Kenneth L. and Zhao, Xudong},
  title =               {Efficient Generation of Counterexamples and
                         Witnesses in Symbolic Model Checking},
  booktitle =           {{P}roceedings of the 32nd {D}esign {A}utomation
                         {C}onference ({DAC}'95)},
  acronym =             {{DAC}'95},
  publisher =           {ACM Press},
  pages =               {427-432},
  year =                {1995},
  month =               jun,
}

@book{MC2000-CGP,
  author =              {Clarke, Edmund M. and Grumberg, Orna and Peled,
                         Doron A.},
  title =               {Model checking},
  publisher =           {MIT Press},
  year =                {2000},
}

@inproceedings{frocos2002-CGPRST,
  author =              {Cimatti, Alessandro and Giunchiglia, Enrico and
                         Pistore, Marco and Roveri, Marco and Sebastiani,
                         Roberto and Tacchella, Armando},
  title =               {Integrating {BDD}-based and {SAT}-based Symbolic
                         Model Checking},
  editor =              {Armando, Alessandro},
  booktitle =           {{P}roceedings of the 4th {I}nternational {W}orkshop
                         on {F}rontiers of {C}ombining {S}ystems
                         ({FroCoS}'02)},
  acronym =             {{FroCoS}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2309},
  pages =               {49-56},
  year =                {2002},
  month =               apr,
}

@inproceedings{aaai-iaai1998-CGS,
  author =              {Cadoli, Marco and Giovanardi, Andrea and Schaerf,
                         Marco},
  title =               {An Algorithm to Evaluate Quantified Boolean
                         Formulae},
  booktitle =           {{P}roceedings of the 15th {N}ational {C}onference on
                         {A}rtificial {I}ntelligence ({AAAI}'98) and 10th
                         {I}nnovative {A}pplications of {A}rtificial
                         {I}ntelligence {C}onference ({IAAI}'98)},
  acronym =             {{AAAI-IAAI}'98},
  publisher =           {MIT Press},
  pages =               {262-267},
  year =                {1998},
  month =               jul,
}

@inproceedings{rp2014-CH,
  author =              {Carayol, Arnaud and Hague, Matthew},
  title =               {Regular Strategies In Pushdown Reachability Games},
  editor =              {Ouaknine, Jo{\"e}l and Potapov, Igor and Worrell,
                         James},
  booktitle =           {{P}roceedings of the 8th {W}orkshop on
                         {R}eachability {P}roblems in {C}omputational
                         {M}odels ({RP}'14)},
  acronym =             {{RP}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8762},
  pages =               {58-71},
  year =                {2014},
  month =               sep,
  doi =                 {10.1007/978-3-319-11439-2_5},
}

@inproceedings{cav2000-Cha,
  author =              {Chan, William},
  title =               {Temporal-Logic Queries},
  editor =              {Emerson, E. Allen and Sistla, A. Prasad},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'00)},
  acronym =             {{CAV}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1855},
  pages =               {450-463},
  year =                {2000},
  month =               jul,
}

@phdthesis{phd-chatterjee,
  author =              {Chatterjee, Krishnendu},
  title =               {Stochastic {\(\omega\)}-regular games},
  year =                {2007},
  school =              {University of Califormia at Berkeley, USA},
}

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

@inproceedings{icalp2014-Cha,
  author =              {Chaturvedi, Namit},
  title =               {Toward a structure theory of regular infinitary
                         trace languages},
  editor =              {Esparza, Javier and Fraigniaud, Pierre and
                         Koutsoupias, Elias},
  booktitle =           {{P}roceedings of the 41st {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'14)~-- Part~{II}},
  acronym =             {{ICALP}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8573},
  pages =               {134-145},
  year =                {2014},
  month =               jul,
  doi =                 {10.1007/978-3-662-43951-7_12},
}

@techreport{AIB-2014-04,
  author =              {Chaturvedi, Namit},
  title =               {Languages of Infinite Traces and Deterministic
                         Asynchronous Automata},
  number =              {AIB-2014-004},
  year =                {2014},
  month =               feb,
  institution =         {RWTH Aachen, Germany},
  type =                {Research Report},
}

@inproceedings{lics2004-CHJ,
  author =              {Chatterjee, Krishnendu and Henzinger, Thomas A. and
                         Jurdzi{\'n}ski, Marcin},
  title =               {Games with Secure Equilibria},
  booktitle =           {{P}roceedings of the 19th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'04)},
  acronym =             {{LICS}'04},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {160-169},
  year =                {2004},
  month =               jul,
}

@inproceedings{lics2005-CHJ,
  author =              {Chatterjee, Krishnendu and Henzinger, Thomas A. and
                         Jurdzi{\'n}ski, Marcin},
  title =               {Mean-payoff Parity Games},
  booktitle =           {{P}roceedings of the 20th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'05)},
  acronym =             {{LICS}'05},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {178-187},
  year =                {2005},
  month =               jul,
}

@article{tcs365(1-2)-CHJ,
  author =              {Chatterjee, Krishnendu and Henzinger, Thomas A. and
                         Jurdzi{\'n}ski, Marcin},
  title =               {Games with Secure Equilibria},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {365},
  number =              {1-2},
  pages =               {67-82},
  year =                {2006},
  month =               nov,
}

@phdthesis{phd-chockler,
  author =              {Chockler, Hana},
  title =               {Coverage Metrics for Model Checking},
  year =                {2003},
  month =               sep,
  school =              {Hebrew University, Jerusalem, Israel},
}

@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{fossacs2007-CHP,
  author =              {Chatterjee, Krishnendu and Henzinger, Thomas A. and
                         Piterman, Nir},
  title =               {Generalized Parity Games},
  editor =              {Seidl, Helmut},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'07)},
  acronym =             {{FoSSaCS}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4423},
  pages =               {153-167},
  year =                {2007},
  month =               mar,
}

@inproceedings{concur2007-CHP,
  author =              {Chatterjee, Krishnendu and Henzinger, Thomas A. and
                         Piterman, Nir},
  title =               {Strategy Logic},
  editor =              {Caires, Lu{\'\i}s and Vasconcelos, Vasco T.},
  booktitle =           {{P}roceedings of the 18th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'07)},
  acronym =             {{CONCUR}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4703},
  pages =               {59-73},
  year =                {2007},
  month =               sep,
  doi =                 {10.1007/978-3-540-74407-8_5},
}

@techreport{corr0805.2620-CHP,
  author =              {Chatterjee, Krishnendu and Henzinger, Thomas A. and
                         Piterman, Nir},
  title =               {Algorithms for {B}{\"u}chi games},
  number =              {0805.2620},
  year =                {2008},
  month =               may,
  institution =         {arXiv},
  type =                {Research Report},
}

@article{icomp208(6)-CHP,
  author =              {Chatterjee, Krishnendu and Henzinger, Thomas A. and
                         Piterman, Nir},
  title =               {Strategy Logic},
  publisher =           {Elsevier},
  journal =             {Information and Computation},
  volume =              {208},
  number =              {6},
  pages =               {677-693},
  year =                {2010},
  month =               jun,
  doi =                 {10.1016/j.ic.2009.07.004},
}

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

@inproceedings{hscc2002-CHR,
  author =              {Cassez, Franck and Henzinger, Thomas A. and Raskin,
                         Jean-Fran{\c c}ois},
  title =               {A Comparison of Control Problems for Timed and
                         Hybrid Systems},
  editor =              {Tomlin, Claire and Greenstreet, Mark R.},
  booktitle =           {{P}roceedings of the 5th {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
                         ({HSCC}'02)},
  acronym =             {{HSCC}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2289},
  pages =               {134-148},
  year =                {2002},
  month =               mar,
}

@article{tcs413(1)-CHR,
  author =              {{\v{C}}ern{\'y}, Pavol and Henzinger, Thomas A. and
                         Radhakrishna, Arjun},
  title =               {Simulation distances},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {413},
  number =              {1},
  pages =               {21-35},
  year =                {2012},
  month =               jan,
  doi =                 {10.1016/j.tcs.2011.08.002},
}

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

@inproceedings{sisl1957-Chu,
  author =              {Church, Alonzo},
  title =               {Applications of recursive arithmetic to the problem
                         of circuit synthesis},
  booktitle =           {{S}ummaries of the {S}ummer {I}nstitute of
                         {S}ymbolic {L}ogic~-- Volume~1},
  publisher =           {Institute for Defense Analyses},
  pages =               {3-50},
  year =                {1960},
  confyear =            {1957},
}

@inproceedings{icm1962-Chu,
  author =              {Church, Alonzo},
  title =               {Logic, arithmetic, and automata},
  booktitle =           {{P}roceedings of the {I}nternational {C}ongress of
                         {M}athematicians ({ICM}'62)},
  acronym =             {{ICM}'62},
  pages =               {23-35},
  year =                {1963},
  confyear =            {1962},
  confmonth =           {8},
}

@book{hbmc18-CHVB,
  author =              {Clarke, Edmund M. and Henzinger, Thomas A. and
                         Veith, Helmut and Bloem, Roderick},
  title =               {Handbook of Model Checking},
  publisher =           {Springer-Verlag},
  year =                {2018},
  month =               apr,
  doi =                 {10.1007/978-3-319-10575-8},
}

@inproceedings{lics1997-CJ,
  author =              {Comon, Hubert and Jacquemard, Florent},
  title =               {Ground Reducibility is {EXPTIME}-Complete},
  booktitle =           {{P}roceedings of the 12th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'97)},
  acronym =             {{LICS}'97},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {26-34},
  year =                {1997},
  month =               jun,
}

@inproceedings{cav1998-CJ,
  author =              {Comon, Hubert and Jurski, Yan},
  title =               {Multiple counters automata, safety analysis, and
                         {P}resburger arithmetic},
  editor =              {Hu, Alan J. and Vardi, Moshe Y.},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'98)},
  acronym =             {{CAV}'98},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1427},
  pages =               {268-279},
  year =                {1998},
  month =               jun,
  doi =                 {10.1007/BFb0028751},
}

@techreport{lsv-99-6,
  author =              {Comon, Hubert and Jurski, Yan},
  title =               {Timed Automata and the Theory of Real Numbers},
  number =              {LSV-99-6},
  year =                {1999},
  month =               jul,
  institution =         {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {Research Report},
}

@inproceedings{concur1999-CJ,
  author =              {Comon, Hubert and Jurski, Yan},
  title =               {Timed Automata and the Theory of Real Numbers},
  editor =              {Baeten, Jos C. M. and Mauw, Sjouke},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'99)},
  acronym =             {{CONCUR}'99},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1664},
  pages =               {242-257},
  year =                {1999},
  month =               aug,
  doi =                 {10.1007/3-540-48320-9_18},
}

@article{moor44(4)-CJKU,
  author =              {Correa, Jos{\'e} R. and de~Jong, Jasper and
                         de~Keizer, Bart and Uetz, Marc},
  title =               {The inefficiency of {N}ash and subgame-perfect
                         equilibria for network routing},
  publisher =           {Informs},
  journal =             {Mathematics of Operations Research},
  volume =              {44},
  number =              {4},
  pages =               {1286-1303},
  year =                {2019},
  month =               nov,
  doi =                 {10.1287/moor.2018.0968},
}

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

@inproceedings{lics2002-CJLV,
  author =              {Clarke, Edmund M. and Jha, Somesh and Lu, Yuan and
                         Veith, Helmut},
  title =               {Tree-Like Counterexamples in Model Checking},
  booktitle =           {{P}roceedings of the 17th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'02)},
  acronym =             {{LICS}'02},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {19-29},
  year =                {2002},
  month =               jul,
}

Résumé

Timed automata are a convenient mathematical model for modelling and reasoning about real-time systems. While they provide a powerful way of representing timing aspects of such systems, timed automata assume arbitrary precision and zero-delay actions; in particular, a state might be declared reachable in a timed automaton, but impossible to reach in the physical system it models.

In this paper, we consider permissive strategies as a way to overcome this problem: such strategies propose intervals of delays instead of single delays, and aim at reaching a target state whichever delay actually takes place. We develop an algorithm for computing the optimal permissiveness (and an associated maximally-permissive strategy) in acyclic timed automata and games.

@inproceedings{formats2020-CJMM,
  author =              {Clement, Emily and J{\'e}ron, Thierry and Markey,
                         Nicolas and Mentr{\'e}, David},
  title =               {Computing maximally-permissive strategies in acyclic
                         timed automata},
  editor =              {Bertrand, Nathalie and Jansen, Nils},
  booktitle =           {{P}roceedings of the 18th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'20)},
  acronym =             {{FORMATS}'20},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {12288},
  pages =               {111-126},
  year =                {2020},
  month =               sep,
  doi =                 {10.1007/978-3-030-57628-8_7},
  abstract =            {Timed automata are a convenient mathematical model
                         for modelling and reasoning about real-time systems.
                         While they provide a powerful way of representing
                         timing aspects of such systems, timed automata
                         assume arbitrary precision and zero-delay actions;
                         in~particular, a~state might be declared reachable
                         in a timed automaton, but impossible to reach in the
                         physical system it models. \par In this paper, we
                         consider permissive strategies as a way to overcome
                         this problem: such strategies propose intervals of
                         delays instead of single delays, and aim at reaching
                         a target state whichever delay actually takes place.
                         We develop an algorithm for computing the optimal
                         permissiveness (and~an associated
                         maximally-permissive strategy) in acyclic timed
                         automata and games.},
}

@inproceedings{stoc2005-CK,
  author =              {Christodoulou, George and Koutsoupias, Elias},
  title =               {The price of anarchy of finite congestion games},
  editor =              {Gabow, Harold N. and Fagin, Ronald},
  booktitle =           {{P}roceedings of the 37th {A}nnual {ACM} {S}ymposium
                         on the {T}heory of {C}omputing ({STOC}'05)},
  acronym =             {{STOC}'05},
  publisher =           {ACM Press},
  pages =               {67-73},
  year =                {2005},
  month =               may,
  doi =                 {10.1145/1060590.1060600},
}

@inproceedings{CKL-icccn1998,
  author =              {Castanet, Richard and Kon{\'e}, Ousmane and
                         Lauren{\c{c}}ot, Patrice},
  title =               {On-the-fly Test Generation for Real Time Protocols},
  booktitle =           {{P}roceedings of the {I}nternational {C}onference On
                         {C}omputer {C}ommunications and {N}etworks
                         ({ICCCN}'98)},
  acronym =             {{ICCCN}'98},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {378-387},
  year =                {1998},
  month =               oct,
  doi =                 {10.1109/ICCCN.1998.998798},
}

@article{jacm28(1)-CKS,
  author =              {Chandra, Ashok K. and Kozen, Dexter C. and
                         Stockmeyer, Larry J.},
  title =               {Alternation},
  publisher =           {ACM Press},
  journal =             {Journal of the~ACM},
  volume =              {28},
  number =              {1},
  pages =               {114-133},
  year =                {1981},
  month =               jan,
}

@inproceedings{tacas2001-CKV,
  author =              {Chockler, Hana and Kupferman, Orna and Vardi, Moshe
                         Y.},
  title =               {Coverage Metrics for Temporal Logic Model Checking},
  editor =              {Margaria, Tiziana and Yi, Wang},
  booktitle =           {{P}roceedings of the 7th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'01)},
  acronym =             {{TACAS}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2031},
  pages =               {528-542},
  year =                {2001},
  month =               apr,
}

@inproceedings{concur2000-CL,
  author =              {Cassez, Franck and Larsen, Kim Guldstrand},
  title =               {The Impressive Power of Stopwatches},
  editor =              {Palamidessi, Catuscia},
  booktitle =           {{P}roceedings of the 11th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'00)},
  acronym =             {{CONCUR}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1877},
  pages =               {138-152},
  year =                {2000},
  month =               aug,
  doi =                 {10.1007/3-540-44618-4_12},
}

@inproceedings{express2002-CL,
  author =              {Cleaveland, Rance and L{\"u}ttgen, Gerald},
  title =               {A Logical Process Calculi},
  editor =              {Nestmann, Uwe and Panangaden, Prakash},
  booktitle =           {{P}roceedings of the 9th {I}nternational {W}orkshop
                         on {E}xpressiveness in {C}oncurrency ({EXPRESS}'02)},
  acronym =             {{EXPRESS}'02},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {68},
  number =              {2},
  pages =               {33-50},
  year =                {2002},
  month =               aug,
}

@inproceedings{stacs2004-CL,
  author =              {Colcombet, {\relax Th}omas and L{\"o}ding, Christof},
  title =               {On the Expressiveness of Deterministic transducers
                         over Infinite Trees},
  editor =              {Diekert, Volker and Habib, Michel},
  booktitle =           {{P}roceedings of the 21st {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'04)},
  acronym =             {{STACS}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2996},
  pages =               {428-439},
  year =                {2003},
  month =               mar,
}

@incollection{CSEH2003-CL,
  author =              {Crochemore, Maxime and Lecrocq, {\relax Th}ierry},
  title =               {Pattern Matching and Text Compression Algorithms},
  editor =              {Tucker, Allen B.},
  booktitle =           {Computer Science and Engineering Handbook},
  publisher =           {CRC Press},
  pages =               {161-202},
  year =                {2003},
}

@inproceedings{fskd2007-CL,
  author =              {Chen, Taolue and Lu, Jian},
  title =               {Probabilistic Alternating-time Temporal Logic and
                         Model Checking Algorithm},
  editor =              {Lei, J.},
  booktitle =           {{P}roceedings of the 4th {I}nternational
                         {C}onference on {F}uzzy {S}ystems and {K}nowledge
                         {D}iscovery ({FSKD}'07)},
  acronym =             {{FSKD}'07},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {35-39},
  year =                {2007},
  month =               aug,
  doi =                 {10.1109/FSKD.2007.458},
}

@inproceedings{aaai2015-CLM,
  author =              {{\v{C}}erm{\'a}k, Petr and Lomuscio, Alessio and
                         Murano, Aniello},
  title =               {Verifying and Synthesising Multi-Agent Systems
                         against One-Goal Strategy Logic Specifications},
  editor =              {Bonet, Blai and Koenig, Sven},
  booktitle =           {{P}roceedings of the 29th {AAAI} {C}onference on
                         {A}rtificial {I}ntelligence ({AAAI}'15)},
  acronym =             {{AAAI}'15},
  publisher =           {AAAI Press},
  pages =               {2038-2044},
  year =                {2015},
  month =               jan,
}

@inproceedings{cav2014-CLMM,
  author =              {{\v{C}}erm{\'a}k, Petr and Lomuscio, Alessio and
                         Mogavero, Fabio and Murano, Aniello},
  title =               {{MCMAS-SLK}: A~Model Checker for the Verification of
                         Strategy Logic Specifications},
  editor =              {Biere, Armin and Bloem, Roderick},
  booktitle =           {{P}roceedings of the 26th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'14)},
  acronym =             {{CAV}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8559},
  pages =               {525-532},
  year =                {2014},
  month =               jul,
  doi =                 {10.1007/978-3-319-08867-9_34},
}

Résumé

In this report, the program, research issues, and results of Dagstuhl Seminar 15061 "Non-Zero-Sum-Games and Control" are described. The area of non-zero-sum games is addressed in a wide range of topics: multi-player games, partial-observation games, quantitative game models, and—as a special focus—connections with control engineering (supervisory control).

@proceedings{dagrep5(2)-CLMT,
  title =               {Non-Zero-Sum-Games and Control ({D}agstuhl
                         Seminar~15061)},
  editor =              {Chatterjee, Krishnendu and Lafortune, St{\'e}phane
                         and Markey, Nicolas and Thomas, Wolfgang},
  booktitle =           {Non-Zero-Sum-Games and Control ({D}agstuhl
                         Seminar~15061)},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  journal =             {Dagstuhl Reports},
  volume =              {5},
  number =              {2},
  pages =               {1-25},
  year =                {2015},
  month =               jun,
  doi =                 {10.4230/DagRep.5.2.1},
  url =                 {http://drops.dagstuhl.de/opus/volltexte/2015/5042},
  abstract =            {In this report, the program, research issues, and
                         results of Dagstuhl Seminar~15061
                         {"}Non-Zero-Sum-Games and Control{"} are described.
                         The area of non-zero-sum games is addressed in a
                         wide range of topics: multi-player games,
                         partial-observation games, quantitative game models,
                         and---as~a special focus---connections with control
                         engineering (supervisory control).},
}

@inproceedings{lcc1994-Clo,
  author =              {Clote, Peter},
  title =               {Computation Models and Function Algebras},
  editor =              {Leivant, Daniel},
  booktitle =           {{P}roceedings of the 1st {I}nternational {W}orkshop
                         on {L}ogic and {C}omputation {C}omplexity
                         ({LCC}'94)},
  acronym =             {{LCC}'94},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {960},
  pages =               {98-130},
  year =                {1994},
  month =               oct,
}

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

@inproceedings{tacas2001-CLS,
  author =              {Ciardo, Gianfranco and L{\"u}ttgen, Gerald and
                         Siminiceanu, Radu},
  title =               {Saturation: An Efficient Iteration Strategy for
                         Symbolic State-Space Generation},
  editor =              {Margaria, Tiziana and Yi, Wang},
  booktitle =           {{P}roceedings of the 7th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'01)},
  acronym =             {{TACAS}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2031},
  pages =               {328-342},
  year =                {2001},
  month =               apr,
}

@article{tcs109(1-2)-CM,
  author =              {Courcelle, Bruno and Mosbah, Mohamed},
  title =               {Monadic second-order evaluations on
                         tree-decomposable graphs},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {109},
  number =              {1-2},
  pages =               {49-82},
  year =                {1993},
  doi =                 {10.1016/0304-3975(93)90064-Z},
}

@incollection{dimacs35-CM,
  author =              {Cook, Stephen A. and Mitchell, David G.},
  title =               {Finding Hard Instances of the Satisfiability
                         Problem: A Survey},
  editor =              {Du, Ding-zhu and Gu, Jun and Pardalos, Panos M.},
  booktitle =           {Satisfiability Problem: Theory and Applications},
  publisher =           {American Mathematical Society},
  series =              {DIMACS Series in Discrete Mathematics and
                         Theoretical Computer Science},
  volume =              {35},
  pages =               {1-17},
  year =                {1997},
  month =               oct,
}

@inproceedings{express2002-CM,
  author =              {Carbone, Marco and Maffeis, Sergio},
  title =               {On the Expressive Power of Polyadic Synchronisation
                         in {\(\pi\)}-calculus},
  editor =              {Nestmann, Uwe and Panangaden, Prakash},
  booktitle =           {{P}roceedings of the 9th {I}nternational {W}orkshop
                         on {E}xpressiveness in {C}oncurrency ({EXPRESS}'02)},
  acronym =             {{EXPRESS}'02},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {68},
  number =              {2},
  pages =               {15-32},
  year =                {2002},
  month =               aug,
}

@article{tcs297(1-3)-CM,
  author =              {Carton, Olivier and Michel, Max},
  title =               {Unambiguous B{\"u}chi Automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {297},
  number =              {1-3},
  pages =               {37-81},
  year =                {2003},
  month =               mar,
}

@inproceedings{sat2006-CM,
  author =              {Cotton, Scott and Maler, Oded},
  title =               {Fast and Flexible Difference Constraint Propagation
                         for {DPLL(T)}},
  editor =              {Biere, Armin and Gomes, Carla P.},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {T}heory and {A}pplications of
                         {S}atisfiability {T}esting ({SAT}'06)},
  acronym =             {{SAT}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4121},
  pages =               {170-183},
  year =                {2006},
  month =               aug,
}

@incollection{afsec2008-CM,
  author =              {Cassez, Franck and Markey, Nicolas},
  title =               {Contr{\^o}le des syst{\`e}mes temporis{\'e}s},
  editor =              {Roux, Olivier H. and Jard, Claude},
  booktitle =           {Approches formelles des syst{\`e}mes embarqu{\'e}s
                         communicants},
  publisher =           {Herm{\`e}s},
  pages =               {105-144},
  chapter =             {4},
  year =                {2008},
  month =               oct,
  url =                 {http://e.lavoisier.fr/produit/9782746243156},
}

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

@inproceedings{hscc2008-CMH,
  author =              {Chatterjee, Krishnendu and Majumdar, Rupak and
                         Henzinger, Thomas A.},
  title =               {Controller Synthesis with Budget Constraints},
  editor =              {Egerstedt, Magnus and Mishra, Bud},
  booktitle =           {{P}roceedings of the 11th {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
                         ({HSCC}'08)},
  acronym =             {{HSCC}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4981},
  year =                {2008},
  month =               apr,
}

@inproceedings{csl2004-CMJ,
  author =              {Chatterjee, Krishnendu and Majumdar, Rupak and
                         Jurdzi{\'n}ski, Marcin},
  title =               {On {N}ash equilibria in stochastic games},
  editor =              {Marcinkowski, Jerzy and Tarlecki, Andrzej},
  booktitle =           {{P}roceedings of the 18th {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'04)},
  acronym =             {{CSL}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3210},
  year =                {2004},
  month =               sep,
}

@inproceedings{fmcad2004-CMP,
  author =              {Chou, Ching-Tsun and Mannava, Phanindra K. and Park,
                         Seungjoon},
  title =               {A Simple Method for Parameterized Verification of
                         Cache Coherence Protocols},
  editor =              {Hu, Alan J. and Martin, Andrew K.},
  booktitle =           {{P}roceedings of the 5th {I}nternational
                         {C}onference on {F}ormal {M}ethods in
                         {C}omputer-{A}ided {D}esign ({FMCAD}'04)},
  acronym =             {{FMCAD}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3312},
  pages =               {382-398},
  year =                {2004},
  month =               nov,
  doi =                 {10.1007/978-3-540-30494-4_27},
}

@inproceedings{safecomp2001-CMR,
  author =              {Caspi, Paul and Mazuet, Christine and
                         Reynaud{-}Paligot, Natacha},
  title =               {About the design of distributed control systems:
                         The~quasi-synchronous approach},
  editor =              {Voges, Udo},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {C}onference on {C}omputer {S}afety, {R}eliability
                         and {S}ecurity ({SAFECOMP}'01)},
  acronym =             {{SAFECOMP}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2187},
  pages =               {215-226},
  year =                {2001},
  month =               sep,
  doi =                 {10.1007/3-540-45416-0_21},
}

@article{dam108(1-2)-CMR,
  author =              {Courcelle, Bruno and Makowsky, Johann A. and Rotics,
                         Udi},
  title =               {On the fixed parameter complexity of graph
                         enumeration problems definable in monadic
                         second-order logic},
  publisher =           {Elsevier},
  journal =             {Discrete Applied Mathematics},
  volume =              {108},
  number =              {1-2},
  pages =               {23-52},
  year =                {2001},
  month =               feb,
}

@inproceedings{COG-ftrtft1998,
  author =              {Cardell-Oliver, Rachel and Glover, Tim},
  title =               {A~Practical and Complete Algorithm for Testing
                         Real-Time Systems},
  editor =              {Ravn, Anders P. and Rischel, Hans},
  booktitle =           {{P}roceedings of the 5th {F}ormal {T}echniques in
                         {R}eal-Time and {F}ault-Tolerant {S}ystems
                         ({FTRTFT}'98)},
  acronym =             {{FTRTFT}'98},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1486},
  pages =               {251-261},
  year =                {1998},
  month =               sep,
  doi =                 {10.1007/BFb0055352},
}

@inproceedings{stacs2012-Col,
  author =              {Colcombet, {\relax Th}omas},
  title =               {Forms of determinism for automata},
  editor =              {D{\"u}rr, Christoph and Wilke, Thomas},
  booktitle =           {{P}roceedings of the 29th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'12)},
  acronym =             {{STACS}'12},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {14},
  pages =               {1-23},
  year =                {2012},
  month =               feb,
  doi =                 {10.4230/LIPIcs.STACS.2012.1},
}

@inproceedings{stoc1971-Coo,
  author =              {Cook, Stephen A.},
  title =               {The complexity of Theorem Proving Procedures},
  booktitle =           {{P}roceedings of the 3rd {A}nnual {ACM} {S}ymposium
                         on the {T}heory of {C}omputing ({STOC}'71)},
  acronym =             {{STOC}'71},
  publisher =           {ACM Press},
  pages =               {151-158},
  year =                {1971},
}

@article{icont64(1-3)-cook,
  author =              {Cook, Stephen A.},
  title =               {A Taxonomy of Problems with Fast Parallel
                         Algorithms},
  publisher =           {Academic Press},
  journal =             {Information and Control},
  volume =              {64},
  number =              {1-3},
  pages =               {2-22},
  year =                {1985},
}

@incollection{CCP2004-cook,
  author =              {Cook, Stephen A.},
  title =               {Theories for Complexity Classes and their
                         Propositional Translations},
  editor =              {Kraj{\'\i}{\v c}ek, Jan},
  booktitle =           {Complexity of computations and proofs},
  publisher =           {Dipartimento di Matematica, Seconda Universit{\'a}
                         degli Studi di Napoli, Italy},
  series =              {Quaderni di Matematica},
  volume =              {13},
  pages =               {175-227},
  year =                {2004},
}

@article{icomp85(1)-Cou,
  author =              {Courcelle, Bruno},
  title =               {The Monadic Second-Order Logic of Graphs.
                         {I}:~{R}ecognizable Sets of Finite Graphs},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {85},
  number =              {1},
  pages =               {12-75},
  year =                {1990},
  month =               mar,
}

@incollection{handbookGG1997-Cou,
  author =              {Courcelle, Bruno},
  title =               {The expression of graph properties and graph
                         transformations in monadic second-order logic},
  editor =              {Rozenberg, Grzegorz},
  booktitle =           {Handbook of Graph Grammars},
  publisher =           {World Scientific},
  pages =               {313-400},
  year =                {1997},
}

@inproceedings{ciaa2004-Cou,
  author =              {Couvreur, Jean-Michel},
  title =               {A {BDD}-like Implementation of an Automaton Package},
  editor =              {Domaratzki, Michael and Okhatin, Alexander and
                         Salomaa, Arto and Yu, Sheng},
  booktitle =           {{R}evised {S}elected {P}apers of the 9th
                         {I}nternational {C}onference on Implementation and
                         Application of Automata ({CIAA}'04)},
  acronym =             {{CIAA}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3317},
  pages =               {310-311},
  year =                {2004},
  month =               jul,
}

@phdthesis{hab-couvreur,
  author =              {Couvreur, Jean-Michel},
  title =               {Contribution {\`a} l'algorithmique de la
                         v{\'e}rification},
  year =                {2004},
  month =               jul,
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {M\'emoire d'habilitation},
}

@article{tit18(1)-Cov,
  author =              {Cover, Thomas M.},
  title =               {Broadcast Channels},
  publisher =           {IEEE Inf. Theory Soc.},
  journal =             {IEEE Transactions on Information Theory},
  volume =              {18},
  number =              {1},
  pages =               {2-14},
  year =                {1972},
  month =               jan,
  doi =                 {10.1109/TIT.1972.1054727},
}

@article{tit44(6)-Cov,
  author =              {Cover, Thomas M.},
  title =               {Comments on Broadcast Channels},
  publisher =           {IEEE Inf. Theory Soc.},
  journal =             {IEEE Transactions on Information Theory},
  volume =              {44},
  number =              {6},
  pages =               {2524-2530},
  year =                {1998},
  month =               oct,
  doi =                 {10.1109/18.720547},
}

@inproceedings{acc1997-CP,
  author =              {Chen, Yi-Liang and Provan, Gregory},
  title =               {Modeling and Diagnosis of Timed Discrete Event
                         Systems~-- A~Factory Automation Example},
  booktitle =           {Proceedings of the 1997 American Control Conference
                         ({ACC}'97)},
  acronym =             {{ACC}'97},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {31-36},
  year =                {1997},
  month =               jun,
  doi =                 {10.1109/ACC.1997.611749},
}

@article{lmcs4(2)-CPJ,
  author =              {Comon, Hubert and Perrin, Nicolas and Jacquemard,
                         Florent},
  title =               {Visibly Tree Automata with Memory and Constraints},
  journal =             {Logical Methods in Computer Science},
  volume =              {4},
  number =              {2},
  year =                {2008},
  month =               may,
  doi =                 {10.2168/LMCS-4(2:8)2008},
}

@article{jcss46(3)-CPP,
  author =              {Cohen, Jo{\"e}lle and Perrin, Dominique and Pin,
                         Jean-{\'E}ric},
  title =               {On the Expressive Power of Temporal Logic},
  publisher =           {Academic Press},
  journal =             {Journal of Computer and System Sciences},
  volume =              {46},
  number =              {3},
  pages =               {271-294},
  year =                {1993},
  month =               jun,
}

@inproceedings{vmcai2002-CPRS,
  author =              {Cimatti, Alessandro and Pistore, Marco and Roveri,
                         Marco and Sebastiani, Roberto},
  title =               {Improving the Encoding of {LTL} Model Checking into
                         {SAT}},
  editor =              {Cortesi, Agostino},
  booktitle =           {{P}roceedings of the 3rd {I}nternational {W}orkshop
                         on {V}erification, {M}odel {C}hecking, and
                         {A}bstract {I}nterpretation ({VMCAI}'02)},
  acronym =             {{VMCAI}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2294},
  pages =               {196-207},
  year =                {2002},
  month =               jan,
}

@article{tcs382(2)-CR,
  author =              {Carton, Olivier and Rispal, Chlo{\'e}},
  title =               {Complementation of rational sets on scattered linear
                         orderings of finite rank},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {382},
  number =              {2},
  pages =               {109-119},
  year =                {2007},
  month =               aug,
}

@article{tcs45(1)-Cro,
  author =              {Crochemore, Maxime},
  title =               {Transducers and Repetitions},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {45},
  number =              {1},
  pages =               {63-86},
  year =                {1986},
}

@techreport{arxiv12-CRR,
  author =              {Chatterjee, Krishnendu and Randour, Mickael and
                         Raskin, Jean-Fran{\c c}ois},
  title =               {Strategy Synthesis for Multi-dimensional
                         Quantitative Objectives},
  number =              {1201.5073},
  year =                {2012},
  month =               jan,
  institution =         {arXiv},
  type =                {Research Report},
}

@article{acta51(3-4)-CRR,
  author =              {Chatterjee, Krishnendu and Randour, Mickael and
                         Raskin, Jean-Fran{\c c}ois},
  title =               {Strategy Synthesis for Multi-dimensional
                         Quantitative Objectives},
  publisher =           {Springer-Verlag},
  journal =             {Acta Informatica},
  volume =              {51},
  number =              {3-4},
  pages =               {129-163},
  year =                {2014},
  month =               jun,
  doi =                 {10.1007/s00236-013-0182-6},
}

@inproceedings{fireworks2000-CRS,
  author =              {Cassez, Franck and Ryan, Mark D. and Schobbens,
                         Pierre-Yves},
  title =               {Proving Feature Non-Interaction with
                         Alternating-Time Temporal Logic},
  editor =              {Gilmore, Stephen D. and Ryan, Mark D.},
  booktitle =           {{P}roceedings of the {FIRE}works {W}orkshop on
                         {L}anguage {C}onstructs for {D}escribing {F}eatures},
  publisher =           {Springer-Verlag},
  pages =               {85-104},
  year =                {2001},
  month =               jan,
  confyear =            {2000},
  confmonth =           {5},
}

@inproceedings{gtdt2004-CRVW,
  author =              {Cheng, Shih-Fen and Reeves, Daniel M. and
                         Vorobeychik, Yevgeniy and Wellman, Michael P.},
  title =               {Notes on Equilibria in Symmetric Games},
  editor =              {Parsons, Simon and Gmytrasiewicz, Piotr},
  booktitle =           {{P}roceedings of the 6th {I}nternational {W}orkshop
                         on Game Theoretic and Decision Theoretic Agents
                         ({GTDT}'04)},
  acronym =             {{GTDT}'04},
  pages =               {71-78},
  year =                {2004},
  month =               jun,
}

@article{fmsd2(2)-CS,
  author =              {Cleaveland, Rance and Steffen, Bernhard},
  title =               {A Linear-Time Model-Checking Algorithm for the
                         Alternation-Free Modal Mu-Calculus},
  publisher =           {Kluwer Academic},
  journal =             {Formal Methods in System Design},
  volume =              {2},
  number =              {2},
  pages =               {121-147},
  year =                {1992},
  doi =                 {10.1007/BF01383878},
}

@incollection{HARb-2001-24-CS,
  author =              {Clarke, Edmund M. and Schlingloff, Bernd-Holger},
  title =               {Model Checking},
  editor =              {Robinson, John Alan and Voronkov, Andrei},
  booktitle =           {Handbook of Automated Reasoning},
  publisher =           {Elsevier and MIT Press},
  volume =              {2},
  pages =               {1635-1790},
  year =                {2001},
}

@article{ipl87(3)-CS,
  author =              {Crochemore, Maxime and Stefanov, Valery T.},
  title =               {Waiting time and complexity for matching patterns
                         with automata},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {87},
  number =              {3},
  pages =               {119-125},
  year =                {2003},
  month =               aug,
  doi =                 {10.1016/S0020-0190(03)00271-0},
}

@book{EIT2006-CT,
  author =              {Cover, Thomas M. and Thomas, Joy A.},
  title =               {Elements of Information Theory},
  publisher =           {John Wiley \& Sons},
  edition =             {2},
  year =                {2006},
}

@techreport{tr148-CTL,
  author =              {Collberg, Christian and Thomborson, Clark and Low,
                         Douglas},
  title =               {A Taxonomy of Obfuscating Transformations},
  number =              {148},
  year =                {1997},
  month =               jul,
  institution =         {Department of Computer Science, University of
                         Auckland, New Zealand},
  type =                {Technical Report},
}

@inproceedings{smc1999-CTMKC,
  author =              {Campos, S{\'e}rgio Vale Aguiar and Teixeira,
                         M{\'a}rcio and Minea, Marius and Kuehlmann, Andreas
                         and Clarke, Edmund M.},
  title =               {Model Checking Semi-Continuous Time Models Using
                         {BDD}s},
  editor =              {Cimatti, Alessandro and Grumberg, Orna},
  booktitle =           {{P}roceedings of the 1st {I}nternational {W}orkshop
                         on {S}ymbolic {M}odel {C}hecking ({SMC}'99)},
  acronym =             {{SMC}'99},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {23},
  number =              {2},
  year =                {1999},
  month =               jul,
}

@inproceedings{concur2004-CTTV,
  author =              {Clarke, Edmund M. and Talupur, Muralidhar and
                         Touili, Tayssir and Veith, Helmut},
  title =               {Verification by network decomposition},
  editor =              {Gardner, {\relax Ph}ilippa and Yoshida, Nobuko},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'04)},
  acronym =             {{CONCUR}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3170},
  pages =               {276-291},
  year =                {2004},
  month =               aug,
  doi =                 {10.1007/978-3-540-28644-8_18},
}

@inproceedings{vmcai2006-CTV,
  author =              {Clarke, Edmund M. and Talupur, Muralidhar and Veith,
                         Helmut},
  title =               {Environment Abstraction for Parameterized
                         Verification},
  editor =              {Emerson, E. Allen and Namjoshi, Kedar},
  booktitle =           {{P}roceedings of the 7th {I}nternational {W}orkshop
                         on {V}erification, {M}odel {C}hecking, and
                         {A}bstract {I}nterpretation ({VMCAI}'06)},
  acronym =             {{VMCAI}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3855},
  pages =               {126-141},
  year =                {2006},
  month =               jan,
  doi =                 {10.1007/11609773_9},
}

@inproceedings{lics2012-CV,
  author =              {Chatterjee, Krishnendu and Velner, Yaron},
  title =               {Mean-Payoff Pushdown Games},
  booktitle =           {{P}roceedings of the 27th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'12)},
  acronym =             {{LICS}'12},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {195-204},
  year =                {2012},
  month =               jun,
  doi =                 {10.1109/LICS.2012.30},
}