H
[Haa12] Christoph Haase. On the Complexity of Model Checking Counter Automata. PhD thesis, University of Oxford, UK, Janvier 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 et 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, décembre 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, avril 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, décembre 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. Octobre 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, juillet 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. Novembre 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, Mars 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 et Frits Vaandrager. Adding Symmetry Reduction to Uppaal. In FORMATS'03, Lecture Notes in Computer Science 2791. Springer-Verlag, septembre 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 et 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, décembre 2010.
Résumé

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 et Fausto Giunchiglia. Verification of a Safety-Critical Railway Interlocking System with Real-Time Constraints. Science of Computer Programming 36(1):53-64. Elsevier, janvier 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 et Stephen G. Mitchell. Some Observation about Relativization of Space Bounded Computations. In Grzegorz Rozenberg et 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, juillet 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, septembre 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. Juin 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, septembre 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. Novembre 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, mars 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, Septembre 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 et Rupak Majumdar. Rectangular Hybrid Games. In CONCUR'99, Lecture Notes in Computer Science 1664, pages 320-335. Springer-Verlag, août 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 et 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 et Howard Wong-Toi. A User Guide to HyTech. In TACAS'95, Lecture Notes in Computer Science 1019, pages 41-71. Springer-Verlag, mai 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 et 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, octobre 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 et Neil Immerman. Complete Problems for Dynamic Complexity Classes. In LICS'02, pages 313-322. IEEE Comp. Soc. Press, juillet 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 et Peter Bro Miltersen. A Faster Algorithm for Solving One-Clock Priced Timed Games. Research Report 1201.3498, arXiv, Janvier 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 et 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, août 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 et 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, décembre 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 et Rajeev Joshi. Model-Driven Software Verification. In SPIN'04, Lecture Notes in Computer Science 2989, pages 76-91. Springer-Verlag, avril 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 et Rupak Majumdar. Counterexample-Guided Control. In ICALP'03, Lecture Notes in Computer Science 2719, pages 886-902. Springer-Verlag, juin 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 et 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, juin 2018.
Résumé

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 et Kenneth L. McMillan. Abstractions from Proofs. In POPL'04, pages 232-244. ACM Press, janvier 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,
}
[HJM+02] Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar et Grégoire Sutre. Lazy abstraction. In POPL'02, ACM SIGPLAN Notices 37(1), pages 58-70. ACM Press, janvier 2002.
@inproceedings{popl2002-HJMS,
  author =              {Henzinger, Thomas A. and Jhala, Ranjit and Majumdar,
                         Rupak and Sutre, Gr{\'e}goire},
  title =               {Lazy abstraction},
  booktitle =           {Conference Record of the 29th {ACM}
                         {SIGPLAN}-{SIGACT} {S}ymposium on {P}rinciples of
                         {P}rogramming {L}anguages ({POPL}'02)},
  acronym =             {{POPL}'02},
  publisher =           {ACM Press},
  series =              {ACM SIGPLAN Notices},
  volume =              {37},
  number =              {1},
  pages =               {58-70},
  year =                {2002},
  month =               jan,
}
[HJM+03] Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar et Grégoire Sutre. Software verification with BLAST. In SPIN'03, Lecture Notes in Computer Science 2648, pages 235-239. Springer-Verlag, avril 2003.
@inproceedings{spin2003-HJMS,
  author =              {Henzinger, Thomas A. and Jhala, Ranjit and Majumdar,
                         Rupak and Sutre, Gr{\'e}goire},
  title =               {Software verification with {BLAST}},
  editor =              {Ball, Thomas and Rajamani, Sriram},
  booktitle =           {{P}roceedings of the 10th {I}nternational {SPIN}
                         {W}orkshop ({SPIN}'03)},
  acronym =             {{SPIN}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2648},
  pages =               {235-239},
  year =                {2003},
  month =               apr,
}
[HJR02] Alan J. Hoffman, Kate Jenkins et Tim Roughgarden. On a game in directed graphs. Information Processing Letters 83(1):13-16. Elsevier, juillet 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 et Michael Wooldridge. A Logic for Strategic Reasoning. In AAMAS'05, pages 157-164. ACM Press, juillet 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 et Bruce M. Kapron. Zero-one laws for modal logic. Annals of Pure and Applied Logic 69(2-3):157-193. Elsevier, octobre 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 et Orna Kupferman. From Quantity to Quality. In HART'97, Lecture Notes in Computer Science 1201, pages 48-62. Springer-Verlag, mars 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 et Peter W. Kopke. Discrete-Time Control for Rectangular Hybrid Systems. Theoretical Computer Science 221(1-2):369-392. Elsevier, juin 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 et 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, juin 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 et 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, avril 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 et 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, mars 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 et James Worrell. Reachability in Succinct and Parametric One-Counter Automata. In CONCUR'09, Lecture Notes in Computer Science 5710, pages 369-383. Springer-Verlag, septembre 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 et Rohit Parikh. Process Logic: Expressiveness, Decidability and Completeness. Journal of Computer and System Sciences 25(2):144-170. Academic Press, octobre 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 et Pravin Varaiya. What is decidable about Hybrid Automata?. In STOC'95, pages 373-382. ACM Press, mai 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 et Pravin Varaiya. What is decidable about Hybrid Automata?. Journal of Computer and System Sciences 57(1):94-124. Academic Press, août 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 et 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, décembre 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 et Wolfgang Thomas. Degrees of Lookahead in Regular Infinite Games. In FoSSaCS'10, Lecture Notes in Computer Science 6014, pages 252-266. Springer-Verlag, mars 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 et 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, août 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 et Howard Wong-Toi. The expressive power of clocks. In ICALP'95, Lecture Notes in Computer Science 944, pages 417-428. Springer-Verlag, juillet 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 et 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, juillet 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 et Kim Guldstrand Larsen. Exact Acceleration of real-Time Model Checking. In TPTS'02, Electronic Notes in Theoretical Computer Science 65(6). Elsevier, avril 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 et 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, juillet 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 et Sylvain Peyronnet. Approximate Probabilistic Model Checking. In VMCAI'04, Lecture Notes in Computer Science 2937, pages 73-84. Springer-Verlag, janvier 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 et Jan Tretmans. Quantitative system validation in model driven design. In EMSOFT'10, pages 301-302. ACM Press, octobre 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 et Michael Wooldridge. On the Complexity of Practical ATL Model Checking. In AAMAS'06, pages 201-208. ACM Press, mai 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 et Dirk Walther. Reasoning about Actions Meets Strategic Logics. In LORI'13, Lecture Notes in Computer Science 8196, pages 162-175. Springer-Verlag, octobre 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 et Robin Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32(1). ACM Press, janvier 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 et Pierre McKenzie. Alternating and Empty Alternating Auxiliary Stack Automata. Theoretical Computer Science 299(1-3):307-326. Elsevier, avril 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 et 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, septembre 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 et John Mullins. Concurrent secrets with quantified suspicion. In ACSD'18. IEEE Comp. Soc. Press, juin 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 et Amir Pnueli. What Good are Digital Clocks?. In ICALP'92, Lecture Notes in Computer Science 623, pages 545-558. Springer-Verlag, juillet 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 et 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 et 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 et Amir Pnueli. Temporal Proof Methodologies for Timed Transition Systems. Information and Computation 112(2):273-337. Academic Press, août 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 et Vinayak S. Prabhu. Quantifying Similarities Between Timed Systems. In FORMATS'05, Lecture Notes in Computer Science 3829, pages 226-241. Springer-Verlag, septembre 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 et Sergio Yovine. Symbolic Model Checking for Real Time Systems. Information and Computation 111(2):193-244. Academic Press, juin 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 et 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, novembre 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 et Jan Otop. From Model Checking to Model Measuring. In CONCUR'13, Lecture Notes in Computer Science 8052, pages 273-287. Springer-Verlag, août 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, octobre 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 et 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, mai 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, mars 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. Juillet 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 et James Worrell. Expressive Completeness for Metric Temporal Logic. In LICS'13, pages 349-357. IEEE Comp. Soc. Press, juin 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 et 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 et Vinayak S. Prabhu. Timed Alternating-Time Temporal Logic. In FORMATS'06, Lecture Notes in Computer Science 4202, pages 1-17. Springer-Verlag, septembre 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 et Nir Piterman. Solving Games without Determinization. In CSL'06, Lecture Notes in Computer Science 4207, pages 395-410. Springer-Verlag, septembre 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 et Laurent Viennot. Partition Refinement Techniques: An Interesting Algorithmic Tool Kit. International Journal of Foundations of Computer Science 10(2):147,170. Juin 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 et Sriram Rajamani. You Assume, We Guarantee: Methodology and Case Studies. In CAV'98, Lecture Notes in Computer Science 1427, pages 440-451. Springer-Verlag, juin 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 et Alexander Rabinovich. Quantitative Temporal Logic. In CSL'99, Lecture Notes in Computer Science 1862, pages 172-187. Springer-Verlag, septembre 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 et 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, mars 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 et Grigore Roşu. Synthesizing monitors for safety properties. In TACAS'02, Lecture Notes in Computer Science 2280, pages 342-356. Springer-Verlag, avril 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 et Alexander Rabinovich. Future Temporal Logic Needs Infinitely Many Modalities. Information and Computation 187(2):196-208. Academic Press, décembre 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 et 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 et Mark D. Ryan. Logic in Computer Science. Cambridge University Press, août 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 et Alexander Rabinovich. Timer Formulas and Decidable Metric Temporal Logic. Information and Computation 198(2):148-178. Academic Press, mai 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 et Mark Reynolds. Separation –-mdash; Past, Present, and Future. In Sergei N. Artemov, Howard Barringer, Artur S. d'Avila Garcez, Luís C. Lamb et 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 et Alexander Rabinovich. An Expressive Temporal Logic for Real Time. In MFCS'06, Lecture Notes in Computer Science 4162, pages 492-504. Springer-Verlag, août 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 et Alexander Rabinovich. Expressiveness of Metric modalities for continuous time. Logical Methods in Computer Science 3(1). Mars 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 et Alexander Rabinovich. Decidable Metric Logics. Information and Computation 206(12):1425-1442. Elsevier, décembre 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 et 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, décembre 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 et Pierre-Yves Schobbens. The Regular Real-Time Languages. In ICALP'98, Lecture Notes in Computer Science 1443, pages 580-591. Springer-Verlag, juillet 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 et Pierre-Yves Schobbens. Approximating ATL* in ATL (Extended Abstract). In VMCAI'02, Lecture Notes in Computer Science 2294, pages 289-301. Springer-Verlag, janvier 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 et Pierre-Yves Schobbens. Towards Symbolic Strategy Synthesis for A-LTL. In TIME-ICTL'03, pages 137-146. IEEE Comp. Soc. Press, juillet 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 et 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, avril 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 et Frits Vaandrager. Linear parametric model checking of timed automata. Journal of Logic and Algebraic Programming 52-53:183-220. Elsevier, juin 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 et 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, janvier 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 et Yoav Shoham. A Propositional Modal Logic of Time Intervals. Journal of the ACM 38(4):935-962. ACM Press, octobre 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 et 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, mars 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 et Joseph Sifakis. The Embedded Systems Design Challenge. In FM'06, Lecture Notes in Computer Science 4085, pages 1-15. Springer-Verlag, août 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 et Amir Bhosle. On the Difficulty of Some Shortest Path Problems. In STACS'03, Lecture Notes in Computer Science 2607, pages 343-354. Springer-Verlag, février 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 et 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, décembre 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 et 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, décembre 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 et Igor Walukiewicz. Efficient emptiness check for timed Büchi automata. Formal Methods in System Design 40(2):122-146. Springer-Verlag, avril 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 et Igor Walukiewicz. Better abstractions for timed automata. In LICS'12, pages 375-384. IEEE Comp. Soc. Press, juin 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 et Igor Walukiewicz. Lazy Abstractions for Timed Automata. In CAV'13, Lecture Notes in Computer Science 8044, pages 990-1005. Springer-Verlag, juillet 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 et Farn Wang. Model Checking Iterated Games. In TACAS'13, Lecture Notes in Computer Science 7795, pages 154-168. Springer-Verlag, mars 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 et Igor Walukiewicz. Efficient emptiness check for timed Büchi automata. Information and Computation 251:67-90. Elsevier, décembre 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 et Robert Endre Tarjan. Efficient Planarity Testing. Journal of the ACM 21(4):549-568. ACM Press, octobre 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 et 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, septembre 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 et 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, Janvier 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, septembre 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, septembre 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. Juin 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 et Marc C.W. Geilen. Real-Time Property Preservation in Concurrent Real-time Systems. In RTCSA'04. Août 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 et Gerd Wechsung. The Operators min and max on the Polynomial Hierarchy. Technical Report TR97-025, Electronic Colloquium on Computational Complexity, Mai 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 et Michael Zakharyaschev. Decidable and Undecidable Fragments of First-Order Branching Temporal Logics. In LICS'02, pages 393-402. IEEE Comp. Soc. Press, juillet 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,
}