Nicolas Markey

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

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

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

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

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

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

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

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

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

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

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

@book{AB09-CCMA,
  author =              {Arora, Sanjeev and Barak, Boaz},
  title =               {Computational Complexity: A~Modern Approach},
  publisher =           {Cambridge University Press},
  year =                {2009},
}

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

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

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

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

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

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

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

@inproceedings{icalp2013-ABK,
  author =              {Almagor, Shaull and Boker, Udi and Kupferman, Orna},
  title =               {Formalizing and Reasoning about Quality},
  editor =              {Fomin, Fedor V. and Freivalds, Rusins and
                         Kwiatkowska, Marta and Peleg, David},
  booktitle =           {{P}roceedings of the 40th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'13)~-- Part~{II}},
  acronym =             {{ICALP}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7966},
  pages =               {15-27},
  year =                {2013},
  month =               jul,
}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Résumé

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

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

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

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

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

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

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

@phdthesis{phd-alur,
  author =              {Alur, Rajeev},
  title =               {Techniques for Automatic Verification of Real-Time
                         Systems},
  year =                {1991},
  school =              {Stanford University},
}

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

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

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

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

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

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

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

Résumé

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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