H
[Haa12] Christoph Haase. On the Complexity of Model Checking Counter Automata. PhD thesis, University of Oxford, UK, January 2012.
@phdthesis{phd-haase,
  author =              {Haase, Christoph},
  title =               {On the Complexity of Model Checking Counter
                         Automata},
  year =                {2012},
  month =               jan,
  school =              {University of Oxford, UK},
}
[HAB02] William Hesse, Eric Allender, and David A. Mix Barrington. Uniform constant-depth threshold circuits for division and iterated multiplication. Journal of Computer and System Sciences 65(4):695-716. Academic Press, December 2002.
@article{jcss65(4)-HAB,
  author =              {Hesse, William and Allender, Eric and Barrington,
                         David A. Mix},
  title =               {Uniform constant-depth threshold circuits for
                         division and iterated multiplication},
  publisher =           {Academic Press},
  journal =             {Journal of Computer and System Sciences},
  volume =              {65},
  number =              {4},
  pages =               {695-716},
  year =                {2002},
  month =               dec,
}
[Had18] Serge Haddad. Memoryless determinacy of finite parity games: Another simple proof. Information Processing Letters 132:19-21. Elsevier, April 2018.
@article{ipl132()-Had,
  author =              {Haddad, Serge},
  title =               {Memoryless determinacy of finite parity games:
                         Another simple proof},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {132},
  pages =               {19-21},
  year =                {2018},
  month =               apr,
  doi =                 {10.1016/j.ipl.2017.11.012},
}
[Hag11] Matthew Hague. Parameterised Pushdown Systems with Non-Atomic Writes. In FSTTCS'11, Leibniz International Proceedings in Informatics 13, pages 457-468. Leibniz-Zentrum für Informatik, December 2011.
@inproceedings{fsttcs11-Hag,
  author =              {Hague, Matthew},
  title =               {Parameterised Pushdown Systems with Non-Atomic
                         Writes},
  editor =              {Chakraborty, Supratik and Kumar, Amit},
  booktitle =           {{P}roceedings of the 31st {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'11)},
  acronym =             {{FSTTCS}'11},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {13},
  pages =               {457-468},
  year =                {2011},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2011.457},
}
[Hal03] Joseph Y. Halpern. A computer scientist looks at game theory. Games and Economic Behavior 45(1):114-131. October 2003.
@article{geb45(1)-Hal,
  author =              {Halpern, Joseph Y.},
  title =               {A computer scientist looks at game theory},
  journal =             {Games and Economic Behavior},
  volume =              {45},
  number =              {1},
  pages =               {114-131},
  year =                {2003},
  month =               oct,
  doi =                 {10.1016/S0899-8256(02)00529-8},
}
[Hal05] Nicolas Halbwachs. A Synchronous Language at Work: the Story of Lustre. In MEMOCODE'05, pages 3-11. IEEE Comp. Soc. Press, July 2005.
@inproceedings{memocode2005-Hal,
  author =              {Halbwachs, Nicolas},
  title =               {A Synchronous Language at Work: the Story of Lustre},
  booktitle =           {{P}roceedings of the {T}hird {ACM} and {IEEE}
                         {I}nternational {C}onference on {F}ormal {M}ethods
                         and {M}odels for {C}o-{D}esign ({MEMOCODE}'05)},
  acronym =             {{MEMOCODE}'05},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {3-11},
  year =                {2005},
  month =               jul,
  doi =                 {10.1109/MEMCOD.2005.1487884},
}
[Har67] John C. Harsanyi. Games with incomplete information played by "Bayesian" players – (I) The basic model. Management Science 14(3):159-182. November 1967.
@article{ms14(3)-Har,
  author =              {Harsanyi, John C.},
  title =               {Games with incomplete information played by
                         {"}{B}ayesian{"} players~-- (I)~The~basic model},
  journal =             {Management Science},
  volume =              {14},
  number =              {3},
  pages =               {159-182},
  year =                {1967},
  month =               nov,
}
[Har85] David Harel. Recurring Dominoes: Making the Highly Undecidable Highly Understandable. Annals of Discrete Mathematics 24:51-72. North-Holland, 1985.
@article{adm24()-Har,
  author =              {Harel, David},
  title =               {Recurring Dominoes: Making the Highly Undecidable
                         Highly Understandable},
  publisher =           {North-Holland},
  journal =             {Annals of Discrete Mathematics},
  volume =              {24},
  pages =               {51-72},
  year =                {1985},
}
[Har05] Aidan Harding. Symbolic Strategy Synthesis for Games with LTL Winning Conditions. PhD thesis, School of Computer Science, University of Birmingham, UK, March 2005.
@phdthesis{phd-harding,
  author =              {Harding, Aidan},
  title =               {Symbolic Strategy Synthesis for Games with {LTL}
                         Winning Conditions},
  year =                {2005},
  month =               mar,
  school =              {School of Computer Science, University of
                         Birmingham, UK},
}
[HBL+03] Martijn Hendriks, Gerd Behrmann, Kim Guldstrand Larsen, Peter Niebert, and Frits Vaandrager. Adding Symmetry Reduction to Uppaal. In FORMATS'03, Lecture Notes in Computer Science 2791. Springer-Verlag, September 2003.
@inproceedings{formats2003-HBLNV,
  author =              {Hendriks, Martijn and Behrmann, Gerd and Larsen, Kim
                         Guldstrand and Niebert, Peter and Vaandrager, Frits},
  title =               {Adding Symmetry Reduction to {U}ppaal},
  editor =              {Larsen, Kim Guldstrand and Niebert, Peter},
  booktitle =           {{R}evised {P}apers of the 1st {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'03)},
  acronym =             {{FORMATS}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2791},
  year =                {2003},
  month =               sep,
}
[HBM+10] Paul Hunter, Patricia Bouyer, Nicolas Markey, Joël Ouaknine, and James Worrell. Computing Rational Radical Sums in Uniform TC0. In FSTTCS'10, Leibniz International Proceedings in Informatics 8, pages 308-316. Leibniz-Zentrum für Informatik, December 2010.
Abstract

A fundamental problem in numerical computation and computational geometry is to determine the sign of arithmetic expressions in radicals. Here we consider the simpler problem of deciding whether i=1m Ci . AiXi is zero for given rational numbers Ai, CiXi. It has been known for almost twenty years that this can be decided in polynomial time. In this paper we improve this result by showing membership in uniform TC0. This requires several significant departures from Blömer's polynomial-time algorithm as the latter crucially relies on primitives, such as gcd computation and binary search, that are not known to be in TC0.

@inproceedings{fsttcs2010-HBMOW,
  author =              {Hunter, Paul and Bouyer, Patricia and Markey,
                         Nicolas and Ouaknine, Jo{\"e}l and Worrell, James},
  title =               {Computing Rational Radical Sums in Uniform
                         {TC\textsuperscript{0}}},
  editor =              {Lodaya, Kamal and Mahajan, Meena},
  booktitle =           {{P}roceedings of the 30th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'10)},
  acronym =             {{FSTTCS}'10},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {8},
  pages =               {308-316},
  year =                {2010},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2010.308},
  abstract =            {A~fundamental problem in numerical computation and
                         computational geometry is to determine the sign of
                         arithmetic expressions in radicals. Here we consider
                         the simpler problem of deciding whether
                         \(\sum_{i=1}^m C_i \cdot A_i^{X_i}\) is zero for
                         given rational numbers~\(A_i\), \(C_i\),~\(X_i\).
                         It~has been known for almost twenty years that this
                         can be decided in polynomial time. In this paper we
                         improve this result by showing membership in uniform
                         \(\textsf{TC}^0\). This requires several significant
                         departures from Bl{\"o}mer's polynomial-time
                         algorithm as the latter crucially relies on
                         primitives, such as gcd computation and binary
                         search, that are not known to be
                         in~\(\textsf{TC}^0\).},
}
[HCC+00] Vicky Hartonas-Garmhausen, Sérgio Vale Aguiar Campos, Alessandro Cimatti, Edmund M. Clarke, and Fausto Giunchiglia. Verification of a Safety-Critical Railway Interlocking System with Real-Time Constraints. Science of Computer Programming 36(1):53-64. Elsevier, January 2000.
@article{scp36(1)-HCCCG,
  author =              {Hartonas{-}Garmhausen, Vicky and Campos, S{\'e}rgio
                         Vale Aguiar and Cimatti, Alessandro and Clarke,
                         Edmund M. and Giunchiglia, Fausto},
  title =               {Verification of a Safety-Critical Railway
                         Interlocking System with Real-Time Constraints},
  publisher =           {Elsevier},
  journal =             {Science of Computer Programming},
  volume =              {36},
  number =              {1},
  pages =               {53-64},
  year =                {2000},
  month =               jan,
}
[HCK+93] Juris Hartmanis, Richard Chang, Jim Kadin, and Stephen G. Mitchell. Some Observation about Relativization of Space Bounded Computations. In Grzegorz Rozenberg and Arto Salomaa (eds.), Current Trends in Theoretical Computer Science, World Scientific Series in Computer Science 40, pages 423-433. World Scientific, 1993.
@incollection{CTTCS-HCK,
  author =              {Hartmanis, Juris and Chang, Richard and Kadin, Jim
                         and Mitchell, Stephen G.},
  title =               {Some Observation about Relativization of Space
                         Bounded Computations},
  editor =              {Rozenberg, Grzegorz and Salomaa, Arto},
  booktitle =           {Current Trends in Theoretical Computer Science},
  publisher =           {World Scientific},
  series =              {World Scientific Series in Computer Science},
  volume =              {40},
  pages =               {423-433},
  year =                {1993},
}
[Hem98] Harald Hempel. Boolean Hierarchies – On Collapse Properties and Query Order. PhD thesis, Friedrich-Schiller Universität Jena, Germany, 1998.
@phdthesis{phd-hempel,
  author =              {Hempel, Harald},
  title =               {Boolean Hierarchies~-- On~Collapse Properties and
                         Query Order},
  year =                {1998},
  school =              {Friedrich-Schiller Universit{\"a}t Jena, Germany},
}
[Hen61] Leon Henkin. Some Remarks on Infinitely Long Formulas. In Infinitistic Methods – Proceedings of the Symposium on Foundations of Mathematics, pages 167-183. Pergamon Press, 1961.
@inproceedings{sofm1959-Hen,
  author =              {Henkin, Leon},
  title =               {Some Remarks on Infinitely Long Formulas},
  booktitle =           {{I}nfinitistic {M}ethods~-- {P}roceedings of the
                         {S}ymposium on {F}oundations of {M}athematics},
  publisher =           {Pergamon Press},
  pages =               {167-183},
  year =                {1961},
  confyear =            {1959},
  confmonth =           {9},
}
[Hen91] Thomas A. Henzinger. The Temporal Specification and Verification of Real-Time Systems. PhD thesis, Stanford University, 1991.
@phdthesis{phd-henzinger,
  author =              {Henzinger, Thomas A.},
  title =               {The Temporal Specification and Verification of
                         Real-Time Systems},
  year =                {1991},
  school =              {Stanford University},
}
[Hen96] Thomas A. Henzinger. The Theory of Hybrid Automata. In LICS'96, pages 278-292. IEEE Comp. Soc. Press, July 1996.
@inproceedings{lics1996-Hen,
  author =              {Henzinger, Thomas A.},
  title =               {The Theory of Hybrid Automata},
  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 =               {278-292},
  year =                {1996},
  month =               jul,
}
[Hen98] Thomas A. Henzinger. It's About Time: Real-Time Logics Reviewed. In CONCUR'98, Lecture Notes in Computer Science 1466, pages 439-454. Springer-Verlag, September 1998.
@inproceedings{concur1998-Hen,
  author =              {Henzinger, Thomas A.},
  title =               {It's About Time: Real-Time Logics Reviewed},
  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 =               {439-454},
  year =                {1998},
  month =               sep,
}
[Hen05] Thomas A. Henzinger. Games in system design and verification. In TARK'05, pages 1-4. June 2005.
@inproceedings{tark2005-Hen,
  author =              {Henzinger, Thomas A.},
  title =               {Games in system design and verification},
  editor =              {van der Meyden, Ron},
  booktitle =           {{P}roceedings of the 10th {C}onference on
                         {T}heoretical {A}spects of {R}ationality and
                         {K}nowledge ({TARK}'05)},
  acronym =             {{TARK}'05},
  pages =               {1-4},
  year =                {2005},
  month =               jun,
}
[Hen12] Thomas A. Henzinger. Quantitative Reactive Models. In MODELS'12, Lecture Notes in Computer Science 7590, pages 1-2. Springer-Verlag, September 2012.
@inproceedings{models2012-Hen,
  author =              {Henzinger, Thomas A.},
  title =               {Quantitative Reactive Models},
  editor =              {France, Robert B. and Kazmeier, J{\"u}rgen and Breu,
                         Ruth and Atkinson, Colin},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {M}odel {D}riven {E}ngineering
                         {L}anguages and {S}ystems ({MODELS}'12)},
  acronym =             {{MODELS}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7590},
  pages =               {1-2},
  year =                {2012},
  month =               sep,
  doi =                 {10.1007/978-3-642-33666-9_1},
}
[Hen13] Thomas A. Henzinger. Quantitative reactive modeling and verification. Computer Science – Research and Development 28(4):331-344. November 2013.
@article{csrd28(4)-Hen,
  author =              {Henzinger, Thomas A.},
  title =               {Quantitative reactive modeling and verification},
  journal =             {Computer Science~-- Research and Development},
  volume =              {28},
  number =              {4},
  pages =               {331-344},
  year =                {2013},
  month =               nov,
  doi =                 {10.1007/s00450-013-0251-7},
}
[Her98] Philippe Herrmann. Timed Automata and Recognizability. Information Processing Letters 65(6):313-318. Elsevier, March 1998.
@article{ipl65(6)-Her,
  author =              {Herrmann, {\relax Ph}ilippe},
  title =               {Timed Automata and Recognizability},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {65},
  number =              {6},
  pages =               {313-318},
  year =                {1998},
  month =               mar,
}
[Hes03] William Hesse. Dynamic Computational Complexity. PhD thesis, Department of Computer Science, University of Massachusetts at Amherst, USA, September 2003.
@phdthesis{phd-hesse,
  author =              {Hesse, William},
  title =               {Dynamic Computational Complexity},
  year =                {2003},
  month =               sep,
  school =              {Department of Computer Science, University of
                         Massachusetts at Amherst, USA},
}
[HHM99] Thomas A. Henzinger, Benjamin Horowitz, and Rupak Majumdar. Rectangular Hybrid Games. In CONCUR'99, Lecture Notes in Computer Science 1664, pages 320-335. Springer-Verlag, August 1999.
@inproceedings{concur1999-HHM,
  author =              {Henzinger, Thomas A. and Horowitz, Benjamin and
                         Majumdar, Rupak},
  title =               {Rectangular Hybrid Games},
  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 =               {320-335},
  year =                {1999},
  month =               aug,
}
[HvdH+03] Paul Harrenstein, Wiebe van der Hoek, John-Jules Meyer, and Cees Witteveen. A Modal Characterization of Nash Equilibrium. Fundamenta Informaticae 57(2-4):281-321. IOS Press, 2003.
@article{fundi57(2-4)-HHMW,
  author =              {Harrenstein, Paul and van der Hoek, Wiebe and Meyer,
                         John-Jules and Witteveen, Cees},
  title =               {A Modal Characterization of {N}ash Equilibrium},
  publisher =           {IOS Press},
  journal =             {Fundamenta Informaticae},
  volume =              {57},
  number =              {2-4},
  pages =               {281-321},
  year =                {2003},
}
[HHW95] Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi. A User Guide to HyTech. In TACAS'95, Lecture Notes in Computer Science 1019, pages 41-71. Springer-Verlag, May 1995.
@inproceedings{tacas1995-HHW,
  author =              {Henzinger, Thomas A. and Ho, Pei-Hsin and
                         Wong{-}Toi, Howard},
  title =               {A~User Guide to {H}y{T}ech},
  editor =              {Brinksma, Ed and Cleaveland, Rance and Larsen, Kim
                         Guldstrand and Margaria, Tiziana and Steffen,
                         Bernhard},
  booktitle =           {{P}roceedings of the 1st {I}nternational {W}orkshop
                         on {T}ools and {A}lgorithms for {C}onstruction and
                         {A}nalysis of {S}ystems ({TACAS}'95)},
  acronym =             {{TACAS}'95},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1019},
  pages =               {41-71},
  year =                {1995},
  month =               may,
  doi =                 {10.1007/3-540-60630-0_3},
}
[HHW97] Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi. HyTech: A Model-Checker for Hybrid Systems. International Journal on Software Tools for Technology Transfer 1(1-2):110-122. Springer-Verlag, October 1997.
@article{sttt1(1-2)-HHW,
  author =              {Henzinger, Thomas A. and Ho, Pei-Hsin and
                         Wong{-}Toi, Howard},
  title =               {{H}y{T}ech: A~Model-Checker for Hybrid Systems},
  publisher =           {Springer-Verlag},
  journal =             {International Journal on Software Tools for
                         Technology Transfer},
  volume =              {1},
  number =              {1-2},
  pages =               {110-122},
  year =                {1997},
  month =               oct,
}
[HI02] William Hesse and Neil Immerman. Complete Problems for Dynamic Complexity Classes. In LICS'02, pages 313-322. IEEE Comp. Soc. Press, July 2002.
@inproceedings{lics2002-HI,
  author =              {Hesse, William and Immerman, Neil},
  title =               {Complete Problems for Dynamic Complexity Classes},
  booktitle =           {{P}roceedings of the 17th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'02)},
  acronym =             {{LICS}'02},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {313-322},
  year =                {2002},
  month =               jul,
}
[Hig52] Graham Higman. Ordering by Divisibility in Abstract Algebras. Proceedings of the London Mathematical Society s3-2(1):326-336. 1952.
@article{plms-s3-2(1)-Hig,
  author =              {Higman, Graham},
  title =               {Ordering by Divisibility in Abstract Algebras},
  journal =             {Proceedings of the London Mathematical Society},
  volume =              {s3-2},
  number =              {1},
  pages =               {326-336},
  year =                {1952},
}
[HIM12] Thomas Dueholm Hansen, Rasmus Ibsen-Jensen, and Peter Bro Miltersen. A Faster Algorithm for Solving One-Clock Priced Timed Games. Research Report 1201.3498, arXiv, January 2012.
@techreport{arxiv12-HIM,
  author =              {Hansen, Thomas Dueholm and Ibsen{-}Jensen, Rasmus
                         and Miltersen, Peter Bro},
  title =               {A~Faster Algorithm for Solving One-Clock Priced
                         Timed Games},
  number =              {1201.3498},
  year =                {2012},
  month =               jan,
  institution =         {arXiv},
  type =                {Research Report},
}
[HIM13] Thomas Dueholm Hansen, Rasmus Ibsen-Jensen, and Peter Bro Miltersen. A Faster Algorithm for Solving One-Clock Priced Timed Games. In CONCUR'13, Lecture Notes in Computer Science 8052, pages 531-545. Springer-Verlag, August 2013.
@inproceedings{concur2013-HIM,
  author =              {Hansen, Thomas Dueholm and Ibsen{-}Jensen, Rasmus
                         and Miltersen, Peter Bro},
  title =               {A~Faster Algorithm for Solving One-Clock Priced
                         Timed Games},
  editor =              {D{'}Argenio, Pedro R. and Melgratt, Hern{\'a}n C.},
  booktitle =           {{P}roceedings of the 24th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'13)},
  acronym =             {{CONCUR}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8052},
  pages =               {531-545},
  year =                {2013},
  month =               aug,
}
[HJ96] Dang Van Hung and Wang Ji. On the Design of Hybrid Control Systems Using Automata Models. In FSTTCS'96, Lecture Notes in Computer Science 1180, pages 156-176. Springer-Verlag, December 1996.
@inproceedings{fsttcs1996-HJ,
  author =              {Hung, Dang Van and Ji, Wang},
  title =               {On the Design of Hybrid Control Systems Using
                         Automata Models},
  editor =              {Chandru, Vijay and Vinay, V.},
  booktitle =           {{P}roceedings of the 16th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'96)},
  acronym =             {{FSTTCS}'96},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1180},
  pages =               {156-176},
  year =                {1996},
  month =               dec,
}
[HJ04] Gerard J. Holzmann and Rajeev Joshi. Model-Driven Software Verification. In SPIN'04, Lecture Notes in Computer Science 2989, pages 76-91. Springer-Verlag, April 2004.
@inproceedings{spin2004-HJ,
  author =              {Holzmann, Gerard J. and Joshi, Rajeev},
  title =               {Model-Driven Software Verification},
  editor =              {Graf, Susanne and Mounier, Laurent},
  booktitle =           {{P}roceedings of the 11th {I}nternational {SPIN}
                         {W}orkshop ({SPIN}'04)},
  acronym =             {{SPIN}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2989},
  pages =               {76-91},
  year =                {2004},
  month =               apr,
  doi =                 {10.1007/978-3-540-24732-6_6},
}
[HJM03] Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Counterexample-Guided Control. In ICALP'03, Lecture Notes in Computer Science 2719, pages 886-902. Springer-Verlag, June 2003.
@inproceedings{icalp2003-HJM,
  author =              {Henzinger, Thomas A. and Jhala, Ranjit and Majumdar,
                         Rupak},
  title =               {Counterexample-Guided Control},
  editor =              {Baeten, Jos C. M. and Lenstra, Jan Karel and Parrow,
                         Joachim and Woeginger, Gerhard J.},
  booktitle =           {{P}roceedings of the 30th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'03)},
  acronym =             {{ICALP}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2719},
  pages =               {886-902},
  year =                {2003},
  month =               jun,
}
[HJM18] Léo Henry, Thierry Jéron, and Nicolas Markey. Control strategies for off-line testing of timed systems. In SPIN'18, Lecture Notes in Computer Science 10869, pages 171-189. Springer-Verlag, June 2018.
Abstract

Partial observability and controllability are two well-known issues in test-case synthesis for interactive systems. We address the problem of partial control in the synthesis of test cases from timed-automata specifications. Building on the tioco timed testing framework, we extend a previous game interpretation of the test-synthesis problem from the untimed to the timed setting. This extension requires a deep reworking of the models, game interpretation and test-synthesis algorithms. We exhibit strategies of a game that tries to minimize both control losses and distance to the satisfaction of a test purpose, and prove they are winning under some fairness assumptions. This entails that when turning those strategies into test cases, we get properties such as soundness and exhaustiveness of the test synthesis method.

@inproceedings{spin2018-HJM,
  author =              {Henry, L{\'e}o and J{\'e}ron, Thierry and Markey,
                         Nicolas},
  title =               {Control strategies for off-line testing of timed
                         systems},
  editor =              {Gallardo, Mar{\'\i}a-del-Mar and Merino, Pedro},
  booktitle =           {{P}roceedings of the 25th {I}nternational
                         {S}ymposium on {M}odel-{C}herking {S}oftware
                         ({SPIN}'18)},
  acronym =             {{SPIN}'18},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {10869},
  pages =               {171-189},
  year =                {2018},
  month =               jun,
  doi =                 {10.1007/978-3-319-94111-0_10},
  abstract =            {Partial observability and controllability are two
                         well-known issues in test-case synthesis for
                         interactive systems. We~address the problem of
                         partial control in the synthesis of test cases from
                         timed-automata specifications. Building on the tioco
                         timed testing framework, we~extend a previous game
                         interpretation of the test-synthesis problem from
                         the untimed to the timed setting. This extension
                         requires a deep reworking of the models, game
                         interpretation and test-synthesis algorithms.
                         We~exhibit strategies of a game that tries to
                         minimize both control losses and distance to the
                         satisfaction of a test purpose, and prove they are
                         winning under some fairness assumptions. This
                         entails that when turning those strategies into test
                         cases, we get properties such as soundness and
                         exhaustiveness of the test synthesis method.},
}
[HJM+04] Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Kenneth L. McMillan. Abstractions from Proofs. In POPL'04, pages 232-244. ACM Press, January 2004.
@inproceedings{popl2004-HJMM,
  author =              {Henzinger, Thomas A. and Jhala, Ranjit and Majumdar,
                         Rupak and McMillan, Kenneth L.},
  title =               {Abstractions from Proofs},
  editor =              {Jones, Neil D. and Leroy, Xavier},
  booktitle =           {Conference Record of the 31st {ACM}
                         {SIGPLAN}-{SIGACT} {S}ymposium on {P}rinciples of
                         {P}rogramming {L}anguages ({POPL}'04)},
  acronym =             {{POPL}'04},
  publisher =           {ACM Press},
  pages =               {232-244},
  year =                {2004},
  month =               jan,
}
[HJR02] Alan J. Hoffman, Kate Jenkins, and Tim Roughgarden. On a game in directed graphs. Information Processing Letters 83(1):13-16. Elsevier, July 2002.
@article{ipl83(1)-HJR,
  author =              {Hoffman, Alan J. and Jenkins, Kate and Roughgarden,
                         Tim},
  title =               {On a game in directed graphs},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {83},
  number =              {1},
  pages =               {13-16},
  year =                {2002},
  month =               jul,
}
[vdH+05] Wiebe van der Hoek, Wojciech Jamroga, and Michael Wooldridge. A Logic for Strategic Reasoning. In AAMAS'05, pages 157-164. ACM Press, July 2005.
@inproceedings{aamas2005-HJW,
  author =              {van der Hoek, Wiebe and Jamroga, Wojciech and
                         Wooldridge, Michael},
  title =               {A Logic for Strategic Reasoning},
  editor =              {Dignum, Franck and Dignum, Virginia and Koenig, Sven
                         and Kraus, Sarit and Singh, Munindar P. and
                         Wooldridge, Michael},
  booktitle =           {{P}roceedings of the 4th {I}nternational {J}oint
                         {C}onference on {A}utonomous {A}gents and
                         {M}ultiagent {S}ystems ({AAMAS}'05)},
  acronym =             {{AAMAS}'05},
  publisher =           {ACM Press},
  pages =               {157-164},
  year =                {2005},
  month =               jul,
}
[HK94] Joseph Y. Halpern and Bruce M. Kapron. Zero-one laws for modal logic. Annals of Pure and Applied Logic 69(2-3):157-193. Elsevier, October 1994.
@article{apal69(2-3)-HK,
  author =              {Halpern, Joseph Y. and Kapron, Bruce M.},
  title =               {Zero-one laws for modal logic},
  publisher =           {Elsevier},
  journal =             {Annals of Pure and Applied Logic},
  volume =              {69},
  number =              {2-3},
  pages =               {157-193},
  year =                {1994},
  month =               oct,
}
[HK97] Thomas A. Henzinger and Orna Kupferman. From Quantity to Quality. In HART'97, Lecture Notes in Computer Science 1201, pages 48-62. Springer-Verlag, March 1997.
@inproceedings{hart1997-HK,
  author =              {Henzinger, Thomas A. and Kupferman, Orna},
  title =               {From Quantity to Quality},
  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 =               {48-62},
  year =                {1997},
  month =               mar,
}
[HK99] Thomas A. Henzinger and Peter W. Kopke. Discrete-Time Control for Rectangular Hybrid Systems. Theoretical Computer Science 221(1-2):369-392. Elsevier, June 1999.
@article{tcs221(1-2)-HK,
  author =              {Henzinger, Thomas A. and Kopke, Peter W.},
  title =               {Discrete-Time Control for Rectangular Hybrid
                         Systems},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {221},
  number =              {1-2},
  pages =               {369-392},
  year =                {1999},
  month =               jun,
}
[HK16] Loïc Hélouët and Karim Kecir. Realizability of Schedules by Stochastic Time Petri Nets with Blocking Semantics. In PETRI NETS'16, Lecture Notes in Computer Science 9698, pages 155-175. Springer-Verlag, June 2016.
@inproceedings{pn2016-HK,
  author =              {H{\'e}lou{\"e}t, Lo{\"\i}c and Kecir, Karim},
  title =               {Realizability of Schedules by Stochastic Time
                         {P}etri Nets with Blocking Semantics},
  editor =              {Kordon, Fabrice and Moldt, Daniel},
  booktitle =           {{P}roceedings of the 37th {I}nternational
                         {C}onference on {A}pplications and {T}heory of
                         {P}etri Nets and {C}oncurrency ({PETRI NETS}'16)},
  acronym =             {{PETRI~NETS}'16},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9698},
  pages =               {155-175},
  year =                {2016},
  month =               jun,
  doi =                 {10.1007/978-3-319-39086-4_11},
}
[HKM03] Thomas A. Henzinger, Orna Kupferman, and Rupak Majumdar. On the Universal and Existential Fragments of the μ-Calculus. In TACAS'03, Lecture Notes in Computer Science 2619, pages 49-64. Springer-Verlag, April 2003.
@inproceedings{tacas2003-HKM,
  author =              {Henzinger, Thomas A. and Kupferman, Orna and
                         Majumdar, Rupak},
  title =               {On the Universal and Existential Fragments of the
                         {\(\mu\)}-Calculus},
  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 =               {49-64},
  year =                {2003},
  month =               apr,
}
[HKN+06] Andrew Hinton, Marta Kwiatkowska, Gethin Norman, and David Parker. PRISM: A Tool for Automatic Verification of Probabilistic Systems. In TACAS'06, Lecture Notes in Computer Science 3920, pages 441-444. Springer-Verlag, March 2006.
@inproceedings{tacas2006-HKNP,
  author =              {Hinton, Andrew and Kwiatkowska, Marta and Norman,
                         Gethin and Parker, David},
  title =               {{PRISM}: A~Tool for Automatic Verification of
                         Probabilistic Systems},
  editor =              {Hermanns, Holger and Palsberg, Jens},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'06)},
  acronym =             {{TACAS}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3920},
  pages =               {441-444},
  year =                {2006},
  month =               mar,
}
[HKO+09] Christoph Haase, Stephan Kreutzer, Joël Ouaknine, and James Worrell. Reachability in Succinct and Parametric One-Counter Automata. In CONCUR'09, Lecture Notes in Computer Science 5710, pages 369-383. Springer-Verlag, September 2009.
@inproceedings{concur2009-HKOW,
  author =              {Haase, Christoph and Kreutzer, Stephan and Ouaknine,
                         Jo{\"e}l and Worrell, James},
  title =               {Reachability in Succinct and Parametric One-Counter
                         Automata},
  editor =              {Bravetti, Mario and Zavattaro, Gianluigi},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'09)},
  acronym =             {{CONCUR}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5710},
  pages =               {369-383},
  year =                {2009},
  month =               sep,
  doi =                 {10.1007/978-3-642-04081-8_25},
}
[HKP82] David Harel, Dexter C. Kozen, and Rohit Parikh. Process Logic: Expressiveness, Decidability and Completeness. Journal of Computer and System Sciences 25(2):144-170. Academic Press, October 1982.
@article{jcss25(2)-HKP,
  author =              {Harel, David and Kozen, Dexter C. and Parikh, Rohit},
  title =               {Process Logic: Expressiveness, Decidability and
                         Completeness},
  publisher =           {Academic Press},
  journal =             {Journal of Computer and System Sciences},
  volume =              {25},
  number =              {2},
  pages =               {144-170},
  year =                {1982},
  month =               oct,
}
[HKP+95] Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya. What is decidable about Hybrid Automata?. In STOC'95, pages 373-382. ACM Press, May 1995.
@inproceedings{stoc1995-HKPV,
  author =              {Henzinger, Thomas A. and Kopke, Peter W. and Puri,
                         Anuj and Varaiya, Pravin},
  title =               {What is decidable about Hybrid Automata?},
  booktitle =           {{P}roceedings of the 27th {A}nnual {ACM} {S}ymposium
                         on the {T}heory of {C}omputing ({STOC}'95)},
  acronym =             {{STOC}'95},
  publisher =           {ACM Press},
  pages =               {373-382},
  year =                {1995},
  month =               may,
}
[HKP+98] Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya. What is decidable about Hybrid Automata?. Journal of Computer and System Sciences 57(1):94-124. Academic Press, August 1998.
@article{jcss57(1)-HKPV,
  author =              {Henzinger, Thomas A. and Kopke, Peter W. and Puri,
                         Anuj and Varaiya, Pravin},
  title =               {What is decidable about Hybrid Automata?},
  publisher =           {Academic Press},
  journal =             {Journal of Computer and System Sciences},
  volume =              {57},
  number =              {1},
  pages =               {94-124},
  year =                {1998},
  month =               aug,
}
[HKS+11] Frédéric Herbreteau, Dileep Kini, B. Srivathsan, and Igor Walukiewicz. Using non-convex approximations for efficient analysis of timed automata. In FSTTCS'11, Leibniz International Proceedings in Informatics 13, pages 78-89. Leibniz-Zentrum für Informatik, December 2011.
@inproceedings{fsttcs2011-HKSW,
  author =              {Herbreteau, Fr{\'e}d{\'e}ric and Kini, Dileep and
                         Srivathsan, B. and Walukiewicz, Igor},
  title =               {Using non-convex approximations for efficient
                         analysis of timed automata},
  editor =              {Chakraborty, Supratik and Kumar, Amit},
  booktitle =           {{P}roceedings of the 31st {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'11)},
  acronym =             {{FSTTCS}'11},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {13},
  pages =               {78-89},
  year =                {2011},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2011.78},
}
[HKT10] Michael Holtmann, łukasz Kaiser, and Wolfgang Thomas. Degrees of Lookahead in Regular Infinite Games. In FoSSaCS'10, Lecture Notes in Computer Science 6014, pages 252-266. Springer-Verlag, March 2010.
@inproceedings{fossacs2010-HKT,
  author =              {Holtmann, Michael and Kaiser, {\L}ukasz and Thomas,
                         Wolfgang},
  title =               {Degrees of Lookahead in Regular Infinite Games},
  editor =              {Ong, Luke},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'10)},
  acronym =             {{FoSSaCS}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6014},
  pages =               {252-266},
  year =                {2010},
  month =               mar,
}
[HKV96] Thomas A. Henzinger, Orna Kupferman, and Moshe Y. Vardi. A Space-Efficient On-the-fly Algorithm for Real-Time Model Checking. In CONCUR'96, Lecture Notes in Computer Science 1119, pages 514-529. Springer-Verlag, August 1996.
@inproceedings{concur1996-HKV,
  author =              {Henzinger, Thomas A. and Kupferman, Orna and Vardi,
                         Moshe Y.},
  title =               {A Space-Efficient On-the-fly Algorithm for Real-Time
                         Model Checking},
  editor =              {Montanari, Ugo and Sassone, Vladimiro},
  booktitle =           {{P}roceedings of the 7th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'96)},
  acronym =             {{CONCUR}'96},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1119},
  pages =               {514-529},
  year =                {1996},
  month =               aug,
}
[HKW95] Thomas A. Henzinger, Peter W. Kopke, and Howard Wong-Toi. The expressive power of clocks. In ICALP'95, Lecture Notes in Computer Science 944, pages 417-428. Springer-Verlag, July 1995.
@inproceedings{icalp1995-HKW,
  author =              {Henzinger, Thomas A. and Kopke, Peter W. and
                         Wong{-}Toi, Howard},
  title =               {The expressive power of clocks},
  editor =              {F{\"u}l{\"o}p, Zolt{\'a}n and Gecseg, Ferenc},
  booktitle =           {{P}roceedings of the 22nd {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'95)},
  acronym =             {{ICALP}'95},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {944},
  pages =               {417-428},
  year =                {1995},
  month =               jul,
}
[HL89] Hans Hüttel and Kim Guldstrand Larsen. The Use of Static Constructs in a Modal Process Logic. In Logic at Botik 89 – Proceedings of the Symposium on Logical Foundations of Computer Science, Lecture Notes in Computer Science 363, pages 163-180. Springer-Verlag, July 1989.
@inproceedings{botik89-HL,
  author =              {H{\"u}ttel, Hans and Larsen, Kim Guldstrand},
  title =               {The Use of Static Constructs in a Modal Process
                         Logic},
  editor =              {Meyer, Albert R. and Taitslin, Michael A.},
  booktitle =           {{L}ogic at {B}otik~89 -- {P}roceedings of the
                         {S}ymposium on {L}ogical {F}oundations of {C}omputer
                         {S}cience},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {363},
  pages =               {163-180},
  year =                {1989},
  month =               jul,
}
[HL02] Martijn Hendriks and Kim Guldstrand Larsen. Exact Acceleration of real-Time Model Checking. In TPTS'02, Electronic Notes in Theoretical Computer Science 65(6). Elsevier, April 2002.
@inproceedings{tpts2002-HL,
  author =              {Hendriks, Martijn and Larsen, Kim Guldstrand},
  title =               {Exact Acceleration of real-Time Model Checking},
  editor =              {Asarin, Eugene and Maler, Oded and Yovine, Sergio},
  booktitle =           {{P}roceedings of the 1st {W}orkshop on {T}heory and
                         {P}ractice of {T}imed {S}ystems ({TPTS}'02)},
  acronym =             {{TPTS}'02},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {65},
  number =              {6},
  year =                {2002},
  month =               apr,
}
[HLL+14] Henri Hansen, Shang-Wei Lin, Yang Liu, Truong Khanh Nguyen, and Jun Sun. Diamonds Are a Girl's Best Friend: Partial Order Reduction for Timed Automata with Abstractions. In CAV'14, Lecture Notes in Computer Science 8559, pages 391-406. Springer-Verlag, July 2014.
@inproceedings{cav2014-HLLNS,
  author =              {Hansen, Henri and Lin, Shang{-}Wei and Liu, Yang and
                         Nguyen, Truong Khanh and Sun, Jun},
  title =               {Diamonds Are a Girl's Best Friend: Partial Order
                         Reduction for Timed Automata with Abstractions},
  editor =              {Biere, Armin and Bloem, Roderick},
  booktitle =           {{P}roceedings of the 26th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'14)},
  acronym =             {{CAV}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8559},
  pages =               {391-406},
  year =                {2014},
  month =               jul,
  doi =                 {10.1007/978-3-319-08867-9_26},
}
[HLM+04] Thomas Hérault, Richard Lassaigne, Frédéric Magniette, and Sylvain Peyronnet. Approximate Probabilistic Model Checking. In VMCAI'04, Lecture Notes in Computer Science 2937, pages 73-84. Springer-Verlag, January 2004.
@inproceedings{vmcai2004-HLMP,
  author =              {H{\'e}rault, {\relax Th}omas and Lassaigne, Richard
                         and Magniette, Fr{\'e}d{\'e}ric and Peyronnet,
                         Sylvain},
  title =               {Approximate Probabilistic Model Checking},
  editor =              {Steffen, Bernhard and Levi, Giorgio},
  booktitle =           {{P}roceedings of the 5th {I}nternational {W}orkshop
                         on {V}erification, {M}odel {C}hecking, and
                         {A}bstract {I}nterpretation ({VMCAI}'04)},
  acronym =             {{VMCAI}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2937},
  pages =               {73-84},
  year =                {2004},
  month =               jan,
}
[HLR+10] Holger Hermanns, Kim Guldstrand Larsen, Jean-François Raskin, and Jan Tretmans. Quantitative system validation in model driven design. In EMSOFT'10, pages 301-302. ACM Press, October 2010.
@inproceedings{emsoft2010-HLRT,
  author =              {Hermanns, Holger and Larsen, Kim Guldstrand and
                         Raskin, Jean-Fran{\c c}ois and Tretmans, Jan},
  title =               {Quantitative system validation in model driven
                         design},
  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 =               {301-302},
  year =                {2010},
  month =               oct,
}
[vdH+06] Wiebe van der Hoek, Alessio Lomuscio, and Michael Wooldridge. On the Complexity of Practical ATL Model Checking. In AAMAS'06, pages 201-208. ACM Press, May 2006.
@inproceedings{aamas2006-HLW,
  author =              {van der Hoek, Wiebe and Lomuscio, Alessio and
                         Wooldridge, Michael},
  title =               {On the Complexity of Practical {ATL} Model Checking},
  editor =              {Nakashima, Hideyuki and Wellman, Michael P. and
                         Weiss, Gerhard and Stone, Peter},
  booktitle =           {{P}roceedings of the 5th {I}nternational {J}oint
                         {C}onference on {A}utonomous {A}gents and
                         {M}ultiagent {S}ystems ({AAMAS}'06)},
  acronym =             {{AAMAS}'06},
  publisher =           {ACM Press},
  pages =               {201-208},
  year =                {2006},
  month =               may,
}
[HLW13] Andreas Herzig, Emiliano Lorini, and Dirk Walther. Reasoning about Actions Meets Strategic Logics. In LORI'13, Lecture Notes in Computer Science 8196, pages 162-175. Springer-Verlag, October 2013.
@inproceedings{lori2013-HLW,
  author =              {Herzig, Andreas and Lorini, Emiliano and Walther,
                         Dirk},
  title =               {Reasoning about Actions Meets Strategic Logics},
  editor =              {Grossi, Davide and Roy, Olivier and Huang, Huaxin},
  booktitle =           {{P}roceedings of the 4th {W}orkshop on {L}ogic,
                         {R}ationality, and {I}nteraction ({LORI}'13)},
  acronym =             {{LORI}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8196},
  pages =               {162-175},
  year =                {2013},
  month =               oct,
  doi =                 {10.1007/978-3-642-40948-6_13},
}
[HM85] Matthew C. B. Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32(1). ACM Press, January 1985.
@article{jacm32(1)-HM,
  author =              {Hennessy, Matthew C. B. and Milner, Robin},
  title =               {Algebraic laws for nondeterminism and concurrency},
  publisher =           {ACM Press},
  journal =             {Journal of the ACM},
  volume =              {32},
  number =              {1},
  year =                {1985},
  month =               jan,
}
[HM03] Markus Holzer and Pierre McKenzie. Alternating and Empty Alternating Auxiliary Stack Automata. Theoretical Computer Science 299(1-3):307-326. Elsevier, April 2003.
@article{tcs299(1-3)-HM,
  author =              {Holzer, Markus and McKenzie, Pierre},
  title =               {Alternating and Empty Alternating Auxiliary Stack
                         Automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {299},
  number =              {1-3},
  pages =               {307-326},
  year =                {2003},
  month =               apr,
}
[HMB07] Michael R. Hansen, Jan Madsen, and Aske Wiid Brekling. Semantics and Verification of a Language for Modelling Hardware Architectures. In Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bjørner and Chaochen Zhou on the Occasion of Their 70th Birthdays, Lecture Notes in Computer Science 4700, pages 300-319. Springer-Verlag, September 2007.
@inproceedings{BZbday07-HMB,
  author =              {Hansen, Michael R. and Madsen, Jan and Brekling,
                         Aske Wiid},
  title =               {Semantics and Verification of a Language for
                         Modelling Hardware Architectures},
  editor =              {Jones, Cliff B. and Liu, Zhiming and Woodcock, Jim},
  booktitle =           {Formal Methods and Hybrid Real-Time Systems, Essays
                         in Honor of Dines~Bj{\o}rner and Chaochen~Zhou on
                         the Occasion of Their 70th Birthdays},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4700},
  pages =               {300-319},
  year =                {2007},
  month =               sep,
  doi =                 {10.1007/978-3-540-75221-9_13},
}
[HMM18] Loïc Hélouët, Hervé Marchand, and John Mullins. Concurrent secrets with quantified suspicion. In ACSD'18. IEEE Comp. Soc. Press, June 2018.
@inproceedings{acsd2018-HMM,
  author =              {H{\'e}lou{\"e}t, Lo{\"\i}c and Marchand, Herv{\'e}
                         and Mullins, John},
  title =               {Concurrent secrets with quantified suspicion},
  editor =              {Chatain, {\relax Th}omas and Grosu, Radu and
                         Juh{\'a}s, Gabriel},
  booktitle =           {{P}roceedings of the 18th {I}nternational
                         {C}onference on {A}pplication of {C}oncurrency to
                         {S}ystem {D}esign ({ACSD}'18)},
  acronym =             {{ACSD}'18},
  publisher =           {IEEE Comp. Soc. Press},
  year =                {2018},
  month =               jun,
}
[HMP92] Thomas A. Henzinger, Zohar Manna, and Amir Pnueli. What Good are Digital Clocks?. In ICALP'92, Lecture Notes in Computer Science 623, pages 545-558. Springer-Verlag, July 1992.
@inproceedings{icalp1992-HMP,
  author =              {Henzinger, Thomas A. and Manna, Zohar and Pnueli,
                         Amir},
  title =               {What Good are Digital Clocks?},
  editor =              {Kuich, Werner},
  booktitle =           {{P}roceedings of the 19th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'92)},
  acronym =             {{ICALP}'92},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {623},
  pages =               {545-558},
  year =                {1992},
  month =               jul,
}
[HMP92] Thomas A. Henzinger, Zohar Manna, and Amir Pnueli. Timed Transition Systems. In REX'91, Lecture Notes in Computer Science 600, pages 226-251. Springer-Verlag, 1992.
@inproceedings{rex1991-HMP,
  author =              {Henzinger, Thomas A. and Manna, Zohar and Pnueli,
                         Amir},
  title =               {Timed Transition Systems},
  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 =               {226-251},
  year =                {1992},
  confyear =            {1991},
  confmonth =           {6},
}
[HMP93] Thomas A. Henzinger, Zohar Manna, and Amir Pnueli. Towards Refining Temporal Specifications into Hybrid Systems. In HSCC'92, Lecture Notes in Computer Science 736, pages 60-76. Springer-Verlag, 1993.
@inproceedings{hscc1992-HMP,
  author =              {Henzinger, Thomas A. and Manna, Zohar and Pnueli,
                         Amir},
  title =               {Towards Refining Temporal Specifications into 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 =               {60-76},
  year =                {1993},
}
[HMP94] Thomas A. Henzinger, Zohar Manna, and Amir Pnueli. Temporal Proof Methodologies for Timed Transition Systems. Information and Computation 112(2):273-337. Academic Press, August 1994.
@article{icomp112(2)-HMP,
  author =              {Henzinger, Thomas A. and Manna, Zohar and Pnueli,
                         Amir},
  title =               {Temporal Proof Methodologies for Timed Transition
                         Systems},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {112},
  number =              {2},
  pages =               {273-337},
  year =                {1994},
  month =               aug,
}
[HMP05] Thomas A. Henzinger, Rupak Majumdar, and Vinayak S. Prabhu. Quantifying Similarities Between Timed Systems. In FORMATS'05, Lecture Notes in Computer Science 3829, pages 226-241. Springer-Verlag, September 2005.
@inproceedings{formats2005-HMP,
  author =              {Henzinger, Thomas A. and Majumdar, Rupak and Prabhu,
                         Vinayak S.},
  title =               {Quantifying Similarities Between Timed Systems},
  editor =              {Pettersson, Paul and Yi, Wang},
  booktitle =           {{P}roceedings of the 3rd {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'05)},
  acronym =             {{FORMATS}'05},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3829},
  pages =               {226-241},
  year =                {2005},
  month =               sep,
}
[HNS+94] Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. Symbolic Model Checking for Real Time Systems. Information and Computation 111(2):193-244. Academic Press, June 1994.
@article{icomp111(2)-HNSY,
  author =              {Henzinger, Thomas A. and Nicollin, Xavier and
                         Sifakis, Joseph and Yovine, Sergio},
  title =               {Symbolic Model Checking for Real Time Systems},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {111},
  number =              {2},
  pages =               {193-244},
  year =                {1994},
  month =               jun,
}
[HvdN+06] Martijn Hendriks, Barend van den Nieuwelaar, and Frits Vaandrager. Model checker aided design of a controller for a wafer scanner. International Journal on Software Tools for Technology Transfer 8(6):633-647. Springer-Verlag, November 2006.
@article{sttt8(6)-HVN,
  author =              {Hendriks, Martijn and van den Nieuwelaar, Barend and
                         Vaandrager, Frits},
  title =               {Model checker aided design of a controller for a
                         wafer scanner},
  publisher =           {Springer-Verlag},
  journal =             {International Journal on Software Tools for
                         Technology Transfer},
  volume =              {8},
  number =              {6},
  pages =               {633-647},
  year =                {2006},
  month =               nov,
}
[HO13] Thomas A. Henzinger and Jan Otop. From Model Checking to Model Measuring. In CONCUR'13, Lecture Notes in Computer Science 8052, pages 273-287. Springer-Verlag, August 2013.
@inproceedings{concur2013-HO,
  author =              {Henzinger, Thomas A. and Otop, Jan},
  title =               {From Model Checking to Model Measuring},
  editor =              {D{'}Argenio, Pedro R. and Melgratt, Hern{\'a}n C.},
  booktitle =           {{P}roceedings of the 24th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'13)},
  acronym =             {{CONCUR}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8052},
  pages =               {273-287},
  year =                {2013},
  month =               aug,
  doi =                 {10.1007/978-3-642-40184-8_20},
}
[Hoa69] Charles Antony Richard Hoare. An axiomatic basis for computer programming. Communications of the ACM 12(10):576-580. ACM Press, October 1969.
@article{cacm12(10)-Hoa,
  author =              {Hoare, Charles Antony Richard},
  title =               {An axiomatic basis for computer programming},
  publisher =           {ACM Press},
  journal =             {Communications of the ACM},
  volume =              {12},
  number =              {10},
  pages =               {576-580},
  year =                {1969},
  month =               oct,
  doi =                 {10.1145/363235.363259},
}
[Hoa80] Charles Antony Richard Hoare. A Model for Communicating Sequential Processes. In R. M. McKeag and A. M. MacNaghten (eds.), On the Construction of Programs – An advanced course. Cambridge University Press, 1980.
@incollection{CPAC-CSP-Hoare,
  author =              {Hoare, Charles Antony Richard},
  title =               {A Model for Communicating Sequential Processes},
  editor =              {McKeag, R. M. and MacNaghten, A. M.},
  booktitle =           {On the Construction of Programs~-- An advanced
                         course},
  publisher =           {Cambridge University Press},
  pages =               {229-254},
  year =                {1980},
}
[Hol97] Gerard J. Holzmann. The Model Checker SPIN. IEEE Transactions on Software Engineering 23(5):279-295. IEEE Comp. Soc. Press, May 1997.
@article{tse23(5)-Hol,
  author =              {Holzmann, Gerard J.},
  title =               {The Model Checker {SPIN}},
  publisher =           {IEEE Comp. Soc. Press},
  journal =             {IEEE Transactions on Software Engineering},
  volume =              {23},
  number =              {5},
  pages =               {279-295},
  year =                {1997},
  month =               may,
}
[Hor45] Robert E. Horton. Erosional development of streams and their drainage basins; hydrophysical approach to quantitative morphology. Geological Society of America Bulletin 56(3):275-370. Geological Society of America, March 1945.
@article{gsab56(3)-Hor,
  author =              {Horton, Robert E.},
  title =               {Erosional development of streams and their drainage
                         basins; hydrophysical approach to quantitative
                         morphology},
  publisher =           {Geological Society of America},
  journal =             {Geological Society of America Bulletin},
  volume =              {56},
  number =              {3},
  pages =               {275-370},
  year =                {1945},
  month =               mar,
  doi =                 {10.1130/0016-7606(1945)56[275:EDOSAT]2.0.CO;2},
}
[Hor05] Florian Horn. Streett Games on Finite Graphs. In GDV'05. July 2005.
@inproceedings{gdv2005-Horn,
  author =              {Horn, Florian},
  title =               {{S}treett Games on Finite Graphs},
  editor =              {Jurdzi{\'n}ski, Marcin and Majumdar, Rupak},
  booktitle =           {{P}roceedings of the 2nd {W}orkshop on {G}ames in
                         {D}esign and {V}erification ({GDV}'05)},
  acronym =             {{GDV}'05},
  year =                {2005},
  month =               jul,
}
[HOW13] Paul Hunter, Joël Ouaknine, and James Worrell. Expressive Completeness for Metric Temporal Logic. In LICS'13, pages 349-357. IEEE Comp. Soc. Press, June 2013.
@inproceedings{lics2013-HOW,
  author =              {Hunter, Paul and Ouaknine, Jo{\"e}l and Worrell,
                         James},
  title =               {Expressive Completeness for Metric Temporal Logic},
  booktitle =           {{P}roceedings of the 28th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'13)},
  acronym =             {{LICS}'13},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {349-357},
  year =                {2013},
  month =               jun,
  doi =                 {10.1109/LICS.2013.41},
}
[HP85] David Harel and David Peleg. Process Logic with Regular Formulas. Theoretical Computer Science 38:307-322. Elsevier, 1985.
@article{tcs38()-HP,
  author =              {Harel, David and Peleg, David},
  title =               {Process Logic with Regular Formulas},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {38},
  pages =               {307-322},
  year =                {1985},
}
[HP06] Thomas A. Henzinger and Vinayak S. Prabhu. Timed Alternating-Time Temporal Logic. In FORMATS'06, Lecture Notes in Computer Science 4202, pages 1-17. Springer-Verlag, September 2006.
@inproceedings{formats2006-HP,
  author =              {Henzinger, Thomas A. and Prabhu, Vinayak S.},
  title =               {Timed Alternating-Time Temporal Logic},
  editor =              {Asarin, Eugene and Bouyer, Patricia},
  booktitle =           {{P}roceedings of the 4th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'06)},
  acronym =             {{FORMATS}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4202},
  pages =               {1-17},
  year =                {2006},
  month =               sep,
}
[HP06] Thomas A. Henzinger and Nir Piterman. Solving Games without Determinization. In CSL'06, Lecture Notes in Computer Science 4207, pages 395-410. Springer-Verlag, September 2006.
@inproceedings{csl2006-HP,
  author =              {Henzinger, Thomas A. and Piterman, Nir},
  title =               {Solving Games without Determinization},
  editor =              {{\'E}sik, Zolt{\'a}n},
  booktitle =           {{P}roceedings of the 20th {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'06)},
  acronym =             {{CSL}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4207},
  pages =               {395-410},
  year =                {2006},
  month =               sep,
}
[HPV99] Michel Habib, Christophe Paul, and Laurent Viennot. Partition Refinement Techniques: An Interesting Algorithmic Tool Kit. International Journal of Foundations of Computer Science 10(2):147,170. June 1999.
@article{ijfcs10(2)-HPV,
  author =              {Habib, Michel and Paul, {\relax Ch}ristophe and
                         Viennot, Laurent},
  title =               {Partition Refinement Techniques: An Interesting
                         Algorithmic Tool Kit},
  journal =             {International Journal of Foundations of Computer
                         Science},
  volume =              {10},
  number =              {2},
  pages =               {147,170},
  year =                {1999},
  month =               jun,
}
[HQR98] Thomas A. Henzinger, Shaz Qadeer, and Sriram Rajamani. You Assume, We Guarantee: Methodology and Case Studies. In CAV'98, Lecture Notes in Computer Science 1427, pages 440-451. Springer-Verlag, June 1998.
@inproceedings{cav1998-HQR,
  author =              {Henzinger, Thomas A. and Qadeer, Shaz and Rajamani,
                         Sriram},
  title =               {You Assume, We Guarantee: Methodology and Case
                         Studies},
  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 =               {440-451},
  year =                {1998},
  month =               jun,
}
[HR99] Yoram Hirshfeld and Alexander Rabinovich. Quantitative Temporal Logic. In CSL'99, Lecture Notes in Computer Science 1862, pages 172-187. Springer-Verlag, September 1999.
@inproceedings{csl1999-HR,
  author =              {Hirshfeld, Yoram and Rabinovich, Alexander},
  title =               {Quantitative Temporal Logic},
  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 =               {172-187},
  year =                {1999},
  month =               sep,
}
[HR00] Thomas A. Henzinger and Jean-François Raskin. Robust Indecidability of Timed and Hybrid Systems. In HSCC'00, Lecture Notes in Computer Science 1790, pages 145-159. Springer-Verlag, March 2000.
@inproceedings{hscc2000-HR,
  author =              {Henzinger, Thomas A. and Raskin, Jean-Fran{\c c}ois},
  title =               {Robust Indecidability of Timed and Hybrid Systems},
  editor =              {Lynch, Nancy and Krogh, Bruce H.},
  booktitle =           {{P}roceedings of the 3rd {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
                         ({HSCC}'00)},
  acronym =             {{HSCC}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1790},
  pages =               {145-159},
  year =                {2000},
  month =               mar,
}
[HR02] Klaus Havelund and Grigore Roşu. Synthesizing monitors for safety properties. In TACAS'02, Lecture Notes in Computer Science 2280, pages 342-356. Springer-Verlag, April 2002.
@inproceedings{tacas2002-HR,
  author =              {Havelund, Klaus and Ro{\c{s}}u, Grigore},
  title =               {Synthesizing monitors for safety properties},
  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 =               {342-356},
  year =                {2002},
  month =               apr,
}
[HR03] Yoram Hirshfeld and Alexander Rabinovich. Future Temporal Logic Needs Infinitely Many Modalities. Information and Computation 187(2):196-208. Academic Press, December 2003.
@article{icomp187(2)-HR,
  author =              {Hirshfeld, Yoram and Rabinovich, Alexander},
  title =               {Future Temporal Logic Needs Infinitely Many
                         Modalities},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {187},
  number =              {2},
  pages =               {196-208},
  year =                {2003},
  month =               dec,
}
[HR04] Yoram Hirshfeld and Alexander Rabinovich. Logics for Real Time: Decidability and Complexity. Fundamenta Informaticae 62(1):1-28. IOS Press, 2004.
@article{fi62(1)-HR,
  author =              {Hirshfeld, Yoram and Rabinovich, Alexander},
  title =               {Logics for Real Time: Decidability and Complexity},
  publisher =           {IOS Press},
  journal =             {Fundamenta Informaticae},
  volume =              {62},
  number =              {1},
  pages =               {1-28},
  year =                {2004},
}
[HR04] Michael Huth and Mark D. Ryan. Logic in Computer Science. Cambridge University Press, August 2004.
@book{lics-HR,
  author =              {Huth, Michael and Ryan, Mark D.},
  title =               {Logic in Computer Science},
  publisher =           {Cambridge University Press},
  year =                {2004},
  month =               aug,
}
[HR05] Yoram Hirshfeld and Alexander Rabinovich. Timer Formulas and Decidable Metric Temporal Logic. Information and Computation 198(2):148-178. Academic Press, May 2005.
@article{icomp198(2)-HR,
  author =              {Hirshfeld, Yoram and Rabinovich, Alexander},
  title =               {Timer Formulas and Decidable Metric Temporal Logic},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {198},
  number =              {2},
  pages =               {148-178},
  year =                {2005},
  month =               may,
  doi =                 {10.1016/j.ic.2004.12.002},
}
[HR05] Ian Hodkinson and Mark Reynolds. Separation –-mdash; Past, Present, and Future. In Sergei N. Artemov, Howard Barringer, Artur S. d'Avila Garcez, Luís C. Lamb, and John Woods (eds.), We Will Show Them – Essays in Honour of Dov Gabbay. College Publications, 2005.
@incollection{wwst2005b-HR,
  author =              {Hodkinson, Ian and Reynolds, Mark},
  title =               {Separation~--- Past, Present, and Future},
  editor =              {Artemov, Sergei N. and Barringer, Howard and d'Avila
                         Garcez, Artur S. and Lamb, Lu{\'\i}s C. and Woods,
                         John},
  booktitle =           {We Will Show Them~-- Essays in Honour of
                         {D}ov~{G}abbay},
  publisher =           {College Publications},
  volume =              {2},
  pages =               {117-142},
  year =                {2005},
}
[HR06] Yoram Hirshfeld and Alexander Rabinovich. An Expressive Temporal Logic for Real Time. In MFCS'06, Lecture Notes in Computer Science 4162, pages 492-504. Springer-Verlag, August 2006.
@inproceedings{mfcs2006-HR,
  author =              {Hirshfeld, Yoram and Rabinovich, Alexander},
  title =               {An Expressive Temporal Logic for Real Time},
  editor =              {Kr{\'a}lovi{{c}}, Rastislav and Urzyczyn, Pawel},
  booktitle =           {{P}roceedings of the 31st {I}nternational
                         {S}ymposium on {M}athematical {F}oundations of
                         {C}omputer {S}cience ({MFCS}'06)},
  acronym =             {{MFCS}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4162},
  pages =               {492-504},
  year =                {2006},
  month =               aug,
}
[HR07] Yoram Hirshfeld and Alexander Rabinovich. Expressiveness of Metric modalities for continuous time. Logical Methods in Computer Science 3(1). March 2007.
@article{lmcs3(1)-HR,
  author =              {Hirshfeld, Yoram and Rabinovich, Alexander},
  title =               {Expressiveness of Metric modalities for continuous
                         time},
  journal =             {Logical Methods in Computer Science},
  volume =              {3},
  number =              {1},
  year =                {2007},
  month =               mar,
  doi =                 {10.2168/LMCS-3(1:3)2007},
}
[HR08] Yoram Hirshfeld and Alexander Rabinovich. Decidable Metric Logics. Information and Computation 206(12):1425-1442. Elsevier, December 2008.
@article{icomp206(12)-HR,
  author =              {Hirshfeld, Yoram and Rabinovich, Alexander},
  title =               {Decidable Metric Logics},
  publisher =           {Elsevier},
  journal =             {Information and Computation},
  volume =              {206},
  number =              {12},
  pages =               {1425-1442},
  year =                {2008},
  month =               dec,
  doi =                 {10.1016/j.ic.2008.08.004},
}
[HR14] Paul Hunter and Jean-François Raskin. Quantitative games with interval objectives. In FSTTCS'14, Leibniz International Proceedings in Informatics 29, pages 365-377. Leibniz-Zentrum für Informatik, December 2014.
@inproceedings{fsttcs2014-HR,
  author =              {Hunter, Paul and Raskin, Jean-Fran{\c c}ois},
  title =               {Quantitative games with interval objectives},
  editor =              {Raman, Venkatesh and Suresh, S. P.},
  booktitle =           {{P}roceedings of the 34th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'14)},
  acronym =             {{FSTTCS}'14},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {29},
  pages =               {365-377},
  year =                {2014},
  month =               dec,
}
[HRS98] Thomas A. Henzinger, Jean-François Raskin, and Pierre-Yves Schobbens. The Regular Real-Time Languages. In ICALP'98, Lecture Notes in Computer Science 1443, pages 580-591. Springer-Verlag, July 1998.
@inproceedings{icalp1998-HRS,
  author =              {Henzinger, Thomas A. and Raskin, Jean-Fran{\c c}ois
                         and Schobbens, Pierre-Yves},
  title =               {The Regular Real-Time Languages},
  editor =              {Larsen, Kim Guldstrand and Skyum, Sven and Winskel,
                         Glynn},
  booktitle =           {{P}roceedings of the 25th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'98)},
  acronym =             {{ICALP}'98},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1443},
  pages =               {580-591},
  year =                {1998},
  month =               jul,
}
[HRS02] Aidan Harding, Mark D. Ryan, and Pierre-Yves Schobbens. Approximating ATL* in ATL (Extended Abstract). In VMCAI'02, Lecture Notes in Computer Science 2294, pages 289-301. Springer-Verlag, January 2002.
@inproceedings{vmcai2002-HRS,
  author =              {Harding, Aidan and Ryan, Mark D. and Schobbens,
                         Pierre-Yves},
  title =               {Approximating {ATL}{\(^*\)} in~{ATL} (Extended
                         Abstract)},
  editor =              {Cortesi, Agostino},
  booktitle =           {{P}roceedings of the 3rd {I}nternational {W}orkshop
                         on {V}erification, {M}odel {C}hecking, and
                         {A}bstract {I}nterpretation ({VMCAI}'02)},
  acronym =             {{VMCAI}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2294},
  pages =               {289-301},
  year =                {2002},
  month =               jan,
}
[HRS03] Aidan Harding, Mark D. Ryan, and Pierre-Yves Schobbens. Towards Symbolic Strategy Synthesis for A-LTL. In TIME-ICTL'03, pages 137-146. IEEE Comp. Soc. Press, July 2003.
@inproceedings{time2003-HRS,
  author =              {Harding, Aidan and Ryan, Mark D. and Schobbens,
                         Pierre-Yves},
  title =               {Towards Symbolic Strategy Synthesis for
  {\(\langle\)\,\llap{\(\langle\)}A\(\rangle\)\,\llap{\(\rangle\)}}-{LTL}},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {S}ymposium on {T}emporal {R}epresentation and
                         {R}easoning and of the 4th {I}nternational
                         {C}onference on {T}emporal {L}ogic
                         ({TIME}-{ICTL}'03)},
  acronym =             {{TIME-ICTL}'03},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {137-146},
  year =                {2003},
  month =               jul,
}
[HRS05] Aidan Harding, Mark D. Ryan, and Pierre-Yves Schobbens. A New Algorithm for Strategy Synthesis in LTL Games. In TACAS'05, Lecture Notes in Computer Science 3440, pages 477-492. Springer-Verlag, April 2005.
@inproceedings{tacas2005-HRS,
  author =              {Harding, Aidan and Ryan, Mark D. and Schobbens,
                         Pierre-Yves},
  title =               {A New Algorithm for Strategy Synthesis in {LTL}
                         Games},
  editor =              {Halbwachs, Nicolas and Zuck, Lenore D.},
  booktitle =           {{P}roceedings of the 11th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'05)},
  acronym =             {{TACAS}'05},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3440},
  pages =               {477-492},
  year =                {2005},
  month =               apr,
}
[HRS+02] Thomas Hune, Judi Romijn, Mariëlle Stoelinga, and Frits Vaandrager. Linear parametric model checking of timed automata. Journal of Logic and Algebraic Programming 52-53:183-220. Elsevier, June 2002.
@article{jlap52-53-hrsv,
  author =              {Hune, Thomas and Romijn, Judi and Stoelinga,
                         Mari{\"e}lle and Vaandrager, Frits},
  title =               {Linear parametric model checking of timed automata},
  publisher =           {Elsevier},
  journal =             {Journal of Logic and Algebraic Programming},
  volume =              {52-53},
  pages =               {183-220},
  year =                {2002},
  month =               jun,
}
[HS89] Jaakko Hintikka and Gabriel Sandu. Informational Independence as a Semantical Phenomenon. In Proceedings of the 8th International Congress of Logic, Methodology and Philosophy of Science, Studies in Logic and the Foundations of Mathematics 70, pages 571-589. North-Holland, January 1989.
@inproceedings{iclmps1989-HS,
  author =              {Hintikka, Jaakko and Sandu, Gabriel},
  title =               {Informational Independence as a Semantical
                         Phenomenon},
  editor =              {Fenstad, Jens Erik and Frolov, Ivan T. and
                         Hilppinen, Risto},
  booktitle =           {{P}roceedings of the 8th {I}nternational {C}ongress
                         of {L}ogic, {M}ethodology and {P}hilosophy of
                         {S}cience},
  publisher =           {North-Holland},
  series =              {Studies in Logic and the Foundations of Mathematics},
  volume =              {70},
  pages =               {571-589},
  year =                {1989},
  month =               jan,
  doi =                 {10.1016/S0049-237X(08)70066-1},
}
[HS91] Joseph Y. Halpern and Yoav Shoham. A Propositional Modal Logic of Time Intervals. Journal of the ACM 38(4):935-962. ACM Press, October 1991.
@article{jacm38(4)-HS,
  author =              {Halpern, Joseph Y. and Shoham, Yoav},
  title =               {A Propositional Modal Logic of Time Intervals},
  publisher =           {ACM Press},
  journal =             {Journal of the ACM},
  volume =              {38},
  number =              {4},
  pages =               {935-962},
  year =                {1991},
  month =               oct,
}
[HS96] Klaus Havelund and Natarajan Shankar. Experiments in Theorem Proving and Model Checking for Protocol Verification. In FME'96, Lecture Notes in Computer Science 1051, pages 662-681. Springer-Verlag, March 1996.
@inproceedings{fme1996-HS,
  author =              {Havelund, Klaus and Shankar, Natarajan},
  title =               {Experiments in Theorem Proving and Model Checking
                         for Protocol Verification},
  editor =              {Gaudel, Marie-Claude and Woodcock, Jim},
  booktitle =           {Industrial Benefit and Advances in Formal
                         Methods~--- {P}roceedings of the 3rd {I}nternational
                         {S}ymposium of {F}ormal {M}ethods {E}urope
                         ({FME}'96)},
  acronym =             {{FME}'96},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1051},
  pages =               {662-681},
  year =                {1996},
  month =               mar,
}
[HS06] Thomas A. Henzinger and Joseph Sifakis. The Embedded Systems Design Challenge. In FM'06, Lecture Notes in Computer Science 4085, pages 1-15. Springer-Verlag, August 2006.
@inproceedings{fm2006-HS,
  author =              {Henzinger, Thomas A. and Sifakis, Joseph},
  title =               {The Embedded Systems Design Challenge},
  editor =              {Misra, Jayadev and Nipkow, Tobias and Sekerinski,
                         Emil},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {S}ymposium on {F}ormal {M}ethods ({FM}'06)},
  acronym =             {{FM}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4085},
  pages =               {1-15},
  year =                {2006},
  month =               aug,
  doi =                 {10.1007/11813040_1},
}
[HSB03] John Hershberger, Subhash Suri, and Amir Bhosle. On the Difficulty of Some Shortest Path Problems. In STACS'03, Lecture Notes in Computer Science 2607, pages 343-354. Springer-Verlag, February 2003.
@inproceedings{stacs2003-HSB,
  author =              {Hershberger, John and Suri, Subhash and Bhosle,
                         Amir},
  title =               {On the Difficulty of Some Shortest Path Problems},
  editor =              {Alt, Helmut and Habib, Michel},
  booktitle =           {{P}roceedings of the 20th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'03)},
  acronym =             {{STACS}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2607},
  pages =               {343-354},
  year =                {2003},
  month =               feb,
}
[HSL+97] Klaus Havelund, Arne Skou, Kim Guldstrand Larsen, and Kristian Lund. Formal Modelling and Analysis of an Audio/Video Protocol: An Industrial Case Study Using Uppaal. In RTSS'97, pages 2-13. IEEE Comp. Soc. Press, December 1997.
@inproceedings{rts1997-HSLL,
  author =              {Havelund, Klaus and Skou, Arne and Larsen, Kim
                         Guldstrand and Lund, Kristian},
  title =               {Formal Modelling and Analysis of an
                         Audio{\slash}Video Protocol: An Industrial Case
                         Study Using {U}ppaal},
  booktitle =           {{P}roceedings of the 18th {S}ymposium on {R}eal-Time
                         {S}ystems ({RTSS}'97)},
  acronym =             {{RTSS}'97},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {2-13},
  year =                {1997},
  month =               dec,
}
[HST+16] Frédéric Herbreteau, B. Srivathsan, Thanh-Tung Tran, and Igor Walukiewicz. Why liveness for timed automata is hard, and what we can do about it. In FSTTCS'16, Leibniz International Proceedings in Informatics, pages 48:1-48:14. Leibniz-Zentrum für Informatik, December 2016.
@inproceedings{fsttcs2016-HSTW,
  author =              {Herbreteau, Fr{\'e}d{\'e}ric and Srivathsan, B. and
                         Tran, Thanh-Tung and Walukiewicz, Igor},
  title =               {Why liveness for timed automata is hard, and what we
                         can do about~it},
  editor =              {Akshay, S. and Lal, Akash and Saurabh, Saket and
                         Sen, Sandeep},
  booktitle =           {{P}roceedings of the 36th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'16)},
  acronym =             {{FSTTCS}'16},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  pages =               {48:1-48:14},
  year =                {2016},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2016.48},
}
[HSW12] Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Efficient emptiness check for timed Büchi automata. Formal Methods in System Design 40(2):122-146. Springer-Verlag, April 2012.
@article{fmsd40(2)-HSW,
  author =              {Herbreteau, Fr{\'e}d{\'e}ric and Srivathsan, B. and
                         Walukiewicz, Igor},
  title =               {Efficient emptiness check for timed {B}{\"u}chi
                         automata},
  publisher =           {Springer-Verlag},
  journal =             {Formal Methods in System Design},
  volume =              {40},
  number =              {2},
  pages =               {122-146},
  year =                {2012},
  month =               apr,
  doi =                 {10.1007/s10703-011-0133-1},
}
[HSW12] Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Better abstractions for timed automata. In LICS'12, pages 375-384. IEEE Comp. Soc. Press, June 2012.
@inproceedings{lics2012-HSW,
  author =              {Herbreteau, Fr{\'e}d{\'e}ric and Srivathsan, B. and
                         Walukiewicz, Igor},
  title =               {Better abstractions for timed automata},
  booktitle =           {{P}roceedings of the 27th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'12)},
  acronym =             {{LICS}'12},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {375-384},
  year =                {2012},
  month =               jun,
  doi =                 {10.1109/LICS.2012.48},
}
[HSW13] Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Lazy Abstractions for Timed Automata. In CAV'13, Lecture Notes in Computer Science 8044, pages 990-1005. Springer-Verlag, July 2013.
@inproceedings{cav2013-HSW,
  author =              {Herbreteau, Fr{\'e}d{\'e}ric and Srivathsan, B. and
                         Walukiewicz, Igor},
  title =               {Lazy Abstractions for Timed Automata},
  editor =              {Sharygina, Natasha and Veith, Helmut},
  booktitle =           {{P}roceedings of the 25th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'13)},
  acronym =             {{CAV}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8044},
  pages =               {990-1005},
  year =                {2013},
  month =               jul,
  doi =                 {10.1007/978-3-642-39799-8_71},
}
[HSW13] Chung-Hao Huang, Sven Schewe, and Farn Wang. Model Checking Iterated Games. In TACAS'13, Lecture Notes in Computer Science 7795, pages 154-168. Springer-Verlag, March 2013.
@inproceedings{tacas2013-HSW,
  author =              {Huang, Chung-Hao and Schewe, Sven and Wang, Farn},
  title =               {Model Checking Iterated Games},
  editor =              {Piterman, Nir and Smolka, Scott A.},
  booktitle =           {{P}roceedings of the 19th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'13)},
  acronym =             {{TACAS}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7795},
  pages =               {154-168},
  year =                {2013},
  month =               mar,
  doi =                 {10.1007/978-3-642-36742-7_11},
}
[HSW16] Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Efficient emptiness check for timed Büchi automata. Information and Computation 251:67-90. Elsevier, December 2016.
@article{icomp251()-HSW,
  author =              {Herbreteau, Fr{\'e}d{\'e}ric and Srivathsan, B. and
                         Walukiewicz, Igor},
  title =               {Efficient emptiness check for timed {B}{\"u}chi
                         automata},
  publisher =           {Elsevier},
  journal =             {Information and Computation},
  volume =              {251},
  pages =               {67-90},
  year =                {2016},
  month =               dec,
  doi =                 {10.1016/j.ic.2016.07.004},
}
[HT74] John Hopcroft and Robert Endre Tarjan. Efficient Planarity Testing. Journal of the ACM 21(4):549-568. ACM Press, October 1974.
@article{jacm21(4)-HT,
  author =              {Hopcroft, John and Tarjan, Robert Endre},
  title =               {Efficient Planarity Testing},
  publisher =           {ACM Press},
  journal =             {Journal of the ACM},
  volume =              {21},
  number =              {4},
  pages =               {549-568},
  year =                {1974},
  month =               oct,
}
[HT15] Frédéric Herbreteau and Thanh-Tung Tran. Improving Search Order for Reachability Testing in Timed Automata. In FORMATS'15, Lecture Notes in Computer Science 9268, pages 124-139. Springer-Verlag, September 2015.
@inproceedings{formats2015-HT,
  author =              {Herbreteau, Fr{\'e}d{\'e}ric and Tran, Thanh-Tung},
  title =               {Improving Search Order for Reachability Testing in
                         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 =               {124-139},
  year =                {2015},
  month =               sep,
  doi =                 {10.1007/978-3-319-22975-1_9},
}
[HTS+00] Masahiro Hirao, Masayuki Takeda, Ayumi Shinohara, and Setsuo Arikawa. Faster Fully Compressed Pattern Matching Algorithm for a Subclass of Straight-Line Programs. Technical Report DOI-TR-169, Dept. of Informatics, Kyushu University, Fukuoka, Japan, January 2000.
@techreport{DOI-TR-169-HTSA,
  author =              {Hirao, Masahiro and Takeda, Masayuki and Shinohara,
                         Ayumi and Arikawa, Setsuo},
  title =               {Faster Fully Compressed Pattern Matching Algorithm
                         for a Subclass of Straight-Line Programs},
  number =              {DOI-TR-169},
  year =                {2000},
  month =               jan,
  institution =         {Dept. of Informatics, Kyushu University, Fukuoka,
                         Japan},
  type =                {Technical Report},
}
[Hun13] Paul Hunter. When is Metric Temporal Logic Expressively Complete?. In CSL'13, Leibniz International Proceedings in Informatics 23, pages 380-394. Leibniz-Zentrum für Informatik, September 2013.
@inproceedings{csl2013-Hun,
  author =              {Hunter, Paul},
  title =               {When is Metric Temporal Logic Expressively
                         Complete?},
  editor =              {Ronchi{ }Della{~}Rocca, Simona},
  booktitle =           {{P}roceedings of the 27th {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'13)},
  acronym =             {{CSL}'13},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {23},
  pages =               {380-394},
  year =                {2013},
  month =               sep,
  doi =                 {10.4230/LIPIcs.CSL.2013.380},
}
[Hun15] Paul Hunter. Reachability in Succinct One-Counter Games. In RP'15, Lecture Notes in Computer Science 9328, pages 37-49. Springer-Verlag, September 2015.
@inproceedings{rp2015-Hun,
  author =              {Hunter, Paul},
  title =               {Reachability in Succinct One-Counter Games},
  editor =              {Boja{\'n}czyk, Miko{\l}aj and Lasota, S{\l}awomir
                         and Potapov, Igor},
  booktitle =           {{P}roceedings of the 9th {W}orkshop on
                         {R}eachability {P}roblems in {C}omputational
                         {M}odels ({RP}'15)},
  acronym =             {{RP}'15},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9328},
  pages =               {37-49},
  year =                {2015},
  month =               sep,
  doi =                 {10.1007/978-3-319-24537-9 5},
}
[Huy82] Thiet-Dung Huynh. The Complexity of Semilinear Sets. Elektronische Informationsverarbeitung und Kybernetik 18(6):291-338. June 1982.
@article{eik18(6)-Huy,
  author =              {Huynh, Thiet-Dung},
  title =               {The Complexity of Semilinear Sets},
  journal =             {Elektronische Informationsverarbeitung und
                         Kybernetik},
  volume =              {18},
  number =              {6},
  pages =               {291-338},
  year =                {1982},
  month =               jun,
}
[HVG04] Jinfeng Huang, Jeroen Voeten, and Marc C.W. Geilen. Real-Time Property Preservation in Concurrent Real-time Systems. In RTCSA'04. August 2004.
@inproceedings{rtcsa2004-HVG,
  author =              {Huang, Jinfeng and Voeten, Jeroen and Geilen, Marc
                         C.W.},
  title =               {Real-Time Property Preservation in Concurrent
                         Real-time Systems},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {C}onference on {R}eal-{T}ime {C}omputing {S}ystems
                         and {A}pplications ({RTCSA}'04)},
  acronym =             {{RTCSA}'04},
  year =                {2004},
  month =               aug,
}
[HW97] Harald Hempel and Gerd Wechsung. The Operators min and max on the Polynomial Hierarchy. Technical Report TR97-025, Electronic Colloquium on Computational Complexity, May 1997.
@techreport{ECCC-TR97-025-HW,
  author =              {Hempel, Harald and Wechsung, Gerd},
  title =               {The Operators min and max on the Polynomial
                         Hierarchy},
  number =              {TR97-025},
  year =                {1997},
  month =               may,
  institution =         {Electronic Colloquium on Computational Complexity},
  type =                {Technical Report},
}
[HWZ02] Ian Hodkinson, Frank Wolter, and Michael Zakharyaschev. Decidable and Undecidable Fragments of First-Order Branching Temporal Logics. In LICS'02, pages 393-402. IEEE Comp. Soc. Press, July 2002.
@inproceedings{lics2002-HWZ,
  author =              {Hodkinson, Ian and Wolter, Frank and Zakharyaschev,
                         Michael},
  title =               {Decidable and Undecidable Fragments of First-Order
                         Branching Temporal Logics},
  booktitle =           {{P}roceedings of the 17th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'02)},
  acronym =             {{LICS}'02},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {393-402},
  year =                {2002},
  month =               jul,
}