C
[tC06] Balder ten Cate. Expressivity of Second Order Propositional Modal Logic. Journal of Philosophical Logic 35(2):209-223. Springer-Verlag, September 2006. 
@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,
}
[Cac03] Thierry Cachat. Games on Pushdown Graphs and Extensions. Thèse de doctorat, RWTH Aachen, Germany, December 2003. 
@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},
}
[Cac06] Thierry Cachat. Tree Automata Make Ordinal Theory Easy. In FSTTCS'06, Lecture Notes in Computer Science 4337, pages 285-296. Springer-Verlag, December 2006. 
@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,
}
[CdA+06] Krishnendu Chatterjee, Luca de Alfaro, and Thomas A. Henzinger. The Complexity of Quantitative Concurrent Parity Games. In SODA'06, pages 678-687. Society for Industrial and Applied Math., January 2006. 
@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},
}
[CdA+06] Krishnendu Chatterjee, Luca de Alfaro, and Thomas A. Henzinger. Strategy Improvement for Concurrent Reachability Games. In QEST'06, pages 291-300. IEEE Comp. Soc. Press, September 2006. 
@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},
}
[CdA+03] Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, and Mariëlle Stoelinga. Resource Interfaces. In EMSOFT'03, Lecture Notes in Computer Science 2855, pages 117-133. Springer-Verlag, October 2003. 
@inproceedings{emsoft2003-CAHS,
  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,
}
[Cai03] Benoît Caillaud. Project-Team S4. Activity Report, IRISA, Rennes, France, 2003. 
@techreport{AR-s4-2003,
  author =              {Caillaud, Beno{\^\i}t},
  title =               {Project-Team {S4}},
  year =                {2003},
  institution =         {IRISA, Rennes, France},
  type =                {Activity Report},
}
[CAM+04] Scott Cotton, Eugene Asarin, Oded Maler, and Peter Niebert. Some Progress in Satisfiability Checking for Difference Logic. In FORMATS-FTRTFT'04, Lecture Notes in Computer Science 3253, pages 263-276. Springer-Verlag, September 2004. 
@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,
}
[Cas87] Ilaria Castellani. Bisimulations and abstraction homomorphisms. Journal of Computer and System Sciences 34(2-3):210-235. Academic Press, April 1987. 
@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,
}
[Cas09] Franck Cassez. A note on fault diagnosis algorithms. In CDC'09, pages 6941-6946. IEEE Comp. Soc. Press, December 2009. 
@inproceedings{cdc2009-Cas,
  author =              {Cassez, Franck},
  title =               {A~note on fault diagnosis algorithms},
  booktitle =           {{P}roceedings of the 48th {IEEE} {C}onference on
                         {D}ecision and {C}ontrol ({CDC}'09)},
  acronym =             {{CDC}'09},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {6941-6946},
  year =                {2009},
  month =               dec,
  doi =                 {10.1109/CDC.2009.5399968},
}
[CB13] Franck Cassez and Jean-Luc Béchennec. Timing Analysis of Binary Programs with UPPAAL. In ACSD'13, pages 41-50. IEEE Comp. Soc. Press, July 2013. 
@inproceedings{acsd2013-CB,
  author =              {Cassez, Franck and B{\'e}chennec, Jean-Luc},
  title =               {Timing Analysis of Binary Programs with {UPPAAL}},
  editor =              {Carmona, Josep and Lazarescu, Mihai T. and
                         Pietkiewicz-Koutny, Marta},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {A}pplication of {C}oncurrency to
                         {S}ystem {D}esign ({ACSD}'13)},
  acronym =             {{ACSD}'13},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {41-50},
  year =                {2013},
  month =               jul,
  doi =                 {10.1109/ACSD.2013.7},
}
[CBC13] Christophe Chareton, Julien Brunel, and David Chemouil. Towards an Updatable Strategy Logic. In SR'13, Electronic Proceedings in Theoretical Computer Science 112, pages 91-98. March 2013. 
@inproceedings{sr2013-BCC,
  author =              {Chareton, Christophe and Brunel, Julien and
                         Chemouil, David},
  title =               {Towards an Updatable Strategy Logic},
  booktitle =           {{P}roceedings of the 1st {I}nternational {W}orkshop
                         on {S}trategic {R}easoning ({SR}'13)},
  acronym =             {{SR}'13},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {112},
  pages =               {91-98},
  year =                {2013},
  month =               mar,
  doi =                 {10.4204/EPTCS.112.14},
}
[CBK+13] Maximilien Colange, Souheib Baarir, Fabrice Kordon, and Yann Thierry-Mieg. Towards Distributed Software Model-Checking using Decision Diagrams. In CAV'13, Lecture Notes in Computer Science 8044, pages 830-845. Springer-Verlag, July 2013. 
@inproceedings{cav2013-CBKT,
  author =              {Colange, Maximilien and Baarir, Souheib and Kordon,
                         Fabrice and Thierry{-}Mieg, Yann},
  title =               {Towards Distributed Software Model-Checking using
                         Decision Diagrams},
  editor =              {Sharygina, Natasha and Veith, Helmut},
  booktitle =           {{P}roceedings of the 25th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'13)},
  acronym =             {{CAV}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8044},
  pages =               {830-845},
  year =                {2013},
  month =               jul,
  doi =                 {10.1007/978-3-642-39799-8_58},
}
[CC79] Patrick Cousot and Radhia Cousot. Constructive Versions of Tarski's Fixed Point Theorems. Pacific Journal of Mathematics 82(1):43-57. 1979. 
@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},
}
[CC94] Sérgio Vale Aguiar Campos and Edmund M. Clarke. Real-Time Symbolic Model Checking for Discrete Time Models. Technical Report CMU-CS-94-146, Computer Science Deparment, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA, May 1994. 
@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},
}
[CC95] Sérgio Vale Aguiar Campos and Edmund M. Clarke. Real-time symbolic model checking for discrete time models. In Teodor Rus and Charles Rattray (eds.), Real-time symbolic model checking for discrete time models, AMAST Series in Computing 2, pages 129-145. World Scientific, January 1995. 
@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,
}
[CC99] Sérgio Vale Aguiar Campos and Edmund M. Clarke. Analysis and verification of real-time systems using quantitative symbolic algorithms. International Journal on Software Tools for Technology Transfer 2(3):260-269. Springer-Verlag, November 1999. 
@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},
}
[CC00] Hubert Comon and Véronique Cortier. Flatness is not Weakness. In CSL'00, Lecture Notes in Computer Science 1862, pages 262-276. Springer-Verlag, August 2000. 
@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,
}
[CC01] Sérgio Vale Aguiar Campos and Edmund M. Clarke. The Verus Language: Representing Time Efficiently with BDDs. Theoretical Computer Science 253(1):95-118. Elsevier, February 2001. 
@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,
}
[CC02] Cristian S. Calude and Elena Calude. The Bridge Crossing Problem. EATCS Bulletin 77:180-190. EATCS, June 2002. 
@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,
}
[CCG+02] Alessandro Cimatti, Edmund M. Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. NuSMV2: An OpenSource Tool for Symbolic Model Checking. In CAV'02, Lecture Notes in Computer Science 2404, pages 359-364. Springer-Verlag, July 2002. 
@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,
}
[CCG+99] Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, and Marco Roveri. NuSMV: A New Symbolic Model Verifier. In CAV'99, Lecture Notes in Computer Science 1633, pages 495-499. Springer-Verlag, July 1999. 
@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,
}
[CCG+00] Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, and Marco Roveri. NuSMV: A New Symbolic Model Checker. International Journal on Software Tools for Technology Transfer 2(4):410-425. Springer-Verlag, March 2000. 
@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,
}
[CCJ06] Franck Cassez, Thomas Chatain, and Claude Jard. Symbolic Unfoldings for Networks of Timed Automata. In ATVA'06, Lecture Notes in Computer Science 4218, pages 307-321. Springer-Verlag, October 2006. 
@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},
}
[CCM+95] Sérgio Vale Aguiar Campos, Edmund M. Clarke, Wilfredo R. Marrero, and Marius Minea. Verifying the performance of the PCI local bus using symbolic techniques. In ICCD'95, pages 72-78. IEEE Comp. Soc. Press, October 1995. 
@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,
}
[CCM+94] Sérgio Vale Aguiar Campos, Edmund M. Clarke, Wilfredo R. Marrero, Marius Minea, and Hiromi Hiraishi. Computing Quantitative Characteristics of Finite-State Real-Time Systems. Technical Report CMU-CS-94-147, Computer Science Deparment, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA, May 1994. 
@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},
}
[CD88] Edmund M. Clarke and I. A. Draghicescu. Expressibility Results for Linear-Time and Branching-Time Logics. In REX'88, Lecture Notes in Computer Science 354, pages 428-437. Springer-Verlag, May 1988. 
@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,
}
[CD10] Krishnendu Chatterjee and Laurent Doyen. Energy Parity Games. In ICALP'10, Lecture Notes in Computer Science 6199, pages 599-610. Springer-Verlag, July 2010. 
@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,
}
[CD12] Krishnendu Chatterjee and Laurent Doyen. Energy Parity Games. Theoretical Computer Science 458:49-60. Elsevier, November 2012. 
@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},
}
[CDC04] Krishnendu Chatterjee, Pallab Dasgupta, and P. P. Chakrabarti. The power of first-order quantification over states in branching and linear time temporal logics. Information Processing Letters 91(5):201-210. Elsevier, September 2004. 
@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,
}
[CDF+05] Franck Cassez, Alexandre David, Emmanuel Fleury, Kim Guldstrand Larsen, and Didier Lime. Efficient On-the-fly Algorithms for the Analysis of Timed Games. In CONCUR'05, Lecture Notes in Computer Science 3653, pages 66-80. Springer-Verlag, August 2005. 
@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},
}
[CDH08] Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Quantitative Languages. In CSL'08, Lecture Notes in Computer Science 5213, pages 385-400. Springer-Verlag, September 2008. 
@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},
}
[CDH10] Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Quantitative Languages. ACM Transactions on Computational Logic 11(4). ACM Press, July 2010. 
@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},
}
[CDH+06] Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. Algorithms for Omega-Regular Games with Imperfect Information. In CSL'06, Lecture Notes in Computer Science 4207, pages 287-302. Springer-Verlag, September 2006. 
@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,
}
[CDH+10] Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. Generalized Mean-payoff and Energy Games. In FSTTCS'10, Leibniz International Proceedings in Informatics 8, pages 505-516. Leibniz-Zentrum für Informatik, December 2010. 
@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,
}
[CDL+07] Franck Cassez, Alexandre David, Kim Guldstrand Larsen, Didier Lime, and Jean-François Raskin. Timed Control with Observation Based and Stuttering Invariant Strategies. In ATVA'07, Lecture Notes in Computer Science 4762, pages 192-206. Springer-Verlag, October 2007. 
@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},
}
[CDM12] Franck Cassez, Jérémy Dubreil, and Hervé Marchand. Synthesis of opaque systems with static and dynamic masks. Formal Methods in System Design 40(1):88-115. Springer-Verlag, February 2012. 
@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},
}
[CDR+13] Krishnendu Chatterjee, Laurent Doyen, Mickael Randour, and Jean-François Raskin. Looking at Mean-Payoff and Total-Payoff through Windows. In ATVA'13, Lecture Notes in Computer Science 8172, pages 118-132. Springer-Verlag, October 2013. 
@inproceedings{atva2013-CDRR,
  author =              {Chatterjee, Krishnendu and Doyen, Laurent and
                         Randour, Mickael and Raskin, Jean-Fran{\c c}ois},
  title =               {Looking at Mean-Payoff and Total-Payoff through
                         Windows},
  editor =              {Hung, Dang Van and Ogawa, Mizuhito},
  booktitle =           {{P}roceedings of the 11th {I}nternational
                         {S}ymposium on {A}utomated {T}echnology for
                         {V}erification and {A}nalysis ({ATVA}'13)},
  acronym =             {{ATVA}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8172},
  pages =               {118-132},
  year =                {2013},
  month =               oct,
}
[CDR+15] Krishnendu Chatterjee, Laurent Doyen, Mickael Randour, and Jean-François Raskin. Looking at Mean-Payoff and Total-Payoff through Windows. Information and Computation 242:25-52. Elsevier, June 2015. 
@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},
}
[CDV02] Diego Calvanese, Giuseppe De Giacomo, and Moshe Y. Vardi. Reasoning about Actions and Planning in LTL Action Theories. In KR'02, pages 593-602. Morgan Kaufmann Publishers, April 2002. 
@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,
}
[CE80] Edmund M. Clarke and E. Allen Emerson. Characterizing properties of parallel programs as fixpoints. In ICALP'80, Lecture Notes in Computer Science 85, pages 169-181. Springer-Verlag, July 1980. 
@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,
}
[CE82] Edmund M. Clarke and E. Allen Emerson. Design and Synthesis of Synchronization Skeletons using Branching-Time Temporal Logic. In LOP'81, Lecture Notes in Computer Science 131, pages 52-71. Springer-Verlag, 1982. 
@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},
}
[CE11] Bruno Courcelle and Joost Engelfriet. Graph Structure and Monadic Second-Order Logic, a Language Theoretic Approach. Cambridge University Press, 2011. 
@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},
}
[CEJ+98] Edmund M. Clarke, E. Allen Emerson, Somesh Jha, and A. Prasad Sistla. Symmetry Reductions in Model Checking. In CAV'98, Lecture Notes in Computer Science 1427, pages 147-158. Springer-Verlag, June 1998. 
@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},
}
[Cer64] Ján Černý. Poznámka k homogénnym experimentom s konečnými automatmi. Matematicko-fyzikálny časopis 14(3):208-216. 1964. 
@article{mfc14(3)-Cer,
  author =              {{{C}}ern{\'y}, J{\'a}n},
  title =               {Pozn{\'a}mka k homog{\'e}nnym experimentom s
                         kone{{c}}n{\'y}mi automatmi},
  journal =             {Matematicko-fyzik{\'a}lny {{c}}asopis},
  volume =              {14},
  number =              {3},
  pages =               {208-216},
  year =                {1964},
}
[Cer93] Kārlis Čerāns. Decidability of Bisimulation Equivalences for Parallel Timer Processes. In CAV'92, Lecture Notes in Computer Science 663, pages 302-315. Springer-Verlag, 1993. 
@inproceedings{cav1992-Cer,
  author =              {{{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},
}
[CER93] Bruno Courcelle, Joost Engelfriet, and Grzegorz Rozenberg. Handle-rewriting hypergraph grammars. Journal of Computer and System Sciences 46(2). Academic Press, April 1993. 
@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},
}
[Cer14] Petr Čermák. A Model Checker for Strategy Logic. Master's thesis, Dept. of Computing, Imperial College London, UK, June 2014. 
@mastersthesis{master14-Cer,
  author =              {{{C}}erm{\'a}k, Petr},
  title =               {A~Model Checker for Strategy Logic},
  year =                {2014},
  month =               jun,
  school =              {Dept. of Computing, Imperial College London, UK},
}
[CES83] Edmund M. Clarke, E. Allen Emerson, and A. Prasad Sistla. Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications: A Practical Approach. In POPL'83, pages 117-126. ACM Press, January 1983. 
@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,
}
[CES86] Edmund M. Clarke, E. Allen Emerson, and A. Prasad Sistla. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems 8(2):244-263. ACM Press, April 1986. 
@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,
}
[CES09] Edmund M. Clarke, E. Allen Emerson, and Joseph Sifakis. Model checking: algorithmic verification and debugging. Communications of the ACM 52(11):74-84. ACM Press, November 2009. 
@article{cacm52(11)-CES,
  author =              {Clarke, Edmund M. and Emerson, E. Allen and Sifakis,
                         Joseph},
  title =               {Model checking: algorithmic verification and
                         debugging},
  publisher =           {ACM Press},
  journal =             {Communications of the ACM},
  volume =              {52},
  number =              {11},
  pages =               {74-84},
  year =                {2009},
  month =               nov,
  doi =                 {10.1145/1592761.1592781},
}
[CFG+16] Rodica Condurache, Emmanuel Filiot, Raffaella Gentilini, and Jean-François Raskin. The Complexity of Rational Synthesis. In ICALP'16, Leibniz International Proceedings in Informatics 55, pages 121:1-121:15. Leibniz-Zentrum für Informatik, July 2016. 
@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},
}
[CFH+03] Edmund M. Clarke, Ansgar Fehnker, Zhi Han, Bruce H. Krogh, Joël Ouaknine, Olaf Stursberg, and Michael Theobald. Abstraction and Countrexample-Guided Refinement in Model Checking of Hybrid Systems. International Journal of Foundations of Computer Science 14(4):583-604. August 2003. 
@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},
}
[CFK+12] Taolue Chen, Vojtěch Forejt, Marta Kwiatkowska, David Parker, and Aistis Simaitis. Automatic Verification of Competitive Stochastic Systems. In TACAS'12, Lecture Notes in Computer Science 7214, pages 315-330. Springer-Verlag, March 2012. 
@inproceedings{CFKPS-tacas2012,
  author =              {Chen, Taolue and Forejt, Vojt{{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,
}
[CFK+12] Taolue Chen, Vojtěch Forejt, Marta Kwiatkowska, Aistis Simaitis, Ashutosh Trivedi, and Michael Ummels. Playing Stochastic Games Precisely. In CONCUR'12, Lecture Notes in Computer Science 7454, pages 348-363. Springer-Verlag, September 2012. 
@inproceedings{CFKSTU-concur2012,
  author =              {Chen, Taolue and Forejt, Vojt{{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,
}
[CFP+96] Gérard Cécé, Alain Finkel, and S. Purushothaman Iyer. Unreliable Channels are Easier to Verify Than Perfect Channels. Information and Computation 124(1):20-31. Academic Press, January 1996. 
@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,
}
[CG87] Edmund M. Clarke and Orna Grumberg. Research on Automatic Verification of Finite-State Concurrent Systems. Annual Review of Computer Science 2:269-290. Annual Reviews Inc., 1987. 
@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},
}
[CG96] Boris V. Cherkassky and Andrew V. Goldberg. Negative-Cycle Detection Algorithm. In ESA'96, Lecture Notes in Computer Science 1136, pages 349-363. Springer-Verlag, September 1996. 
@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,
}
[CG14] Namit Chaturvedi and Marcus Gelderie. Weak ω-Regular Trace Languages. Research Report 1402.3199, arXiv, February 2014. 
@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},
}
[CGH97] Edmund M. Clarke, Orna Grumberg, and Kiyoharu Hamaguchi. Another Look at LTL Model Checking. Formal Methods in System Design 10(1):47-71. Kluwer Academic, February 1997. 
@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,
}
[CGJ+01] Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Progress on the State Explosion Problem in Model Checking. In Reinhard Wilhelm (eds.), Informatics – 10 Years Back. 10 Years Ahead, Lecture Notes in Computer Science 2000, pages 176-194. Springer-Verlag, 2001. 
@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},
}
[CGJ+03] Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-Guided Abstraction Refinement for Symbolic Model Checking. Journal of the ACM 50(5):752-794. ACM Press, September 2003. 
@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},
}
[CGL93] Kārlis Čerāns, Jens Christian Godskesen, and Kim Guldstrand Larsen. Timed Modal Specification - Theory and Tools. In CAV'93, Lecture Notes in Computer Science 697, pages 253-267. Springer-Verlag, June 1993. 
@inproceedings{cav1993-CGL,
  author =              {{{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,
}
[CGL94] Edmund M. Clarke, Orna Grumberg, and David E. Long. Model Checking. ACM Transactions on Programming Languages and Systems 16(5):1-45. ACM Press, September 1994. 
@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,
}
[CGM+95] Edmund M. Clarke, Orna Grumberg, Kenneth L. McMillan, and Xudong Zhao. Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. In DAC'95, pages 427-432. ACM Press, June 1995. 
@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,
}
[CGP00] Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model checking. MIT Press, 2000. 
@book{MC2000-CGP,
  author =              {Clarke, Edmund M. and Grumberg, Orna and Peled,
                         Doron A.},
  title =               {Model checking},
  publisher =           {MIT Press},
  year =                {2000},
}
[CGP+02] Alessandro Cimatti, Enrico Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. Integrating BDD-based and SAT-based Symbolic Model Checking. In FroCoS'02, Lecture Notes in Computer Science 2309, pages 49-56. Springer-Verlag, April 2002. 
@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,
}
[CGS98] Marco Cadoli, Andrea Giovanardi, and Marco Schaerf. An Algorithm to Evaluate Quantified Boolean Formulae. In AAAI-IAAI'98, pages 262-267. MIT Press, July 1998. 
@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,
}
[CH14] Arnaud Carayol and Matthew Hague. Regular Strategies In Pushdown Reachability Games. In RP'14, Lecture Notes in Computer Science 8762, pages 58-71. Springer-Verlag, September 2014. 
@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},
}
[Cha00] William Chan. Temporal-Logic Queries. In CAV'00, Lecture Notes in Computer Science 1855, pages 450-463. Springer-Verlag, July 2000. 
@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,
}
[Cha09] Patryk Chamuczyński. Algorithms and data structures for parametric analysis of real time systems. Thèse de doctorat, University of Göttingen, Germany, 2009. 
@phdthesis{phd-chamuczynski09,
  author =              {Patryk Chamuczy{\'n}ski},
  title =               {Algorithms and data structures for parametric
                         analysis of real time systems},
  year =                {2009},
  school =              {University of G{\"o}ttingen, Germany},
  type =                {Th\`ese de doctorat},
}
[Cha14] Namit Chaturvedi. Toward a structure theory of regular infinitary trace languages. In ICALP'14, Lecture Notes in Computer Science 8573, pages 134-145. Springer-Verlag, July 2014. 
@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},
}
[Cha14] Namit Chaturvedi. Languages of Infinite Traces and Deterministic Asynchronous Automata. Research Report AIB-2014-004, RWTH Aachen, Germany, February 2014. 
@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},
}
[CHJ04] Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdziński. Games with Secure Equilibria. In LICS'04, pages 160-169. IEEE Comp. Soc. Press, July 2004. 
@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,
}
[CHJ05] Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdziński. Mean-payoff Parity Games. In LICS'05, pages 178-187. IEEE Comp. Soc. Press, July 2005. 
@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,
}
[CHJ06] Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdziński. Games with Secure Equilibria. Theoretical Computer Science 365(1-2):67-82. Elsevier, November 2006. 
@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,
}
[Cho03] Hana Chockler. Coverage Metrics for Model Checking. PhD thesis, Hebrew University, Jerusalem, Israel, September 2003. 
@phdthesis{phd-chockler,
  author =              {Chockler, Hana},
  title =               {Coverage Metrics for Model Checking},
  year =                {2003},
  month =               sep,
  school =              {Hebrew University, Jerusalem, Israel},
}
[CHO+13] Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop, and Andreas Pavlogiannis. Distributed synthesis for LTL fragments. In FMCAD'13, pages 18-25. IEEE Comp. Soc. Press, October 2013. 
@inproceedings{fmcad2013-CHOP,
  author =              {Chatterjee, Krishnendu and Henzinger, Thomas A. and
                         Otop, Jan and Pavlogiannis, Andreas},
  title =               {Distributed synthesis for {LTL} fragments},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {F}ormal {M}ethods in
                         {C}omputer-{A}ided {D}esign ({FMCAD}'13)},
  acronym =             {{FMCAD}'13},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {18-25},
  year =                {2013},
  month =               oct,
}
[CHP07] Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. Generalized Parity Games. In FoSSaCS'07, Lecture Notes in Computer Science 4423, pages 153-167. Springer-Verlag, March 2007. 
@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,
}
[CHP07] Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. Strategy Logic. In CONCUR'07, Lecture Notes in Computer Science 4703, pages 59-73. Springer-Verlag, September 2007. 
@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},
}
[CHP08] Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. Algorithms for Büchi games. Research Report 0805.2620, Computing Research Repository, May 2008. 
@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 =         {Computing Research Repository},
  type =                {Research Report},
}
[CHP10] Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. Strategy Logic. Information and Computation 208(6):677-693. Elsevier, June 2010. 
@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},
}
[CHP11] Krishnendu Chatterjee, Thomas A. Henzinger, and Vinayak S. Prabhu. Timed Parity Games: Complexity and Robustness. Logical Methods in Computer Science 7(4). December 2011. 
@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},
}
[CHR02] Franck Cassez, Thomas A. Henzinger, and Jean-François Raskin. A Comparison of Control Problems for Timed and Hybrid Systems. In HSCC'02, Lecture Notes in Computer Science 2289, pages 134-148. Springer-Verlag, March 2002. 
@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,
}
[CHR12] Pavol Černý, Thomas A. Henzinger, and Arjun Radhakrishna. Simulation distances. Theoretical Computer Science 413(1):21-35. Elsevier, January 2012. 
@article{tcs413(1)-CHR,
  author =              {{{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},
}
[CHR13] Pavol Černý, Thomas A. Henzinger, and Arjun Radhakrishna. Quantitative abstraction refinement. In POPL'13, pages 115-128. ACM Press, January 2013. 
@inproceedings{popl2013-CHR,
  author =              {{{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},
}
[CHS11] Arnaud Carayol, Axel Haddad, and Olivier Serre. Qualitative Tree Languages. In LICS'11, pages 13-22. IEEE Comp. Soc. Press, June 2011. 
@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},
}
[Chu60] Alonzo Church. Applications of recursive arithmetic to the problem of circuit synthesis. In Summaries of the Summer Institute of Symbolic Logic – Volume 1, pages 3-50. Institute for Defense Analyses, 1960. 
@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},
}
[Chu63] Alonzo Church. Logic, arithmetic, and automata. In ICM'62, pages 23-35. 1963. 
@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},
}
[CHV+18] Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem. Handbook of Model Checking. Springer-Verlag, April 2018. 
@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},
}
[CJ97] Hubert Comon and Florent Jacquemard. Ground Reducibility is EXPTIME-Complete. In LICS'97, pages 26-34. IEEE Comp. Soc. Press, June 1997. 
@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,
}
[CJ98] Hubert Comon and Yan Jurski. Multiple counters automata, safety analysis, and Presburger arithmetic. In CAV'98, Lecture Notes in Computer Science 1427, pages 268-279. Springer-Verlag, June 1998. 
@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},
}
[CJ99] Hubert Comon and Yan Jurski. Timed Automata and the Theory of Real Numbers. Research Report LSV-99-6, Lab. Spécification & Vérification, ENS Cachan, France, July 1999. 
@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},
}
[CJ99] Hubert Comon and Yan Jurski. Timed Automata and the Theory of Real Numbers. In CONCUR'99, Lecture Notes in Computer Science 1664, pages 242-257. Springer-Verlag, August 1999. 
@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},
}
[CJL+09] Franck Cassez, Jan J. Jensen, Kim Guldstrand Larsen, Jean-François Raskin, and Pierre-Alain Reynier. Automatic Synthesis of Robust and Optimal Controllers – An Industrial Case Study. In HSCC'09, Lecture Notes in Computer Science 5469, pages 90-104. Springer-Verlag, April 2009. 
@inproceedings{hscc2009-CJLRR,
  author =              {Cassez, Franck and Jensen, Jan J. and Larsen, Kim
                         Guldstrand and Raskin, Jean-Fran{\c c}ois and
                         Reynier, Pierre-Alain},
  title =               {Automatic Synthesis of Robust and Optimal
                         Controllers~-- An~Industrial Case Study},
  editor =              {Majumdar, Rupak and Tabuada, Paulo},
  booktitle =           {{P}roceedings of the 12th {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
                         ({HSCC}'09)},
  acronym =             {{HSCC}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5469},
  pages =               {90-104},
  year =                {2009},
  month =               apr,
}
[CJL+02] Edmund M. Clarke, Somesh Jha, Yuan Lu, and Helmut Veith. Tree-Like Counterexamples in Model Checking. In LICS'02, pages 19-29. IEEE Comp. Soc. Press, July 2002. 
@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,
}
[CKL98] Richard Castanet, Ousmane Koné, and Patrice Laurençot. On-the-fly Test Generation for Real Time Protocols. In ICCCN'98, pages 378-387. IEEE Comp. Soc. Press, October 1998. 
@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},
}
[CKS81] Ashok K. Chandra, Dexter C. Kozen, and Larry J. Stockmeyer. Alternation. Journal of the ACM 28(1):114-133. ACM Press, January 1981. 
@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,
}
[CKV01] Hana Chockler, Orna Kupferman, and Moshe Y. Vardi. Coverage Metrics for Temporal Logic Model Checking. In TACAS'01, Lecture Notes in Computer Science 2031, pages 528-542. Springer-Verlag, April 2001. 
@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,
}
[CL00] Franck Cassez and Kim Guldstrand Larsen. The Impressive Power of Stopwatches. In CONCUR'00, Lecture Notes in Computer Science 1877, pages 138-152. Springer-Verlag, August 2000. 
@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},
}
[CL02] Rance Cleaveland and Gerald Lüttgen. A Logical Process Calculi. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 33-50. Elsevier, August 2002. 
@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,
}
[CL03] Thomas Colcombet and Christof Löding. On the Expressiveness of Deterministic transducers over Infinite Trees. In STACS'04, Lecture Notes in Computer Science 2996, pages 428-439. Springer-Verlag, March 2003. 
@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,
}
[CL03] Maxime Crochemore and Thierry Lecrocq. Pattern Matching and Text Compression Algorithms. In Allen B. Tucker (eds.), Computer Science and Engineering Handbook. CRC Press, 2003. 
@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},
}
[CLM15] Petr Čermák, Alessio Lomuscio, and Aniello Murano. Verifying and Synthesising Multi-Agent Systems against One-Goal Strategy Logic Specifications. In AAAI'15, pages 2038-2044. AAAI Press, January 2015. 
@inproceedings{aaai2015-CLM,
  author =              {{{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,
}
[CLM+14] Petr Čermák, Alessio Lomuscio, Fabio Mogavero, and Aniello Murano. MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications. In CAV'14, Lecture Notes in Computer Science 8559, pages 525-532. Springer-Verlag, July 2014. 
@inproceedings{cav2014-CLMM,
  author =              {{{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},
}
[CLM+15] Krishnendu Chatterjee, Stéphane Lafortune, Nicolas Markey, and Wolfgang Thomas (eds.) Non-Zero-Sum-Games and Control (Dagstuhl Seminar 15061). Dagstuhl Reports 5(2):1-25. Leibniz-Zentrum für Informatik, June 2015.
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–-mdash;as a special focus–-mdash;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).},
}
[Clo94] Peter Clote. Computation Models and Function Algebras. In LCC'94, Lecture Notes in Computer Science 960, pages 98-130. Springer-Verlag, October 1994. 
@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,
}
[CLP+11] Laura Carnevali, Giuseppe Lipari, Alessandro Pinzuti, and Enrico Vicario. A Formal Approach to Design and Verification of Two-Level Hierarchical Scheduling Systems. In ADA-EUROPE'11, Lecture Notes in Computer Science 6652, pages 118-131. Springer-Verlag, 2011. 
@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},
}
[CLS01] Gianfranco Ciardo, Gerald Lüttgen, and Radu Siminiceanu. Saturation: An Efficient Iteration Strategy for Symbolic State-Space Generation. In TACAS'01, Lecture Notes in Computer Science 2031, pages 328-342. Springer-Verlag, April 2001. 
@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,
}
[CM93] Bruno Courcelle and Mohamed Mosbah. Monadic second-order evaluations on tree-decomposable graphs. Theoretical Computer Science 109(1-2):49-82. Elsevier, 1993. 
@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},
}
[CM97] Stephen A. Cook and David G. Mitchell. Finding Hard Instances of the Satisfiability Problem: A Survey. In Ding-zhu Du, Jun Gu, and Panos M. Pardalos (eds.), Satisfiability Problem: Theory and Applications, DIMACS Series in Discrete Mathematics and Theoretical Computer Science 35, pages 1-17. American Mathematical Society, October 1997. 
@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,
}
[CM02] Marco Carbone and Sergio Maffeis. On the Expressive Power of Polyadic Synchronisation in π-calculus. In EXPRESS'02, Electronic Notes in Theoretical Computer Science 68(2), pages 15-32. Elsevier, August 2002. 
@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,
}
[CM03] Olivier Carton and Max Michel. Unambiguous Büchi Automata. Theoretical Computer Science 297(1-3):37-81. Elsevier, March 2003. 
@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,
}
[CM06] Scott Cotton and Oded Maler. Fast and Flexible Difference Constraint Propagation for DPLL(T). In SAT'06, Lecture Notes in Computer Science 4121, pages 170-183. Springer-Verlag, August 2006. 
@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,
}
[CM08] Franck Cassez and Nicolas Markey. Contrôle des systèmes temporisés. In Olivier H. Roux and Claude Jard (eds.), Approches formelles des systèmes embarqués communicants. Hermès, October 2008. 
@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://www.lavoisier.fr/notice/fr335499.html},
}
[CM09] Franck Cassez and Nicolas Markey. Control of Timed Systems. In Claude Jard and Olivier H. Roux (eds.), Communicating Embedded Systems – Software and Design. Wiley-ISTE, October 2009. 
@incollection{ces2009-CM,
  author =              {Cassez, Franck and Markey, Nicolas},
  title =               {Control of Timed Systems},
  editor =              {Jard, Claude and Roux, Olivier H.},
  booktitle =           {Communicating Embedded Systems~-- Software and
                         Design},
  publisher =           {Wiley-ISTE},
  pages =               {83-120},
  chapter =             {3},
  year =                {2009},
  month =               oct,
  url =                 {http://www.iste.co.uk/index.php?f=x&ACTION=View&id=288},
}
[CMH08] Krishnendu Chatterjee, Rupak Majumdar, and Thomas A. Henzinger. Controller Synthesis with Budget Constraints. In HSCC'08, Lecture Notes in Computer Science 4981. Springer-Verlag, April 2008. 
@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,
}
[CMJ04] Krishnendu Chatterjee, Rupak Majumdar, and Marcin Jurdziński. On Nash equilibria in stochastic games. In CSL'04, Lecture Notes in Computer Science 3210. Springer-Verlag, September 2004. 
@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,
}
[CMP04] Ching-Tsun Chou, Phanindra K. Mannava, and Seungjoon Park. A Simple Method for Parameterized Verification of Cache Coherence Protocols. In FMCAD'04, Lecture Notes in Computer Science 3312, pages 382-398. Springer-Verlag, November 2004. 
@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},
}
[CMR01] Paul Caspi, Christine Mazuet, and Natacha Reynaud-Paligot. About the design of distributed control systems: The quasi-synchronous approach. In SAFECOMP'01, Lecture Notes in Computer Science 2187, pages 215-226. Springer-Verlag, September 2001. 
@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},
}
[CMR01] Bruno Courcelle, Johann A. Makowsky, and Udi Rotics. On the fixed parameter complexity of graph enumeration problems definable in monadic second-order logic. Discrete Applied Mathematics 108(1-2):23-52. Elsevier, February 2001. 
@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,
}
[COG98] Rachel Cardell-Oliver and Tim Glover. A Practical and Complete Algorithm for Testing Real-Time Systems. In FTRTFT'98, Lecture Notes in Computer Science 1486, pages 251-261. Springer-Verlag, September 1998. 
@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},
}
[Coo71] Stephen A. Cook. The complexity of Theorem Proving Procedures. In STOC'71, pages 151-158. ACM Press, 1971. 
@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},
}
[Coo85] Stephen A. Cook. A Taxonomy of Problems with Fast Parallel Algorithms. Information and Control 64(1-3):2-22. Academic Press, 1985. 
@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},
}
[Coo04] Stephen A. Cook. Theories for Complexity Classes and their Propositional Translations. In Jan Krajíček (eds.), Complexity of computations and proofs, Quaderni di Matematica 13, pages 175-227. Dipartimento di Matematica, Seconda Universitá degli Studi di Napoli, Italy, 2004. 
@incollection{CCP2004-cook,
  author =              {Cook, Stephen A.},
  title =               {Theories for Complexity Classes and their
                         Propositional Translations},
  editor =              {Kraj{\'\i}{ 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},
}
[Cou90] Bruno Courcelle. The Monadic Second-Order Logic of Graphs. I: Recognizable Sets of Finite Graphs. Information and Computation 85(1):12-75. Academic Press, March 1990. 
@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,
}
[Cou97] Bruno Courcelle. The expression of graph properties and graph transformations in monadic second-order logic. In Grzegorz Rozenberg (eds.), Handbook of Graph Grammars. World Scientific, 1997. 
@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},
}
[Cou04] Jean-Michel Couvreur. A BDD-like Implementation of an Automaton Package. In CIAA'04, Lecture Notes in Computer Science 3317, pages 310-311. Springer-Verlag, July 2004. 
@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,
}
[Cou04] Jean-Michel Couvreur. Contribution à l'algorithmique de la vérification. Mémoire d'habilitation, Lab. Spécification & Vérification, ENS Cachan, France, July 2004. 
@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},
}
[Cov72] Thomas M. Cover. Broadcast Channels. IEEE Transactions on Information Theory 18(1):2-14. IEEE Inf. Theory Soc., January 1972. 
@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},
}
[Cov98] Thomas M. Cover. Comments on Broadcast Channels. IEEE Transactions on Information Theory 44(6):2524-2530. IEEE Inf. Theory Soc., October 1998. 
@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},
}
[CP97] Yi-Liang Chen and Gregory Provan. Modeling and Diagnosis of Timed Discrete Event Systems – A Factory Automation Example. In ACC'97, pages 31-36. IEEE Comp. Soc. Press, June 1997. 
@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},
}
[CPJ08] Hubert Comon, Nicolas Perrin, and Florent Jacquemard. Visibly Tree Automata with Memory and Constraints. Logical Methods in Computer Science 4(2). May 2008. 
@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},
}
[CPP93] Joëlle Cohen, Dominique Perrin, and Jean-Éric Pin. On the Expressive Power of Temporal Logic. Journal of Computer and System Sciences 46(3):271-294. Academic Press, June 1993. 
@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,
}
[CPR+02] Alessandro Cimatti, Marco Pistore, Marco Roveri, and Roberto Sebastiani. Improving the Encoding of LTL Model Checking into SAT. In VMCAI'02, Lecture Notes in Computer Science 2294, pages 196-207. Springer-Verlag, January 2002. 
@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,
}
[CR07] Olivier Carton and Chloé Rispal. Complementation of rational sets on scattered linear orderings of finite rank. Theoretical Computer Science 382(2):109-119. Elsevier, August 2007. 
@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,
}
[Cro86] Maxime Crochemore. Transducers and Repetitions. Theoretical Computer Science 45(1):63-86. Elsevier, 1986. 
@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},
}
[CRR12] Krishnendu Chatterjee, Mickael Randour, and Jean-François Raskin. Strategy Synthesis for Multi-dimensional Quantitative Objectives. Research Report 1201.5073, arXiv, January 2012. 
@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},
}
[CRR14] Krishnendu Chatterjee, Mickael Randour, and Jean-François Raskin. Strategy Synthesis for Multi-dimensional Quantitative Objectives. Acta Informatica 51(3-4):129-163. Springer-Verlag, June 2014. 
@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},
}
[CRS01] Franck Cassez, Mark D. Ryan, and Pierre-Yves Schobbens. Proving Feature Non-Interaction with Alternating-Time Temporal Logic. In Proceedings of the FIREworks Workshop on Language Constructs for Describing Features, pages 85-104. Springer-Verlag, January 2001. 
@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},
}
[CRV+04] Shih-Fen Cheng, Daniel M. Reeves, Yevgeniy Vorobeychik, and Michael P. Wellman. Notes on Equilibria in Symmetric Games. In GTDT'04, pages 71-78. June 2004. 
@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,
}
[CS92] Rance Cleaveland and Bernhard Steffen. A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-Calculus. Formal Methods in System Design 2(2):121-147. Kluwer Academic, 1992. 
@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},
}
[CS01] Edmund M. Clarke and Bernd-Holger Schlingloff. Model Checking. In John Alan Robinson and Andrei Voronkov (eds.), Handbook of Automated Reasoning. Elsevier and MIT Press, 2001. 
@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},
}
[CS03] Maxime Crochemore and Valery T. Stefanov. Waiting time and complexity for matching patterns with automata. Information Processing Letters 87(3):119-125. Elsevier, August 2003. 
@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},
}
[CT06] Thomas M. Cover and Joy A. Thomas. Elements of Information Theory. John Wiley & Sons, 2006. 
@book{EIT2006-CT,
  author =              {Cover, Thomas M. and Thomas, Joy A.},
  title =               {Elements of Information Theory},
  publisher =           {John Wiley \& Sons},
  edition =             {2},
  year =                {2006},
}
[CTL97] Christian Collberg, Clark Thomborson, and Douglas Low. A Taxonomy of Obfuscating Transformations. Technical Report 148, Department of Computer Science, University of Auckland, New Zealand, July 1997. 
@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},
}
[CTM+99] Sérgio Vale Aguiar Campos, Márcio Teixeira, Marius Minea, Andreas Kuehlmann, and Edmund M. Clarke. Model Checking Semi-Continuous Time Models Using BDDs. In SMC'99, Electronic Notes in Theoretical Computer Science 23(2). Elsevier, July 1999. 
@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,
}
[CTT+04] Edmund M. Clarke, Muralidhar Talupur, Tayssir Touili, and Helmut Veith. Verification by network decomposition. In CONCUR'04, Lecture Notes in Computer Science 3170, pages 276-291. Springer-Verlag, August 2004. 
@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},
}
[CTV06] Edmund M. Clarke, Muralidhar Talupur, and Helmut Veith. Environment Abstraction for Parameterized Verification. In VMCAI'06, Lecture Notes in Computer Science 3855, pages 126-141. Springer-Verlag, January 2006. 
@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},
}
[CV12] Krishnendu Chatterjee and Yaron Velner. Mean-Payoff Pushdown Games. In LICS'12, pages 195-204. IEEE Comp. Soc. Press, June 2012. 
@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},
}
[CVW+91] Costas Courcoubetis, Moshe Y. Vardi, Pierre Wolper, and Mihalis Yannakakis. Memory-Efficient Algorithms for the Verification of Temporal Properties. In CAV'90, Lecture Notes in Computer Science 531, pages 233-242. Springer-Verlag, 1991. 
@inproceedings{cav1990-CVWY,
  author =              {Courcoubetis, Costas and Vardi, Moshe Y. and Wolper,
                         Pierre and Yannakakis, Mihalis},
  title =               {Memory-Efficient Algorithms for the Verification of
                         Temporal Properties},
  editor =              {Clarke, Edmund M. and Kurshan, Robert P.},
  booktitle =           {{P}roceedings of the 2nd {I}nternational {W}orkshop
                         on {C}omputer {A}ided {V}erification ({CAV}'90)},
  acronym =             {{CAV}'90},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {531},
  pages =               {233-242},
  year =                {1991},
  confyear =            {1990},
  confmonth =           {6},
}
[CY92] Costas Courcoubetis and Mihalis Yannakakis. Minimum and Maximum Delay Problems in Real-Time Systems. Formal Methods in System Design 1(4):385-415. Kluwer Academic, December 1992. 
@article{fmsd1(4)-CY,
  author =              {Courcoubetis, Costas and Yannakakis, Mihalis},
  title =               {Minimum and Maximum Delay Problems in Real-Time
                         Systems},
  publisher =           {Kluwer Academic},
  journal =             {Formal Methods in System Design},
  volume =              {1},
  number =              {4},
  pages =               {385-415},
  year =                {1992},
  month =               dec,
}
[CY95] Costas Courcoubetis and Mihalis Yannakakis. The Complexity of Probabilistic Verification. Journal of the ACM 42(4):857-907. ACM Press, July 1995. 
@article{jacm42(4)-CY,
  author =              {Courcoubetis, Costas and Yannakakis, Mihalis},
  title =               {The Complexity of Probabilistic Verification},
  publisher =           {ACM Press},
  journal =             {Journal of the ACM},
  volume =              {42},
  number =              {4},
  pages =               {857-907},
  year =                {1995},
  month =               jul,
}