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,
}
[AAB23] Shaull Almagor, Daniel Assa, and Udi Boker. Synchronized CTL over One-Counter Automata. In FSTTCS'23, Leibniz International Proceedings in Informatics 284, pages 19:1-19:22. Leibniz-Zentrum für Informatik, December 2023. 
@inproceedings{fsttcs2023-AAB,
  author =              {Almagor, Shaull and Assa, Daniel and Boker, Udi},
  title =               {Synchronized {CTL} over One-Counter Automata},
  editor =              {Bouyer, Patricia and Srinivasan, Srikanth},
  booktitle =           {{P}roceedings of the 43rd {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'23)},
  acronym =             {{FSTTCS}'23},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {284},
  pages =               {19:1-19:22},
  year =                {2023},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2023.19},
}
[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},
}
[AAE05] Baruch Awerbuch, Yossi Azar, and Amir Epstein. The price of routing unsplittable flow. In STOC'05, pages 57-66. ACM Press, May 2005. 
@inproceedings{stoc2005-AAE,
  author =              {Awerbuch, Baruch and Azar, Yossi and Epstein, Amir},
  title =               {The price of routing unsplittable flow},
  editor =              {Gabow, Harold N. and Fagin, Ronald},
  booktitle =           {{P}roceedings of the 37th {A}nnual {ACM} {S}ymposium
                         on the {T}heory of {C}omputing ({STOC}'05)},
  acronym =             {{STOC}'05},
  publisher =           {ACM Press},
  pages =               {57-66},
  year =                {2005},
  month =               may,
  doi =                 {10.1145/1060590.1060599},
}
[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,
}
[AB09] Sanjeev Arora and Boaz Barak. Computational Complexity: A Modern Approach. Cambridge University Press, 2009. 
@book{AB09-CCMA,
  author =              {Arora, Sanjeev and Barak, Boaz},
  title =               {Computational Complexity: A~Modern Approach},
  publisher =           {Cambridge University Press},
  year =                {2009},
}
[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},
}
[ABD+17] Ernst Althaus, Björn Beber, Werner Damm, Stefan Disch, Willem Hagemann, Astrid Rakow, Christoph Scholl, Uwe Waldmann, and Boris Wirtz. Verification of linear hybrid systems with large discrete state spaces using counterexample-guided abstraction refinement. Science of Computer Programming 148:123-160. Elsevier, November 2017. 
@article{scp148()-ABDDHRSWW,
  author =              {Althaus, Ernst and Beber, Bj{\"o}rn and Damm, Werner
                         and Disch, Stefan and Hagemann, Willem and Rakow,
                         Astrid and Scholl, Christoph and Waldmann, Uwe and
                         Wirtz, Boris},
  title =               {Verification of linear hybrid systems with large
                         discrete state spaces using counterexample-guided
                         abstraction refinement},
  publisher =           {Elsevier},
  journal =             {Science of Computer Programming},
  volume =              {148},
  pages =               {123-160},
  year =                {2017},
  month =               nov,
  doi =                 {10.1016/j.scico.2017.04.010},
}
[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}},
  acronym =             {{ICALP}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7966},
  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}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8413},
  pages =               {424-439},
  year =                {2014},
  month =               apr,
  doi =                 {10.1007/978-3-642-54862-8_37},
}
[ABK16] Shaull Almagor, Udi Boker, and Orna Kupferman. Formally Reasoning about Quality. Journal of the ACM 63(3):24:1-24:56. ACM Press, September 2016. 
@article{jacm63(3)-ABK,
  author =              {Almagor, Shaull and Boker, Udi and Kupferman, Orna},
  title =               {Formally Reasoning about Quality},
  publisher =           {ACM Press},
  journal =             {Journal of the~ACM},
  volume =              {63},
  number =              {3},
  pages =               {24:1-24:56},
  year =                {2016},
  month =               sep,
  doi =                 {10.1145/2875421},
}
[ABK+97] Eugene Asarin, Marius Bozga, Alain Kerbrat, Oded Maler, Amir Pnueli, and Anne Rasse. Data-Structures 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-Structures 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}'97},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1201},
  pages =               {346-360},
  year =                {1997},
  month =               mar,
}
[ABK+03] Roy Armoni, Doron Bustan, Orna Kupferman, and Moshe Y. Vardi. Resets vs. Aborts in 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.} Aborts in 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}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2619},
  pages =               {65-80},
  year =                {2003},
  month =               apr,
}
[ABM99] Carlos Areces, Patrick Blackburn, and Maarten Marx. A Road-Map on Complexity 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 Complexity for Hybrid Logics},
  editor =              {Flum, 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}'99},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1862},
  pages =               {307-321},
  year =                {1999},
  month =               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
                         Logics},
  publisher =           {Oxford University Press},
  journal =             {Logic Journal of the IGPL},
  volume =              {8},
  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}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  pages =               {122-133},
  year =                {2004},
}
[ABO97] Eric Allender, Robert Beals, and Mitsunori Ogihara. The Complexity of Matrix Rank and Feasible Systems of Linear Equations. Technical Report 97-40, Rutgers 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 Equations},
  number =              {97-40},
  year =                {1997},
  month =               sep,
  institution =         {Rutgers University, New Jersey, USA},
}
[Abr79] Karl Abrahamson. Modal Logic of Concurrent Nondeterministic 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 Nondeterministic Programs},
  editor =              {Kahn, Gilles},
  booktitle =           {{P}roceedings of the International Symposium
                         Semantics of Concurrent Computation ({SCC}'79)},
  acronym =             {{SCC}'79},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {70},
  pages =               {21-33},
  year =                {1979},
  month =               jul,
}
[AC02] Jean-Pierre Aubin and Francine Catté. Bilateral Fixed-point and Algebraic Properties of Viability Kernels and Capture 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 =               {Bilateral Fixed-point and Algebraic Properties of
                         Viability Kernels and Capture Basins of Sets},
  number =              {02-10},
  year =                {2002},
  month =               apr,
  institution =         {CeReMaDe, Universit\'e Paris 9, Paris, France},
}
[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 Computation},
  volume =              {104},
  number =              {1},
  pages =               {2-34},
  year =                {1993},
  month =               may,
}
[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'92, pages 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. Henzinger. 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 Henzinger,
                         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 =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {836},
  pages =               {162-177},
  year =                {1994},
  month =               aug,
}
[ACH97] Rajeev Alur, Costas Courcoubetis, and Thomas A. Henzinger. Computing Accumulated Delays in Real Time Systems. Formal Methods in System Design 11(2):137-155. Kluwer Academic, August 1997. 
@article{fmsd11(2)-ACH,
  author =              {Alur, Rajeev and Courcoubetis, Costas and Henzinger,
                         Thomas A.},
  title =               {Computing Accumulated Delays in Real Time Systems},
  publisher =           {Kluwer Academic},
  journal =             {Formal Methods in System Design},
  volume =              {11},
  number =              {2},
  pages =               {137-155},
  year =                {1997},
  month =               aug,
}
[ACH+93] Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger, and Pei-Hsin Ho. Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems. In HSCC'92, Lecture Notes in Computer Science 736, pages 209-229. Springer-Verlag, 1993. 
@inproceedings{hscc1992-ACHH,
  author =              {Alur, Rajeev and Courcoubetis, Costas and Henzinger,
                         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, Hans},
  booktitle =           {{H}ybrid {S}ystems ({HSCC}'92)},
  acronym =             {{HSCC}'92},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {736},
  pages =               {209-229},
  year =                {1993},
}
[ACH+95] Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A. Henzinger, 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 Henzinger, 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 Science},
  volume =              {138},
  number =              {1},
  pages =               {3-34},
  year =                {1995},
}
[ACJ+96] Parosh Aziz Abdulla, Kārlis Čerāns, Bengt Jonsson, and Yih-Kuen Tsay. General 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 {\v{C}}er{\={a}}ns,
                         K{\={a}}rlis and Jonsson, Bengt and Tsay, Yih-Kuen},
  title =               {General 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 Maler. 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 Maler, 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,
}
[ACZ+20] Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, and Miaomiao Zhang. Learning One-Clock Timed Automata. In TACAS'20 (Part I), Lecture Notes in Computer Science 12078, pages 444-462. Springer-Verlag, April 2020. 
@inproceedings{tacas2020-ACZZZ,
  author =              {An, Jie and Chen, Mingshuai and Zhan, Bohua and
                         Zhan, Naijun and Zhang, Miaomiao},
  title =               {Learning One-Clock Timed Automata},
  editor =              {Biere, Armin and Parker, David},
  booktitle =           {{P}roceedings of the 26th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'20)~-- {P}art~{I}},
  acronym =             {{TACAS}'20 (Part~{I})},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {12078},
  pages =               {444-462},
  year =                {2020},
  month =               apr,
  doi =                 {10.1007/978-3-030-45190-5_25},
}
[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 Computation},
  volume =              {82},
  number =              {2},
  pages =               {198-229},
  year =                {1989},
  month =               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 =              {Paterson, 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 =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {443},
  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 Science},
  volume =              {126},
  number =              {2},
  pages =               {183-235},
  year =                {1994},
  month =               apr,
}
[AD09] Timos Antonopoulos and Anuj Dawar. Separating 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 Dawar, Anuj},
  title =               {Separating 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 =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5504},
  pages =               {63-77},
  year =                {2009},
  month =               mar,
}
[ADK+04] Elliot Anshelevich, Anirban Dasgupta, Jon Kleinberg, Éva Tardos, Tom Wexler, 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 Wexler, 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},
}
[ADK+08] Elliot Anshelevich, Anirban Dasgupta, Jon Kleinberg, Éva Tardos, Tom Wexler, and Tim Roughgarden. The Price of Stability for Network Design with Fair Cost Allocation. SIAM Journal on Computing 38(4):1602-1623. Society for Industrial and Applied Math., 2008. 
@article{siamcomp38(4)-ADKTWR,
  author =              {Anshelevich, Elliot and Dasgupta, Anirban and
                         Kleinberg, Jon and Tardos, {\'E}va and Wexler, Tom
                         and Roughgarden, Tim},
  title =               {The~Price of Stability for Network Design with Fair
                         Cost Allocation},
  publisher =           {Society for Industrial and Applied Math.},
  journal =             {SIAM Journal on Computing},
  volume =              {38},
  number =              {4},
  pages =               {1602-1623},
  year =                {2008},
  doi =                 {10.1137/070680096},
}
[ADM04] Parosh Aziz Abdulla, Johann Deneux, and Pritha Mahata. Multi-clock timed networks. In LICS'04, pages 345-354. IEEE Comp. Soc. Press, July 2004. 
@inproceedings{lics2004-ADM,
  author =              {Abdulla, Parosh Aziz and Deneux, Johann and Mahata,
                         Pritha},
  title =               {Multi-clock timed networks},
  booktitle =           {{P}roceedings of the 19th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'04)},
  acronym =             {{LICS}'04},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {345-354},
  year =                {2004},
  month =               jul,
  doi =                 {10.1109/LICS.2004.1319629},
}
[ADM+09] Rajeev Alur, Aldric Degorre, Oded Maler, 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 Maler, 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 =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5504},
  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 =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3580},
  pages =               {1089-1101},
  year =                {2005},
  month =               jul,
}
[AEL+01] Rajeev Alur, Kousha Etessami, Salvatore La Torre, and Doron A. Peled. Parametric Temporal Logic for "Model Measuring". ACM Transactions on Computational Logic 2(3):388-407. ACM Press, July 2001. 
@article{tocl2(3)-AELP,
  author =              {Alur, Rajeev and Etessami, Kousha and La{~}Torre,
                         Salvatore and Peled, Doron A.},
  title =               {Parametric Temporal Logic for {"}Model Measuring{"}},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {2},
  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 Singerman, Andreas Tiemeyer, Moshe Y. Vardi, and Yael Zbar. The ForSpec Temporal Logic: A New Temporal Property-Specification Language. In TACAS'02, Lecture 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 Singerman,
                         Eli and Tiemeyer, Andreas and Vardi, Moshe Y. and
                         Zbar, Yael},
  title =               {The {ForSpec} Temporal Logic: A New Temporal
                         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 =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2280},
  pages =               {296-311},
  year =                {2002},
  month =               apr,
}
[AFF+03] Roy Armoni, Limor Fix, Alon Flaisher, Orna Grumberg, Nir Piterman, Andreas Tiemeyer, and Moshe Y. Vardi. Enhanced Vacuity Detection in Linear Temporal Logic. 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 Piterman, Nir and Tiemeyer,
                         Andreas and Vardi, Moshe Y.},
  title =               {Enhanced Vacuity Detection in Linear Temporal Logic},
  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 =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2725},
  pages =               {368-380},
  year =                {2003},
  month =               jul,
  doi =                 {10.1007/978-3-540-45069-6_35},
}
[AFH91] Rajeev Alur, Tómas Feder, and Thomas A. Henzinger. The Benefits of Relaxing Punctuality. In PODC'91, pages 139-152. ACM Press, August 1991. 
@inproceedings{podc1991-AFH,
  author =              {Alur, Rajeev and Feder, T{\'o}mas and Henzinger,
                         Thomas A.},
  title =               {The Benefits of Relaxing Punctuality},
  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. Henzinger. 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 Henzinger, 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 =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {818},
  pages =               {1-13},
  year =                {1994},
  month =               jun,
}
[AFH96] Rajeev Alur, Tómas Feder, and Thomas A. Henzinger. The Benefits of Relaxing Punctuality. Journal of the ACM 43(1):116-146. ACM Press, January 1996. 
@article{jacm43(1)-AFH,
  author =              {Alur, Rajeev and Feder, T{\'o}mas and Henzinger,
                         Thomas A.},
  title =               {The Benefits of Relaxing Punctuality},
  publisher =           {ACM Press},
  journal =             {Journal of the~ACM},
  volume =              {43},
  number =              {1},
  pages =               {116-146},
  year =                {1996},
  month =               jan,
}
[AFH99] Rajeev Alur, Limor Fix, and Thomas A. Henzinger. 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 Henzinger, Thomas
                         A.},
  title =               {Event-Clock Automata: A Determinizable Class of
                         Timed Automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  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. Henzinger, Rupak Majumdar, and Mariëlle Stoelinga. The Element of Surprise in 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 Henzinger,
                         Thomas A. and Majumdar, Rupak and Stoelinga,
                         Mari{\"e}lle},
  title =               {The Element of Surprise in 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 =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2761},
  pages =               {142-156},
  year =                {2003},
  month =               aug,
}
[dAF+05] Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, and Mariëlle Stoelinga. Model checking discounted temporal properties. Theoretical Computer Science 345(1):139-170. Elsevier, November 2005. 
@article{tcs345(1)-AFHMS,
  author =              {de Alfaro, Luca and Faella, Marco and Henzinger,
                         Thomas A. and Majumdar, Rupak and Stoelinga,
                         Mari{\"e}lle},
  title =               {Model checking discounted temporal properties},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {345},
  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'02, Lecture 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, Wang},
  title =               {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 =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2280},
  pages =               {460-464},
  year =                {2002},
  month =               apr,
}
[AG00] Carme Àlvarez and Raymond Greenlaw. A Compendium 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, Raymond},
  title =               {A Compendium of Problems Complete for Symmetric
                         Logarithmic Space},
  publisher =           {Birkh{\"a}user},
  journal =             {Computational Complexity},
  volume =              {9},
  number =              {2},
  pages =               {123-145},
  year =                {2000},
}
[AG11] Krzysztof Apt and Erich Grädel. Lectures in Game Theory for Computer Scientists. Cambridge University Press, 2011. 
@book{AG-gt4cs11,
  author =              {Apt, Krzysztof and Gr{\"a}del, Erich},
  title =               {Lectures in Game Theory for Computer Scientists},
  publisher =           {Cambridge University Press},
  year =                {2011},
}
[AGG08] Xavier Allamigeon, Stéphane Gaubert, and Éric Goubault. Inferring Min and Max Invariants Using 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 =               {Inferring Min and Max Invariants Using 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 =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5079},
  pages =               {189-204},
  year =                {2008},
  month =               jul,
}
[AGJ07] Thomas Ågotnes, Valentin Goranko, and Wojciech Jamroga. Alternating-time Temporal Logics with Irrevocable Strategies. In TARK'07, pages 15-24. June 2007. 
@inproceedings{tark2007-AGJ,
  author =              {{\AA}gotnes, Thomas and Goranko, Valentin and
                         Jamroga, Wojciech},
  title =               {Alternating-time Temporal Logics with Irrevocable
                         Strategies},
  editor =              {Samet, Dov},
  booktitle =           {{P}roceedings of the 11th {C}onference on
                         {T}heoretical {A}spects of {R}ationality and
                         {K}nowledge ({TARK}'07)},
  acronym =             {{TARK}'07},
  pages =               {15-24},
  year =                {2007},
  month =               jun,
}
[AGJ08] Thomas Ågotnes, Valentin Goranko, and Wojciech Jamroga. Strategic Commitment and Release in Logics for Multi-Agent Systems (Extended abstract). Technical Report 08-01, Clausthal University of Technology, Germany, 2008. 
@techreport{clausthal0801-AGJ,
  author =              {{\AA}gotnes, Thomas and Goranko, Valentin and
                         Jamroga, Wojciech},
  title =               {Strategic Commitment and Release in Logics for
                         Multi-Agent Systems (Extended abstract)},
  number =              {08-01},
  year =                {2008},
  institution =         {Clausthal University of Technology, Germany},
}
[AGK16] S. Akshay, Paul Gastin, and Shankara Narayanan Krishna. Analyzing Timed Systems Using Tree Automata. In CONCUR'16, Leibniz International Proceedings in 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
                         Narayanan},
  title =               {Analyzing Timed Systems Using 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 Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {59},
  pages =               {27:1-27:14},
  year =                {2016},
  month =               aug,
  doi =                 {10.4230/LIPIcs.CONCUR.2016.27},
}
[AGK17] Guy Avni, Shibashis Guha, and Orna Kupferman. Timed Network Games. In MFCS'17, Leibniz International Proceedings in Informatics 84, pages 37:1-37:16. Leibniz-Zentrum für Informatik, August 2017. 
@inproceedings{mfcs2017-AGK,
  author =              {Avni, Guy and Guha, Shibashis and Kupferman, Orna},
  title =               {Timed Network Games},
  editor =              {Larsen, Kim Guldstrand and Bodlaender, Hans L. and
                         Raskin, Jean-Fran{\c c}ois},
  booktitle =           {{P}roceedings of the 42nd {I}nternational
                         {S}ymposium on {M}athematical {F}oundations of
                         {C}omputer {S}cience ({MFCS}'17)},
  acronym =             {{MFCS}'17},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {84},
  pages =               {37:1-37:16},
  year =                {2017},
  month =               aug,
  doi =                 {10.4230/LIPIcs.MFCS.2017.37},
}
[AGK18] Guy Avni, Shibashis Guha, and Orna Kupferman. Timed Network Games with Clocks. In MFCS'18, Leibniz International Proceedings in Informatics 117, pages 23:1-23:18. Leibniz-Zentrum für Informatik, August 2018. 
@inproceedings{mfcs2018-AGK,
  author =              {Avni, Guy and Guha, Shibashis and Kupferman, Orna},
  title =               {Timed Network Games with Clocks},
  editor =              {Potapov, Igor and Spirakis, Paul G. and Worrell,
                         James},
  booktitle =           {{P}roceedings of the 43rd {I}nternational
                         {S}ymposium on {M}athematical {F}oundations of
                         {C}omputer {S}cience ({MFCS}'18)},
  acronym =             {{MFCS}'18},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {117},
  pages =               {23:1-23:18},
  year =                {2018},
  month =               aug,
  doi =                 {10.4230/LIPIcs.MFCS.2018.23},
}
[AGK+17] S. Akshay, Paul Gastin, Shankara Narayanan Krishna, and Ilias Sarkar. Towards an Efficient Tree Automata Based Technique for Timed Systems. In CONCUR'17, Leibniz International Proceedings in 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 Sarkar, Ilias},
  title =               {Towards an Efficient Tree Automata Based Technique
                         for Timed Systems},
  editor =              {Meyer, Roland and Nestmann, Uwe},
  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 Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {85},
  pages =               {39:1-39:15},
  year =                {2017},
  month =               sep,
  doi =                 {10.4230/LIPIcs.CONCUR.2017.39},
}
[AGP+99] Karine Altisen, Gregor Gößler, Amir Pnueli, Joseph Sifakis, Stavros Tripakis, and Sergio Yovine. A Framework for Scheduler Synthesis. In RTSS'99, pages 154-163. IEEE Comp. 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, Sergio},
  title =               {A Framework for Scheduler Synthesis},
  booktitle =           {{P}roceedings of the 20th {S}ymposium on {R}eal-Time
                         {S}ystems ({RTSS}'99)},
  acronym =             {{RTSS}'99},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {154-163},
  year =                {1999},
  month =               dec,
}
[AGS00] Karine Altisen, Gregor Gößler, and Joseph Sifakis. A Methodology for the Construction of Scheduled 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, Joseph},
  title =               {A Methodology for the Construction of Scheduled
                         Systems},
  editor =              {Joseph, Mathai},
  booktitle =           {{P}roceedings of the 6th {F}ormal {T}echniques in
                         {R}eal-Time and {F}ault-Tolerant {S}ystems
                         ({FTRTFT}'00)},
  acronym =             {{FTRTFT}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1926},
  pages =               {106-120},
  year =                {2000},
  month =               sep,
}
[AH89] Rajeev Alur and Thomas A. Henzinger. A Really Temporal Logic. In FOCS'89, pages 164-169. IEEE Comp. Soc. Press, October 1989. 
@inproceedings{focs1989-AH,
  author =              {Alur, Rajeev and Henzinger, Thomas A.},
  title =               {A Really Temporal Logic},
  booktitle =           {{P}roceedings of the 30th {A}nnual {S}ymposium on
                         {F}oundations of {C}omputer {S}cience ({FOCS}'89)},
  acronym =             {{FOCS}'89},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {164-169},
  year =                {1989},
  month =               oct,
}
[AH92] Rajeev Alur and Thomas A. Henzinger. 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 Henzinger, Thomas A.},
  title =               {Logics and Models of Real Time: A~Survey},
  editor =              {de~Bakker, Jaco W. and Huizing, Cornelis and de
                         Roever, 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 =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {600},
  pages =               {74-106},
  year =                {1992},
  confyear =            {1991},
  confmonth =           {6},
}
[AH92] Rajeev Alur and Thomas A. Henzinger. Back to the Future: Towards a Theory of Timed Regular Languages. In FOCS'92, pages 177-186. IEEE Comp. Soc. Press, October 1992. 
@inproceedings{focs1992-AH,
  author =              {Alur, Rajeev and Henzinger, Thomas A.},
  title =               {Back to the Future: Towards a Theory of Timed
                         Regular Languages},
  booktitle =           {{P}roceedings of the 33rd {A}nnual {S}ymposium on
                         {F}oundations of {C}omputer {S}cience ({FOCS}'92)},
  acronym =             {{FOCS}'92},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {177-186},
  year =                {1992},
  month =               oct,
}
[AH93] Rajeev Alur and Thomas A. Henzinger. 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 Henzinger, Thomas A.},
  title =               {Real-time Logics: Complexity and Expressiveness},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {104},
  number =              {1},
  pages =               {35-77},
  year =                {1993},
  month =               may,
}
[AH94] Rajeev Alur and Thomas A. Henzinger. A Really Temporal Logic. Journal of the ACM 41(1):181-203. ACM Press, January 1994. 
@article{jacm41(1)-AH,
  author =              {Alur, Rajeev and Henzinger, Thomas A.},
  title =               {A Really Temporal Logic},
  publisher =           {ACM Press},
  journal =             {Journal of the~ACM},
  volume =              {41},
  number =              {1},
  pages =               {181-203},
  year =                {1994},
  month =               jan,
}
[dAH00] Luca de Alfaro and Thomas A. Henzinger. Concurrent Omera-Regular Games. In LICS'00, pages 141-154. IEEE Comp. Soc. Press, June 2000. 
@inproceedings{lics2000-AH,
  author =              {de Alfaro, Luca and Henzinger, Thomas A.},
  title =               {Concurrent Omera-Regular Games},
  booktitle =           {{P}roceedings of the 15th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'00)},
  acronym =             {{LICS}'00},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {141-154},
  year =                {2000},
  month =               jun,
  doi =                 {10.1109/LICS.2000.855763},
}
[dAH01] Luca de Alfaro and Thomas A. Henzinger. Interface automata. In FSE'01, pages 109-120. ACM Press, September 2001. 
@inproceedings{fse2001-AH,
  author =              {de Alfaro, Luca and Henzinger, Thomas A.},
  title =               {Interface automata},
  booktitle =           {{P}roceedings of the 9th {A}nnual {S}ymposium on
                         {F}oundations of {S}oftware {E}ngineering
                         ({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 Computation},
  volume =              {179},
  number =              {2},
  pages =               {194-212},
  year =                {2002},
  month =               dec,
  doi =                 {10.1006/inco.2001.2948},
}
[AHH96] Rajeev Alur, Thomas A. Henzinger, and Pei-Hsin Ho. Automatic Symbolic Verification of Embedded Systems. IEEE Transactions on Software Engineering 22(3):181-201. IEEE Comp. Soc. Press, March 1996. 
@article{tse22(3)-AHH,
  author =              {Alur, Rajeev and Henzinger, Thomas A. and Ho,
                         Pei-Hsin},
  title =               {Automatic Symbolic Verification of Embedded Systems},
  publisher =           {IEEE Comp. Soc. Press},
  journal =             {IEEE Transactions on Software Engineering},
  volume =              {22},
  number =              {3},
  pages =               {181-201},
  year =                {1996},
  month =               mar,
}
[AHK97] Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time Temporal Logic. In FOCS'97, pages 100-109. IEEE Comp. Soc. Press, October 1997. 
@inproceedings{focs1997-AHK,
  author =              {Alur, Rajeev and Henzinger, Thomas A. and Kupferman,
                         Orna},
  title =               {Alternating-time Temporal Logic},
  booktitle =           {{P}roceedings of the 38th {A}nnual {S}ymposium on
                         {F}oundations of {C}omputer {S}cience ({FOCS}'97)},
  acronym =             {{FOCS}'97},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {100-109},
  year =                {1997},
  month =               oct,
}
[AHK98] Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time Temporal Logic. In COMPOS'97, Lecture Notes in Computer Science 1536, pages 23-60. Springer-Verlag, 1998. 
@inproceedings{compos1997-AHK,
  author =              {Alur, Rajeev and Henzinger, Thomas A. and Kupferman,
                         Orna},
  title =               {Alternating-time Temporal Logic},
  editor =              {de Roever, Willem-Paul and Langmaack, Hans and
                         Pnueli, Amir},
  booktitle =           {{R}evised {L}ectures of the 1st {I}nternational
                         {S}ymposium on {C}ompositionality: {T}he
                         {S}ignificant {D}ifference ({COMPOS}'97)},
  acronym =             {{COMPOS}'97},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1536},
  pages =               {23-60},
  year =                {1998},
  confyear =            {1997},
  confmonth =           {9},
}
[dAH+98] Luca de Alfaro, Thomas A. Henzinger, and Orna Kupferman. Concurrent Reachability Games. In FOCS'98, pages 564-575. IEEE Comp. Soc. Press, November 1998. 
@inproceedings{focs1998-AHK,
  author =              {de Alfaro, Luca and Henzinger, Thomas A. and
                         Kupferman, Orna},
  title =               {Concurrent Reachability Games},
  booktitle =           {{P}roceedings of the 39th {A}nnual {S}ymposium on
                         {F}oundations of {C}omputer {S}cience ({FOCS}'98)},
  acronym =             {{FOCS}'98},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {564-575},
  year =                {1998},
  month =               nov,
}
[AHK02] Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time Temporal Logic. Journal of the ACM 49(5):672-713. ACM Press, September 2002. 
@article{jacm49(5)-AHK,
  author =              {Alur, Rajeev and Henzinger, Thomas A. and Kupferman,
                         Orna},
  title =               {Alternating-time Temporal Logic},
  publisher =           {ACM Press},
  journal =             {Journal of the~ACM},
  volume =              {49},
  number =              {5},
  pages =               {672-713},
  year =                {2002},
  month =               sep,
  doi =                 {10.1145/585265.585270},
}
[dAH+07] Luca de Alfaro, Thomas A. Henzinger, and Orna Kupferman. Concurrent Reachability Games. Theoretical Computer Science 386(3):188-217. Elsevier, November 2007. 
@article{tcs386(3)-AHK,
  author =              {de Alfaro, Luca and Henzinger, Thomas A. and
                         Kupferman, Orna},
  title =               {Concurrent Reachability Games},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {386},
  number =              {3},
  pages =               {188-217},
  year =                {2007},
  month =               nov,
  doi =                 {10.1016/j.tcs.2007.07.008},
}
[AHK16] Guy Avni, Thomas A. Henzinger, and Orna Kupferman. Dynamic Resource Allocation Games. In SAGT'16, Lecture Notes in Computer Science 9928, pages 153-166. Springer-Verlag, September 2016. 
@inproceedings{sagt2016-AHK,
  author =              {Avni, Guy and Henzinger, Thomas A. and Kupferman,
                         Orna},
  title =               {Dynamic Resource Allocation Games},
  booktitle =           {{P}roceedings of the 9th {I}nternational {S}ymposium
                         on {A}lgorithmic {G}ame {T}heory ({SAGT}'16)},
  acronym =             {{SAGT}'16},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9928},
  pages =               {153-166},
  year =                {2016},
  month =               sep,
  doi =                 {10.1007/978-3-662-53354-3_13},
}
[AHK20] Guy Avni, Thomas A. Henzinger, and Orna Kupferman. Dynamic Resource Allocation Games. Theoretical Computer Science 807:42-55. Elsevier, February 2020. 
@article{tcs807()-AHK,
  author =              {Avni, Guy and Henzinger, Thomas A. and Kupferman,
                         Orna},
  title =               {Dynamic Resource Allocation Games},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {807},
  pages =               {42-55},
  year =                {2020},
  month =               feb,
  doi =                 {10.1016/j.tcs.2019.06.031},
}
[AHK+98] Rajeev Alur, Thomas A. Henzinger, 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 Henzinger, 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}oncurrency {T}heory
                         ({CONCUR}'98)},
  acronym =             {{CONCUR}'98},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1466},
  pages =               {163-178},
  year =                {1998},
  month =               sep,
}
[dAH+00] Luca de Alfaro, Thomas A. Henzinger, and Freddy Y. C. Mang. The Control 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 Henzinger, Thomas A. and Mang,
                         Freddy Y. C.},
  title =               {The Control of Synchronous Systems},
  editor =              {Palamidessi, Catuscia},
  booktitle =           {{P}roceedings of the 11th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'00)},
  acronym =             {{CONCUR}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1877},
  pages =               {458-473},
  year =                {2000},
  month =               aug,
}
[dAH+01] Luca de Alfaro, Thomas A. Henzinger, and Freddy Y. C. Mang. The Control 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 Henzinger, Thomas A. and Mang,
                         Freddy Y. C.},
  title =               {The Control of Synchronous Systems, Part~{II}},
  editor =              {Larsen, Kim Guldstrand and Nielsen, Mogens},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'01)},
  acronym =             {{CONCUR}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2154},
  pages =               {566-582},
  year =                {2001},
  month =               aug,
}
[dAH+01] Luca de Alfaro, Thomas A. Henzinger, and Rupak Majumdar. 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 Henzinger, Thomas A. and
                         Majumdar, 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}oncurrency {T}heory
                         ({CONCUR}'01)},
  acronym =             {{CONCUR}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2154},
  pages =               {536-550},
  year =                {2001},
  month =               aug,
}
[dAH+01] Luca de Alfaro, Thomas A. Henzinger, and Rupak Majumdar. From Verification to Control: Dynamic Programs for Omega-Regular Objectives. In LICS'01, pages 279-290. IEEE Comp. Soc. Press, June 2001. 
@inproceedings{lics2001-AHM,
  author =              {de Alfaro, Luca and Henzinger, Thomas A. and
                         Majumdar, Rupak},
  title =               {From Verification to Control: Dynamic Programs for
                         Omega-Regular Objectives},
  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 =               {279-290},
  year =                {2001},
  month =               jun,
}
[AHM+98] Rajeev Alur, Thomas A. Henzinger, Freddy Y. C. Mang, Shaz Qadeer, Sriram Rajamani, and Serdar Taşiran. MOCHA: Modularity in Model Checking. In CAV'98, Lecture Notes in Computer Science 1427, pages 521-525. Springer-Verlag, June 1998. 
@inproceedings{cav1998-AHMQRT,
  author =              {Alur, Rajeev and Henzinger, Thomas A. and Mang,
                         Freddy Y. C. and Qadeer, Shaz and Rajamani, Sriram
                         and Ta{\c s}iran, Serdar},
  title =               {{MOCHA}: Modularity in Model Checking},
  editor =              {Hu, Alan J. and Vardi, Moshe Y.},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'98)},
  acronym =             {{CAV}'98},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1427},
  pages =               {521-525},
  year =                {1998},
  month =               jun,
}
[AHR00] Myla Archer, Constance L. Heitmeyer, and Elvinia Riccobene. Using TAME to prove invariants of automata models: Two case studies. In FMSP'00, pages 25-36. ACM Press, August 2000. 
@inproceedings{fmsp2000-AHR,
  author =              {Archer, Myla and Heitmeyer, Constance L. and
                         Riccobene, Elvinia},
  title =               {Using {TAME} to prove invariants of automata models:
                         Two~case studies},
  editor =              {Heimdahl, Mats Per Erik},
  booktitle =           {{P}roceedings of the 3rd {W}orkshop on {F}ormal
                         {M}ethods in {S}oftware {P}ractice ({FMSP}'00)},
  acronym =             {{FMSP}'00},
  publisher =           {ACM Press},
  pages =               {25-36},
  year =                {2000},
  month =               aug,
  doi =                 {10.1145/349360.351127},
}
[AHV93] Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi. Parametric Real-Time Reasoning. In STOC'93, pages 592-601. ACM Press, 1993. 
@inproceedings{stoc1993-AHV,
  author =              {Alur, Rajeev and Henzinger, Thomas A. and Vardi,
                         Moshe Y.},
  title =               {Parametric Real-Time Reasoning},
  booktitle =           {{P}roceedings of the 25th {A}nnual {ACM} {S}ymposium
                         on the {T}heory of {C}omputing ({STOC}'93)},
  acronym =             {{STOC}'93},
  publisher =           {ACM Press},
  pages =               {592-601},
  year =                {1993},
}
[AI01] Micah Adler and Neil Immerman. An n! Lower Bound On Formula Size. In LICS'01, pages 197-206. IEEE Comp. Soc. Press, June 2001. 
@inproceedings{lics2001-AI,
  author =              {Adler, Micah and Immerman, Neil},
  title =               {An {{\(n!\)}} Lower Bound On Formula Size},
  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 =               {197-206},
  year =                {2001},
  month =               jun,
}
[AI03] Micah Adler and Neil Immerman. An n! Lower Bound On Formula Size. ACM Transactions on Computational Logic 4(3):296-314. ACM Press, July 2003. 
@article{tocl4(3)-AI,
  author =              {Adler, Micah and Immerman, Neil},
  title =               {An {{\(n!\)}} Lower Bound On Formula Size},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {4},
  number =              {3},
  pages =               {296-314},
  year =                {2003},
  month =               jul,
}
[AIK+95] Rajeev Alur, Alon Itai, Robert P. Kurshan, and Mihalis Yannakakis. Timing Verification by Successive Approximation. Information and Computation 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 Verification by Successive Approximation},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {118},
  number =              {1},
  pages =               {142-157},
  year =                {1995},
  month =               apr,
}
[AIP+00] Luca Aceto, Anna Ingólfsdóttir, Mikkel Lykke Pedersen, and Jan Poulsen. Characteristic Formulae for Timed Automata. RAIRO – Theoretical Informatics and Applications 34(6):565-584. EDP Sciences, 2000. 
@article{rairo-tia34(6)-AIPP,
  author =              {Aceto, Luca and Ing{\'o}lfsd{\'o}ttir, Anna and
                         Pedersen, Mikkel Lykke and Poulsen, Jan},
  title =               {Characteristic Formulae for Timed Automata},
  publisher =           {EDP Sciences},
  journal =             {RAIRO~-- Theoretical Informatics and Applications},
  volume =              {34},
  number =              {6},
  pages =               {565-584},
  year =                {2000},
  doi =                 {10.1051/ita:2000131},
}
[AJ95] Carme Àlvarez and Birgit Jenner. On adaptive DLOGTIME and POLYLOGTIME reductions. Theoretical Computer Science 148(2):183-205. Elsevier, September 1995. 
@article{tcs148(2)-AJ,
  author =              {{\`A}lvarez, Carme and Jenner, Birgit},
  title =               {On adaptive {DLOGTIME} and {POLYLOGTIME} reductions},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {148},
  number =              {2},
  pages =               {183-205},
  year =                {1995},
  month =               sep,
}
[AJ96] Parosh Aziz Abdulla and Bengt Jonsson. Verifying Programs with Unreliable Channels. Information and Computation 127(2):91-101. Academic Press, June 1996. 
@article{icomp127(2)-AJ,
  author =              {Abdulla, Parosh Aziz and Jonsson, Bengt},
  title =               {Verifying Programs with Unreliable Channels},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {127},
  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 Invariants for Verifying Parameterized Systems. In Correct System Design, Recent Insight and Advances, 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 Invariants for Verifying
                         Parameterized Systems},
  editor =              {Olderog, Ernst R{\"u}diger and Steffen, Bernhard},
  booktitle =           {Correct System Design, Recent Insight and Advances},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1710},
  pages =               {180-197},
  year =                {1999},
}
[AJ03] Parosh Aziz Abdulla and Bengt Jonsson. Model checking of systems with many identical timed processes. Theoretical Computer Science 290(1):241-264. Elsevier, January 2003. 
@article{tcs290(1)-AJ,
  author =              {Abdulla, Parosh Aziz and Jonsson, Bengt},
  title =               {Model checking of systems with many identical timed
                         processes},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {290},
  number =              {1},
  pages =               {241-264},
  year =                {2003},
  month =               jan,
  doi =                 {10.1016/S0304-3975(01)00330-9},
}
[AJK16] Simon Außerlechner, 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}erlechner, Simon and Jacobs, Swen and
                         Khalimov, Ayrat},
  title =               {Tight Cutoffs for Guarded Protocols with Fairness},
  editor =              {Jobstmann, Barbara and Leino, K. Rustan M.},
  booktitle =           {{P}roceedings of the 17th {I}nternational {W}orkshop
                         on {V}erification, {M}odel {C}hecking, and
                         {A}bstract {I}nterpretation ({VMCAI}'16)},
  acronym =             {{VMCAI}'16},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9583},
  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 Checking 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 Checking of Token-Passing
                         Systems},
  editor =              {McMillan, Kenneth L. and Rival, Xavier},
  booktitle =           {{P}roceedings of the 15th {I}nternational {W}orkshop
                         on {V}erification, {M}odel {C}hecking, and
                         {A}bstract {I}nterpretation ({VMCAI}'14)},
  acronym =             {{VMCAI}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8318},
  pages =               {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 Checking. 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 Checking},
  editor =              {Gardner, {\relax Ph}ilippa and Yoshida, Nobuko},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'04)},
  acronym =             {{CONCUR}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3170},
  pages =               {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 verification of finite-state concurrent systems. Information Processing Letters 22(6):307-309. Elsevier, May 1986. 
@article{ipl22(6)-AK,
  author =              {Apt, Krzysztof and Kozen, Dexter C.},
  title =               {Limits for automatic verification of finite-state
                         concurrent systems},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {22},
  number =              {6},
  pages =               {307-309},
  year =                {1986},
  month =               may,
  doi =                 {10.1016/0020-0190(86)90071-2},
}
[AK16] Shaull Almagor and Orna Kupferman. High-Quality Synthesis Against Stochastic Environments. In CSL'16, Leibniz International Proceedings in Informatics 62, pages 28:1-28:17. Leibniz-Zentrum für Informatik, September 2016. 
@inproceedings{csl2016-AK,
  author =              {Almagor, Shaull and Kupferman, Orna},
  title =               {High-Quality Synthesis Against Stochastic
                         Environments},
  editor =              {Talbot, Jean-Marc and Regnier, Laurent},
  booktitle =           {{P}roceedings of the 25th {EACSL} {A}nnual
                         {C}onference on {C}omputer {S}cience {L}ogic
                         ({CSL}'16)},
  acronym =             {{CSL}'16},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {62},
  pages =               {28:1-28:17},
  year =                {2016},
  month =               sep,
  doi =                 {10.4230/LIPIcs.CSL.2016.28},
}
[AKK15] Shaull Almagor, Denis Kuperberg, and Orna Kupferman. The Sensing Cost of Monitoring and Synthesis. In FSTTCS'15, Leibniz International Proceedings in Informatics 45, pages 380-393. Leibniz-Zentrum für Informatik, December 2015. 
@inproceedings{fsttcs2015-AKK,
  author =              {Almagor, Shaull and Kuperberg, Denis and Kupferman,
                         Orna},
  title =               {The~Sensing Cost of Monitoring and Synthesis},
  editor =              {Harsha, Prahladh and Ramalingam, G.},
  booktitle =           {{P}roceedings of the 35th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'15)},
  acronym =             {{FSTTCS}'15},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {45},
  pages =               {380-393},
  year =                {2015},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2015.380},
}
[AKM03] Yasmina Abdeddaïm, Abdelkarim Kerbaa, and Oded Maler. Task Graph Scheduling Using Timed Automata. In IPDPS'03, pages 237. IEEE Comp. Soc. Press, April 2003. 
@inproceedings{ipdps2003-AKM,
  author =              {Abdedda{\"\i}m, Yasmina and Kerbaa, Abdelkarim and
                         Maler, Oded},
  title =               {Task Graph Scheduling Using Timed Automata},
  booktitle =           {{P}roceedings of the 17th International Parallel and
                         Distributed Processing Symposium ({IPDPS}'03)},
  acronym =             {{IPDPS}'03},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {237},
  year =                {2003},
  month =               apr,
}
[AKP18] Shaull Almagor, Orna Kupferman, and Giuseppe Perelli. Synthesis of Controllable Nash Equilibria in Quantitative Objective Games. In IJCAI'18, pages 35-41. IJCAI organization, July 2018. 
@inproceedings{ijcai2018-AKP,
  author =              {Almagor, Shaull and Kupferman, Orna and Perelli,
                         Giuseppe},
  title =               {Synthesis of Controllable {N}ash Equilibria in
                         Quantitative Objective Games},
  editor =              {Lang, J{\'e}r{\^o}me},
  booktitle =           {{P}roceedings of the 27th {I}nternational {J}oint
                         {C}onference on {A}rtificial {I}ntelligence
                         ({IJCAI}'18)},
  acronym =             {{IJCAI}'18},
  publisher =           {IJCAI organization},
  pages =               {35-41},
  year =                {2018},
  month =               jul,
  doi =                 {10.24963/ijcai.2018/5},
}
[AKR+14] Benjamin Aminof, Tomer Kotek, Sasha Rubin, Francesco Spegni, and Helmut Veith. Parameterized Model Checking 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, Tomer and Rubin, Sasha
                         and Spegni, Francesco and Veith, Helmut},
  title =               {Parameterized Model Checking of Rendezvous Systems},
  editor =              {Baldan, Paolo and Gorla, Daniele},
  booktitle =           {{P}roceedings of the 25th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'14)},
  acronym =             {{CONCUR}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8704},
  pages =               {109-124},
  year =                {2014},
  month =               sep,
  doi =                 {10.1007/978-3-662-44584-6_9},
}
[AKR+17] Shaull Almagor, Orna Kupferman, Jan Oliver Ringert, and Yaron Velner. Quantitative Assume Guarantee Synthesis. In CAV'17, Lecture Notes in Computer Science 10427, pages 353-374. Springer-Verlag, July 2017. 
@inproceedings{cav2017-AKRV,
  author =              {Almagor, Shaull and Kupferman, Orna and Ringert, Jan
                         Oliver and Velner, Yaron},
  title =               {Quantitative Assume Guarantee Synthesis},
  editor =              {Majumdar, Rupak and Kuncak, Viktor},
  booktitle =           {{P}roceedings of the 29th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'17)},
  acronym =             {{CAV}'17},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {10427},
  pages =               {353-374},
  year =                {2017},
  month =               jul,
  doi =                 {10.1007/978-3-319-63390-9_19},
}
[AKV98] Rajeev Alur, Robert P. Kurshan, and Mahesh Viswanathan. Membership Question for Timed and Hybrid Automata. In RTSS'98, pages 254-263. IEEE Comp. 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 Comp. Soc. Press},
  pages =               {254-263},
  year =                {1998},
  month =               dec,
}
[AKY10] Parosh Aziz Abdulla, Pavel Krčál, and Wang 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{\v{c}}{\'a}l, Pavel and
                         Yi, Wang},
  title =               {Sampled Semantics of Timed Automata},
  journal =             {Logical Methods in Computer Science},
  volume =              {6},
  number =              {3},
  year =                {2010},
  month =               sep,
  doi =                 {10.2168/LMCS-6(3:14)2010},
}
[AL92] Martín Abadi and Leslie Lamport. An old-fashioned recipe for real time. In REX'91, Lecture Notes in Computer Science 600, pages 1-27. Springer-Verlag, 1992. 
@inproceedings{rex1991-AL,
  author =              {Abadi, Mart{\'\i}n and Lamport, Leslie},
  title =               {An old-fashioned recipe for real time},
  editor =              {de~Bakker, Jaco W. and Huizing, Cornelis and de
                         Roever, 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 =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {600},
  pages =               {1-27},
  year =                {1992},
  confyear =            {1991},
  confmonth =           {6},
  doi =                 {10.1007/BFb0031985},
}
[AL02] Luca Aceto and François Laroussinie. Is your Model Checker on Time?. Journal of Logic and Algebraic Programming 52-53:3-51. Elsevier, June 2002. 
@article{jlap52-53()-AL,
  author =              {Aceto, Luca and Laroussinie, Fran{\c c}ois},
  title =               {Is your Model Checker on Time?},
  publisher =           {Elsevier},
  journal =             {Journal of Logic and Algebraic Programming},
  volume =              {52-53},
  pages =               {3-51},
  year =                {2002},
  month =               jun,
}
[AL04] Rajeev Alur and Salvatore La Torre. Deterministic Generators and Games for LTL Fragments. ACM Transactions on Computational Logic 5(1):297-322. ACM Press, January 2004. 
@article{tocl5(1)-AL,
  author =              {Alur, Rajeev and La{~}Torre, Salvatore},
  title =               {Deterministic Generators and Games for {LTL}
                         Fragments},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {5},
  number =              {1},
  pages =               {297-322},
  year =                {2004},
  month =               jan,
}
[All89] Eric Allender. P-Uniform Circuit Complexity. Journal of the ACM 36(4):912-928. ACM Press, October 1989. 
@article{jacm36(4)-All,
  author =              {Allender, Eric},
  title =               {{P}-Uniform Circuit Complexity},
  publisher =           {ACM Press},
  journal =             {Journal of the~ACM},
  volume =              {36},
  number =              {4},
  pages =               {912-928},
  year =                {1989},
  month =               oct,
}
[All97] Eric Allender. Making Computation Count: Arithmetic Circuits in the Nineties. SIGACT News 28(4):2-15. ACM Press, December 1997. 
@article{sigact-news28(4)-All,
  author =              {Allender, Eric},
  title =               {Making Computation Count: Arithmetic Circuits in the
                         Nineties},
  publisher =           {ACM Press},
  journal =             {SIGACT News},
  volume =              {28},
  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}oncurrency {T}heory
                         ({CONCUR}'03)},
  acronym =             {{CONCUR}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2761},
  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, Lothar},
  booktitle =           {{P}roceedings of the 8th {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
                         ({HSCC}'05)},
  acronym =             {{HSCC}'05},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3414},
  pages =               {70-85},
  year =                {2005},
  month =               mar,
}
[ALM20] Étienne André, Didier Lime, and Nicolas Markey. Language-preservation problems in parametric timed automata. Logical Methods in Computer Science 16(1). January 2020.
Abstract

Parametric timed automata (PTA) are a powerful formalism to model and reason about concurrent systems with some unknown timing delays. In this paper, we address the (untimed) language- and trace-preservation problems: given a reference parameter valuation, does there exist another parameter valuation with the same untimed language, or with the same set of traces? We show that these problems are undecidable both for general PTA and for the restricted class of L/U-PTA, even for integer-valued parameters, or over bounded time. On the other hand, we exhibit decidable subclasses: 1-clock PTA, and 1-parameter deterministic L-PTA and U-PTA. We also consider robust versions of these problems, where we additionally require that the language be preserved for all valuations between the reference valuation and the new valuation.

@article{lmcs16(1)-ALM,
  author =              {Andr{\'e}, {\'E}tienne and Lime, Didier and Markey,
                         Nicolas},
  title =               {Language-preservation problems in parametric timed
                         automata},
  journal =             {Logical Methods in Computer Science},
  volume =              {16},
  number =              {1},
  year =                {2020},
  month =               jan,
  doi =                 {10.23638/LMCS-16(1:5)2020},
  abstract =            {Parametric timed automata (PTA) are a powerful
                         formalism to model and reason about concurrent
                         systems with some unknown timing delays. In~this
                         paper, we~address the (untimed) language- and
                         trace-preservation problems: given a reference
                         parameter valuation, does there exist another
                         parameter valuation with the same untimed language,
                         or with the same set of traces? We~show that these
                         problems are undecidable both for general PTA and
                         for the restricted class of L{\slash}U-PTA, even for
                         integer-valued parameters, or over bounded time.
                         On~the other~hand, we~exhibit decidable subclasses:
                         1-clock PTA, and 1-parameter deterministic L-PTA and
                         U-PTA. We~also consider robust versions of these
                         problems, where we additionally require that the
                         language be preserved for all valuations between the
                         reference valuation and the new valuation.},
}
[ALN+10] Natasha Alechina, Brian Logan, Nguyen Hoang Nga, and Abdur 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-ALHNR,
  author =              {Alechina, Natasha and Logan, Brian and Nga, Nguyen
                         Hoang and Rakib, Abdur},
  title =               {Resource-bounded alternating-time temporal logic},
  editor =              {van der Hoek, Wiebe and Kaminka, Gal A. and
                         Lesp{\'e}rance, Yves and Luck, Michael and Sen,
                         Sandeep},
  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 paths in 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 paths in 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}omputation and {C}ontrol
                         ({HSCC}'01)},
  acronym =             {{HSCC}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2034},
  pages =               {49-62},
  year =                {2001},
  month =               mar,
  doi =                 {10.1007/3-540-45351-2_8},
}
[ALP04] Rajeev Alur, Salvatore La Torre, and George J. Pappas. Optimal paths in weighted timed automata. Theoretical Computer Science 318(3):297-322. Elsevier, June 2004. 
@article{tcs318(3)-ALP,
  author =              {Alur, Rajeev and La{~}Torre, Salvatore and Pappas,
                         George J.},
  title =               {Optimal paths in weighted timed automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {318},
  number =              {3},
  pages =               {297-322},
  year =                {2004},
  month =               jun,
  doi =                 {10.1016/j.tcs.2003.10.038},
}
[ALR98] Eric Allender, Michael C. Loui, and Kenneth W. Regan. Complexity Classes. In Mikhail J. Atallah (eds.), Handbook of Algorithms and Theory of Computation. CRC Press, November 1998. 
@incollection{hatc1998-ALRa,
  author =              {Allender, Eric and Loui, Michael C. and Regan,
                         Kenneth W.},
  title =               {Complexity Classes},
  editor =              {Atallah, Mikhail J.},
  booktitle =           {Handbook of Algorithms and Theory of Computation},
  publisher =           {CRC Press},
  pages =               {27.1-27.23},
  year =                {1998},
  month =               nov,
}
[ALR98] Eric Allender, Michael C. Loui, and Kenneth W. Regan. Reducibility and Completeness. In Mikhail J. Atallah (eds.), Handbook of Algorithms and Theory of Computation. CRC Press, November 1998. 
@incollection{hatc1998-ALRb,
  author =              {Allender, Eric and Loui, Michael C. and Regan,
                         Kenneth W.},
  title =               {Reducibility and Completeness},
  editor =              {Atallah, Mikhail J.},
  booktitle =           {Handbook of Algorithms and Theory of Computation},
  publisher =           {CRC Press},
  pages =               {28.1-28.28},
  year =                {1998},
  month =               nov,
}
[ALR98] Eric Allender, Michael C. Loui, and Kenneth W. Regan. Other Complexity Classes and Measures. In Mikhail J. Atallah (eds.), Handbook of Algorithms and Theory of Computation. CRC Press, November 1998. 
@incollection{hatc1998-ALRc,
  author =              {Allender, Eric and Loui, Michael C. and Regan,
                         Kenneth W.},
  title =               {Other Complexity Classes and Measures},
  editor =              {Atallah, Mikhail J.},
  booktitle =           {Handbook of Algorithms and Theory of Computation},
  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, Stanford University, 1991. 
@phdthesis{phd-alur,
  author =              {Alur, Rajeev},
  title =               {Techniques for Automatic Verification of Real-Time
                         Systems},
  year =                {1991},
  school =              {Stanford 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}omputer {A}ided {V}erification
                         ({CAV}'99)},
  acronym =             {{CAV}'99},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1633},
  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ín Abadi, Leslie Lamport, and Pierre Wolper. 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 Wolper,
                         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}rogramming ({ICALP}'89)},
  acronym =             {{ICALP}'89},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {372},
  pages =               {1-17},
  year =                {1989},
  month =               jul,
  doi =                 {10.1007/BFb0035748},
}
[AM99] Eugene Asarin and Oded Maler. As Soon as Possible: Time Optimal Control 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 Maler, Oded},
  title =               {As~Soon as Possible: Time Optimal Control for Timed
                         Automata},
  editor =              {Vaandrager, Frits and van Schuppen, Jan H.},
  booktitle =           {{P}roceedings of the 2nd {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
                         ({HSCC}'99)},
  acronym =             {{HSCC}'99},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1569},
  pages =               {19-30},
  year =                {1999},
  month =               mar,
}
[AM01] Yasmina Abdeddaïm and Oded Maler. Job-Shop Scheduling Using 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 Maler, Oded},
  title =               {Job-Shop Scheduling Using 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}omputer {A}ided {V}erification
                         ({CAV}'01)},
  acronym =             {{CAV}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2102},
  pages =               {478-492},
  year =                {2001},
  month =               jul,
}
[AM02] Yasmina Abdeddaïm and Oded Maler. Preemptive Job-Shop Scheduling using 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 Maler, Oded},
  title =               {Preemptive Job-Shop Scheduling using 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 =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2280},
  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}omputer, {C}ommunication and
                         {S}oftware {S}ystems ({SFM-RT}'04)},
  acronym =             {{SFM-RT}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3185},
  pages =               {1-24},
  year =                {2004},
  month =               sep,
}
[AM15] Étienne André and Nicolas Markey. Language Preservation Problems in 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 some unknown timing delays. In this paper, we address the (untimed) language- and trace-preservation problems: given a reference parameter valuation, does there exist another parameter valuation with the same 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 deterministic L-PTA and U-PTA.

@inproceedings{formats2015-AM,
  author =              {Andr{\'e}, {\'E}tienne and Markey, Nicolas},
  title =               {Language Preservation Problems in Parametric Timed
                         Automata},
  editor =              {Sankaranarayanan, Sriram and Vicario, Enrico},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'15)},
  acronym =             {{FORMATS}'15},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9268},
  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 some unknown timing delays. In this
                         paper, we address the (untimed) language- and
                         trace-preservation problems: given a reference
                         parameter valuation, does there exist another
                         parameter valuation with the same 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 deterministic L-PTA and U-PTA.},
}
[AMM+16] Benjamin Aminof, Vadim Malvone, Aniello Murano, and Sasha Rubin. Graded Strategy Logic: Reasoning about Uniqueness of Nash Equilibria. In AAMAS'16, pages 698-706. International Foundation for Autonomous Agents and Multiagent Systems, May 2016. 
@inproceedings{aamas2016-AMMR,
  author =              {Aminof, Benjamin and Malvone, Vadim and Murano,
                         Aniello and Rubin, Sasha},
  title =               {Graded Strategy Logic: Reasoning about Uniqueness of
                         Nash Equilibria},
  editor =              {Jonker, Catholijn M. and Marsella, Stacy and
                         Thangarajah, John and Tuyls, Karl},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {A}utonomous {A}gents and
                         {M}ultiagent {S}ystems ({AAMAS}'16)},
  acronym =             {{AAMAS}'16},
  publisher =           {International Foundation for Autonomous Agents and
                         Multiagent Systems},
  pages =               {698-706},
  year =                {2016},
  month =               may,
}
[AMM+18] Benjamin Aminof, Vadim Malvone, Aniello Murano, and Sasha Rubin. Graded modalities in Strategy Logic. Information and Computation 261(4):634-649. Elsevier, August 2018. 
@article{icomp261(4)-AMMR,
  author =              {Aminof, Benjamin and Malvone, Vadim and Murano,
                         Aniello and Rubin, Sasha},
  title =               {Graded modalities in Strategy Logic},
  publisher =           {Elsevier},
  journal =             {Information and Computation},
  volume =              {261},
  number =              {4},
  pages =               {634-649},
  year =                {2018},
  month =               aug,
  doi =                 {10.1016/j.ic.2018.02.021},
}
[AMP95] Eugene Asarin, Oded Maler, and Amir Pnueli. Reachability Analysis of Dynamical Systems Having Piecewise-Constant Derivatives. Theoretical Computer Science 138(1):35-65. Elsevier, 1995. 
@article{tcs138(1)-AMP,
  author =              {Asarin, Eugene and Maler, Oded and Pnueli, Amir},
  title =               {Reachability Analysis of Dynamical Systems Having
                         Piecewise-Constant Derivatives},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {138},
  number =              {1},
  pages =               {35-65},
  year =                {1995},
}
[AMP95] Eugene Asarin, Oded Maler, and Amir Pnueli. Symbolic Controller 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 Maler, Oded and Pnueli, Amir},
  title =               {Symbolic Controller 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 =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {999},
  pages =               {1-20},
  year =                {1995},
}
[AMP98] Eugene Asarin, Oded Maler, and Amir Pnueli. On Discretization of Delays in 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 Maler, Oded and Pnueli, Amir},
  title =               {On Discretization of Delays in Timed Automata and
                         Digital Circuits},
  editor =              {Sangiorgi, Davide and de Simone, Robert},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'98)},
  acronym =             {{CONCUR}'98},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1466},
  pages =               {470-484},
  year =                {1998},
  month =               sep,
}
[AMP+20] Gal Amram, Shahar Maoz, Or Pistiner, and Jan Oliver Ringert. Energy μ-Calculus: Symbolic Fixed-Point Algorithms for ω-Regular Energy Games. Technical Report 2005.00641, arXiv, May 2020. 
@techreport{arxiv-AMPR,
  author =              {Amram, Gal and Maoz, Shahar and Pistiner, Or and
                         Ringert, Jan Oliver},
  title =               {Energy {{\(\mu\)}}-Calculus: Symbolic Fixed-Point
                         Algorithms for {{\(\omega\)}}-Regular Energy Games},
  number =              {2005.00641},
  year =                {2020},
  month =               may,
  institution =         {arXiv},
}
[AMP+98] Eugene Asarin, Oded Maler, Amir Pnueli, and Joseph Sifakis. Controller Synthesis for Timed Automata. In SSC'98, pages 469-474. Elsevier, July 1998. 
@inproceedings{sssc1998-AMPS,
  author =              {Asarin, Eugene and Maler, Oded and Pnueli, Amir and
                         Sifakis, Joseph},
  title =               {Controller Synthesis for Timed Automata},
  booktitle =           {{P}roceedings of the 5th {IFAC} {C}conference on
                         {S}ystem {S}tructure and {C}ontrol ({SSC}'98)},
  acronym =             {{SSC}'98},
  publisher =           {Elsevier},
  pages =               {469-474},
  year =                {1998},
  month =               jul,
}
[AMR+05] Karine Altisen, Nicolas Markey, Pierre-Alain Reynier, and Stavros Tripakis. Implémentabilité des automates temporisé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}ctes du 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é Arnold and Maurice Nivat. 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 Nivat, Maurice},
  title =               {The metric space of infinite trees. Algebraic and
                         topological properties},
  publisher =           {IOS Press},
  journal =             {Fundamenta Informaticae},
  volume =              {3},
  number =              {4},
  pages =               {445-476},
  year =                {1980},
}
[AN01] André Arnold and Damian Niwiński. Complete lattices and fixed-point theorems. In Rudiments of μ-calculus, Studies in Logic and the Foundations of Mathematics 146, pages 1-39. North-Holland, 2001. 
@incollection{Rmc2001-ANa,
  author =              {Arnold, Andr{\'e} and Niwi{\'n}ski, Damian},
  title =               {Complete lattices and fixed-point theorems},
  booktitle =           {Rudiments of {\(\mu\)}-calculus},
  publisher =           {North-Holland},
  series =              {Studies in Logic and the Foundations of Mathematics},
  volume =              {146},
  pages =               {1-39},
  chapter =             {1},
  year =                {2001},
}
[And95] Henrik Reif Andersen. Partial Model-Checking (Extended Abstract). In LICS'95, pages 398-407. IEEE Comp. Soc. Press, June 1995. 
@inproceedings{lics1995-And,
  author =              {Andersen, Henrik Reif},
  title =               {Partial Model-Checking (Extended Abstract)},
  booktitle =           {{P}roceedings of the 10th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'95)},
  acronym =             {{LICS}'95},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {398-407},
  year =                {1995},
  month =               jun,
  doi =                 {10.1109/LICS.1995.523274},
}
[And06] Daniel Andersson. An improved algorithm for discounted payoff games. In Proceedings of the 11th ESSLLI Student Session, pages 91-98. August 2006. 
@inproceedings{esslli2006-students-And,
  author =              {Andersson, Daniel},
  title =               {An improved algorithm for discounted payoff games},
  editor =              {Huitink, Janneke and Katrenko, Sophia},
  booktitle =           {{P}roceedings of the 11th {ESSLLI} {S}tudent
                         {S}ession},
  pages =               {91-98},
  year =                {2006},
  month =               aug,
}
[Ang80] Dana Angluin. On Counting Problems and the Polynomial Hierarchy. Theoretical Computer Science 12:161-173. Elsevier, 1980. 
@article{tcs12()-Ang,
  author =              {Angluin, Dana},
  title =               {On Counting Problems and the Polynomial Hierarchy},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {12},
  pages =               {161-173},
  year =                {1980},
}
[Ang87] Dana Angluin. Learning regular sets from queries and counterexamples. Information and Computation 75(2):87-106. Academic Press, November 1987. 
@article{icomp75(2)-Ang,
  author =              {Angluin, Dana},
  title =               {Learning regular sets from queries and
                         counterexamples},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {75},
  number =              {2},
  pages =               {87-106},
  year =                {1987},
  month =               nov,
  doi =                 {10.1016/0890-5401(87)90052-6},
}
[AO96] Eric Allender and Mitsunori Ogihara. Relationships Among PL, #;L, and the Determinant. 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 Among {PL}, {\#L}, and the
                         Determinant},
  publisher =           {EDP Sciences},
  journal =             {RAIRO~-- Theoretical Informatics and Applications},
  volume =              {30},
  number =              {1},
  pages =               {1-21},
  year =                {1996},
}
[AP06] Horacio Arló-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 Logica},
  volume =              {84},
  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 Testing the Truth of Certain Quantified Boolean Formulas. Information Processing Letters 8(3):121-123. Elsevier, 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 Testing the Truth of
                         Certain Quantified Boolean Formulas},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {8},
  number =              {3},
  pages =               {121-123},
  year =                {1979},
  month =               mar,
  note =                {erratum as~\cite{ipl14(4)-APT}},
}
[APT82] Bengt Aspvall, Michael F. Plass, and Robert Endre Tarjan. Erratum (A Linear-Time Algorithm for Testing the Truth of Certain Quantified Boolean Formulas). Information Processing Letters 14(4):195. Elsevier, June 1982. 
@article{ipl14(4)-APT,
  author =              {Aspvall, Bengt and Plass, Michael F. and Tarjan,
                         Robert Endre},
  title =               {Erratum (A Linear-Time Algorithm for Testing the
                         Truth of Certain Quantified Boolean Formulas)},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {14},
  number =              {4},
  pages =               {195},
  year =                {1982},
  month =               jun,
}
[AR14] Benjamin Aminof and Sasha Rubin. First Cycle Games. In SR'14, Electronic Proceedings in 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}easoning ({SR}'14)},
  acronym =             {{SR}'14},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {146},
  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 in Parameterised 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
                         in Parameterised Systems},
  editor =              {Davis, Martin and Fehnker, Ansgar and McIver,
                         Annabelle K. and Voronkov, Andrei},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {C}onference {L}ogic {P}rogramming and {A}utomated
                         {R}easoning ({LPAR}'15)},
  acronym =             {{LPAR}'15},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9450},
  pages =               {313-328},
  year =                {2015},
  month =               nov,
  doi =                 {10.1007/978-3-662-48899-7_22},
}
[AS89] Bowen Alpern and Fred B. Schneider. Verifying Temporal Properties without Temporal Logic. ACM Transactions on Programming Languages and Systems 11(1):147-167. ACM Press, January 1989. 
@article{toplas11(1)-AS,
  author =              {Alpern, Bowen and Schneider, Fred B.},
  title =               {Verifying Temporal Properties without Temporal
                         Logic},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Programming Languages and
                         Systems},
  volume =              {11},
  number =              {1},
  pages =               {147-167},
  year =                {1989},
  month =               jan,
}
[AS02] Eugene Asarin and Gerardo Schneider. Widening 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 =               {Widening the Boundary between Decidable and
                         Undecidable Hybrid Systems},
  editor =              {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v
                         r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era,
                         Anton{\'\i}n},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'02)},
  acronym =             {{CONCUR}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2421},
  pages =               {193-208},
  year =                {2002},
  month =               aug,
}
[AS04] Robert Airapetyan and Thorsten Schneider. Protecting Applications with Petri Nets. The Code Breaker's Journal 1(1). 2004. 
@article{cbj1(1)-AS,
  author =              {Airapetyan, Robert and Schneider, Thorsten},
  title =               {Protecting Applications with {P}etri Nets},
  journal =             {The Code Breaker's Journal},
  volume =              {1},
  number =              {1},
  year =                {2004},
}
[Asp02] James Aspnes. Fast deterministic consensus in a noisy environment. Journal of Algorithms 45(1):16-39. Elsevier, October 2002. 
@article{ja45(1)-Asp,
  author =              {Aspnes, James},
  title =               {Fast deterministic consensus in a noisy environment},
  publisher =           {Elsevier},
  journal =             {Journal of Algorithms},
  volume =              {45},
  number =              {1},
  pages =               {16-39},
  year =                {2002},
  month =               oct,
  doi =                 {10.1016/S0196-6774(02)00220-1},
}
[ASS+00] Adnan Aziz, Kumud Sanwal, Vigyan Singhal, and Robert K. Brayton. Model-checking continous-time Markov chains. ACM Transactions on Computational Logic 1(1):162-170. ACM Press, July 2000. 
@article{tocl1(1)-ASSB,
  author =              {Aziz, Adnan and Sanwal, Kumud and Singhal, Vigyan
                         and Brayton, Robert K.},
  title =               {Model-checking continous-time {M}arkov chains},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {1},
  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}omputation and {C}ontrol
                         ({HSCC}'01)},
  acronym =             {{HSCC}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2034},
  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. Elsevier, 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 =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {379},
  number =              {1-2},
  pages =               {231-265},
  year =                {2007},
  month =               jun,
}
[AT96] Rajeev Alur and Gadi Taubenfeld. Fast Timing-based Algorithms. Distributed Computing 10:1-10. Springer-Verlag, 1996. 
@article{discomp10(1)-AT,
  author =              {Alur, Rajeev and Taubenfeld, Gadi},
  title =               {Fast Timing-based Algorithms},
  publisher =           {Springer-Verlag},
  journal =             {Distributed Computing},
  volume =              {10},
  pages =               {1-10},
  year =                {1996},
}
[AT02] Karine Altisen and Stavros Tripakis. Tools for Controller Synthesis of Timed Systems. In RT-TOOLS'02. August 2002. 
@inproceedings{rttools2002-AT,
  author =              {Altisen, Karine and Tripakis, Stavros},
  title =               {Tools for Controller Synthesis of Timed Systems},
  editor =              {Pettersson, Paul and Yi, Wang},
  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, Wang},
  booktitle =           {{P}roceedings of the 3rd {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'05)},
  acronym =             {{FORMATS}'05},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3829},
  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 News},
  volume =              {48},
  number =              {1},
  pages =               {55-90},
  year =                {2017},
  month =               mar,
  doi =                 {10.1145/3061640.3061652},
}
[Ats02] Albert Atserias. Unsatisfiable Random Formulas are Hard to Certify. In LICS'02, pages 325-334. IEEE Comp. Soc. Press, July 2002. 
@inproceedings{lics2002-Ats,
  author =              {Atserias, Albert},
  title =               {Unsatisfiable Random Formulas are Hard to Certify},
  booktitle =           {{P}roceedings of the 17th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'02)},
  acronym =             {{LICS}'02},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {325-334},
  year =                {2002},
  month =               jul,
}
[AVW03] André Arnold, Aymeric Vincent, and Igor Walukiewicz. Games for Synthesis of Controllers with Partial Observation. Theoretical Computer Science 303(1):7-34. Elsevier, June 2003. 
@article{tcs303(1)-AVW,
  author =              {Arnold, Andr{\'e} and Vincent, Aymeric and
                         Walukiewicz, Igor},
  title =               {Games for Synthesis of Controllers with Partial
                         Observation},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {303},
  number =              {1},
  pages =               {7-34},
  year =                {2003},
  month =               jun,
}
[AZZ+21] Jie An, Bohua Zhan, Naijun Zhan, and Miaomiao Zhang. Learning nondeterministic real-time automata. ACM Transactions on Embedded Computing Systems 20(5s):99:1-99:26. ACM Press, October 2021. 
@article{tecs20(5s)-AZZZ,
  author =              {An, Jie and Zhan, Bohua and Zhan, Naijun and Zhang,
                         Miaomiao},
  title =               {Learning nondeterministic real-time automata},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Embedded Computing Systems},
  volume =              {20},
  number =              {5s},
  pages =               {99:1-99:26},
  year =                {2021},
  month =               oct,
  doi =                 {10.1145/3477030},
}
List of authors