Nicolas Markey

@phdthesis{phd-haase,
  author =              {Haase, Christoph},
  title =               {On the Complexity of Model Checking Counter
                         Automata},
  year =                {2012},
  month =               jan,
  school =              {University of Oxford, UK},
}

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

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

@book{Had20-IEDES,
  author =              {Hadjicostis, Christoforos N.},
  title =               {Estimation and Inference in Discrete Event
                         Systems~-- A~model-based approach with finite
                         automata},
  publisher =           {Springer-Verlag},
  series =              {Communications and Control Engineering},
  year =                {2020},
}

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

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

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

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

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

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

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

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, Ci, Xi. 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\).},
}

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

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

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

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

@phdthesis{phd-henzinger,
  author =              {Henzinger, Thomas A.},
  title =               {The Temporal Specification and Verification of
                         Real-Time Systems},
  year =                {1991},
  school =              {Stanford University},
}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Résumé

Active learning of timed languages is concerned with the inference of timed automata by observing some of the timed words in their languages. The learner can query for the membership of words in the language, or propose a candidate model and ask if it is equivalent to the target. The major difficulty of this framework is the inference of clock resets, which are central to the dynamics of timed automata but not directly observable.

Interesting first steps have already been made by restricting to the subclass of event-recording automata, where clock resets are tied to observations. In order to advance towards learning of general timed automata, we generalize this method to a new class, called reset-free event-recording automata, where some transitions may reset no clocks.

Central to our contribution is the notion of invalidity, and the algorithm and data structures to deal with it, allowing on-the-fly detection and pruning of reset hypotheses that contradict observations. This notion is a key to any efficient active-learning procedure for generic timed automata.

@inproceedings{formats2020-HJM,
  author =              {Henry, L{\'e}o and J{\'e}ron, Thierry and Markey,
                         Nicolas},
  title =               {Active learning of timed automata with unobservable
                         resets},
  editor =              {Bertrand, Nathalie and Jansen, Nils},
  booktitle =           {{P}roceedings of the 18th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'20)},
  acronym =             {{FORMATS}'20},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {12288},
  pages =               {144-160},
  year =                {2020},
  month =               sep,
  doi =                 {10.1007/978-3-030-57628-8_9},
  abstract =            {Active learning of timed languages is concerned with
                         the inference of timed automata by observing some of
                         the timed words in their languages. The learner can
                         query for the membership of words in the language,
                         or propose a candidate model and ask if it is
                         equivalent to the target. The major difficulty of
                         this framework is the inference of clock resets,
                         which are central to the dynamics of timed automata
                         but not directly observable. \par Interesting first
                         steps have already been made by restricting to the
                         subclass of event-recording automata, where clock
                         resets are tied to observations. In order to advance
                         towards learning of general timed automata, we
                         generalize this method to a new class, called
                         reset-free event-recording automata, where some
                         transitions may reset no clocks. \par Central to our
                         contribution is the notion of invalidity, and the
                         algorithm and data structures to deal with it,
                         allowing on-the-fly detection and pruning of reset
                         hypotheses that contradict observations. This notion
                         is a key to any efficient active-learning procedure
                         for generic timed automata.},
}

Résumé

Partial observability and controllability are two well-known issues in test-case synthesis for reactive systems. We address the problem of partial control in the synthesis of test cases from timed-automata specifications. We extend a previous approach to this 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 try to minimize both cooperations of the system and distance to the satisfaction of a test purpose or to the next cooperation, 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. We finally propose a symbolic algorithm to compute those strategies.

@article{fmsd60(2)-HJM,
  author =              {Henry, L{\'e}o and J{\'e}ron, Thierry and Markey,
                         Nicolas},
  title =               {Control strategies for off-line testing of timed
                         systems},
  publisher =           {Springer-Verlag},
  journal =             {Formal Methods in System Design},
  volume =              {60},
  number =              {2},
  pages =               {147-194},
  year =                {2022},
  month =               apr,
  doi =                 {10.1007/s10703-022-00403-w},
  abstract =            {Partial observability and controllability are two
                         well-known issues in test-case synthesis for
                         reactive systems. We address the problem of partial
                         control in the synthesis of test cases from
                         timed-automata specifications. We extend a previous
                         approach to this 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 try to minimize both cooperations of the
                         system and distance to the satisfaction of a test
                         purpose or to the next cooperation, 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. We
                         finally propose a symbolic algorithm to compute
                         those strategies.},
}

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

Résumé

In formal verification, runtime monitoring consists of observing the execution of a system in order to decide as quickly as possible whether or not it satisfies a given property. We consider monitoring in a distributed setting, for properties given as reachability timed automata. In such a setting, the system is made of several components, each equipped with its own local clock and monitor. The monitors observe events occurring on their associated component, and receive timestamped events from other monitors through FIFO channels. Since clocks are local, they cannot be perfectly synchronized, resulting in imprecise timestamps. Consequently, they must be seen as intervals, leading monitors to consider possible reorderings of events. In this context, each monitor aims to provide, as early as possible, a verdict on the property it is monitoring, based on its potentially incomplete and imprecise knowledge of the current execution. In this paper, we propose an on-line monitoring algorithm for timed properties, robust to time imprecision and partial information from distant components. We first identify the date at which a monitor can safely compute a verdict based on received events. We then propose a monitoring algorithm that updates this date when new information arrives, maintains the current set of states in which the property can reside, and updates its verdict accordingly.

@inproceedings{rv2024-HJMR,
  author =              {Henry, L{\'e}o and J{\'e}ron, Thierry and Markey,
                         Nicolas and Roussanaly, Victor},
  title =               {Distributed Monitoring of Timed Properties},
  editor =              {{\'A}brah{\'a}m, Erikz and Abbas, Houssam},
  booktitle =           {{P}roceedings of the 24th {I}nternational {W}orkshop
                         on {R}untime {V}erification ({RV}'24)},
  acronym =             {{RV}'24},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {15191},
  pages =               {243-261},
  year =                {2024},
  month =               oct,
  doi =                 {10.1007/978-3-031-74234-7_16},
  abstract =            {In formal verification, runtime monitoring consists
                         of observing the execution of a system in order to
                         decide as quickly as possible whether or not it
                         satisfies a given property. We consider monitoring
                         in a distributed setting, for properties given as
                         reachability timed automata. In~such a setting,
                         the~system is made of several components, each
                         equipped with its own local clock and monitor.
                         The~monitors observe events occurring on their
                         associated component, and receive timestamped events
                         from other monitors through FIFO channels. Since
                         clocks are local, they cannot be perfectly
                         synchronized, resulting in imprecise timestamps.
                         Consequently, they must be seen as intervals,
                         leading monitors to consider possible reorderings of
                         events. In this context, each monitor aims to
                         provide, as early as possible, a verdict on the
                         property it is monitoring, based on its potentially
                         incomplete and imprecise knowledge of the current
                         execution. In~this~paper, we~propose an on-line
                         monitoring algorithm for timed properties, robust to
                         time imprecision and partial information from
                         distant components. We~first identify the date at
                         which a monitor can safely compute a verdict based
                         on received events. We~then propose a monitoring
                         algorithm that updates this date when new
                         information arrives, maintains the current set of
                         states in which the property can reside, and updates
                         its verdict accordingly.},
}

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

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

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

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

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

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

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

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

@inproceedings{csl2023-HK,
  author =              {Hazard, {\'E}mile and Kuperberg, Denis},
  title =               {Explorable automata},
  editor =              {Klin, Bartek and Pimentel, Elaine},
  booktitle =           {{P}roceedings of the 31st {EACSL} {A}nnual
                         {C}onference on {C}omputer {S}cience {L}ogic
                         ({CSL}'23)},
  acronym =             {{CSL}'23},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {252},
  pages =               {24:1-24:18},
  year =                {2023},
  month =               feb,
  doi =                 {10.4230/LIPIcs.CSL.2023.24},
}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@inproceedings{concur2022-HLT,
  author =              {Henzinger, Thomas A. and Lehtinen, Karoliina and
                         Totzke, Patrick},
  title =               {History-deterministic timed automata},
  editor =              {Klin, Bartek and Lasota, S{\l}awomir and Muscholl,
                         Anca},
  booktitle =           {{P}roceedings of the 33rd {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'22)},
  acronym =             {{CONCUR}'22},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {243},
  pages =               {14:1-14:21},
  year =                {2022},
  month =               sep,
  doi =                 {10.4230/LIPIcs.CONCUR.2022.14},
}

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

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

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

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

@article{tocl19(4)-HvdM,
  author =              {Huang, Xiaowei and van der Meyden, Ron},
  title =               {An Epistemic Strategy Logic},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {19},
  number =              {4},
  pages =               {26:1-26:45},
  year =                {2018},
  month =               dec,
  doi =                 {10.1145/3233769},
}

@inproceedings{wine2022-HM,
  author =              {Hao, Bainian and Michini, Carla},
  title =               {Inefficiency of Pure Nash Equilibria in
                         Series-Parallel Network Congestion Games},
  editor =              {Hansen, Kristoffer Arnsfelt and Liu, Tracy Xiao and
                         Malekian, Azarakhsh},
  booktitle =           {{P}roceedings of the 18th {I}nternational
                         {C}onference on {W}eb and {I}nternet {E}conomics
                         ({WINE}'22)},
  acronym =             {{WINE}'22},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {13778},
  pages =               {3-20},
  year =                {2022},
  month =               jul,
  doi =                 {10.1007/978-3-031-22832-2_1},
}

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

@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},
  pages =               {75-84},
  year =                {2018},
  month =               jun,
  doi =                 {10.1109/ACSD.2018.00011},
}

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

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

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

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

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

Résumé

We study games with reachability objectives under energy constraints. We first prove that under strict energy constraints (either only lower-bound constraint or interval constraint), those games are LOGSPACE-equivalent to energy games with the same energy constraints but without reachability objective (i.e., for infinite runs). We then consider two kinds of relaxations of the upper-bound constraints (while keeping the lower-bound constraint strict): in the first one, called weak upper bound, the upper bound is absorbing, in the sense that it allows receiving more energy when the upper bound is already reached, but the extra energy will not be stored; in the second one, we allow for temporary violations of the upper bound, imposing limits on the number or on the amount of violations.

We prove that when considering weak upper bound, reachability objectives require memory, but can still be solved in polynomial-time for one-player arenas; we prove that they are in coNP in the two-player setting. Allowing for bounded violations makes the problem PSPACE-complete for one-player arenas and EXPTIME-complete for two players.

@inproceedings{gandalf2019-HMR,
  author =              {H{\'e}lou{\"e}t, Lo{\"\i}c and Markey, Nicolas and
                         Raha, Ritam},
  title =               {Reachability games with relaxed energy constraints},
  editor =              {Leroux, J{\'e}r{\^o}me and Raskin, Jean-Fran{\c
                         c}ois},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {S}ymposium on {G}ames, {A}utomata, {L}ogics and
                         {F}ormal {V}erification ({GandALF}'19)},
  acronym =             {{GandALF}'19},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {305},
  pages =               {17-33},
  year =                {2019},
  month =               sep,
  doi =                 {10.4204/EPTCS.305.2},
  abstract =            {We study games with reachability objectives under
                         energy constraints. We first prove that under strict
                         energy constraints (either only lower-bound
                         constraint or interval constraint), those games are
                         \textsf{LOGSPACE}-equivalent to energy games with
                         the same energy constraints but without reachability
                         objective (i.e., for infinite runs). We then
                         consider two kinds of relaxations of the upper-bound
                         constraints (while keeping the lower-bound
                         constraint strict): in the first one, called
                         \emph{weak upper bound}, the upper bound is
                         \emph{absorbing}, in the sense that it allows
                         receiving more energy when the upper bound is
                         already reached, but the extra energy will not be
                         stored; in~the second~one, we~allow for
                         \emph{temporary violations} of the upper bound,
                         imposing limits on the number or on the amount of
                         violations.\par We prove that when considering weak
                         upper bound, reachability objectives require memory,
                         but can still be solved in polynomial-time for
                         one-player arenas; we prove that they are in
                         \textsf{coNP} in the two-player setting. Allowing
                         for bounded violations makes the problem
                         \textsf{PSPACE}-complete for one-player arenas and
                         \textsf{EXPTIME}-complete for two players.},
}

Résumé

We study games with reachability objectives under energy constraints. We first prove that under strict energy constraints (either only lower-bound constraint or interval constraint), those games are LOGSPACE-equivalent to energy games with the same energy constraints but without reachability objective (i.e., for infinite runs). We then consider two relaxations of the upper-bound constraints (while keeping the lower-bound constraint strict): in the first one, called weak upper bound, the upper bound is absorbing, i.e., when the upper bound is reached, the extra energy is not stored; in the second one, we allow for temporary violations of the upper bound, imposing limits on the number or on the amount of violations.

We prove that when considering weak upper bound, reachability objectives require memory, but can still be solved in polynomial-time for one-player arenas; we prove that they are in NP in the two-player setting. Allowing for bounded violations makes the problem PSPACE-complete for one-player arenas and EXPTIME-complete for two players. We then address the problem of existence of bounds for a given arena. We show that with reachability objectives, existence can be a simpler problem than the game itself, and conversely that with infinite games, existence can be harder.

@article{icomp2022-HMR,
  author =              {H{\'e}lou{\"e}t, Lo{\"\i}c and Markey, Nicolas and
                         Raha, Ritam},
  title =               {Reachability games with relaxed energy constraints},
  publisher =           {Elsevier},
  journal =             {Information and Computation},
  volume =              {285~(Part~B)},
  year =                {2022},
  month =               may,
  doi =                 {10.1016/j.ic.2021.104806},
  abstract =            {We study games with reachability objectives under
                         energy constraints. We first prove that under strict
                         energy constraints (either only lower-bound
                         constraint or interval constraint), those games are
                         LOGSPACE-equivalent to energy games with the same
                         energy constraints but without reachability
                         objective (i.e., for infinite runs). We then
                         consider two relaxations of the upper-bound
                         constraints (while keeping the lower-bound
                         constraint strict): in the first one, called weak
                         upper bound, the upper bound is absorbing, i.e.,
                         when the upper bound is reached, the extra energy is
                         not stored; in the second one, we allow for
                         temporary violations of the upper bound, imposing
                         limits on the number or on the amount of violations.
                         \par We prove that when considering weak upper
                         bound, reachability objectives require memory, but
                         can still be solved in polynomial-time for
                         one-player arenas; we prove that they are in NP in
                         the two-player setting. Allowing for bounded
                         violations makes the problem PSPACE-complete for
                         one-player arenas and EXPTIME-complete for two
                         players. We then address the problem of existence of
                         bounds for a given arena. We show that with
                         reachability objectives, existence can be a simpler
                         problem than the game itself, and conversely that
                         with infinite games, existence can be harder.},
}

@article{tcs412(39)-HMRT,
  author =              {Hoefer, Martin and Mirrokni, Vahab S. and
                         R{\"{o}}glin, Heiko and Teng, Shang-Hua},
  title =               {Competitive routing over time},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {412},
  number =              {39},
  pages =               {5420-5432},
  year =                {2011},
  month =               sep,
  doi =                 {10.1016/j.tcs.2011.05.055},
}

@book{HMU01-IATLC,
  author =              {Hopcroft, John and Motwani, Rajeev and Ullman,
                         Jeffrey D.},
  title =               {Introduction to Automata Theory, Languages, and
                         Computation},
  publisher =           {Pearson},
  year =                {2001},
}

@article{tssc4(2)-HNR,
  author =              {Hart, Peter E. and Nilsson, Nils J. and Raphael,
                         Bertram},
  title =               {A~Formal Basis for the Heuristic Determination of
                         Minimum Cost Paths},
  publisher =           {IEEE},
  journal =             {IEEE Transactions on Systems Science and
                         Cybernetics},
  volume =              {4},
  number =              {2},
  pages =               {100-107},
  year =                {1968},
  month =               jul,
  doi =                 {10.1109/TSSC.1968.300136},
}

@article{sigart-news37()-HNR,
  author =              {Hart, Peter E. and Nilsson, Nils J. and Raphael,
                         Bertram},
  title =               {Correction to {"}A~Formal Basis for the Heuristic
                         Determination of Minimum Cost Paths{"}},
  publisher =           {ACM Press},
  journal =             {SIGACT News},
  volume =              {37},
  pages =               {28-29},
  year =                {1972},
  month =               dec,
  doi =                 {10.1145/1056777.1056779},
}

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

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

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

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

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

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

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

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

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

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

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

@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,
  doi =                 {10.1007/11874683_26},
}

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

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

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

@inproceedings{hscc2000-HR,
  author =              {Henzinger, Thomas A. and Raskin, Jean-Fran{\c c}ois},
  title =               {Robust Undecidability 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,
  doi =                 {10.1007/3-540-46430-1_15},
}

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

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

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

@book{lics-HR,
  author =              {Huth, Michael and Ryan, Mark D.},
  title =               {Logic in Computer Science},
  publisher =           {Cambridge University Press},
  year =                {2004},
  month =               aug,
}

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

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

@inproceedings{mfcs2006-HR,
  author =              {Hirshfeld, Yoram and Rabinovich, Alexander},
  title =               {An Expressive Temporal Logic for Real Time},
  editor =              {Kr{\'a}lovi{\v{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,
}

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

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

@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,
  doi =                 {10.4230/LIPIcs.FSTTCS.2014.365},
}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@phdthesis{phd-hune,
  author =              {Hune, Thomas},
  title =               {Analyzing real-time systems: theory and tools},
  year =                {2001},
  school =              {University of Aarhus, Denmark},
}

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

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

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

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

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

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

@inproceedings{tase2010-HZHSG,
  author =              {He, Fei and Zhu, He and Hung, William N. N. and
                         Song, Xiaoyu and Gu, Ming},
  title =               {Compositional Abstraction Refinement for Timed
                         Systems},
  editor =              {Liu, Jing and Peled, Doron A. and Wang, Bow-Yaw and
                         Wang, Farn},
  booktitle =           {{P}roceedings of the 4th {I}nternational {S}ymposium
                         on {T}heoretical {A}spects of {S}oftware
                         {E}ngineering ({TASE}'10)},
  acronym =             {{TASE}'10},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {168-176},
  year =                {2010},
  month =               aug,
  doi =                 {10.1109/TASE.2010.27},
}