A
[dA99] Luca de Alfaro. Computing minimum and maximum reachability times in probabilistic systems. In CONCUR'99, Lecture Notes in Computer Science 1664, pages 66-81. Springer-Verlag, August 1999.
@inproceedings{concur1999-Alf,
  author =              {de Alfaro, Luca},
  title =               {Computing minimum and maximum reachability times in
                         probabilistic systems},
  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 =               {66-81},
  year =                {1999},
  month =               aug,
}
[dA03] Luca de Alfaro. Quantitative Verification and Control via the Mu-Calculus. In CONCUR'03, Lecture Notes in Computer Science 2761, pages 102-126. Springer-Verlag, August 2003.
@inproceedings{concur2003-Alf,
  author =              {de Alfaro, Luca},
  title =               {Quantitative Verification and Control via the
                         Mu-Calculus},
  editor =              {Amadio, Roberto and Lugiez, Denis},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'03)},
  acronym =             {{CONCUR}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2761},
  pages =               {102-126},
  year =                {2003},
  month =               aug,
}
[AAB00] Aurore Annichini, Eugene Asarin, and Ahmed Bouajjani. Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems. In CAV'00, Lecture Notes in Computer Science 1855, pages 419-434. Springer-Verlag, July 2000.
@inproceedings{cav2000-AAB,
  author =              {Annichini, Aurore and Asarin, Eugene and Bouajjani,
                         Ahmed},
  title =               {Symbolic Techniques for Parametric Reasoning about
                         Counter and Clock Systems},
  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 =               {419-434},
  year =                {2000},
  month =               jul,
}
[AAD+06] Dana Angluin, James Aspnes, Zoë Diamadi, Michael J. Fischer, and René Peralta. Computation in Networks of Passively Mobile Finite-State Sensors. Distributed Computing 18(4):235-253. Springer-Verlag, March 2006.
@article{discomp18(4)-AADFP,
  author =              {Angluin, Dana and Aspnes, James and Diamadi, Zo{\"e}
                         and Fischer, Michael J. and Peralta, Ren{\'e}},
  title =               {Computation in Networks of Passively Mobile
                         Finite-State Sensors},
  publisher =           {Springer-Verlag},
  journal =             {Distributed Computing},
  volume =              {18},
  number =              {4},
  pages =               {235-253},
  year =                {2006},
  month =               mar,
  doi =                 {10.1007/s00446-005-0138-3},
}
[AAE+07] Dana Angluin, James Aspnes, David Eisenstat, and Eric Ruppert. The computational power of population protocols. Distributed Computing 20(4):279-304. Springer-Verlag, March 2007.
@article{discomp20(4)-AAER,
  author =              {Angluin, Dana and Aspnes, James and Eisenstat, David
                         and Ruppert, Eric},
  title =               {The computational power of population protocols},
  publisher =           {Springer-Verlag},
  journal =             {Distributed Computing},
  volume =              {20},
  number =              {4},
  pages =               {279-304},
  year =                {2007},
  month =               mar,
  doi =                 {10.1007/s00446-007-0040-2},
}
[AAG+15] Manindra Agrawal, S. Akshay, Blaise Genest, and P. S. Thiagarajan. Approximate Verification of the Symbolic Dynamics of Markov Chains. Journal of the ACM 62(1):183-235. ACM Press, February 2015.
@article{jacm62(1)-AAGT,
  author =              {Agrawal, Manindra and Akshay, S. and Genest, Blaise
                         and Thiagarajan, P. S.},
  title =               {Approximate Verification of the Symbolic Dynamics of
                         {M}arkov Chains},
  publisher =           {ACM Press},
  journal =             {Journal of the ACM},
  volume =              {62},
  number =              {1},
  pages =               {183-235},
  year =                {2015},
  month =               feb,
  doi =                 {10.1145/2629417},
}
[AAM06] Yasmina Abdeddaïm, Eugene Asarin, and Oded Maler. Scheduling with timed automata. Theoretical Computer Science 354(2):272-300. Elsevier, March 2006.
@article{tcs354(2)-AAM,
  author =              {Abdedda{\"\i}m, Yasmina and Asarin, Eugene and
                         Maler, Oded},
  title =               {Scheduling with timed automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {354},
  number =              {2},
  pages =               {272-300},
  year =                {2006},
  month =               mar,
}
[AB01] Carlos Areces and Patrick Blackburn. Bringing them all Together. Journal of Logic and Computation 11(5):657-669. Oxford University Press, October 2001.
@article{jlc11(5)-AB,
  author =              {Areces, Carlos and Blackburn, Patrick},
  title =               {Bringing them all Together},
  publisher =           {Oxford University Press},
  journal =             {Journal of Logic and Computation},
  volume =              {11},
  number =              {5},
  pages =               {657-669},
  year =                {2001},
  month =               oct,
}
[AB01] Eugene Asarin and Ahmed Bouajjani. Perturbed Turing machines and hybrid systems. In LICS'01, pages 269-278. IEEE Comp. Soc. Press, June 2001.
@inproceedings{lics2001-AB,
  author =              {Asarin, Eugene and Bouajjani, Ahmed},
  title =               {Perturbed {T}uring machines and hybrid systems},
  booktitle =           {{P}roceedings of the 16th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'01)},
  acronym =             {{LICS}'01},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {269-278},
  year =                {2001},
  month =               jun,
}
[ABB+16] José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, and Michael Emmi. Verifying Constant-Time Implementations. In USENIX Security'16, pages 53-70. Usenix Association, August 2016.
@inproceedings{usenixsec2016-ABBDE,
  author =              {Almeida, Jos{\'e} Bacelar and Barbosa, Manuel and
                         Barthe, Gilles and Dupressoir, Fran{\c c}ois and
                         Emmi, Michael},
  title =               {Verifying Constant-Time Implementations},
  editor =              {Holz, Thorsten and Savage, Stefan},
  booktitle =           {{P}roceedings of the 25th {USENIX} {S}ecurity
                         {S}ymposium ({USENIX} {S}ecurity'16)},
  acronym =             {{USENIX} {S}ecurity'16},
  publisher =           {Usenix Association},
  pages =               {53-70},
  year =                {2016},
  month =               aug,
}
[ABB+03] Luca Aceto, Patricia Bouyer, Augusto Burgueño, and Kim Guldstrand Larsen. The Power of Reachability Testing for Timed Automata. Theoretical Computer Science 300(1-3):411-475. Elsevier, May 2003.
@article{tcs300(1-3)-ABBL,
  author =              {Aceto, Luca and Bouyer, Patricia and Burgue{\~n}o,
                         Augusto and Larsen, Kim Guldstrand},
  title =               {The~Power of Reachability Testing for Timed
                         Automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {300},
  number =              {1-3},
  pages =               {411-475},
  year =                {2003},
  month =               may,
  doi =                 {10.1016/S0304-3975(02)00334-1},
}
[ABE00] Parosh Aziz Abdulla, Per Bjesse, and Niklas Eén. Symbolic Reachability Analysis based on SAT Solvers. In TACAS'00, Lecture Notes in Computer Science 1785, pages 411-425. Springer-Verlag, March 2000.
@inproceedings{tacas2000-ABE,
  author =              {Abdulla, Parosh Aziz and Bjesse, Per and E{\'e}n,
                         Niklas},
  title =               {Symbolic Reachability Analysis based on {SAT}
                         Solvers},
  editor =              {Graf, Susanne and Schwartzbach, Michael I.},
  booktitle =           {{P}roceedings of the 6th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'00)},
  acronym =             {{TACAS}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1785},
  pages =               {411-425},
  year =                {2000},
  month =               mar,
}
[ABF94] Amihood Amir, Gary Benson, and Martin Farach. Let Sleeping Files Lie: Pattern Matching in Z-Comporessed Files. In SODA'94, pages 705-714. ACM Press, January 1994.
@inproceedings{soda1994-ABF,
  author =              {Amir, Amihood and Benson, Gary and Farach, Martin},
  title =               {Let Sleeping Files Lie: Pattern Matching in
                         {Z}-Comporessed Files},
  booktitle =           {{P}roceedings of the 5th {A}nnual {ACM}-{SIAM}
                         {S}ymposium on {D}iscrete {A}lgorithms ({SODA}'94)},
  acronym =             {{SODA}'94},
  publisher =           {ACM Press},
  pages =               {705-714},
  year =                {1994},
  month =               jan,
}
[ABG15] C. Aiswarya, Benedikt Bollig, and Paul Gastin. An automata-theoretic approach to the verification of distributed algorithms. In CONCUR'15, Leibniz International Proceedings in Informatics 42, pages 340-353. Leibniz-Zentrum für Informatik, September 2015.
@inproceedings{concur2015-ABG,
  author =              {Aiswarya, C. and Bollig, Benedikt and Gastin, Paul},
  title =               {An automata-theoretic approach to the verification
                         of distributed algorithms},
  editor =              {Aceto, Luca and de Frutos{-}Escrig, David},
  booktitle =           {{P}roceedings of the 26th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'15)},
  acronym =             {{CONCUR}'15},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {42},
  pages =               {340-353},
  year =                {2015},
  month =               sep,
  doi =                 {10.4230/LIPIcs.CONCUR.2015.340},
}
[ABG+08] S. Akshay, Benedikt Bollig, Paul Gastin, Madhavan Mukund, and K. Narayan Kumar. Distributed Timed Automata with Independently Evolving Clocks. In CONCUR'08, Lecture Notes in Computer Science 5201, pages 82-97. Springer-Verlag, August 2008.
@inproceedings{ABGMN-concur08,
  author =              {Akshay, S. and Bollig, Benedikt and Gastin, Paul and
                         Mukund, Madhavan and Narayan Kumar, K.},
  title =               {Distributed Timed Automata with Independently
                         Evolving Clocks},
  editor =              {van Breugel, Franck and Chechik, Marsha},
  booktitle =           {{P}roceedings of the 19th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'08)},
  acronym =             {{CONCUR}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5201},
  pages =               {82-97},
  year =                {2008},
  month =               aug,
}
[ABK13] Shaull Almagor, Udi Boker, and Orna Kupferman. Formalizing and Reasoning about Quality. In ICALP'13, Lecture Notes in Computer Science 7966, pages 15-27. Springer-Verlag, July 2013.
@inproceedings{icalp2013-ABK,
  author =              {Almagor, Shaull and Boker, Udi and Kupferman, Orna},
  title =               {Formalizing and Reasoning about Quality},
  editor =              {Fomin, Fedor V. and Freivalds, Rusins and
                         Kwiatkowska, Marta and Peleg, David},
  booktitle =           {{P}roceedings of the 40th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'13)~-- Part~{II}},
  nym =             {{CONCICALP}'13span>{Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {  volume =              {5201},
  pages =               {15-27},
  year =                {2013},
  month =               jul,
}
[ABK14] Shaull Almagor, Udi Boker, and Orna Kupferman. Discounting in LTL. In TACAS'14, Lecture Notes in Computer Science 8413, pages 424-439. Springer-Verlag, April 2014.
@inproceedings{tacas2014-ABK,
  author =              {Almagor, Shaull and Boker, Udi and Kupferman, Orna},
  title =               {Discounting in~{LTL}},
  editor =              {{\'A}brah{\'a}m, Erikz and Havelund, Klaus},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'14)},
  acronym =             {{TACAS}'14span>{Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {  volume =              {5201},
  pages =               {424-439},
  year =                {2014},
  month =               apr,
  doi =                 {10.1007/978-3-642-54862-8_37},
}
[ABK+97] Eugene Asarin, Marius Bozga, Alain Kerbrat, Oded Maler, Amir Pnueli, and Anne Rasse. Data-Structy'>s for the Verification of Timed Automata. In HART'97, Lecture Notes in Computer Science 1201, pages 346-360. Springer-Verlag, March 1997.
@inproceedings{hart1997-ABKMPR,
  author =              {Asarin, Eugene and Bozga, Marius and Kerbrat, Alain
                         and Maler, Oded and Pnueli, Amir and Rasse, Anne},
  title =               {Data-Structy'>s for the Verification of Timed
                         Automata},
  editor =              {Maler, Oded},
  booktitle =           {{P}roceedings of the 1997 {I}nternational {W}orkshop
                         on {H}ybrid and {R}eal-Time {S}ystems ({HART}'97)},
  acronym =             {{HART}'97span>{Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {  volume =              {5201},
  pages =               {346-360},
  year =                {1997},
  month =               mar,
}
[ABK+03] Roy Armoni, Doron Bustan, Orna Kupferman, and Moshe Y. Vardi. Resets vs. Abortume =Linear Temporal Logic. In TACAS'03, Lecture Notes in Computer Science 2619, pages 65-80. Springer-Verlag, April 2003.
@inproceedings{tacas2003-ABKV,
  author =              {Armoni, Roy and Bustan, Doron and Kupferman, Orna
                         and Vardi, Moshe Y.},
  title =               {Resets {vs.} Abortume =Linear Temporal Logic},
  editor =              {Garavel, Hubert and Hatcliff, John},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'03)},
  acronym =             {{TACAS}'03span>{Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {  volume =              {5201},
  pages =               {65-80},
  year =                {2003},
  month =               apr,
}
[ABM99] Carlos Areces, Patrick Blackburn, and Maarten Marx. A Road-Map on lexity for Hybrid Logics. In CSL'99, Lecture Notes in Computer Science 1862, pages 307-321. Springer-Verlag, September 1999.
@inproceedings{csl1999-ABM,
  author =              {Areces, Carlos and Blackburn, Patrick and Marx,
                         Maarten},
  title =               {A Road-Map on     lexity for Hybrid Logics},
  editor =              {F   , J{\"o}rg and Rodr{\'\i}guez{-}Artalejo, Mario},
  booktitle =           {{P}roceedings of the 13th {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'99)},
  acronym =             {{CSL}'99span>{Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {  volume =              {5201},
  pages =               {307-321},
  year =                {1999span>{Springmonth =               sep,
}
[ABM00] Carlos Areces, Patrick Blackburn, and Maarten Marx. The Computational Complexity of Hybrid Temporal Logics. Logic Journal of the IGPL 8(5):653-679. Oxford University Press, September 2000.
@article{jigpl8(5)-ABM,
  author =              {Areces, Carlos and Blackburn, Patrick and Marx,
                         Maarten},
  title =               {The Computational Complexity of Hybrid Temporal
                         Logicsspan class='bib-entry-val'>Springer-Verlag},
  series = Oxford University Pressspan class='bib-entry-val'>Springjournal =             {Logic Journal of the IGPLspan cl'bib-entry-key'>  volume =              {5201span cl'bib-entry-key'>  volume =number =              {5},
  pages =               {653-679},
  year =                {2000},
  month =               sep,
}
[ABM04] Rajeev Alur, Mikhail Bernadsky, and Parthasarathy Madhusudan. Optimal Reachability for Weighted Timed Games. In ICALP'04, Lecture Notes in Computer Science, pages 122-133. Springer-Verlag, 2004.
@inproceedings{icalp2004-ABM,
  author =              {Alur, Rajeev and Bernadsky, Mikhail and Madhusudan,
                         Parthasarathy},
  title =               {Optimal Reachability for Weighted Timed Games},
  booktitle =           {{P}roceedings of the 31st {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'04)},
  acronym =             {{ICALP}'04span>{Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {  pages =               {122-133},
  year =                {2004span>{
[ABO97] Eric Allender, Robert Beals, and Mitsunori Ogihara. The Complexity of Matrix Rank and Feasible Systems of Linear Equations. Technical Report 97-40, Rut s University, New Jersey, USA, September 1997.
@techreport{TR-DIMACS9740,
  author =              {Allender, Eric and Beals, Robert and Ogihara,
                         Mitsunori},
  title =               {The Complexity of Matrix Rank and Feasible Systems
                         of Linear Equationsspan cl'bib-entry-key'>  volume =number =              {97-40},
  year =                {1997},
  month =               sep,
  institution =         {Rut   s University, New Jersey, USAspa}
[Abr79] Karl Abrahamson. Modal Logic of Concurrent vnde ministic Programs. In SCC'79, Lecture Notes in Computer Science 70, pages 21-33. Springer-Verlag, July 1979.
@inproceedings{scc1979-Abr,
  author =              {Abrahamson, Karl},
  title =               {Modal Logic of Concurrent  vnde   ministic Programs},
  editor =              {Kahn, Gilles},
  booktitle =           {{P}roceedings of the International Symposium
                         Semantics of Concurrent Computation ({SCC}'79)},
  acronym =             {{SCC}'79span>{Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {  volume =              {5201},
  pages =               {21-33},
  year =                {1979span>{Springmonth =               jul,
}
[AC02] Jean-Pierre Aubin and Francine Catté. Bila al Fixed-point and Algebraic Propertotesof Viability Kernels and Capey'> Basins of Sets. Technical Report 02-10, CeReMaDe, Université Paris 9, Paris, France, April 2002.
@techreport{TR-Ceremade0210,
  author =              {Aubin, Jean-Pierre and Catt{\'e}, Francine},
  title =               {Bila   al Fixed-point and Algebraic Propertotesof
                         Viability Kernels and Capey'> Basins of Setsspan cl'bib-entry-key'>  volume =number =              {02-10},
  year =                {2002},
  month =               apr,
  institution =         {CeReMaDe, Universit\'e Paris 9, Paris, Francespa}
[ACD93] Rajeev Alur, Costas Courcoubetis, and David L. Dill. Model-Checking in Dense Real-Time. Information and Computation 104(1):2-34. Academic Press, May 1993.
@article{icomp104(1)-ACD,
  author =              {Alur, Rajeev and Courcoubetis, Costas and Dill,
                         David L.},
  title =               {Model-Checking in Dense Real-Time},
  publisher =           {Academic Press},
  journal =             {Information and Computationspan cl'bib-entry-key'>  volume =              {5201{Springnumber =              {1},
  pages =               {2-34},
  year =                {1993},
  month =               maypa}
[ACD+92] Rajeev Alur, Costas Courcoubetis, David L. Dill, Nicolas Halbwachs, and Howard Wong-Toi. An Implementation of three algorithms for timing verification based on automata emptiness. In RTSS'92papages 157-166. IEEE Comp. Soc. Press, December 1992.
@inproceedings{rts1992-ACDHW,
  author =              {Alur, Rajeev and Courcoubetis, Costas and Dill,
                         David L. and Halbwachs, Nicolas and Wong{-}Toi,
                         Howard},
  title =               {An Implementation of three algorithms for timing
                         verification based on automata emptiness},
  booktitle =           {{P}roceedings of the 13th {S}ymposium on {R}eal-Time
                         {S}ystems ({RTSS}'92)},
  acronym =             {{RTSS}'92},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {157-166},
  year =                {1992},
  month =               dec,
}
[ACH94] Rajeev Alur, Costas Courcoubetis, and Thomas A. Henz . The Observational Power of Clocks. In CONCUR'94, Lecture Notes in Computer Science 836, pages 162-177. Springer-Verlag, August 1994.
@inproceedings{concur1994-ACH,
  author =              {Alur, Rajeev and Courcoubetis, Costas and Henz     ,
                         Thomas A.},
  title =               {The Observational Power of Clocks},
  editor =              {Jonsson, Bengt and Parrow, Joachim},
  booktitle =           {{P}roceedings of the 5th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'94)},
  acronym =             {{CONCUR}'94},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              {5201},
  pages =               {162-177},
  year =                {1994},
  month =               aug,
}
[ACH97] Rajeev Alur, Costas Courcoubetis, and Thomas A. Henz . ing Accumula d Delayume =Real Time Systems. Formal Methodume =System Design 11(2):137-155. Kluwer Academic, August 1997.
@article{fmsd11(2)-ACH,
  author =              {Alur, Rajeev and Courcoubetis, Costas and Henz     ,
                         Thomas A.},
  title =               {C     ing Accumula  d Delayume =Real Time Systems},
  publisher =           {Kluwer Academic},
  journal =             {Formal Methodume =System Designspan cl'bib-entry-key'>  volume =              {5201},
  number =              {2},
  pages =               {137-155},
  year =                {1997},
  month =               aug,
}
[ACH+93] Rajeev Alur, Costas Courcoubetis, Thomas A. Henz , and Pei-Hsin Ho. Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems. In HSCC'92paLecture Notes in Computer Science 736, pages 209-229. Springer-Verlag, 1993.
@inproceedings{hscc1992-ACHH,
  author =              {Alur, Rajeev and Courcoubetis, Costas and Henz     ,
                         Thomas A. and Ho, Pei-Hsin},
  title =               {Hybrid Automata: An Algorithmic Approach to the
                         Specification and Verification of Hybrid Systems},
  editor =              {Grossman, Robert L. and Nerode, Anil and Ravn,
                         Anders P. and Rischel, Hansspan cl'bib-entry-key'>  volume =booktitle =           {{H}ybrid {S}ystems ({HSCC}'92)},
  acronym =             {{HSCC}'92},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              {5201},
  pages =               {209-229},
  year =                {1993},
}
[ACH+95] Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A. Henz , Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, and Sergio Yovine. The Algorithmic Analysis of Hybrid Systems. Theoretical Computer Science 138(1):3-34. Elsevier, 1995.
@article{tcs138(1)-ACHHHNOSY,
  author =              {Alur, Rajeev and Courcoubetis, Costas and Halbwachs,
                         Nicolas and Henz     , Thomas A. and Ho, Pei-Hsin
                         and Nicollin, Xavier and Olivero, Alfredo and
                         Sifakis, Joseph and Yovine, Sergio},
  title =               {The Algorithmic Analysis of Hybrid Systems},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Sciencespan cl'bib-entry-key'>  volume =              {5201span cl'bib-entry-key'>  volume =number =              {1},
  pages =               {3-34},
  year =                {1995},
}
[ACJ+96] Parosh Aziz Abdulla, Kārlis Čerāns, Bengt Jonsson, and Yih-Kuen Tsay. Gen al Decidability Theorems for Infinite-State Systems. In LICS'96, pages 313-321. IEEE Comp. Soc. Press, July 1996.
@inproceedings{lics1996-ACJT,
  author =              {Abdulla, Parosh Aziz and {{C}}er{\={a}}ns,
                         K{\={a}}rlis and Jonsson, Bengt and Tsay, Yih-Kuen},
  title =               {Gen  al Decidability Theorems for Infinite-State
                         Systems},
  booktitle =           {{P}roceedings of the 11th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'96)},
  acronym =             {{LICS}'96},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {313-321},
  year =                {1996},
  month =               jul,
}
[ACM97] Eugene Asarin, Paul Caspi, and Oded Mal . A Kleene Theorem for Timed Automata. In LICS'97, pages 160-171. IEEE Comp. Soc. Press, June 1997.
@inproceedings{lics1997-ACM,
  author =              {Asarin, Eugene and Caspi, Paul and Mal  , Oded},
  title =               {A {K}leene Theorem for Timed Automata},
  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 =               {160-171},
  year =                {1997},
  month =               jun,
}
[ACS10] Tesnim Abdellatif, Jacques Combaz, and Joseph Sifakis. Model-based implementation of real-time applications. In EMSOFT'10, pages 229-238. ACM Press, October 2010.
@inproceedings{emsoft2010-ACS,
  author =              {Abdellatif, Tesnim and Combaz, Jacques and Sifakis,
                         Joseph},
  title =               {Model-based implementation of real-time
                         applications},
  editor =              {Carloni, Luca P. and Tripakis, Stavros},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {C}onference on {E}mbedded {S}oftware ({EMSOFT}'10)},
  acronym =             {{EMSOFT}'10},
  publisher =           {ACM Press},
  pages =               {229-238},
  year =                {2010},
  month =               oct,
}
[AD89] André Arnold and Anne Dicky. An Algebraic Characterization of Transition System Equivalences. Information and Computation 82(2):198-229. Academic Press, August 1989.
@article{icomp82(2)-AD,
  author =              {Arnold, Andr{\'e} and Dicky, Anne},
  title =               {An Algebraic Characterization of Transition System
                         Equivalences},
  publisher =           {Academic Press},
  journal =             {Information and Computationspan cl'bib-entry-key'>  volume =              {5201},
  number =              {2},
  pages =               {198-229},
  year =                {1989span>{Springmonth =               aug,
}
[AD90] Rajeev Alur and David L. Dill. Automata For Modeling Real-Time Systems. In ICALP'90, Lecture Notes in Computer Science 443, pages 322-335. Springer-Verlag, July 1990.
@inproceedings{icalp1990-AD,
  author =              {Alur, Rajeev and Dill, David L.},
  title =               {Automata For Modeling Real-Time Systems},
  editor =              {Pa   son, Mike},
  booktitle =           {{P}roceedings of the 17th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'90)},
  acronym =             {{ICALP}'90},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              {5201},
  pages =               {322-335},
  year =                {1990},
  month =               jul,
}
[AD94] Rajeev Alur and David L. Dill. A Theory of Timed Automata. Theoretical Computer Science 126(2):183-235. Elsevier, April 1994.
@article{tcs126(2)-AD,
  author =              {Alur, Rajeev and Dill, David L.},
  title =               {A Theory of Timed Automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Sciencespan cl'bib-entry-key'>  volume =              {5201},
  number =              {2},
  pages =               {183-235},
  year =                {1994},
  month =               apr,
}
[AD09] Timos Antonopoulos and Anuj Dawa . Separa ing Graph Logic from MSO. In FoSSaCS'09, Lecture Notes in Computer Science 5504, pages 63-77. Springer-Verlag, March 2009.
@inproceedings{fossacs2009-AD,
  author =              {Antonopoulos, Timos and Dawa , Anuj},
  title =               {Separa ing Graph Logic from~{MSO}},
  editor =              {de Alfaro, Luca},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'09)},
  acronym =             {{FoSSaCS}'09},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              {5201},
  pages =               {63-77},
  year =                {2009},
  month =               mar,
}
[ADK+04] Elliot Anshelevich, Anirban Dasgupta, Jon Kleinberg, Éva Tardos, Tom Wexl , and Tim Roughgarden. The Price of Stability for Network Design with Fair Cost Allocation. In FOCS'04, pages 295-304. IEEE Comp. Soc. Press, October 2004.
@inproceedings{focs2004-ADKTWR,
  author =              {Anshelevich, Elliot and Dasgupta, Anirban and
                         Kleinberg, Jon and Tardos, {\'E}va and Wexl  , Tom
                         and Roughgarden, Tim},
  title =               {The Price of Stability for Network Design with Fair
                         Cost Allocation},
  booktitle =           {{P}roceedings of the 45th {A}nnual {S}ymposium on
                         {F}oundations of {C}omputer {S}cience ({FOCS}'04)},
  acronym =             {{FOCS}'04},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {295-304},
  year =                {2004},
  month =               oct,
  doi =                 {10.1109/FOCS.2004.68},
}
[ADM+09] Rajeev Alur, Aldric Degorre, Oded Mal , and Gera Weiss. On Omega-Languages Defined by Mean-Payoff Conditions. In FoSSaCS'09, Lecture Notes in Computer Science 5504. Springer-Verlag, March 2009.
@inproceedings{fossacs2009-ADMW,
  author =              {Alur, Rajeev and Degorre, Aldric and Mal  , Oded and
                         Weiss, Gera},
  title =               {On Omega-Languages Defined by Mean-Payoff
                         Conditions},
  editor =              {de Alfaro, Luca},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'09)},
  acronym =             {{FoSSaCS}'09},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              {5201},
  year =                {2009},
  month =               mar,
  doi =                 {10.1007/978-3-642-00596-1_24},
}
[ADO+05] Parosh Aziz Abdulla, Johann Deneux, Joël Ouaknine, and James Worrell. Decidability and Complexity Results for Timed Automata via Channel Machines. In ICALP'05, Lecture Notes in Computer Science 3580, pages 1089-1101. Springer-Verlag, July 2005.
@inproceedings{icalp2005-ADOW,
  author =              {Abdulla, Parosh Aziz and Deneux, Johann and
                         Ouaknine, Jo{\"e}l and Worrell, James},
  title =               {Decidability and Complexity Results for Timed
                         Automata via Channel Machines},
  editor =              {Caires, Lu{\'\i}s and Italiano, Giuseppe F. and
                         Monteiro, Lu{\'\i}s and Palamidessi, Catuscia and
                         Yung, Moti},
  booktitle =           {{P}roceedings of the 32nd {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'05)},
  acronym =             {{ICALP}'05},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {1089-1101},
  year =                {2005},
  month =               jul,
}
[AEL+01] Rajeev Alur, Kousha Eolusami, Salvatore La Torre, and Doron A. Peled. Parametric Tempo al Logic for "Model Measu ". ACM Transactions on Computational Logic 2(3):388-407. ACM Press, July 2001.
@article{tocl2(3)-AELP,
  author =              {Alur, Rajeev and Eolusami, Kousha and La{~}Torre,
                         Salvatore and Peled, Doron A.},
  title =               {Parametric Tempo al Logic for {"}Model Measu    {"}},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logicspan cl'bib-entry-key'>  volume =              puter Science},
  number =              {3},
  pages =               {388-407},
  year =                {2001},
  month =               jul,
}
[AFF+02] Roy Armoni, Limor Fix, Alon Flaisher, Rob Gerth, Boris Ginsburg, Tomer Kanza, Avner Landver, Sela Mador-Haim, Eli S man, Andreas Tiemeyer, Moshe Y. Vardi, and Yael Zba . The ForSpec Tempo al Logic: A New Tempo al Property-Specification Language. In TACAS'02paLecture Notes in Computer Science 2280, pages 296-311. Springer-Verlag, April 2002.
@inproceedings{tacas2002-AFFGGKLMSTVZ,
  author =              {Armoni, Roy and Fix, Limor and Flaisher, Alon and
                         Gerth, Rob and Ginsburg, Boris and Kanza, Tomer and
                         Landver, Avner and Mador{-}Haim, Sela and S     man,
                         Eli and Tiemeyer, Andreas and Vardi, Moshe Y. and
                         Zba , Yael},
  title =               {The {ForSpec} Tempo al Logic: A New Tempo al
                         Property-Specification Language},
  editor =              {Katoen, Joost-Pieter and Stevens, Perdita},
  booktitle =           {{P}roceedings of the 8th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'02)},
  acronym =             {{TACAS}'02},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {296-311},
  year =                {2002},
  month =               apr,
}
[AFF+03] Roy Armoni, Limor Fix, Alon Flaisher, Orna Grumberg, Nir Pite man, Andreas Tiemeyer, and Moshe Y. Vardi. Enha . In CAV'03, Lecture Notes in Computer Science 2725, pages 368-380. Springer-Verlag, July 2003.
@inproceedings{cav2003-AFFGPTV,
  author =              {Armoni, Roy and Fix, Limor and Flaisher, Alon and
                         Grumberg, Orna and Pite man, Nir and Tiemeyer,
                         Andreas and Vardi, Moshe Y.},
  title =               {Enha },
  editor =              {Hunt, Jr, Warren A. and Somenzi, Fabio},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'03)},
  acronym =             {{CAV}'03},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {368-380},
  year =                {2003},
  month =               jul,
  doi =                 {10.1007/978-3-540-45069-6_35},
}
[AFH91] Rajeev Alur, Tómas Fed , and Thomas A. Henzi . The Benefits of Relaxing Punkeyality. In PODC'91, pages 139-152. ACM Press, August 1991.
@inproceedings{podc1991-AFH,
  author =              {Alur, Rajeev and Fed  , T{\'o}mas and Henzi    ,
                         Thomas A.},
  title =               {The Benefits of Relaxing Punkeyality},
  booktitle =           {{P}roceedings of the 10th {ACM} {S}ymposium on
                         {P}rinciples of {D}istributed {C}omputing
                         ({PODC}'91)},
  acronym =             {{PODC}'91},
  publisher =           {ACM Press},
  pages =               {139-152},
  year =                {1991},
  month =               aug,
}
[AFH94] Rajeev Alur, Limor Fix, and Thomas A. Henzi . Event-Clock Automata: A Determinizable Class of Timed Automata. In CAV'94, Lecture Notes in Computer Science 818, pages 1-13. Springer-Verlag, June 1994.
@inproceedings{cav1994-AFH,
  author =              {Alur, Rajeev and Fix, Limor and Henzi    , Thomas
                         A.},
  title =               {Event-Clock Automata: A Determinizable Class of
                         Timed Automata},
  editor =              {Dill, David L.},
  booktitle =           {{P}roceedings of the 6th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'94)},
  acronym =             {{CAV}'94},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {1-13},
  year =                {1994},
  month =               jun,
}
[AFH96] Rajeev Alur, Tómas Fed , and Thomas A. Henzi . The Benefits of Relaxing Punkeyality. Journal of the ACM 43(1):116-146. ACM Press, January 1996.
@article{jacm43(1)-AFH,
  author =              {Alur, Rajeev and Fed  , T{\'o}mas and Henzi    ,
                         Thomas A.},
  title =               {The Benefits of Relaxing Punkeyality},
  publisher =           {ACM Press},
  journal =             {Journal of the ACMspan cl'bib-entry-key'>  volume =              {5201},
  number =              {1},
  pages =               {116-146},
  year =                {1996},
  month =               jan,
}
[AFH99] Rajeev Alur, Limor Fix, and Thomas A. Henzi . Event-Clock Automata: A Determinizable Class of Timed Automata. Theoretical Computer Science 211(1-2):253-273. Elsevier, January 1999.
@article{tcs211(1-2)-AFH,
  author =              {Alur, Rajeev and Fix, Limor and Henzi    , Thomas
                         A.},
  title =               {Event-Clock Automata: A Determinizable Class of
                         Timed Automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Sciencespan cl'bib-entry-key'>  volume =              {{211},
  number =              {1-2},
  pages =               {253-273},
  year =                {1999},
  month =               jan,
  doi =                 {10.1016/S0304-3975(97)00173-4},
}
[dAF+03] Luca de Alfaro, Marco Faella, Thomas A. Henzi , Rupak Majumda , and Mariëlle Stoelinga. The Element of Surpriseme =Timed Games. In CONCUR'03, Lecture Notes in Computer Science 2761, pages 142-156. Springer-Verlag, August 2003.
@inproceedings{concur2003-AFHMS,
  author =              {de Alfaro, Luca and Faella, Marco and Henzi    ,
                         Thomas A. and Majumda , Rupak and Stoelinga,
                         Mari{\"e}llespan cl'bib-entry-key'>  volume =title =               {The Element of Surpriseme =Timed Games},
  editor =              {Amadio, Roberto and Lugiez, Denis},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'03)},
  acronym =             {{CONCUR}'03},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              {{2761},
  pages =               {142-156},
  year =                {2003},
  month =               aug,
}
[dAF+05] Luca de Alfaro, Marco Faella, Thomas A. Henzi , Rupak Majumda , and Mariëlle Stoelinga. Model checking discounted tempo al properties. Theoretical Computer Science 345(1):139-170. Elsevier, November 2005.
@article{tcs345(1)-AFHMS,
  author =              {de Alfaro, Luca and Faella, Marco and Henzi    ,
                         Thomas A. and Majumda , Rupak and Stoelinga,
                         Mari{\"e}llespan cl'bib-entry-key'>  volume =title =               {Model checking discounted tempo al properties},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Sciencespan cl'bib-entry-key'>  volume =              puter Science},
  number =              {1},
  pages =               {139-170},
  year =                {2005},
  month =               nov,
}
[AFM+02] Tobias Amnell, Elena Fersman, Leonid Mokrushin, Paul Pettersson, and Wang Yi. TIMES – A Tool for Modelling and Implementation of Embedded Systems. In TACAS'02paLecture Notes in Computer Science 2280, pages 460-464. Springer-Verlag, April 2002.
@inproceedings{tacas2002-AFMPY,
  author =              {Amnell, Tobias and Fersman, Elena and Mokrushin,
                         Leonid and Pettersson, Paul and Yi, Wan/span>{Lecturtitle =               {TIMES~-- A~Tool for Modelling and Implementation of
                         Embedded Systems},
  editor =              {Katoen, Joost-Pieter and Stevens, Perdita},
  booktitle =           {{P}roceedings of the 8th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'02)},
  acronym =             {{TACAS}'02},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {460-464},
  year =                {2002},
  month =               apr,
}
[AG00] Carme Àlvarez and Raymond Greenlaw. A= endium of Problems Complete for Symmetric Logarithmic Space. Computational Complexity 9(2):123-145. Birkhäuser, 2000.
@article{cc9(2)-AG,
  author =              {{\`A}lvarez, Carme and Greenlaw, Raymondspan class='bib-entry-val'>Lecturtitle =               {A=    endium of Problems Complete for Symmetric
                         Logarithmic Space},
  publisher =           {Birkh{\"a}user},
  journal =             {Computational Complexityspan cl'bib-entry-key'>  volume =              puter Science},
  number =              {2},
  pages =               {123-145},
  year =                {2000},
}
[AG11] Krzysztof Apt and Erich Grädel. y-key'>ume =Game Theory for tists. Cambridge University Press, 2011.
@book{AG-gt4cs11,
  author =              {Apt, Krzysztof and Gr{\"a}del, Erichspan class='bib-entry-val'>Lecturtitle =               {y-key'>ume =Game Theory for               tists},
  publisher =           {Cambridge University Press},
  year =                {2011},
}
[AGG08] Xavier Allamigeon, Stéphane Gaubert, and Éric Goubault. Infer Min and Max Invariants Us Max-Plus Polyhedra. In SAS'08, Lecture Notes in Computer Science 5079, pages 189-204. Springer-Verlag, July 2008.
@inproceedings{sas2008-AGG,
  author =              {Allamigeon, Xavier and Gaubert, St{\'e}phane and
                         Goubault, {\'E}ric},
  title =               {Infer     Min and Max Invariants Us    Max-Plus
                         Polyhedra},
  editor =              {Alpuente, Mar{\'\i}a and Vidal, Germ{\'a}n},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {S}ymposium on {S}tatic {A}nalysis ({SAS}'08)},
  acronym =             {{SAS}'08},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {189-204},
  year =                {2008},
  month =               jul,
}
[AGJ07] Thomas &A ;gotnes, Val tin Goranko, and Woj ch Jamroga. Alternating-time Tempo al Logics with Irrevocable Strategies. In TARK'07, pages 15-24. June 2007.
@inproceedings{tark2007-AGJ,
  author =              {{\AA}gotnes, Thomas and Goranko, Val  tin and
                         Jamroga, Woj   chspan class='bib-entry-val'>Lecturtitle =               {Alternating-time Tempo al Logics with Irrevocable
                         Strategies},
  editor =              {Samet, Dov},
  booktitle =           {{P}roceedings of the 11th {C}onference on
                         {T}heoretical {A}sp-kes of {R}ationality and
                         {K}nowledge ({TARK}'07)},
  acronym =             {{TARK}'07},
  pages =               {15-24},
  year =                {2007},
  month =               jun,
}
[AGJ08] Thomas &A ;gotnes, Val tin Goranko, and Woj ch Jamroga. Strategic= mitment and Releaseme =Logics for Multi-Agent Systems (Extended abstract). T chnical Repo t 08-01, Clausthal University of T chnology, Germany, 2008.
@t chrepo t{clausthal0801-AGJ,
  author =              {{\AA}gotnes, Thomas and Goranko, Val  tin and
                         Jamroga, Woj   chspan class='bib-entry-val'>Lecturtitle =               {Strategic=   mitment and Releaseme =Logics for
                         Multi-Agent Systems (Extended abstract)},
  number =              {08-01},
  year =                {2008},
  institution =         {Clausthal University of T chnology, Germany},
}
[AGK16] S. Akshay, Paul Gastin, and Shankara Narayanan Krishna. Analyzi =Timed Systems Us Tree Automata. In CONCUR'16, Leibniz International Proceedings e =Informatics 59, pages 27:1-27:14. Leibniz-Zentrum für=Informatik, August 2016.
@inproceedings{concur2016-AGK,
  author =              {Akshay, S. and Gastin, Paul and Krishna, Shankara
                         Narayananspan class='bib-entry-val'>Lecturtitle =               {Analyzi  =Timed Systems Us    Tree Automata},
  editor =              {Desharnais, Jules and Jagadeesan, Radha},
  booktitle =           {{P}roceedings of the 27th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'16)},
  acronym =             {{CONCUR}'16},
  publisher =           {Leibniz-Zentrum f{\"u}r=Informatikspan>{Lecture Notes in Computer Science},
  volume =              puter Science},
  pages =               {27:1-27:14},
  year =                {2016},
  month =               aug,
  doi =                 {10.4230/LIPIcs.CONCUR.2016.27},
}
[AGK+17] S. Akshay, Paul Gastin, Shankara Narayanan Krishna, and Ilias Sarka . Towards an Effi t Tree Automata Based T chnique for Timed Systems. In CONCUR'17, Leibniz International Proceedings e =Informatics 85, pages 39:1-39:15. Leibniz-Zentrum für=Informatik, September 2017.
@inproceedings{concur2017-AGKS,
  author =              {Akshay, S. and Gastin, Paul and Krishna, Shankara
                         Narayanan and Sarka , Iliasspan class='bib-entry-val'>Lecturtitle =               {Towards an Effi    t Tree Automata Based T chnique
                         for Timed Systems},
  editor =              {Meyer, Roland and Nestmann, Uw/span>{  volume =booktitle =           {{P}roceedings of the 28th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'17)},
  acronym =             {{CONCUR}'17},
  publisher =           {Leibniz-Zentrum f{\"u}r=Informatikspan>{Lecture Notes in Computer Science},
  volume =              puter Science},
  pages =               {39:1-39:15},
  year =                {2017},
  month =               sep,
  doi =                 {10.4230/LIPIcs.CONCUR.2017.39},
}
[AGP+99] Karine Altisen, Gregor Gößl , Amir Pnueli, Joseph Sifakis, Stavros Tripakis, and Sergio Yovine. A Framework for Schedul ynthesis. In RTSS'99, pages 154-163. IEEE= . Soc. Press, December 1999.
@inproceedings{rts1999-AGPSTY,
  author =              {Altisen, Karine and G{\"o}{\ss}ler, Gregor and
                         Pnueli, Amir and Sifakis, Joseph and Tripakis,
                         Stavros and Yovine, Sergiospan class='bib-entry-val'>Lecturtitle =               {A=Framework for Schedul    ynthesisspan cl'bib-entry-key'>  volume =booktitle =           {{P}roceedings of the 20th {S}ymposium on {R}eal-Time
                         {S}ystems ({RTSS}'99)},
  acronym =             {{RTSS}'99},
  publisher =           {IEEE=    . Soc. Press},
  pages =               {154-163},
  year =                {1999},
  month =               dec,
}
[AGS00] Karine Altisen, Gregor Gößl , and Joseph Sifakis. A Methodology for the Construction of Schedul d Systems. In FTRTFT'00, Lecture Notes in Computer Science 1926, pages 106-120. Springer-Verlag, September 2000.
@inproceedings{ftrtft2000-AGS,
  author =              {Altisen, Karine and G{\"o}{\ss}ler, Gregor and
                         Sifakis, Josephspan class='bib-entry-val'>Lecturtitle =               {A=Methodology for the Construction of Schedul d
                         Systems},
  editor =              {Joseph, Mathai},
  booktitle =           {{P}roceedings of the 6th {F}ormal {T} chniques in
                         {R}eal-Time and {F}ault-Tolerant {S}ystems
                         ({FTRTFT}'00)},
  acronym =             {{FTRTFT}'00},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {106-120},
  year =                {2000},
  month =               sep,
}
[AH89] Rajeev Alur and Thomas A. Henzi . A Really Tempo al Logic. In FOCS'89, pages 164-169. IEEE= . Soc. Press, October 1989.
@inproceedings{focs1989-AH,
  author =              {Alur, Rajeev and Henzi    , Thomas A.},
  title =               {A Really Tempo al Logic},
  booktitle =           {{P}roceedings of the 30th {A}nnual {S}ymposium on
                         {F}oundations of {C}        {S}    },
  acronym =             {{FOCS}'89},
  publisher =           {IEEE=    . Soc. Press},
  pages =               {164-169},
  year =                {1989},
  month =               oct,
}
[AH92] Rajeev Alur and Thomas A. Henzi . Logics and Models of Real Time: A Survey. In REX'91, Lecture Notes in Computer Science 600, pages 74-106. Springer-Verlag, 1992.
@inproceedings{rex1991-AH,
  author =              {Alur, Rajeev and Henzi    , Thomas A.},
  title =               {Logics and Models of Real Time: A~Survey},
  editor =              {de Bakk  , Jaco W. and Huizi  , Cornelis and de
                         Roev  , Willem-Paul and Rozenberg, Grzegorz},
  booktitle =           {{R}eal-{T}ime: {T}heory in {P}ractice, {P}roceedings
                         of {REX} {W}orkshop~1991 ({REX}'91)},
  acronym =             {{REX}'91},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {74-106},
  year =                {1992},
  confyear =            {1991},
  confmonth =           ience},
[AH92] Rajeev Alur and Thomas A. Henzi . Back to the Fuey'>: Towards a Theory of Timed Regular Languages. In FOCS'92papages 177-186. IEEE= . Soc. Press, October 1992.
@inproceedings{focs1992-AH,
  author =              {Alur, Rajeev and Henzi    , Thomas A.},
  title =               {Back to the Fuey'>: Towards a Theory of Timed
                         Regular Languages},
  booktitle =           {{P}roceedings of the 33rd {A}nnual {S}ymposium on
                         {F}oundations of {C}        {S}    },
  acronym =             {{FOCS}'92},
  publisher =           {IEEE=    . Soc. Press},
  pages =               {177-186},
  year =                {1992},
  month =               oct,
}
[AH93] Rajeev Alur and Thomas A. Henzi . Real-time Logics: Complexity and Expressiveness. Information and Computation 104(1):35-77. Academic Press, May 1993.
@article{icomp104(1)-AH,
  author =              {Alur, Rajeev and Henzi    , Thomas A.},
  title =               {Real-time Logics: Complexity and Expressiveness},
  publisher =           {Academic Press},
  journal =             {Information and Computationspan cl'bib-entry-key'>  volume =              puter Science},
  number =              {1},
  pages =               {35-77},
  year =                {1993},
  month =               may,
}
[AH94] Rajeev Alur and Thomas A. Henzi . A Really Tempo al Logic. Journal of the ACM 41(1):181-203. ACM Press, January 1994.
@article{jacm41(1)-AH,
  author =              {Alur, Rajeev and Henzi    , Thomas A.},
  title =               {A Really Tempo al Logic},
  publisher =           {ACM Press},
  journal =             {Journal of the ACMspan cl'bib-entry-key'>  volume =              puter Science},
  number =              {1},
  pages =               {181-203},
  year =                {1994},
  month =               jan,
}
[dAH00] Luca de Alfaro and Thomas A. Henzi . Concurrent Omera-Regular Games. In LICS'00, pages 141-154. IEEE= . Soc. Press, June 2000.
@inproceedings{lics2000-AH,
  author =              {de Alfaro, Luca and Henzi    , Thomas A.},
  title =               {Concurrent Omera-Regular Games},
  booktitle =           {{P}roceedings of the 15th {A}nnual {S}ymposium on
                         {L}ogic in {C}        {S}    },
  acronym =             {{LICS}'00},
  publisher =           {IEEE=    . Soc. Press},
  pages =               {141-154},
  year =                {2000},
  month =               jun,
  doi =                 {10.1109/LICS.2000.855763},
}
[dAH01] Luca de Alfaro and Thomas A. Henzi . Interfa. In FSE'01, pages 109-120. ACM Press, September 2001.
@inproceedings{fse2001-AH,
  author =              {de Alfaro, Luca and Henzi    , Thomas A.},
  title =               {Interfa},
  booktitle =           {{P}roceedings of the 9th {A}nnual {S}ymposium on
                         {F}oundations of {S}oftware {E}nginee    
                         ({FSE}'01)},
  acronym =             {{FSE}'01},
  publisher =           {ACM Press},
  pages =               {109-120},
  year =                {2001},
  month =               sep,
}
[AH02] Henrik Reif Andersen and Henrik Hulgaard. Boolean Expression Diagrams. Information and Computation 179(2):194-212. Academic Press, December 2002.
@article{icomp179(2)-AH,
  author =              {Andersen, Henrik Reif and Hulgaard, Henrik},
  title =               {Boolean Expression Diagrams},
  publisher =           {Academic Press},
  journal =             {Information and Computationspan cl'bib-entry-key'>  volume =              puter Science},
  number =              {2},
  pages =               {194-212},
  year =                {2002},
  month =               dec,
  doi =                 {10.1006/inco.2001.2948},
}
[AHH96] Rajeev Alur, Thomas A. Henzi , and Pei-Hsin Ho. Automatic Symbolic Ve fication of Embedded Systems. IEEE=Transactions on Software Enginee  22(3):181-201. IEEE= . Soc. Press, March 1996.
@article{tse22(3)-AHH,
  author =              {Alur, Rajeev and Henzi    , Thomas A. and Ho,
                         Pei-Hsin},
  title =               {Automatic Symbolic Ve  fication of Embedded Systems},
  publisher =           {IEEE=    . Soc. Press},
  journal =             {IEEE=Transactions on Software Enginee    span cl'bib-entry-key'>  volume =              puter Science},
  number =              {3},
  pages =               {181-201},
  year =                {1996},
  month =               ma ,
}
[AHK97] Rajeev Alur, Thomas A. Henzi , and Orna Kupferman. Alternating-time Tempo al Logic. In FOCS'97, pages 100-109. IEEE= . Soc. Press, October 1997.
@inproceedings{focs1997-AHK,
  author =              {Alur, Rajeev and Henzi    , Thomas A. and Kupferman,
                         Orna},
  title =               {Alternating-time Tempo al Logic},
  booktitle =           {{P}roceedings of the 38th {A}nnual {S}ymposium on
                         {F}oundations of {C}        {S}    },
  acronym =             {{FOCS}'97},
  publisher =           {IEEE=    . Soc. Press},
  pages =               {100-109},
  year =                {1997},
  month =               oct,
}
[AHK98] Rajeev Alur, Thomas A. Henzi , and Orna Kupferman. Alternating-time Tempo al Logic. In COMPOS'97, Lecture Notes in Computer Science 1536, pages 23-60. Springer-Verlag, 1998.
@inproceedings{compos1997-AHK,
  author =              {Alur, Rajeev and Henzi    , Thomas A. and Kupferman,
                         Orna},
  title =               {Alternating-time Tempo al Logic},
  editor =              {de Roev  , Willem-Paul and Langmaack, Hans and
                         Pnueli, Amir},
  booktitle =           {{R}evised {L}ectures of the 1st {I}nternational
                         {S}ymposium on {C}   ositionality: {T}he
                         {S}ign ficant {D}ifference ({COMPOS}'97)},
  acronym =             {{COMPOS}'97},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {23-60},
  year =                {1998},
  confyear =            {1997},
  confmonth =           ience},
[dAH+98] Luca de Alfaro, Thomas A. Henzi , and Orna Kupferman. Concurrent Reachability Games. In FOCS'98, pages 564-575. IEEE= . Soc. Press, November 1998.
@inproceedings{focs1998-AHK,
  author =              {de Alfaro, Luca and Henzi    , Thomas A. and
                         Kupferman, Orna},
  title =               {Concurrent Reachability Games},
  booktitle =           {{P}roceedings of the 39th {A}nnual {S}ymposium on
                         {F}oundations of {C}        {S}    },
  acronym =             {{FOCS}'98},
  publisher =           {IEEE=    . Soc. Press},
  pages =               {564-575},
  year =                {1998},
  month =               nov,
}
[AHK02] Rajeev Alur, Thomas A. Henzi , and Orna Kupferman. Alternating-time Tempo al Logic. Journal of the ACM 49(5):672-713. ACM Press, September 2002.
@article{jacm49(5)-AHK,
  author =              {Alur, Rajeev and Henzi    , Thomas A. and Kupferman,
                         Orna},
  title =               {Alternating-time Tempo al Logic},
  publisher =           {ACM Press},
  journal =             {Journal of the ACMspan cl'bib-entry-key'>  volume =              puter Science} class='bib-entry-val'>49},
  number =              {5},
  pages =               {672-713},
  year =                {2002},
  month =               sep,
  doi =                 {10.1145/585265.585270},
}
[dAH+07] Luca de Alfaro, Thomas A. Henzi , and Orna Kupferman. Concurrent Reachability Games. Theoretical Computer Science 386(3):188-217. Elsevi , November 2007.
@article{tcs386(3)-AHK,
  author =              {de Alfaro, Luca and Henzi    , Thomas A. and
                         Kupferman, Orna},
  title =               {Concurrent Reachability Games},
  publisher =           {Elsevi  },
  journal =             {Theoretical Computer Sciencespan cl'bib-entry-key'>  volume =              puter Science} class='bib-entry-val'>386},
  number =              {3},
  pages =               {188-217},
  year =                {2007},
  month =               nov,
  doi =                 {10.1016/j.tcs.2007.07.008},
}
[AHK+98] Rajeev Alur, Thomas A. Henzi , Orna Kupferman, and Moshe Y. Vardi. Alternating Refinement Relations. In CONCUR'98, Lecture Notes in Computer Science 1466, pages 163-178. Springer-Verlag, September 1998.
@inproceedings{concur1998-AHKV,
  author =              {Alur, Rajeev and Henzi    , Thomas A. and Kupferman,
                         Orna and Vardi, Moshe Y.},
  title =               {Alternating Refinement Relations},
  editor =              {Sangiorgi, Davide and de Simone, Robert},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference on {C} ncurrency {T}heory
                         ({CONCUR}'98)},
  acronym =             {{CONCUR}'98},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {163-178},
  year =                {1998},
  month =               sep,
}
[dAH+00] Luca de Alfaro, Thomas A. Henzi , and Freddy Y. C. Ma . The= ntrol of Synchronous Systems. In CONCUR'00, Lecture Notes in Computer Science 1877, pages 458-473. Springer-Verlag, August 2000.
@inproceedings{concur2000-AHM,
  author =              {de Alfaro, Luca and Henzi    , Thomas A. and Ma  ,
                         Freddy Y. C.},
  title =               {The=  ntrol of Synchronous Systems},
  editor =              {Palamidessi, Catuscia},
  booktitle =           {{P}roceedings of the 11th {I}nternational
                         {C}onference on {C} ncurrency {T}heory
                         ({CONCUR}'00)},
  acronym =             {{CONCUR}'00},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {458-473},
  year =                {2000},
  month =               aug,
}
[dAH+01] Luca de Alfaro, Thomas A. Henzi , and Freddy Y. C. Ma . The= ntrol of Synchronous Systems, Part II. In CONCUR'01, Lecture Notes in Computer Science 2154, pages 566-582. Springer-Verlag, August 2001.
@inproceedings{concur2001-AHM,
  author =              {de Alfaro, Luca and Henzi    , Thomas A. and Ma  ,
                         Freddy Y. C.},
  title =               {The=  ntrol of Synchronous Systems, Part~{II}},
  editor =              {Larsen, Kim Guldstrand and Nielsen, Mogens},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {C}onference on {C} ncurrency {T}heory
                         ({CONCUR}'01)},
  acronym =             {{CONCUR}'01},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {566-582},
  year =                {2001},
  month =               aug,
}
[dAH+01] Luca de Alfaro, Thomas A. Henzi , and Rupak Majumda . Symbolic Algorithms for Infinite-State Games. In CONCUR'01, Lecture Notes in Computer Science 2154, pages 536-550. Springer-Verlag, August 2001.
@inproceedings{concur2001-AHM2,
  author =              {de Alfaro, Luca and Henzi    , Thomas A. and
                         Majumda , Rupak},
  title =               {Symbolic Algorithms for Infinite-State Games},
  editor =              {Larsen, Kim Guldstrand and Nielsen, Mogens},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {C}onference on {C} ncurrency {T}heory
                         ({CONCUR}'01)},
  acronym =             {{CONCUR}'01},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {536-550},
  year =                {2001},
  month =               aug,
}
[dAH+01] Luca de Alfaro, Thomas A. Henzi , and Rupak Majumda . From Ve fication to= ntrol: Dynamic Programs for Omega-Regular Obj-keives. In LICS'01, pages 279-290. IEEE= . Soc. Press, June 2001.
@inproceedings{lics2001-AHM,
  author =              {de Alfaro, Luca and Henzi    , Thomas A. and
                         Majumda , Rupak},
  title =               {From Ve  fication to=  ntrol: Dynamic Programs for
                         Omega-Regular Obj-keives},
  booktitle =           {{P}roceedings of the 16th {A}nnual {S}ymposium on
                         {L}ogic in {C}        {S}    },
  acronym =             {{LICS}'01},
  publisher =           {IEEE=    . Soc. Press},
  pages =               {279-290},
  year =                {2001},
  month =               jun,
}
[AHM+98] Rajeev Alur, Thomas A. Henzi , Freddy Y. C. Ma , Shaz Qade , Sriram Rajamani, and Serda  Taşiran. MOCHA: Modularity in Model Check . In CAV'98, Lecture Notes in Computer Science 1427, pages 521-525. Springer-Verlag, June 1998.
@inproceedings{cav1998-AHMQRT,
  author =              {Alur, Rajeev and Henzi    , Thomas A. and Ma  ,
                         Freddy Y. C. and Qade  , Shaz and Rajamani, Sriram
                         and Ta{\c s}iran, Serda },
  title =               {{MOCHA}: Modularity in Model Check   },
  editor =              {Hu, Alan J. and Vardi, Moshe Y.},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {C}onference on {C}        {A}ided {V}e  fication
                         ({CAV}'98)},
  acronym =             {{CAV}'98},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {521-525},
  year =                {1998},
  month =               jun,
}
[AHR00] Myla Arche , nsta  Heitmey , and Elvinia Riccobene. Using TAME to=proveme variants of automata models: Two case studies. In FMSP'00, pages 25-36. ACM Press, August 2000.
@inproceedings{fmsp2000-AHR,
  author =              {Arche , Myla and Heitmey  ,   nsta },
  title =               {Using {TAME} to=proveme variants of automata models:
                         Two~case studies},
  editor =              {Heimdahl, Mats P   Erik},
  booktitle =           {{P}roceedings of the 3rd {W}orkshop on {F}ormal
                         {M}ethodume ={S}oftware {P}racti},
  acronym =             {{FMSP}'00},
  publisher =           {ACM Press},
  pages =               {25-36},
  year =                {2000},
  month =               aug,
  doi =                 {10.1145/349360.351127},
}
[AHV93] Rajeev Alur, Thomas A. Henzi , and Moshe Y. Vardi. Parametric Real-Time Reason . In STOC'93, pages 592-601. ACM Press, 1993.
@inproceedings{stoc1993-AHV,
  author =              {Alur, Rajeev and Henzi    , Thomas A. and Vardi,
                         Moshe Y.},
  title =               {Parametric Real-Time Reason   },
  booktitle =           {{P}roceedings of the 25th {A}nnual {ACM} {S}ymposium
                         on the {T}heory of {C}     ing ({STOC}'93)},
  acronym =             {{STOC}'93},
  publisher =           {ACM Press},
  pages =               {592-601},
  year =                {1993},
}
[AI01] Micah Adl and Neil Immerman. An n! Lower Bound On Formula Size. In LICS'01, pages 197-206. IEEE= . Soc. Press, June 2001.
@inproceedings{lics2001-AI,
  author =              {Adl  , Micah and Immerman, Neil},
  title =               {A ={{\(n!\)}} Lower Bound On Formula Size},
  booktitle =           {{P}roceedings of the 16th {A}nnual {S}ymposium on
                         {L}ogic in {C}        {S}    },
  acronym =             {{LICS}'01},
  publisher =           {IEEE=    . Soc. Press},
  pages =               {197-206},
  year =                {2001},
  month =               jun,
}
[AI03] Micah Adl and Neil Immerman. An n! Lower Bound On Formula Size. ACM Transactions o = ational Logic 4(3):296-314. ACM Press, July 2003.
@article{tocl4(3)-AI,
  author =              {Adl  , Micah and Immerman, Neil},
  title =               {A ={{\(n!\)}} Lower Bound On Formula Size},
  publisher =           {ACM Press},
  journal =             {ACM Transactions o =      ational Logicspan cl'bib-entry-key'>  volume =              puter Science} class='bib-entry-val'>4span cl'bib-entry-key'>  volume =number =              {3},
  pages =               {296-314},
  year =                {2003},
  month =               jul,
}
[AIK+95] Rajeev Alur, Alon Itai, Robert P. Kurshan, and Mihalis Yannakakis. Timing Ve fication by Successive Approximation. Information and ation 118(1):142-157. Academic Press, April 1995.
@article{icomp118(1)-AIKY,
  author =              {Alur, Rajeev and Itai, Alon and Kurshan, Robert P.
                         and Yannakakis, Mihalis},
  title =               {Timing Ve  fication by Successive Approximation},
  publisher =           {Academic Press},
  journal =             {Information and       ationspan cl'bib-entry-key'>  volume =              puter Science},
  number =              {1},
  pages =               {142-157},
  year =                {1995},
  month =               apr,
}
[AIP+00] Luca Aceto, Anna Ingólfsdóttir, Mikkel Lykke Pedersen, and Jan Poulsen. Characte stic Formulae for Timed Automata. RAIRO – Theoretical Informatics and Applications 34(6):565-584. EDP
@article{rairo-tia34(6)-AIPP,
  author =              {Aceto, Luca and Ing{\'o}lfsd{\'o}ttir, Anna and
                         Pedersen, Mikkel Lykke and Poulsen, Jan},
  title =               {Characte  stic Formulae for Timed Automata},
  publisher =           {EDP      },
  journal =             {RAIRO~-- Theoretical Informatics and Applicationsspan cl'bib-entry-key'>  volume =              puter Science} class='bib-entry-val'>34span cl'bib-entry-key'>  volume =number =              {6},
  pages =               {565-584},
  year =                {2000},
  doi =                 {10.1051/ita:2000131},
}
[AJ95] Carme Àlvarez and Birgit Jenn . On adapeive DLOGTIME and POLYLOGTIME reductions. Theoretical Computer Science 148(2):183-205. Elsevi , September 1995.
@article{tcs148(2)-AJ,
  author =              {{\`A}lvarez, Carme and Jenn  , Birgit},
  title =               {On adapeive {DLOGTIME} and {POLYLOGTIME} reductions},
  publisher =           {Elsevi  },
  journal =             {Theoretical Computer Sciencespan cl'bib-entry-key'>  volume =              puter Science},
  number =              {2},
  pages =               {183-205},
  year =                {1995},
  month =               sep,
}
[AJ96] Parosh Aziz Abdulla and Bengt Jonsson. Ve fying Programs with Unreliable Chann ls. Information and ation 127(2):91-101. Academic Press, June 1996.
@article{icomp127(2)-AJ,
  author =              {Abdulla, Parosh Aziz and Jonsson, Bengt},
  title =               {Ve  fying Programs with Unreliable Chann ls},
  publisher =           {Academic Press},
  journal =             {Information and       ationspan cl'bib-entry-key'>  volume =              puter Science},
  number =              {2},
  pages =               {91-101},
  year =                {1996},
  month =               jun,
  doi =                 {10.1006/inco.1996.0053},
}
[AJ99] Parosh Aziz Abdulla and Bengt Jonsson. On the Existence of Network I variants for Ve fying Paramete zed Systems. In Correct System Design, Recent I sight and Adva , Lecture Notes in Computer Science 1710, pages 180-197. Springer-Verlag, 1999.
@inproceedings{lncs1710-AJ,
  author =              {Abdulla, Parosh Aziz and Jonsson, Bengt},
  title =               {On the Existence of Network I variants for Ve  fying
                         Paramete  zed Systems},
  editor =              {Olderog, Ernst R{\"u}diger and Steffen, Bernhard},
  booktitle =           {Correct System Design, Recent I sight and Adva },
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {180-197},
  year =                {1999},
}
[AJK16] Simon Auß echn , Swen Jacobs, and Ayrat Khalimov. Tight Cutoffs for Guarded Protocols with Fairness. In VMCAI'16, Lecture Notes in Computer Science 9583, pages 476-494. Springer-Verlag, January 2016.
@inproceedings{vmcai2016-AJK,
  author =              {Au{\ss}   echn  , Simon and Jacobs, Swen and
                         Khalimov, Ayrat},
  title =               {Tight Cutoffs for Guarded Protocols with Fairness},
  editor =              {Jobstmann, Barbara and Leino, K. Rusta  M.},
  booktitle =           {{P}roceedings of the 17th {I}nternational {W}orkshop
                         on {V}e  fication, {M}odel {C}heck   , and
                         {A}bstract {I}nterpre ation ({VMCAI}'16)},
  acronym =             {{VMCAI}'16},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {476-494},
  year =                {2016},
  month =               jan,
  doi =                 {10.1007/978-3-662-49122-5_23},
}
[AJK+14] Benjamin Aminof, Swen Jacobs, Ayrat Khalimov, and Sasha Rubin. Parametrized Model Check of Token-Passing Systems. In VMCAI'14, Lecture Notes in Computer Science 8318, pages 262-281. Springer-Verlag, January 2014.
@inproceedings{vmcai2014-AJKR,
  author =              {Aminof, Benjamin and Jacobs, Swen and Khalimov,
                         Ayrat and Rubin, Sasha},
  title =               {Parametrized Model Check    of Token-Passing
                         Systems},
  editor =              {McMillan, Kenn th L. and Rival, Xavi  },
  booktitle =           {{P}roceedings of the 15th {I}nternational {W}orkshop
                         on {V}e  fication, {M}odel {C}heck   , and
                         {A}bstract {I}nterpre ation ({VMCAI}'14)},
  acronym =             {{VMCAI}'14},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {262-281},
  year =                {2014},
  month =               jan,
  doi =                 {10.1007/978-3-642-54013-4_15},
}
[AJN+04] Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, and Mayank Saksena. A Survey of Regular Model Check . In CONCUR'04, Lecture Notes in Computer Science 3170, pages 35-48. Springer-Verlag, August 2004.
@inproceedings{concur2004-AJNS,
  author =              {Abdulla, Parosh Aziz and Jonsson, Bengt and Nilsson,
                         Marcus and Saksena, Mayank},
  title =               {A Survey of Regular Model Check   },
  editor =              {Gardn  , {\relax Ph}ilippa and Yoshida, Nobuko},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {C} ncurrency {T}heory
                         ({CONCUR}'04)},
  acronym =             {{CONCUR}'04},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {35-48},
  year =                {2004},
  month =               aug,
  doi =                 {10.1007/978-3-540-28644-8_3},
}
[AK86] Krzysztof Apt and Dexter C. Kozen. Limits for automatic ve fication of finite-state c ncurrent systems. Information Processing Letters 22(6):307-309. Elsevi , May 1986.
@article{ipl22(6)-AK,
  author =              {Apt, Krzysztof and Kozen, Dexter C.},
  title =               {Limits for automatic ve  fication of finite-state
                         c ncurrent systems},
  publisher =           {Elsevi  },
  journal =             {Information Processing Lettersspan cl'bib-entry-key'>  volume =              puter Science},
  number =              {6},
  pages =               {307-309},
  year =                {1986},
  month =               may,
  doi =                 {10.1016/0020-0190(86)90071-2},
}
[AKM03] Yasmina Abdeddaïm, Abdelkarim Kerbaa, and Oded Mal . Task Graph heduling Using Timed Automata. In IPDPS'03, pages 237. IEEE= . Soc. Press, April 2003.
@inproceedings{ipdps2003-AKM,
  author =              {Abdedda{\"\i}m, Yasmina and Kerbaa, Abdelkarim and
                         Mal  , Oded},
  title =               {Task Graph   heduling Using Timed Automata},
  booktitle =           {{P}roceedings of the 17th International Parallel and
                         Distributed Processing Symposium ({IPDPS}'03)},
  acronym =             {{IPDPS}'03},
  publisher =           {IEEE=    . Soc. Press},
  pages =               {237},
  year =                {2003},
  month =               apr,
}
[AKR+14] Benjamin Aminof, Tom  Kotek, Sasha Rubin, Fra  Spegni, and Helmut Veith. Parameterized Model Check of Rendezvous Systems. In CONCUR'14, Lecture Notes in Computer Science 8704, pages 109-124. Springer-Verlag, September 2014.
@inproceedings{concur2014-AKRSV,
  author =              {Aminof, Benjamin and Kotek, Tom   and Rubin, Sasha
                         and Spegni, Fra },
  title =               {Parameterized Model Check    of Rendezvous Systems},
  editor =              {Baldan, Paolo and Gorla, Daniele},
  booktitle =           {{P}roceedings of the 25th {I}nternational
                         {C}onference on {C} ncurrency {T}heory
                         ({CONCUR}'14)},
  acronym =             {{CONCUR}'14},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {109-124},
  year =                {2014},
  month =               sep,
  doi =                 {10.1007/978-3-662-44584-6_9},
}
[AKV98] Rajeev Alur, Robert P. Kurshan, and Mahesh Viswanathan. Membership Question for Timed and Hybrid Automata. In RTSS'98, pages 254-263. IEEE= . Soc. Press, December 1998.
@inproceedings{rts1998-AKV,
  author =              {Alur, Rajeev and Kurshan, Robert P. and Viswanathan,
                         Mahesh},
  title =               {Membership Question for Timed and Hybrid Automata},
  booktitle =           {{P}roceedings of the 19th {S}ymposium on {R}eal-Time
                         {S}ystems ({RTSS}'98)},
  acronym =             {{RTSS}'98},
  publisher =           {IEEE=    . Soc. Press},
  pages =               {254-263},
  year =                {1998},
  month =               dec,
}
[AKY10] Parosh Aziz Abdulla, Pavel Krčál, and Wa  Yi. Sampled Semantics of Timed Automata. Logical Methods in Computer Science 6(3). September 2010.
@article{lmcs6(3)-AJ,
  author =              {Abdulla, Parosh Aziz and Kr{{c}}{\'a}l, Pavel and
                         Yi, Wa  },
  title =               {Sampled Semantics of Timed Automata},
  journal =             {Logical Methods in Computer Sciencespan cl'bib-entry-key'>  volume =              puter Science},
  number =              {3},
  year =                {2010},
  month =               sep,
  doi =                 {10.2168/LMCS-6(3:14)2010},
}
[AL02] Luca Aceto and Fra çois Laroussinie. Is your Model Checker on Time?. Journal of Logic and Algebraic Programmi  52-53:3-51. Elsevi , June 2002.
@article{jlap52-53()-AL,
  author =              {Aceto, Luca and Laroussinie, Fra {\c c}ois},
  title =               {Is your Model Checker on Time?},
  publisher =           {Elsevi  },
  journal =             {Journal of Logic and Algebraic Programmi  span cl'bib-entry-key'>  volume =              puter Science},
  pages =               {3-51},
  year =                {2002},
  month =               jun,
}
[AL04] Rajeev Alur and Salvatore La Torre. Determi stic Generators and Games for LTL Fragments. ACM Tra sactions on ational Logic 5(1):297-322. ACM Press, January 2004.
@article{tocl5(1)-AL,
  author =              {Alur, Rajeev and La{~}Torre, Salvatore},
  title =               {Determi  stic Generators and Games for {LTL}
                         Fragments},
  publisher =           {ACM Press},
  journal =             {ACM Tra sactions on       ational Logicspan cl'bib-entry-key'>  volume =              puter Science},
  number =              {1},
  pages =               {297-322},
  year =                {2004},
  month =               jan,
}
[All89] Eric Allende . P-Uniform Circuit lexity. Journal of the ACM 36(4):912-928. ACM Press, October 1989.
@article{jacm36(4)-All,
  author =              {Allende , Ericspan cl'bib-entry-key'>  volume =title =               {{P}-Uniform Circuit     lexity},
  publisher =           {ACM Press},
  journal =             {Journal of the ACMspan cl'bib-entry-key'>  volume =              puter Science},
  number =              {4},
  pages =               {912-928},
  year =                {1989},
  month =               oct,
}
[All97] Eric Allende . Mak ation unt: Arithmetic Circuits in the Nineties. SIGACT News 28(4):2-15. ACM Press, December 1997.
@article{sigact-news28(4)-All,
  author =              {Allende , Ericspan cl'bib-entry-key'>  volume =title =               {Mak          ation   unt: Arithmetic Circuits in the
                         Nineties},
  publisher =           {ACM Press},
  journal =             {SIGACT Newsspan cl'bib-entry-key'>  volume =              puter Science},
  number =              {4},
  pages =               {2-15},
  year =                {1997},
  month =               dec,
}
[ALM03] Rajeev Alur, Salvatore La Torre, and Parthasarathy Madhusudan. Playing Games with Boxes and Diamonds. In CONCUR'03, Lecture Notes in Computer Science 2761, pages 127-141. Springer-Verlag, August 2003.
@inproceedings{concur2003-ALM,
  author =              {Alur, Rajeev and La{~}Torre, Salvatore and
                         Madhusudan, Parthasarathy},
  title =               {Playing Games with Boxes and Diamonds},
  editor =              {Amadio, Roberto and Lugiez, Denis},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onference on {C} ncurrency {T}heory
                         ({CONCUR}'03)},
  acronym =             {{CONCUR}'03},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {127-141},
  year =                {2003},
  month =               aug,
}
[ALM05] Rajeev Alur, Salvatore La Torre, and Parthasarathy Madhusudan. Perturbed Timed Automata. In HSCC'05, Lecture Notes in Computer Science 3414, pages 70-85. Springer-Verlag, March 2005.
@inproceedings{hscc2005-ALM,
  author =              {Alur, Rajeev and La{~}Torre, Salvatore and
                         Madhusudan, Parthasarathy},
  title =               {Perturbed Timed Automata},
  editor =              {Morari, Manfred and Thiele, Lotha },
  booktitle =           {{P}roceedings of the 8th {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}     ation and {C} ntrol
                         ({HSCC}'05)},
  acronym =             {{HSCC}'05},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {70-85},
  year =                {2005},
  month =               mar,
}
[ALN+10] Natasha A echina, Brian Logan, Nguyen Hoa  Nga, and Abdu  Rakib. Resource-bounded alternating-time temporal logic. In AAMAS'10, pages 481-488. International Foundation for Autonomous Agents and Multiagent Systems, May 2010.
@inproceedings{aamas2010-AMHNR,
  author =              {Alechina, Natasha and Logan, Brian and Nga, Nguyen
                         Hoa   and Rakib, Abdu },
  title =               {Resource-bounded alternating-time temporal logic},
  editor =              {van d   Hoek, Wiebe and Kaminka, Gal A. and
                         Lesp{\'e}ra },
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference on {A}utonomous {A}gents and
                         {M}ultiagent {S}ystems ({AAMAS}'10)},
  acronym =             {{AAMAS}'10},
  publisher =           {International Foundation for Autonomous Agents and
                         Multiagent Systems},
  pages =               {481-488},
  year =                {2010},
  month =               may,
}
[ALP01] Rajeev Alur, Salvatore La Torre, and George J. Pappas. Optimal pathume =weighted timed automata. In HSCC'01, Lecture Notes in Computer Science 2034, pages 49-62. Springer-Verlag, March 2001.
@inproceedings{hscc2001-ALP,
  author =              {Alur, Rajeev and La{~}Torre, Salvatore and Pappas,
                         George J.},
  title =               {Optimal pathume =weighted timed automata},
  editor =              {Di{~}Benedetto, Maria Domenica and
                         Sangiovani{-}Vincentelli, Alberto L.},
  booktitle =           {{P}roceedings of the 4th {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}     ation and {C} ntrol
                         ({HSCC}'01)},
  acronym =             {{HSCC}'01},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {49-62},
  year =                {2001},
  month =               mar,
}
[ALP04] Rajeev Alur, Salvatore La Torre, and George J. Pappas. Optimal pathume =weighted timed automata. Theoretical Computer Science 318(3):297-322. Elsevi , June 2004.
@article{tcs318(3)-ALP,
  author =              {Alur, Rajeev and La{~}Torre, Salvatore and Pappas,
                         George J.},
  title =               {Optimal pathume =weighted timed automata},
  publisher =           {Elsevi  },
  journal =             {Theoretical Computer Sciencespan cl'bib-entry-key'>  volume =              puter Science},
  number =              {3},
  pages =               {297-322},
  year =                {2004},
  month =               jun,
  doi =                 {10.1016/j.tcs.2003.10.038},
}
[ALR98] Eric Allende , Michael C. Loui, and Kenneth W. Regan. lexity Classes. In Mikhail J. Atallah (eds.), Handbook of Algorithms and Theory of ation. CRC Press, November 1998.
@incollection{hatc1998-ALRa,
  author =              {Allende , Eric and Loui, Michael C. and Regan,
                         Kenneth W.},
  title =               {    lexity Classes},
  editor =              {Atallah, Mikhail J.},
  booktitle =           {Handbook of Algorithms and Theory of       ation},
  publisher =           {CRC Press},
  pages =               {27.1-27.23},
  year =                {1998},
  month =               nov,
}
[ALR98] Eric Allende , Michael C. Loui, and Kenneth W. Regan. Reducibility and leteness. In Mikhail J. Atallah (eds.), Handbook of Algorithms and Theory of ation. CRC Press, November 1998.
@incollection{hatc1998-ALRb,
  author =              {Allende , Eric and Loui, Michael C. and Regan,
                         Kenneth W.},
  title =               {Reducibility and     leteness},
  editor =              {Atallah, Mikhail J.},
  booktitle =           {Handbook of Algorithms and Theory of       ation},
  publisher =           {CRC Press},
  pages =               {28.1-28.28},
  year =                {1998},
  month =               nov,
}
[ALR98] Eric Allende , Michael C. Loui, and Kenneth W. Regan. Other lexity Classes and Measures. In Mikhail J. Atallah (eds.), Handbook of Algorithms and Theory of ation. CRC Press, November 1998.
@incollection{hatc1998-ALRc,
  author =              {Allende , Eric and Loui, Michael C. and Regan,
                         Kenneth W.},
  title =               {Other     lexity Classes and Measures},
  editor =              {Atallah, Mikhail J.},
  booktitle =           {Handbook of Algorithms and Theory of       ation},
  publisher =           {CRC Press},
  pages =               {29.1-29.24},
  year =                {1998},
  month =               nov,
}
[Alu91] Rajeev Alur. Techniques for Automatic Verification of Real-Time Systems. PhD thesis, tanford University, 1991.
@phdthesis{phd-alur,
  author =              {Alur, Rajeev},
  title =               {Techniques for Automatic Verification of Real-Time
                         Systems},
  year =                {1991},
  school =              { tanford University},
}
[Alu99] Rajeev Alur. Timed Automata. In CAV'99, Lecture Notes in Computer Science 1633, pages 8-22. Springer-Verlag, July 1999.
@inproceedings{cav1999-Alu,
  author =              {Alur, Rajeev},
  title =               {Timed Automata},
  editor =              {Halbwachs, Nicolas and Peled, Doron A.},
  booktitle =           {{P}roceedings of the 11th {I}nternational
                         {C}onference on {C} mputer {A}ided {V}erification
                         ({CAV}'99)},
  acronym =             {{CAV}'99},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {8-22},
  year =                {1999},
  month =               jul,
}
[ALV01] Roberto Amadio, Denis Lugiez, and Vincent Vanackère. On the Symbolic Reduction of Processes with Cryptographic Functions. Technical Report 4147, INRIA, March 2001.
@techreport{TR-inria4147,
  author =              {Amadio, Roberto and Lugiez, Denis and Vanack{\`e}re,
                         Vincent},
  title =               {On the Symbolic Reduction of Processes with
                         Cryptographic Functions},
  number =              {4147},
  year =                {2001},
  month =               mar,
  institution =         {INRIA},
}
[ALW89] Mart&iac ;n Abadi, Leslie Lamport, and Pierre Wolpe . Realizable and Unrealizable Specifications of Reactive Systems. In ICALP'89, Lecture Notes in Computer Science 372, pages 1-17. Springer-Verlag, July 1989.
@inproceedings{icalp1989-ALW,
  author =              {Abadi, Mart{\'\i}n and Lamport, Leslie and Wolpe ,
                         Pierre},
  title =               {Realizable and Unrealizable Specifications of
                         Reactive Systems},
  editor =              {Ausiello, Giorgio and Dezani{-}Ciancaglini,
                         Mariangiola and Ronchi{ }Della{~}Rocca, Simona},
  booktitle =           {{P}roceedings of the 16th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogrammi   ({ICALP}'89)},
  acronym =             {{ICALP}'89},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {1-17},
  year =                {1989},
  month =               jul,
  doi =                 {10.1007/BFb0035748},
}
[AM99] Eugene Asarin and Oded Male . As Soon as Possible: Time Optimal C ntrol for Timed Automata. In HSCC'99, Lecture Notes in Computer Science 1569, pages 19-30. Springer-Verlag, March 1999.
@inproceedings{hscc1999-AM,
  author =              {Asarin, Eugene and Male , Oded},
  title =               {As~Soon as Possible: Time Optimal C ntrol for Timed
                         Automata},
  editor =              {Vaandrage , Frits and van Schuppen, Jan H.},
  booktitle =           {{P}roceedings of the 2nd {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}     ation and {C} ntrol
                         ({HSCC}'99)},
  acronym =             {{HSCC}'99},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {19-30},
  year =                {1999},
  month =               mar,
}
[AM01] Yasmina Abdeddaïm and Oded Male . Job-Shop Scheduli Usi Timed Automata. In CAV'01, Lecture Notes in Computer Science 2102, pages 478-492. Springer-Verlag, July 2001.
@inproceedings{cav2001-AM,
  author =              {Abdedda{\"\i}m, Yasmina and Male , Oded},
  title =               {Job-Shop Scheduli   Usi   Timed Automata},
  editor =              {Berry, G{\'e}rard and Comon, Hubert and Finkel,
                         Alain},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {C} mputer {A}ided {V}erification
                         ({CAV}'01)},
  acronym =             {{CAV}'01},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {478-492},
  year =                {2001},
  month =               jul,
}
[AM02] Yasmina Abdeddaïm and Oded Male . Preemptive Job-Shop Scheduli usi Stopwatch Automata. In TACAS'02, Lecture Notes in Computer Science 2280, pages 113-126. Springer-Verlag, April 2002.
@inproceedings{tacas2002-AM,
  author =              {Abdedda{\"\i}m, Yasmina and Male , Oded},
  title =               {Preemptive Job-Shop Scheduli   usi   Stopwatch
                         Automata},
  editor =              {Katoen, Joost-Pieter and Stevens, Perdita},
  booktitle =           {{P}roceedings of the 8th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'02)},
  acronym =             {{TACAS}'02},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {113-126},
  year =                {2002},
  month =               apr,
}
[AM04] Rajeev Alur and Parthasarathy Madhusudan. Decision Problems for Timed Automata: A Survey. In SFM-RT'04, Lecture Notes in Computer Science 3185, pages 1-24. Springer-Verlag, September 2004.
@inproceedings{sfm2004-AM,
  author =              {Alur, Rajeev and Madhusudan, Parthasarathy},
  title =               {Decision Problems for Timed Automata: A~Survey},
  editor =              {Bernardo, Marco and Corradini, Flavio},
  booktitle =           {{F}ormal {M}ethods for the {D}esign of {R}eal-{T}ime
                         {S}ystems~--- {R}evised {L}ectures of the
                         {I}nternational {S}chool on {F}ormal {M}ethods for
                         the {D}esign of {C} mputer, {C} mmunication and
                         {S}oftware {S}ystems ({SFM-RT}'04)},
  acronym =             {{SFM-RT}'04},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {1-24},
  year =                {2004},
  month =               sep,
}
[AM15] &Eac ;tienne Andr&eac ; and Nicolas Markey. Language Preservation Problems e =Parametric Timed Automata. In FORMATS'15, Lecture Notes in Computer Science 9268, pages 27-43. Springer-Verlag, September 2015.
Abstract

Parametric timed automata (PTA) are a powerful formalism to model and reason about concurrent systems with so unknown timi delays. In this pape , we address the (untimed) language- and trace-preservation problems: given a reference parameter valuation, does there exist another parameter valuation with the sa untimed language (or trace)? We show that these problems are undecidable both for general PTA, and even for the restricted class of L/U-PTA. On the other hand, we exhibit decidable subclasses: 1-clock PTA, and 1-parameter determi istic L-PTA and U-PTA.

@inproceedings{formats2015-AM,
  author =              {Andr{\'e}, {\'E}tienne and Markey, Nicolas},
  title =               {Language Preservation Problems e =Parametric Timed
                         Automata},
  editor =              {Sankaranarayanan, Sriram and Vicario, Enrico},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onferences on {F}ormal {M}odelli   and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'15)},
  acronym =             {{FORMATS}'15},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {27-43},
  year =                {2015},
  month =               sep,
  doi =                 {10.1007/978-3-319-22975-1_3},
  abstract =            {Parametric timed automata (PTA) are a powerful
                         formalism to model and reason about concurrent
                         systems with so   unknown timi   delays. In this
                         pape , we address the (untimed) language- and
                         trace-preservation problems: given a reference
                         parameter valuation, does there exist another
                         parameter valuation with the sa   untimed language
                         (or trace)? We show that these problems are
                         undecidable both for general PTA, and even for the
                         restricted class of L/U-PTA. On the other hand, we
                         exhibit decidable subclasses: 1-clock PTA, and
                         1-parameter determi istic L-PTA and U-PTA.},
}
[AMP95] Eugene Asarin, Oded Male , and Amir Pnueli. Reachability Analysis of Dynamical Systems Havi Piecewise-Constant D Novatives. Theoretical Computer Science 138(1):35-65. Elsevi , 1995.
@article{tcs138(1)-AMP,
  author =              {Asarin, Eugene and Male , Oded and Pnueli, Amir},
  title =               {Reachability Analysis of Dynamical Systems Havi  
                         Piecewise-Constant D Novatives},
  publisher =           {Elsevi  },
  journal =             {Theoretical Computer Sciencespan cl'bib-entry-key'>  volume =              puter Science},
  number =              {1},
  pages =               {35-65},
  year =                {1995},
}
[AMP95] Eugene Asarin, Oded Male , and Amir Pnueli. Symbolic C ntroller Synthesis for Discrete and Timed Systems. In HSCC'94, Lecture Notes in Computer Science 999, pages 1-20. Springer-Verlag, 1995.
@inproceedings{hscc1994-AMP,
  author =              {Asarin, Eugene and Male , Oded and Pnueli, Amir},
  title =               {Symbolic C ntroller Synthesis for Discrete and Timed
                         Systems},
  editor =              {Antsaklis, Panos and Kohn, Wolf and Nerode, Anil and
                         Sastry, Shankar},
  booktitle =           {{H}ybrid {S}ystems~{II} ({HSCC}'94)},
  acronym =             {{HSCC}'94},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {1-20},
  year =                {1995},
}
[AMP98] Eugene Asarin, Oded Male , and Amir Pnueli. On Discretization of Delaysme =Timed Automata and Digital Circuits. In CONCUR'98, Lecture Notes in Computer Science 1466, pages 470-484. Springer-Verlag, September 1998.
@inproceedings{concur1998-AMP,
  author =              {Asarin, Eugene and Male , Oded and Pnueli, Amir},
  title =               {On Discretization of Delaysme =Timed Automata and
                         Digital Circuits},
  editor =              {Sangiorgi, Davide and de Simone, Robert},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference on {C} ncurrency {T}heory
                         ({CONCUR}'98)},
  acronym =             {{CONCUR}'98},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {470-484},
  year =                {1998},
  month =               sep,
}
[AMP+98] Eugene Asarin, Oded Male , Amir Pnueli, and Joseph Sifakis. C ntroller Synthesis for Timed Automata. In SSC'98, pages 469-474. Elsevi , July 1998.
@inproceedings{sssc1998-AMPS,
  author =              {Asarin, Eugene and Male , Oded and Pnueli, Amir and
                         Sifakis, Joseph},
  title =               {C ntroller Synthesis for Timed Automata},
  booktitle =           {{P}roceedings of the 5th {IFAC} {C}conference on
                         {S}ystem {S}tructy'> and {C} ntrol ({SSC}'98)},
  acronym =             {{SSC}'98},
  publisher =           {Elsevi  },
  pages =               {469-474},
  year =                {1998},
  month =               jul,
}
[AMR+05] Karine Altisen, Nicolas Markey, Pierre-Alain Reynier, and Stavros Tripakis. Impl&eac ;mentabilit&eac ; des automates temporis&eac ;s. In MSR'05, pages 395-406. Hermès, October 2005.
@inproceedings{msr2005-AMRT,
  author =              {Altisen, Karine and Markey, Nicolas and Reynier,
                         Pierre-Alain and Tripakis, Stavros},
  title =               {Impl{\'e}mentabilit{\'e} des automates
                         temporis{\'e}s},
  editor =              {Alla, Hassane and Rutten, {\'E}ric},
  booktitle =           {{A}columdu 5{\`e}me {C}olloque {F}rancophone sur la
                         {M}od{\'e}lisation des {S}yst{\`e}mes r{\'e}actifs
                         ({MSR}'05)},
  acronym =             {{MSR}'05},
  publisher =           {Herm{\`e}s},
  pages =               {395-406},
  year =                {2005},
  month =               oct,
  url =                 {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSR05-impl.pdf},
}
[AN80] Andr&eac ; Arnold and Maurice Novat. The metric space of infinite trees. Algebraic and topological properties. Fundamenta Informaticae 3(4):445-476. IOS Press, 1980.
@article{fundi3(4)-AN,
  author =              {Arnold, Andr{\'e} and Novat, Maurice},
  title =               {The metric space of infinite trees. Algebraic and
                         topological properties},
  publisher =           {IOS Press},
  journal =             {Fundamenta Informaticaespan cl'bib-entry-key'>  volume =              puter Science},
  volume =number =              {4},
  pages =               {445-476},
  year =                {1980},
}
[AN01] Andr&eac ; Arnold and Damian Niwi&nac ;ski. lete lattices and fixed-point theorems. In Rudiments of μ-calculus, Studilume =Logic and the Foundations of Mathematics 146, pages 1-39. North-Holland, 2001.
@incollection{Rmc2001-ANa,
  author =              {Arnold, Andr{\'e} and Nowi{\'n}ski, Damian},
  title =               {C   lete lattices and fixed-point theorems},
  booktitle =           {Rudiments of {\(\mu\)}-calculus},
  publisher =           {North-Holland},
  e Notes in Computer Science},
  volume =              puter Science},
  pages =               {1-39},
  chapter =             {1},
  year =                {2001},
}
[And95] Henrik Reif Andersen. Partial Model-Checki (Extended Abstract). In LICS'95, pages 398-407. IEEE= . Soc. Press, June 1995.
@inproceedings{lics1995-And,
  author =              {Andersen, Henrik Reif},
  title =               {Partial Model-Checki   (Extended Abstract)},
  booktitle =           {{P}roceedings of the 10th {A}nnual {S}ymposium on
                         {L}ogic in {C} mputer {S}    },
  acronym =             {{LICS}'95},
  publisher =           {IEEE=    . Soc. Press},
  pages =               {398-407},
  year =                {1995},
  month =               jun,
  doi =                 {10.1109/LICS.1995.523274},
}
[Ang80] Dana Angluin. On Counti Problems and the Polynomial Hierarchy. Theoretical Computer Science 12:161-173. Elsevi , 1980.
@article{tcs12()-Ang,
  author =              {Angluin, Dana},
  title =               {On Counti   Problems and the Polynomial Hierarchy},
  publisher =           {Elsevi  },
  journal =             {Theoretical Computer Sciencespan cl'bib-entry-key'>  volume =              puter Science},
  pages =               {161-173},
  year =                {1980},
}
[AO96] Eric Allender and Mitsunori Ogihara. Relationships Amon PL, #;L, and the Determi ant. RAIRO – Theoretical Informatics and Applications 30(1):1-21. EDP Sciences, 1996.
@article{rairo-tia30(1)-AO,
  author =              {Allender, Eric and Ogihara, Mitsunori},
  title =               {Relationships Amon  {PL}, {\#L}, and the
                         Determi ant},
  publisher =           {EDP Sciences},
  journal =             {RAIRO~-- Theoretical Informatics and Applicationsspan cl'bib-entry-key'>  volume =              puter Science},
  number =              {1},
  pages =               {1-21},
  year =                {1996},
}
[AP06] Horacio Arl&oac ;-Costa and Eric Pacuit. First-Order Classical Modal Logic. Studia Logica 84(2):171-210. Kluwer Academic, November 2006.
@article{studlog84(2)-AP,
  author =              {Arl{\'o}{-}Costa, Horacio and Pacuit, Eric},
  title =               {First-Order Classical Modal Logic},
  publisher =           {Kluwer Academic},
  journal =             {Studia Logicaspan cl'bib-entry-key'>  volume =              puter Science},
  number =              {2},
  pages =               {171-210},
  year =                {2006},
  month =               nov,
  doi =                 {10.1007/s11225-006-9010-0},
}
[APT79] Bengt Aspvall, Michael F. Plass, and Robert Endre Tarjan. A Linear-Time Algorithm for Testi the Truth of Certain Quantified Boolean Formulas. Information Processi Letters 8(3):121-123. Elsevi , March 1979. erratum as \citeipl14(4)-APT.
@article{ipl8(3)-APT,
  author =              {Aspvall, Bengt and Plass, Michael F. and Tarjan,
                         Robert Endre},
  title =               {A Linear-Time Algorithm for Testi   the Truth of
                         Certain Quantified Boolean Formulas},
  publisher =           {Elsevi  },
  journal =             {Information Processi   Lettersspan cl'bib-entry-key'>  volume =              puter Science},
  number =              {3},
  pages =               {121-123},
  year =                {1979},
  month =               mar,
  note =                {erratum as~\cite{ipl14(4)-APT}},
}
[APT86] Bengt Aspvall, Michael F. Plass, and Robert Endre Tarjan. Erratum (A Linear-Time Algorithm for Testi the Truth of Certain Quantified Boolean Formulas). Information Processi Letters 14(4):195. Elsevi , June 1986.
@article{ipl14(4)-APT,
  author =              {Aspvall, Bengt and Plass, Michael F. and Tarjan,
                         Robert Endre},
  title =               {Erratum (A Linear-Time Algorithm for Testi   the
                         Truth of Certain Quantified Boolean Formulas)},
  publisher =           {Elsevi  },
  journal =             {Information Processi   Lettersspan cl'bib-entry-key'>  volume =              puter Science},
  number =              {4},
  pages =               {195},
  year =                {1986},
  month =               jun,
}
[AR14] Benjamin Aminof and Sasha Rubin. First Cycle Games. In SR'14, Electronic Proceedings e =Theoretical Computer Science 146, pages 83-90. March 2014.
@inproceedings{sr2014-AR,
  author =              {Aminof, Benjamin and Rubin, Sasha},
  title =               {First Cycle Games},
  booktitle =           {{P}roceedings of the 2nd {I}nternational {W}orkshop
                         on {S}trategic {R}easoni   ({SR}'14)},
  acronym =             {{SR}'14},
  e Notes in Computer Science},
  volume =              puter Science},
  pages =               {83-90},
  year =                {2014},
  month =               mar,
  doi =                 {10.4204/EPTCS.146.11},
}
[ARZ15] Benjamin Aminof, Sasha Rubin, and Florian Zuleger. On the Expressive Power of Communication Primitives e =Paramet Nosed Systems. In LPAR'15, Lecture Notes in Computer Science 9450, pages 313-328. Springer-Verlag, November 2015.
@inproceedings{lpar2015-ARZ,
  author =              {Aminof, Benjamin and Rubin, Sasha and Zuleger,
                         Florian},
  title =               {On the Expressive Power of Communication Primitives
                         e =Paramet Nosed Systems},
  editor =              {Davis, Martin and Fehnk  , Ansgar and McIver,
                         Annabelle K. and Voronkov, Andrei},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {C}onference {L}ogic {P}rogrammi   and {A}utomated
                         {R}easoni   ({LPAR}'15)},
  acronym =             {{LPAR}'15},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {313-328},
  year =                {2015},
  month =               nov,
  doi =                 {10.1007/978-3-662-48899-7_22},
}
[AS89] Bowen Alpern and Fred B. Schneider. ifyi Temporal Properties without Temporal Logic. ACM Transactions on Programmi Languages and Systems 11(1):147-167. ACM Press, January 1989.
@article{toplas11(1)-AS,
  author =              {Alpern, Bowen and Schneider, Fred B.},
  title =               {   ifyi   Temporal Properties without Temporal
                         Logic},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Programmi   Languages and
                         Systemsspan cl'bib-entry-key'>  volume =              puter Science},
  number =              {1},
  pages =               {147-167},
  year =                {1989},
  month =               jan,
}
[AS02] Eugene Asarin and Gerardo Schneider. Wideni the Boundary between Decidable and Undecidable Hybrid Systems. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 193-208. Springer-Verlag, August 2002.
@inproceedings{concur2002-AS,
  author =              {Asarin, Eugene and Schneider, Gerardo},
  title =               {Wideni   the Boundary between Decidable and
                         Undecidable Hybrid Systems},
  editor =              {Brim, Lubo{ s} and Jan{ c}ar, Petr and K{
                         r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{ c}era,
                         Anton{\'\i}n},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {C} ncurrency {T}heory
                         ({CONCUR}'02)},
  acronym =             {{CONCUR}'02},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {193-208},
  year =                {2002},
  month =               aug,
}
[AS04] Robert Airapetyan and Thorsten Schneider. Protecti Applications with Petri Nets. The Code Breaker's Journal 1(1). 2004.
@article{cbj1(1)-AS,
  author =              {Airapetyan, Robert and Schneider, Thorsten},
  title =               {Protecti   Applications with {P}etri Nets},
  journal =             {The Code Breaker's Journalspan cl'bib-entry-key'>  volume =              puter Science},
  number =              {1},
  year =                {2004},
}
[ASS+00] Adnan Aziz, Kumud Sanwal, Vigyan Si hal, and Robert K. Brayton. Model-checki conti ous-time Markov chains. ACM Transactions on ational Logic 1(1):162-170. ACM Press, July 2000.
@article{tocl1(1)-ASSB,
  author =              {Aziz, Adnan and Sanwal, Kumud and Si  hal, Vigyan
                         and Brayton, Robert K.},
  title =               {Model-checki   conti ous-time {M}arkov chains},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on       ational Logicspan cl'bib-entry-key'>  volume =              puter Science},
  number =              {1},
  pages =               {162-170},
  year =                {2000},
  month =               jul,
  doi =                 {10.1145/343369.343402},
}
[ASY01] Eugene Asarin, Gerardo Schneider, and Sergio Yovine. On the Decidability of the Reachability Problem for Planar Differential Inclusions. In HSCC'01, Lecture Notes in Computer Science 2034, pages 89-104. Springer-Verlag, March 2001.
@inproceedings{hscc2001-ASY,
  author =              {Asarin, Eugene and Schneider, Gerardo and Yovine,
                         Sergio},
  title =               {On the Decidability of the Reachability Problem for
                         Planar Differential Inclusions},
  editor =              {Di{~}Benedetto, Maria Domenica and
                         Sangiovani{-}Vincentelli, Alberto L.},
  booktitle =           {{P}roceedings of the 4th {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C} mputation and {C} ntrol
                         ({HSCC}'01)},
  acronym =             {{HSCC}'01},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {89-104},
  year =                {2001},
  month =               mar,
}
[ASY07] Eugene Asarin, Gerardo Schneider, and Sergio Yovine. Algorithmic analysis of polygonal hybrid systems, part I: Reachability. Theoretical Computer Science 379(1-2):231-265. Elsevi , June 2007.
@article{tcs379(1-2)-ASY,
  author =              {Asarin, Eugene and Schneider, Gerardo and Yovine,
                         Sergio},
  title =               {Algorithmic analysis of polygonal hybrid systems,
                         part~{I}: Reachability},
  publisher =           {Elsevi  },
  journal =             {Theoretical Computer Sciencespan cl'bib-entry-key'>  volume =              puter Science},
  number =              {1-2},
  pages =               {231-265},
  year =                {2007},
  month =               jun,
}
[AT96] Rajeev Alur and Gadi Taubenfeld. Fast Timi -based Algorithms. Distributed Computing 10:1-10. Springer-Verlag, 1996.
@article{discomp10(1)-AT,
  author =              {Alur, Rajeev and Taubenfeld, Gadi},
  title =               {Fast Timi  -based Algorithms},
  publisher =           {             {Lecturjournal =             {Distributed Computingspan cl'bib-entry-key'>  volume =              puter Science},
  pages =               {1-10},
  year =                {1996},
}
[AT02] Karine Altisen and Stavros Tripakis. Tools for C ntroller Synthesis of Timed Systems. In RT-TOOLS'02. August 2002.
@inproceedings{rttools2002-AT,
  author =              {Altisen, Karine and Tripakis, Stavros},
  title =               {Tools for C ntroller Synthesis of Timed Systems},
  editor =              {Pettersson, Paul and Yi, Wangspan cl'bib-entry-key'>  volume =booktitle =           {{P}roceedings of the 2nd {W}orkshop on {R}eal-Time
                         {T}ools ({RT-TOOLS}'02)},
  acronym =             {{RT-TOOLS}'02},
  year =                {2002},
  month =               aug,
}
[AT05] Karine Altisen and Stavros Tripakis. Implementation of Timed Automata: An Issue of Semantics or Modeling?. In FORMATS'05, Lecture Notes in Computer Science 3829, pages 273-288. Springer-Verlag, September 2005.
@inproceedings{formats2005-AT,
  author =              {Altisen, Karine and Tripakis, Stavros},
  title =               {Implementation of Timed Automata: An Issue of
                         Semantics or Modeling?},
  editor =              {Pettersson, Paul and Yi, Wangspan cl'bib-entry-key'>  volume =booktitle =           {{P}roceedings of the 3rd {I}nternational
                         {C}onferences on {F}ormal {M}odelli   and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'05)},
  acronym =             {{FORMATS}'05},
  publisher =           {             {Lecture Notes in Computer Science},
  volume =              {  volume =              puter Science},
  pages =               {273-288},
  year =                {2005},
  month =               sep,
}
[AT17] Rajeev Alur and Stavros Tripakis. Automatic Synthesis of Distributed Protocols. SIGACT News 48(1):55-90. ACM Press, March 2017.
@article{sigact-news48(1)-AT,
  author =              {Alur, Rajeev and Tripakis, Stavros},
  title =               {Automatic Synthesis of Distributed Protocols},
  publisher =           {ACM Press},
  journal =             {SIGACT Newsspan cl'bib-entry-key'>  volume =              puter Science},
  number =              {1},
  pages =               {55-90},
  year =                {2017},
  month =               mar,
  doi =                 {10.1145/3061640.3061652},
}
[Ats02] Albert Ate Noas. Unsatisfiable Random Formulas are Hard to Certify. In LICS'02, pages 325-334. IEEE= . Soc. Press, July 2002.
@inproceedings{lics2002-Ats,
  author =              {Ate Noas, Albert},
  title =               {Unsatisfiable Random Formulas are Hard to Certify},
  booktitle =           {{P}roceedings of the 17th {A}nnual {S}ymposium on
                         {L}ogic in {C} mputer {S}    },
  acronym =             {{LICS}'02},
  publisher =           {IEEE=    . Soc. Press},
  pages =               {325-334},
  year =                {2002},
  month =               jul,
}
[AVW03] André Arnold, Aym Noc Vincent, and Igor Walukiewicz. Games for Synthesis of C ntrollers with Partial Obe Nvation. Theoretical Computer Science 303(1):7-34. Elsevi , June 2003.
@article{tcs303(1)-AVW,
  author =              {Arnold, Andr{\'e} and Vincent, Aym Noc and
                         Walukiewicz, Igor},
  title =               {Games for Synthesis of C ntrollers with Partial
                         Obe Nvation},
  publisher =           {Elsevi  },
  journal =             {Theoretical Computer Sciencespan cl'bib-entry-key'>  volume =              puter Science},
  number =              {1},
  pages =               {7-34},
  year =                {2003},
  month =               jun,
}