Nicolas Markey

@inproceedings{lics2003-vD,
  author =              {van Drimmelen, Govert},
  title =               {Satisfiability in Alternating-time Temporal Logic},
  booktitle =           {{P}roceedings of the 18th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'03)},
  acronym =             {{LICS}'03},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {208-217},
  year =                {2003},
  month =               jun,
}

@phdthesis{phd-dacosta,
  author =              {Da{~}Costa, Arnaud},
  title =               {Propri{\'e}t{\'e}s de jeux multi-agents},
  year =                {2011},
  month =               sep,
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {Th\`ese de doctorat},
}

@inproceedings{esslli1994-Dam,
  author =              {Dam, Mads},
  title =               {Temporal Logic, Automata and Classical Theories},
  booktitle =           {{P}roceedings of the 6th {E}uropean {S}ummer
                         {S}chool in {L}ogic, {L}anguage and {I}nformation
                         ({ESSLLI}'94)},
  acronym =             {{ESSLLI}'94},
  year =                {1994},
  month =               aug,
}

@article{tcs126(1)-Dam,
  author =              {Dams, Dennis Ren{\'e}},
  title =               {{CTL{\textsuperscript{*}}} and
                         {ECTL{\textsuperscript{*}}} as fragments of the
                         modal {{\(\mu\)}}-calculus},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {126},
  number =              {1},
  pages =               {77-96},
  year =                {1994},
  month =               apr,
}

@article{jigpl7(1)-Dam,
  author =              {Dams, Dennis Ren{\'e}},
  title =               {Flat Fragments of {CTL} and {CTL}{\(^*\)}:
                         Separating the Expressive and Distinguishing Powers},
  publisher =           {Oxford University Press},
  journal =             {Logic Journal of the IGPL},
  volume =              {7},
  number =              {1},
  pages =               {55-78},
  year =                {1999},
  month =               jan,
}

@article{tcs302(1-3)-Dang,
  author =              {Dang, Zhe},
  title =               {Pushdown Timed Automata: A~Binary Reachability
                         Characterization and Safety Verification},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {302},
  number =              {1-3},
  pages =               {93-121},
  year =                {2003},
  month =               jun,
}

@inproceedings{acc2010-DBMM,
  author =              {Deng, Kun and Barooah, Prabir and Mehta, Prashant G.
                         and Meyn, Sean P.},
  title =               {Building thermal model reduction via aggregation of
                         states},
  booktitle =           {Proceedings of the 2010 American Control Conference
                         ({ACC}'10)},
  acronym =             {{ACC}'10},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {5118-5123},
  year =                {2010},
  month =               jun,
  doi =                 {10.1109/ACC.2010.5530470},
}

@incollection{thgraph-DBR67,
  author =              {Dantzig, George B. and Blattner, W. O. and Rao, M.
                         R.},
  title =               {Finding a Cycle in a Graph with Minimum Cost to Time
                         Ratio with Application to a Ship Routing Problem},
  editor =              {Rosenstiehl, Pierre},
  booktitle =           {Theory of Graphs},
  publisher =           {Gordon and Breach Science Publishers},
  pages =               {77-84},
  year =                {1967},
}

Résumé

In this paper, we use the constructs of branching temporal logic to formalize reasoning about a class of general flow systems, including discrete-time transition systems, continuous-time differential inclusions, and hybrid-time systems such as hybrid automata. We introduce Full General Flow Logic, GFL*, which has essentially the same syntax as the well-known Full Computation Tree Logic, CTL*, but generalizes the semantics to general flow systems over arbitrary time-lines. We propose an axiomatic proof system for GFL* and establish its soundness w.r.t. the general flow semantics.

@inproceedings{hscc2004-DCMM,
  author =              {Davoren, Jennifer M. and Coulthard, Vaughan and
                         Markey, Nicolas and Moor, Thomas},
  title =               {Non-deterministic Temporal Logics for General Flow
                         Systems},
  editor =              {Alur, Rajeev and Pappas, George J.},
  booktitle =           {{P}roceedings of the 7th {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
                         ({HSCC}'04)},
  acronym =             {{HSCC}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2993},
  pages =               {280-295},
  year =                {2004},
  month =               mar,
  doi =                 {10.1007/978-3-540-24743-2_19},
  abstract =            {In this paper, we use the constructs of branching
                         temporal logic to formalize reasoning about a class
                         of general flow systems, including discrete-time
                         transition systems, continuous-time differential
                         inclusions, and hybrid-time systems such as hybrid
                         automata. We introduce Full General Flow Logic,
                         GFL\(^*\), which has essentially the same syntax as
                         the well-known Full Computation Tree Logic,
                         CTL\(^*\), but generalizes the semantics to general
                         flow systems over arbitrary time-lines. We propose
                         an axiomatic proof system for GFL\(^*\) and
                         establish its soundness w.r.t. the general flow
                         semantics.},
}

@techreport{LSV-03-11-DD,
  author =              {Demri, St{\'e}phane and D'Souza, Deepak},
  title =               {An Automata-Theoretic Approach to Constraint {LTL}},
  number =              {LSV-03-11},
  year =                {2003},
  month =               aug,
  institution =         {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {Research Report},
}

@article{scp77(10-11)-DDDHPSWW,
  author =              {Damm, Werner and Dierks, Henning and Disch, Stefan
                         and Hagemann, Willem and Pigorsch, Florian and
                         Scholl, Christoph and Waldmann, Uwe and Wirtz,
                         Boris},
  title =               {Exact and fully symbolic verification of linear
                         hybrid automata with large discrete state spaces},
  publisher =           {Elsevier},
  journal =             {Science of Computer Programming},
  volume =              {77},
  number =              {10-11},
  pages =               {1122-1150},
  year =                {2012},
  month =               sep,
  doi =                 {10.1016/j.scico.2011.07.006},
}

@inproceedings{lfcs2007-DDG,
  author =              {Demri, St{\'e}phane and D'Souza, Deepak and Gascon,
                         R{\'e}gis},
  title =               {Decidable Temporal Logic with Repeating Values},
  editor =              {Artemov, Sergei N. and Nerode, Anil},
  booktitle =           {{P}roceedings of the {I}nternational {S}ymposium
                         {L}ogical {F}oundations of {C}omputer {S}cience
                         ({LFCS}'07)},
  acronym =             {{LFCS}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4514},
  pages =               {180-194},
  year =                {2007},
  month =               jun,
}

@inproceedings{csl2010-DDGRT,
  author =              {Degorre, Aldric and Doyen, Laurent and Gentilini,
                         Raffaella and Raskin, Jean-Fran{\c c}ois and
                         Toru{\'n}czyk, Szymon},
  title =               {Energy and Mean-Payoff Games with Imperfect
                         Information},
  editor =              {Dawar, Anuj and Veith, Helmut},
  booktitle =           {{P}roceedings of the 24th {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'10)},
  acronym =             {{CSL}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6247},
  pages =               {260-274},
  year =                {2010},
  month =               aug,
  doi =                 {10.1007/978-3-642-15205-4_22},
}

@inproceedings{nasafm2013-DDLLM,
  author =              {David, Alexandre and Du, Dehui and Larsen, Kim
                         Guldstrand and Legay, Axel and Miku{\v{c}}ionis,
                         Marius},
  title =               {Optimizing Control Strategy Using Statistical Model
                         Checking},
  editor =              {Brat, Guillaume and Rungta, Neha and Venet, Arnaud},
  booktitle =           {{P}roceedings of the th {NASA} {F}ormal {M}ethods
                         {S}ymposium ({NFM}'13)},
  acronym =             {{NFM}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7871},
  pages =               {352-367},
  year =                {2013},
  month =               may,
  doi =                 {10.1007/978-3-642-38088-4_24},
}

Résumé

In a former paper, we defined a new semantics for timed automata, the Almost ASAP semantics, which is parameterized by Δ to cope with the reaction delay of the controller. We showed that this semantics is implementable provided there exists a strictly positive value for the parameter Δ for which the strategy is correct. In this paper, we define the implementability problem to be the question of existence of such a Δ. We show that this question is closely related to a notion of robustness for timed automata defined in (A. Puri: Dynamical Properties of Timed Automata. FTRTFT, 1998) and prove that the implementability problem is decidable.

@inproceedings{ftrtft2004-DDMR,
  author =              {De{~}Wulf, Martin and Doyen, Laurent and Markey,
                         Nicolas and Raskin, Jean-Fran{\c c}ois},
  title =               {Robustness and Implementability of Timed Automata},
  editor =              {Lakhnech, Yassine and Yovine, Sergio},
  booktitle =           {{P}roceedings of the {J}oint {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'04) and {F}ormal
                         {T}echniques in {R}eal-Time and {F}ault-Tolerant
                         {S}ystems ({FTRTFT}'04)},
  acronym =             {{FORMATS-FTRTFT}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3253},
  pages =               {118-133},
  year =                {2004},
  month =               sep,
  doi =                 {10.1007/978-3-540-30206-3_10},
  abstract =            {In a former paper, we defined a new semantics for
                         timed automata, the Almost ASAP semantics, which is
                         parameterized by \(\Delta\) to cope with the
                         reaction delay of the controller. We showed that
                         this semantics is implementable provided there
                         exists a strictly positive value for the parameter
                         \(\Delta\) for which the strategy is correct. In
                         this paper, we define the implementability problem
                         to be the question of existence of such a
                         \(\Delta\). We show that this question is closely
                         related to a notion of robustness for timed automata
                         defined in (A.~Puri: \textit{Dynamical Properties of
                         Timed Automata}. FTRTFT, 1998) and prove that the
                         implementability problem is decidable.},
}

Résumé

Timed automata are governed by an idealized semantics that assumes a perfectly precise behavior of the clocks. The traditional semantics is not robust because the slightest perturbation in the timing of actions may lead to completely different behaviors of the automaton. Following several recent works, we consider a relaxation of this semantics, in which guards on transitions are widened by Δ>0 and clocks can drift by ε>0. The relaxed semantics encompasses the imprecisions that are inevitably present in an implementation of a timed automaton, due to the finite precision of digital clocks.

We solve the safety verification problem for this robust semantics: given a timed automaton and a set of bad states, our algorithm decides if there exist positive values for the parameters Δ and ε such that the timed automaton never enters the bad states under the relaxed semantics.

@article{fmsd33(1-3)-DDMR,
  author =              {De{~}Wulf, Martin and Doyen, Laurent and Markey,
                         Nicolas and Raskin, Jean-Fran{\c c}ois},
  title =               {Robust Safety of Timed Automata},
  publisher =           {Springer-Verlag},
  journal =             {Formal Methods in System Design},
  volume =              {33},
  number =              {1-3},
  pages =               {45-84},
  year =                {2008},
  month =               dec,
  doi =                 {10.1007/s10703-008-0056-7},
  abstract =            {Timed automata are governed by an idealized
                         semantics that assumes a perfectly precise behavior
                         of the clocks. The traditional semantics is not
                         robust because the slightest perturbation in the
                         timing of actions may lead to completely different
                         behaviors of the automaton. Following several recent
                         works, we consider a relaxation of this semantics,
                         in which guards on transitions are widened
                         by~\(\Delta>0\) and clocks can drift
                         by~\(\epsilon>0\). The relaxed semantics encompasses
                         the imprecisions that are inevitably present in an
                         implementation of a timed automaton, due to the
                         finite precision of digital clocks.\par We solve the
                         safety verification problem for this robust
                         semantics: given a timed automaton and a set of bad
                         states, our algorithm decides if there exist
                         positive values for the parameters~\(\Delta\)
                         and~\(\epsilon\) such that the timed automaton never
                         enters the bad states under the relaxed semantics.},
}

@inproceedings{hscc2004-DDR,
  author =              {De{~}Wulf, Martin and Doyen, Laurent and Raskin,
                         Jean-Fran{\c c}ois},
  title =               {Almost {ASAP} Semantics: From Timed Models to Timed
                         Implementations},
  editor =              {Alur, Rajeev and Pappas, George J.},
  booktitle =           {{P}roceedings of the 7th {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
                         ({HSCC}'04)},
  acronym =             {{HSCC}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2993},
  pages =               {296-310},
  year =                {2004},
  month =               mar,
}

@article{fac17(3)-DDR,
  author =              {De{~}Wulf, Martin and Doyen, Laurent and Raskin,
                         Jean-Fran{\c c}ois},
  title =               {Almost {ASAP} Semantics: From Timed Models to Timed
                         Implementations},
  publisher =           {Springer-Verlag},
  journal =             {Formal Aspects of Computing},
  volume =              {17},
  number =              {3},
  pages =               {319-341},
  year =                {2005},
}

@article{tcs127(1)-Dea,
  author =              {De{~}Agostino, Sergio},
  title =               {{P}-complete problems in data compression},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {127},
  number =              {1},
  pages =               {181-186},
  year =                {1994},
  month =               may,
}

@article{tcs234(1-2)-Dea,
  author =              {De{~}Agostino, Sergio},
  title =               {Erratum to {"}{P}-complete Problems in Data
                         Compression{"}},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {234},
  number =              {1-2},
  pages =               {325-326},
  year =                {2000},
  month =               mar,
}

@phdthesis{phd-dewulf,
  author =              {De{~}Wulf, Martin},
  title =               {From Timed Models to Timed Implementations},
  year =                {2006},
  month =               dec,
  school =              {D{\'e}partement d'Informatique, Universit{\'e} Libre
                         de Bruxelles, Belgium},
  type =                {Th\`ese de doctorat},
}

@inproceedings{cav2015-DEGM,
  author =              {Durand{-}Gasselin, Antoine and Esparza, Javier and
                         Ganty, Pierre and Majumdar, Rupak},
  title =               {Model Checking Parameterized Asynchronous
                         Shared-Memory Systems},
  editor =              {Kroening, Daniel and Pasareanu, Corina S.},
  booktitle =           {{P}roceedings of the 27th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'15)},
  acronym =             {{CAV}'15},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9206},
  pages =               {67-84},
  year =                {2015},
  month =               jul,
  doi =                 {10.1007/978-3-319-21690-4_5},
}

@article{tcs313(3)-DFFN,
  author =              {Demaine, Erik D. and Fleischer, Rudolf and Fraenkel,
                         Aviezri S. and Nowakowski, Richard J.},
  title =               {Appendix~{B}: {O}pen Problems at the 2002 {D}agstuhl
                         Seminar on Algebraic Combinatorial Game Theory},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {313},
  number =              {3},
  pages =               {539-543},
  year =                {2004},
  month =               feb,
}

@inproceedings{icalp2000-DG,
  author =              {Diekert, Volker and Gastin, Paul},
  title =               {{LTL} is Expressively Complete for {M}azurkiewicz
                         Traces},
  editor =              {Montanari, Ugo and Rolim, Jos\'e D. P. and Welzl,
                         Emo},
  booktitle =           {{P}roceedings of the 27th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'00)},
  acronym =             {{ICALP}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1853},
  pages =               {211-222},
  year =                {2000},
  month =               jul,
}

@inproceedings{aiml2000-DG,
  author =              {Davoren, Jennifer M. and Gore, Rajeev Prabhakar},
  title =               {Bimodal Logics for Reasoning about Continuous
                         Dynamics},
  editor =              {de Rijke, Marteen and Wansing, Heinrich and Wolter,
                         Frank and Zakharyaschev, Michael},
  booktitle =           {{P}roceedings of the 3rd {W}orkshop on {A}dvances in
                         {M}odal {L}ogic ({AIML}'00)},
  acronym =             {{AIML}'00},
  publisher =           {World Scientific},
  year =                {2002},
  confyear =            {2000},
  confmonth =           {10},
}

@article{tcs380(1-2)-DG,
  author =              {Droste, Manfred and Gastin, Paul},
  title =               {Weighted automata and weighted logics},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {380},
  number =              {1-2},
  pages =               {69-86},
  year =                {2007},
  month =               jun,
}

@inproceedings{csl2008-DG,
  author =              {Dawar, Anuj and Gr{\"a}del, Erich},
  title =               {The Descriptive Complexity of Parity Games},
  editor =              {Kaminski, Michael and Martini, Simone},
  booktitle =           {{P}roceedings of the 22nd {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'08)},
  acronym =             {{CSL}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5213},
  pages =               {354-368},
  year =                {2008},
  month =               sep,
  doi =                 {10.1007/978-3-540-87531-4_26},
}

@incollection{lahp2008-DG,
  author =              {Diekert, Volker and Gastin, Paul},
  title =               {First-order definable languages},
  editor =              {Flum, J{\"o}rg and Gr{\"a}del, Erich and Wilke,
                         Thomas},
  booktitle =           {Logic and Automata: History and Perspectives},
  publisher =           {Amsterdam University Press},
  series =              {Texts in Logic and Games},
  volume =              {2},
  pages =               {261-306},
  year =                {2008},
}

@article{jlc19(6)-DG,
  author =              {Demri, St{\'e}phane and Gascon, R{\'e}gis},
  title =               {The Effects of Bounding Syntactic Resources on
                         {P}resburger~{LTL}},
  publisher =           {Oxford University Press},
  journal =             {Journal of Logic and Computation},
  volume =              {19},
  number =              {6},
  pages =               {1541-1575},
  year =                {2009},
  month =               dec,
  doi =                 {10.1093/logcom/exp037},
}

@article{siamcomp39(1)-DGP,
  author =              {Daskalakis, Constantinos and Goldberg, Paul W. and
                         Papadimitriou, {\relax Ch}ristos H.},
  title =               {The complexity of computing a {N}ash equilibrium},
  publisher =           {Society for Industrial and Applied Math.},
  journal =             {SIAM Journal on Computing},
  volume =              {39},
  number =              {1},
  pages =               {195-259},
  year =                {2009},
}

@techreport{CFV-2009-121-DGR,
  author =              {Doyen, Laurent and Gentilini, Raffaella and Raskin,
                         Jean-Fran{\c c}ois},
  title =               {Faster Pseudo-Polynomial Algorithms for Mean-Payoff
                         Games},
  number =              {2009-121},
  year =                {2009},
  institution =         {CFV},
  type =                {Technical Report},
}

@inproceedings{formats2009-DGRR,
  author =              {Doyen, Laurent and Geeraerts, Gilles and Raskin,
                         Jean-Fran{\c c}ois and Reichert, Julien},
  title =               {Realizability of Real-Time Logics},
  editor =              {Ouaknine, Jo{\"e}l and Vaandrager, Frits},
  booktitle =           {{P}roceedings of the 7th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'09)},
  acronym =             {{FORMATS}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5813},
  pages =               {133-148},
  year =                {2009},
  month =               sep,
}

@inproceedings{formats2010-DGRS,
  author =              {Di{~}Giampaolo, Barbara and Geeraerts, Gilles and
                         Raskin, Jean-Fran{\c c}ois and Sznajder, Tali},
  title =               {Safraless procedures for timed specifications},
  editor =              {Chatterjee, Krishnendu and Henzinger, Thomas A.},
  booktitle =           {{P}roceedings of the 8th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'10)},
  acronym =             {{FORMATS}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6246},
  pages =               {2-22},
  year =                {2010},
  month =               sep,
}

@inproceedings{cav1999-DGV,
  author =              {Daniele, Marco and Giunchiglia, Fausto and Vardi,
                         Moshe Y.},
  title =               {Improved Automata Generation for Linear Temporal
                         Logic},
  editor =              {Halbwachs, Nicolas and Peled, Doron A.},
  booktitle =           {{P}roceedings of the 11th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'99)},
  acronym =             {{CAV}'99},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1633},
  pages =               {249-260},
  year =                {1999},
  month =               jul,
}

@article{jsl65(1)-DH,
  author =              {D{'}Agostino, Giovanna and Hollenberg, Marco},
  title =               {Logical Questions Concerning the
                         {{\(\mu\)}}-Calculus: Interpolation, Lyndon and
                         {\L}o{\'s}-Tarski},
  publisher =           {Association for Symbolic Logic},
  journal =             {Journal of Symbolic Logic},
  volume =              {65},
  number =              {1},
  pages =               {310-332},
  year =                {2000},
  month =               mar,
  doi =                 {10.2307/2586539},
}

@inproceedings{formats2006-DHLP,
  author =              {David, Alexandre and H{\aa}kansson, John and Larsen,
                         Kim Guldstrand and Pettersson, Paul},
  title =               {Model Checking Timed Automata with Priorities Using
                         {DBM} Subtraction},
  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 =               {128-142},
  year =                {2006},
  month =               sep,
  doi =                 {10.1007/11867340_10},
}

@article{tcs253(1)-dierks,
  author =              {Dierks, Henning},
  title =               {{PLC}-automata: a new class of implementable
                         real-time automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {253},
  number =              {1},
  pages =               {61-93},
  year =                {2001},
  month =               feb,
}

@inproceedings{vvps2005-dierks,
  author =              {Dierks, Henning},
  title =               {Finding Optimal Plans for Domains with Continuous
                         Effects with {UPPAAL} {C}ora},
  booktitle =           {{P}roceedings of the {ICAPS}'05 {W}orkshop on
                         {V}erification and {V}alidation of {M}odel-Based
                         {P}lanning and {S}chedulin {S}ystems ({VV\&PS}'05)},
  acronym =             {{VV\&PS}'05},
  year =                {2005},
  month =               jun,
}

@article{nm1()-Dij,
  author =              {Dijkstra, Edsger W.},
  title =               {A~note on two problems in connexion with graphs},
  publisher =           {Springer-Verlag},
  journal =             {Numerische Mathematik},
  volume =              {1},
  pages =               {269-271},
  year =                {1959},
  doi =                 {10.1007/BF01386390},
}

@inproceedings{avmfss1989-dill,
  author =              {Dill, David L.},
  title =               {Timing Assumptions and Verification of Finite-State
                         Concurrent Systems},
  editor =              {Sifakis, Joseph},
  booktitle =           {{P}roceedings of the {I}nternational {W}orkshop on
                         {A}utomatic {V}erification {M}ethods for {F}inite
                         {S}tate {S}ystems ({AVMFSS}'89)},
  acronym =             {{AVMFSS}'89},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {407},
  pages =               {197-212},
  year =                {1990},
  confyear =            {1989},
  confmonth =           {6},
  doi =                 {10.1007/3-540-52148-8_17},
}

@inproceedings{stacs2000-Dim,
  author =              {Dima, C{\u a}t{\u a}lin},
  title =               {Real-Time Automata and the {K}leene Algebra of Sets
                         of Real Numbers},
  editor =              {Reichel, Horst and Tison, Sophie},
  booktitle =           {{P}roceedings of the 17th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'00)},
  acronym =             {{STACS}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1770},
  pages =               {279-289},
  year =                {2000},
  month =               mar,
}

@article{jalc6(1)-Dim,
  author =              {Dima, C{\u a}t{\u a}lin},
  title =               {Real-time automata},
  journal =             {Journal of Automata, Languages and Combinatorics},
  volume =              {6},
  number =              {1},
  pages =               {3-23},
  year =                {2001},
  doi =                 {10.25596/jalc-2001-003},
}

@inproceedings{lics2002-Dim,
  author =              {Dima, C{\u a}t{\u a}lin},
  title =               {Computing Reachability Relations in Timed Automata},
  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 =               {177-186},
  year =                {2002},
  month =               jul,
}

@inproceedings{formats2007-Dim,
  author =              {Dima, C{\u a}t{\u a}lin},
  title =               {Dynamical Properties of Timed Automata Revisited},
  editor =              {Raskin, Jean-Fran{\c c}ois and Thiagarajan, P. S.},
  booktitle =           {{P}roceedings of the 5th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'07)},
  acronym =             {{FORMATS}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4763},
  pages =               {130-146},
  year =                {2007},
  month =               oct,
}

@inproceedings{tacas2003-DJJPPSWZ,
  author =              {Dembinski, Piotr and Janowska, Agata and Janowski,
                         Pawe{\l} and Penczek, Wojciech and P{\'o}lrola,
                         Agata and Szreter, Maciej and Wo{\'z}na, Bo{\.z}na
                         and Zbrzezny, Andrzej},
  title =               {Verics: A~Tool for Verifying Timed Automata and
                         Estelle Specifications},
  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 =               {278-283},
  year =                {2003},
  month =               apr,
}

@article{jcss79(1)-DJLL,
  author =              {Demri, St{\'e}phane and Jurdzi{\'n}ski, Marcin and
                         Lachish, Oded and Lazi{\'c}, Ranko},
  title =               {The covering and boundedness problems for branching
                         vector addition systems},
  publisher =           {Elsevier},
  journal =             {Journal of Computer and System Sciences},
  volume =              {79},
  number =              {1},
  pages =               {23-38},
  year =                {2013},
  month =               feb,
  doi =                 {10.1016/j.jcss.2012.04.002},
}

Résumé

The problem of synchronizing automata is concerned with the existence of a word that sends all states ofM the automaton to one and the same state. This problem has classically been studied for complete deterministic finite automata, with the existence problem being NLOGSPACE-complete.

In this paper we consider synchronizing-word problems for weighted and timed automata. We consider the synchronization problem in several variants and combinations of these, including deterministic and non-deterministic timed and weighted automata, synchronization to unique location with possibly different clock valuations or accumulated weights, as well as synchronization with a safety condition forbidding the automaton to visit states outside a safety-set during synchronization (e.g. energy constraints). For deterministic weighted automata, the synchronization problem is proven PSPACE-complete under energy constraints, and in 3-EXPSPACE under general safety constraints. For timed automata the synchronization problems are shown to be PSPACE-complete in the deterministic case, and undecidable in the non-deterministic case.

@inproceedings{fsttcs2014-DJLMS,
  author =              {Doyen, Laurent and Juhl, Line and Larsen, Kim
                         Guldstrand and Markey, Nicolas and Shirmohammadi,
                         Mahsa},
  title =               {Synchronizing words for weighted and timed automata},
  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 =               {121-132},
  year =                {2014},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2014.121},
  abstract =            {The problem of synchronizing automata is concerned
                         with the existence of a word that sends all states
                         ofM the automaton to one and the same state. This
                         problem has classically been studied for complete
                         deterministic finite automata, with the existence
                         problem being NLOGSPACE-complete.\par In this paper
                         we consider synchronizing-word problems for weighted
                         and timed automata. We consider the synchronization
                         problem in several variants and combinations of
                         these, including deterministic and non-deterministic
                         timed and weighted automata, synchronization to
                         unique location with possibly different clock
                         valuations or accumulated weights, as well as
                         synchronization with a safety condition forbidding
                         the automaton to visit states outside a safety-set
                         during synchronization (e.g. energy constraints).
                         For deterministic weighted automata, the
                         synchronization problem is proven PSPACE-complete
                         under energy constraints, and in 3-EXPSPACE under
                         general safety constraints. For timed automata the
                         synchronization problems are shown to be
                         PSPACE-complete in the deterministic case, and
                         undecidable in the non-deterministic case.},
}

@inproceedings{tacas2015-DLLMW,
  author =              {David, Alexandre and Jensen, Peter Gj{\o}l and
                         Larsen, Kim Guldstrand and Miku{\v{c}}ionis, Marius
                         and Taankvist, Jakob Haar},
  title =               {Uppaal Stratego},
  editor =              {Baier, {\relax Ch}ristel and Tinelli, Cesare},
  booktitle =           {{P}roceedings of the 21st {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'15)},
  acronym =             {{TACAS}'15},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9035},
  pages =               {206-211},
  year =                {2015},
  month =               apr,
  doi =                 {10.1007/978-3-662-46681-0_16},
}

@inproceedings{lics1997-DJW,
  author =              {Dziembowski, Stefan and Jurdzi{\'n}ski, Marcin and
                         Walukiewicz, Igor},
  title =               {How Much Memory is Needed to Win Infinite Games},
  booktitle =           {{P}roceedings of the 12th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'97)},
  acronym =             {{LICS}'97},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {99-110},
  year =                {1997},
  month =               jun,
}

@inproceedings{formats06-DK,
  author =              {Daws, Conrado and Kordy, Piotr},
  title =               {Symbolic robustness analysis of timed automata},
  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 =               {143-155},
  year =                {2006},
  month =               sep,
}

@inproceedings{formats2007-DKL,
  author =              {Dierks, Henning and Kupferschmid, Sebastian and
                         Larsen, Kim Guldstrand},
  title =               {Automatic abstraction refinement for timed automata},
  editor =              {Raskin, Jean-Fran{\c c}ois and Thiagarajan, P. S.},
  booktitle =           {{P}roceedings of the 5th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'07)},
  acronym =             {{FORMATS}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4763},
  pages =               {114-129},
  year =                {2007},
  month =               oct,
  doi =                 {10.1007/978-3-540-75454-1_10},
}

@inproceedings{icalp2009-DKL,
  author =              {Dax, Christian and Klaedtke, Felix and Lange,
                         Martin},
  title =               {On Regular Temporal Logics with Past},
  editor =              {Albers, Susanne and Marchetti{-}Spaccamela Alberto
                         and Matias, Yossi and Nikoletseas, Sotiris and
                         Thomas, Wolfgang},
  booktitle =           {{P}roceedings of the 36th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'09)~-- Part~{II}},
  acronym =             {{ICALP}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5556},
  pages =               {175-187},
  year =                {2009},
  month =               jul,
  doi =                 {10.1007/978-3-642-02930-1_15},
}

@inproceedings{icalp2015-DKMSZ,
  author =              {Datta, Samir and Kulkarni, Raghav and Mukherjee,
                         Anish and Schwentick, Thomas and Zeume, Thomas},
  title =               {Reachability is in {D}yn{F}O},
  editor =              {Halld{\'o}rsson, Magn{\'u}s M. and Iwana, Kazuo and
                         Kobayashi, Naoki and Speckmann, Bettina},
  booktitle =           {{P}roceedings of the 42nd {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'15)~-- Part~{II}},
  acronym =             {{ICALP}'15},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9135},
  pages =               {159-170},
  year =                {2015},
  month =               jul,
  doi =                 {10.1007/978-3-662-47666-6_13},
}

@article{tcs83(1)-DKP,
  author =              {Dershowitz, Nachum and Kaplan, St{\'e}phane and
                         Plaisted, David A.},
  title =               {Rewrite, Rewrite, Rewrite, Rewrite, Rewrite,~...},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {83},
  number =              {1},
  pages =               {71-96},
  year =                {1991},
}

@article{fundi84(3-4)-DKR,
  author =              {Droste, Manfred and Kuich, Werner and Rahonis,
                         George},
  title =               {Multi-Valued {MSO} Logics over Words and Trees},
  publisher =           {IOS Press},
  journal =             {Fundamenta Informaticae},
  volume =              {84},
  number =              {13-4},
  pages =               {305-327},
  year =                {2008},
}

@inproceedings{gandalf2017-DKRS,
  author =              {Droste, Manfred and Kutsia, Temur and Rahonis,
                         George and Schreiner, Wolfgang},
  title =               {{MK}-fuzzy Automata and {MSO} Logics},
  editor =              {Bouyer, Patricia and Orlandini, Andrea and
                         San{~}Pietro, Pierluigi},
  booktitle =           {{P}roceedings of the 8th {I}nternational {S}ymposium
                         on {G}ames, {A}utomata, {L}ogics and {F}ormal
                         {V}erification ({GandALF}'17)},
  acronym =             {{GandALF}'17},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {256},
  pages =               {106-120},
  year =                {2017},
  month =               sep,
  doi =                 {10.4204/EPTCS.256.8},
}

@book{hwa-DKV,
  title =               {Handbook of Weighted Automata},
  editor =              {Droste, Manfred and Kuich, Werner and Vogler,
                         Walter},
  booktitle =           {Handbook of Weighted Automata},
  publisher =           {Springer-Verlag},
  year =                {2009},
}

@inproceedings{ecai1994-DGL,
  author =              {De{~}Giacomo, Giuseppe and Lenzerini, Maurizio},
  title =               {Concept Language with Number Restrictions and
                         Fixpoints, and its Relationship with Mu-Calculus},
  editor =              {Cohn, Anthony G.},
  booktitle =           {{P}roceedings of the 11th {E}uropean {C}onference on
                         {A}rtificial {I}ntelligence ({ECAI}'94)},
  acronym =             {{ECAI}'94},
  publisher =           {John Wiley \& Sons},
  pages =               {411-415},
  year =                {1994},
  month =               aug,
}

@inproceedings{atva2016-DLFMRX,
  author =              {Duret{-}Lutz, Alexandre and Lewkowicz, Alexandre and
                         Fauchille, Amaury and Michaud, Thibault and Renault,
                         {\'E}tienne and Xu, Laurent},
  title =               {Spot~2.0~-- {A}~Framework for {LTL} and
                         {{\(\omega\)}}-Automata Manipulation},
  editor =              {Artho, Cyrille and Legay, Axel and Peled, Doron A.},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {S}ymposium on {A}utomated {T}echnology for
                         {V}erification and {A}nalysis ({ATVA}'16)},
  acronym =             {{ATVA}'16},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9938},
  pages =               {122-129},
  year =                {2016},
  month =               oct,
  doi =                 {10.1007/978-3-319-46520-3_8},
}

@inproceedings{isola2012-DLLM,
  author =              {David, Alexandre and Larsen, Kim Guldstrand and
                         Legay, Axel and Miku{\v{c}}ionis, Marius},
  title =               {Schedulability of {H}erschel-{P}lanck Revisited
                         Using Statistical Model Checking},
  editor =              {Margaria, Tiziana and Steffen, Bernhard},
  booktitle =           {{P}roceedings of the 5th {I}nternational {S}ymposium
                         on {L}everaging {A}pplications of {F}ormal {M}ethods
                         ({IS}o{LA}'12)~-- {P}art~{II}: {A}pplications and
                         {C}ase {S}tudies},
  acronym =             {{IS}o{LA}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7610},
  pages =               {293-307},
  year =                {2012},
  month =               oct,
  doi =                 {10.1007/978-3-642-34032-1},
}

@inproceedings{fmco2010-DLLMN,
  author =              {David, Alexandre and Larsen, Kim Guldstrand and Li,
                         Shuhao and Miku{\v{c}}ionis, Marius and Nielsen,
                         Brian},
  title =               {Testing Real-Time Systems under Uncertainty},
  booktitle =           {{R}evised {P}apers of the 13th {I}nternational
                         {C}onference on {F}ormal {M}ethods for {C}omponents
                         and {O}bjects ({FMCO}'10)},
  acronym =             {{FMCO}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6957},
  pages =               {352-371},
  year =                {2010},
  month =               dec,
  doi =                 {10.1007/978-3-642-25271-6_19},
}

@inproceedings{formats2011-DLLMPVW,
  author =              {David, Alexandre and Larsen, Kim Guldstrand and
                         Legay, Axel and Miku{\v{c}}ionis, Marius and
                         Poulsen, Danny B{\o}gsted and van Vliet, Jonas and
                         Wang, Zheng},
  title =               {Statistical Model Checking for Networks of Priced
                         Timed Automata},
  editor =              {Fahrenberg, Uli and Tripakis, Stavros},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'11)},
  acronym =             {{FORMATS}'11},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6919},
  pages =               {80-96},
  year =                {2011},
  month =               sep,
}

@inproceedings{cav2011-DLLMW,
  author =              {David, Alexandre and Larsen, Kim Guldstrand and
                         Legay, Axel and Miku{\v{c}}ionis, Marius and Wang,
                         Zheng},
  title =               {Time for Statistical Model Checking of Real-Time
                         Systems},
  editor =              {Gopalakrishnan, Ganesh and Qadeer, Shaz},
  booktitle =           {{P}roceedings of the 23rd {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'11)},
  acronym =             {{CAV}'11},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6806},
  pages =               {349-355},
  year =                {2011},
  month =               jul,
  doi =                 {10.1007/978-3-642-22110-1_27},
}

@inproceedings{date2008-DLLN,
  author =              {David, Alexandre and Larsen, Kim Guldstrand and Li,
                         Shuhao and Nielsen, Brian},
  title =               {A Game-Theoretic Approach to Real-Time System
                         Testing},
  booktitle =           {{P}roceedings of the 2008 {D}esign, {A}utomation and
                         {T}est in {E}urope ({DATE}'08)},
  acronym =             {{DATE}'08},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {486-491},
  year =                {2008},
  month =               mar,
}

@inproceedings{avocs2013-DLLP,
  author =              {David, Alexandre and Larsen, Kim Guldstrand and
                         Legay, Axel and Poulsen, Danny B{\o}gsted},
  title =               {Statistical Model Checking of Dynamic Networks of
                         Stochastic Hybrid Automata},
  editor =              {Schneider, Steve and Treharne, Helen},
  booktitle =           {{P}roceedings of the 13th {I}nternational {W}orkshop
                         on {A}utomated {V}erification of {C}ritical
                         {S}ystems ({AVOCS}'13)},
  acronym =             {{AVOCS}'13},
  publisher =           {European Association of Software Science and
                         Technology},
  series =              {Electronic Communications of the EASST},
  volume =              {10},
  year =                {2013},
  month =               sep,
}

Résumé

We study the alternating-time temporal logics ATL and ATL* extended with strategy contexts: these make agents commit to their strategies during the evaluation of formulas, contrary to plain ATL and ATL* where strategy quantifiers reset previously selected strategies.

We illustrate the important expressive power of strategy contexts by proving that they make the extended logics, namely ATLsc and ATLsc*, equally expressive: any formula in ATLsc* can be translated into an equivalent, linear-size ATLsc formula. Despite the high expressiveness of these logics, we prove that they remain decidable by designing a tree-automata-based algorithm for model-checking ATLsc on the full class of n-player concurrent game structures.

@inproceedings{fsttcs2010-DLM,
  author =              {Da{~}Costa, Arnaud and Laroussinie, Fran{\c c}ois
                         and Markey, Nicolas},
  title =               {{ATL} with strategy contexts: Expressiveness and
                         Model Checking},
  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 =               {120-132},
  year =                {2010},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2010.120},
  abstract =            {We study the alternating-time temporal logics
                         \(\textsf{ATL}\) and~\(\textsf{ATL}^{*}\) extended
                         with strategy contexts: these make agents commit to
                         their strategies during the evaluation of formulas,
                         contrary to plain \(\textsf{ATL}\)
                         and~\(\textsf{ATL}^{*}\) where strategy quantifiers
                         reset previously selected strategies.\par We
                         illustrate the important expressive power of
                         strategy contexts by proving that they make the
                         extended logics, namely
                         \(\textsf{ATL}_{\textsf{sc}}\)
                         and~\(\textsf{ATL}_{\textsf{sc}}^{*}\), equally
                         expressive: any~formula
                         in~\(\textsf{ATL}_{\textsf{sc}}^{*}\) can be
                         translated into an equivalent, linear-size
                         \(\textsf{ATL}_{\textsf{sc}}\) formula. Despite the
                         high expressiveness of these logics, we prove that
                         they remain decidable by designing a
                         tree-automata-based algorithm for model-checking
                         \(\textsf{ATL}_{\textsf{sc}}\) on the full class of
                         \(n\)-player concurrent game structures.},
}

Résumé

While it was defined long ago, the extension of CTL with quantification over atomic propositions has never been studied extensively. Considering two different semantics (depending whether propositional quantification refers to the Kripke structure or to its unwinding tree), we study its expressiveness (showing in particular that QCTL coincides with Monadic Second-Order Logic for both semantics) and characterize the complexity of its model-checking problem, depending on the number of nested propositional quantifiers (showing that the structure semantics populates the polynomial hierarchy while the tree semantics populates the exponential hierarchy). We also show how these results apply to model checking ATL-like temporal logics for games.

@inproceedings{concur2012-DLM,
  author =              {Da{~}Costa, Arnaud and Laroussinie, Fran{\c c}ois
                         and Markey, Nicolas},
  title =               {Quantified~{CTL}: Expressiveness and Model Checking},
  editor =              {Koutny, Maciej and Ulidowski, Irek},
  booktitle =           {{P}roceedings of the 23rd {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'12)},
  acronym =             {{CONCUR}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7454},
  pages =               {177-192},
  year =                {2012},
  month =               sep,
  doi =                 {10.1007/978-3-642-32940-1_14},
  abstract =            {While it was defined long ago, the extension of CTL
                         with quantification over atomic propositions has
                         never been studied extensively. Considering two
                         different semantics (depending whether propositional
                         quantification refers to the Kripke structure or to
                         its unwinding tree), we study its expressiveness
                         (showing in particular that QCTL coincides with
                         Monadic Second-Order Logic for both semantics) and
                         characterize the complexity of its model-checking
                         problem, depending on the number of nested
                         propositional quantifiers (showing that the
                         structure semantics populates the polynomial
                         hierarchy while the tree semantics populates the
                         exponential hierarchy). We also show how these
                         results apply to model checking ATL-like temporal
                         logics for games.},
}

Résumé

QCTL extends the temporal logic CTL with quantification over atomic propositions. While the algorithmic questions for QCTL and its fragments with limited quantification depth are well-understood (e.g. satisfiability of QCTLk, with at most k nested blocks of quantifiers, is k+1-EXPTIME-complete), very few results are known about the expressiveness of this logic. We address such expressiveness questions in this paper. We first consider the distinguishing power of these logics (i.e., their ability to separate models), their relationship with behavioural equivalences, and their ability to capture the behaviours of finite Kripke structures with so-called characteristic formulas. We then consider their expressive power (i.e., their ability to express a property), showing that in terms of expressiveness the hierarchy QCTLk collapses at level 2 (in other terms, any QCTL formula can be expressed using at most two nested blocks of quantifiers).

@inproceedings{concur2016-DLM,
  author =              {David, Am{\'e}lie and Laroussinie, Fran{\c c}ois and
                         Markey, Nicolas},
  title =               {On~the expressiveness of~{QCTL}},
  editor =              {Desharnais, Jules and Jagadeesan, Radha},
  booktitle =           {{P}roceedings of the 27th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'16)},
  acronym =             {{CONCUR}'16},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {59},
  pages =               {28:1-28:15},
  year =                {2016},
  month =               aug,
  doi =                 {10.4230/LIPIcs.CONCUR.2016.28},
  abstract =            {QCTL extends the temporal logic CTL with
                         quantification over atomic propositions. While the
                         algorithmic questions for QCTL and its fragments
                         with limited quantification depth are
                         well-understood (e.g. satisfiability of
                         QCTL\textsuperscript{\(k\)}, with at most \(k\)
                         nested blocks of quantifiers, is
                         \(k+1\)-EXPTIME-complete), very few results are
                         known about the expressiveness of this logic.
                         We~address such expressiveness questions in this
                         paper. We first consider the \emph{distinguishing
                         power} of these logics (i.e.,~their ability to
                         separate models), their relationship with
                         behavioural equivalences, and their ability to
                         capture the behaviours of finite Kripke structures
                         with so-called characteristic formulas. We then
                         consider their \emph{expressive power} (i.e.,~their
                         ability to express a property), showing that in
                         terms of expressiveness the hierarchy
                         QCTL\textsuperscript{\(k\)} collapses at level~2
                         (in~other terms, any~QCTL formula can be expressed
                         using at most two nested blocks of quantifiers).},
}

@inproceedings{HLMOPRS-seaa2013,
  author =              {Dalsgaard, Peter H. and Le{~}Guilly, Thibault and
                         Middelhede, Daniel and Olsen, Petur and Pedersen,
                         Thomas and Ravn, Anders P. and Skou, Arne},
  title =               {A Toolchain for Home Automation Controller
                         Development},
  editor =              {Demir{\"o}rs, Onur and T{\"u}retken, Oktay},
  booktitle =           {{P}roceedings of the 39th {E}uromicro {C}onference
                         on {S}oftware {E}ngineering and {A}dvanced
                         {A}pplications ({SEAA}'13)},
  acronym =             {{SEAA}'13},
  pages =               {122-129},
  year =                {2013},
  month =               sep,
}

@incollection{mbdes2009-DLRS,
  author =              {David, Alexandre and Larsen, Kim Guldstrand and
                         Rasmussen, Jacob Illum and Skou, Arne},
  title =               {Model-based framework for schedulability analysis
                         using UPPAAL~4.1},
  editor =              {Nicolescu, Gabriela and Mosterman, Pieter J.},
  booktitle =           {Model-Based Design for Embedded Systems},
  publisher =           {CRC Press},
  series =              {Computational Analysis, Synthesis, and Design of
                         Dynamic Systems},
  pages =               {93-119},
  year =                {2009},
}

@inproceedings{stacs2002-DLS,
  author =              {Demri, St{\'e}phane and Laroussinie, Fran{\c c}ois
                         and Schnoebelen, {\relax Ph}ilippe},
  title =               {A Parametric Analysis of the State Explosion Problem
                         in Model Checking (Extended Abstract)},
  editor =              {Alt, Helmut and Ferreira, Afonso},
  booktitle =           {{P}roceedings of the 19th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'02)},
  acronym =             {{STACS}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2285},
  pages =               {620-631},
  year =                {2002},
  month =               mar,
}

@article{tcs411(22-24)-DLS,
  author =              {Demri, St{\'e}phane and Lazi{\'c}, Ranko and
                         Sangnier, Arnaud},
  title =               {Model checking memoryful linear-time logics over
                         one-counter automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {411},
  number =              {22-24},
  pages =               {2298-2316},
  year =                {2010},
  month =               may,
  doi =                 {10.1016/j.tcs.2010.02.021},
}

@article{res53(1)-DM1,
  author =              {Dasgupta, Partha and Maskin, Eric},
  title =               {The Existence of Equilibrium in Discontinuous
                         Economic Games, 1:~{T}heory},
  publisher =           {Oxford University Press},
  journal =             {The Review of Economic Studies},
  volume =              {53},
  number =              {1},
  pages =               {1-26},
  year =                {1986},
  month =               jan,
}

@article{res53(1)-DM2,
  author =              {Dasgupta, Partha and Maskin, Eric},
  title =               {The Existence of Equilibrium in Discontinuous
                         Economic Games, 2:~{A}pplications},
  publisher =           {Oxford University Press},
  journal =             {The Review of Economic Studies},
  volume =              {53},
  number =              {1},
  pages =               {27-41},
  year =                {1986},
  month =               jan,
}

@inproceedings{stacs2002-DM,
  author =              {D'Souza, Deepak and Madhusudan, Parthasarathy},
  title =               {Timed Control Synthesis for External Specifications},
  editor =              {Alt, Helmut and Ferreira, Afonso},
  booktitle =           {{P}roceedings of the 19th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'02)},
  acronym =             {{STACS}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2285},
  pages =               {571-582},
  year =                {2002},
  month =               mar,
}

@inproceedings{aamas2018-DM,
  author =              {Della{ }Monica, Dario and Murano, Aniello},
  title =               {Parity-energy {ATL} for Qualitative and Quantitative
                         Reasoning in~{MAS}},
  editor =              {Andr{\'e}, Elisabeth and Koenig, Sven and Dastani,
                         Mehdi and Sukthankar, Gita},
  booktitle =           {{P}roceedings of the 17th {I}nternational
                         {C}onference on {A}utonomous {A}gents and
                         {M}ultiagent {S}ystems ({AAMAS}'18)},
  acronym =             {{AAMAS}'18},
  publisher =           {International Foundation for Autonomous Agents and
                         Multiagent Systems},
  pages =               {1441-1449},
  year =                {2018},
  month =               jul,
}

@article{tocl19(3)-DMS,
  author =              {Dima, C{\u a}t{\u a}lin and Maubert, Bastien and
                         Pinchinat, Sophie},
  title =               {Relating Paths in Transition Systems: The~Fall of
                         the Modal Mu-Calculus},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {19},
  number =              {3},
  pages =               {23:1-23:33},
  year =                {2018},
  month =               sep,
  doi =                 {10.1145/3231596},
}

@inproceedings{mfcs2011-DMS,
  author =              {Doyen, Laurent and Massart, {\relax Th}ierry and
                         Shirmohammadi, Mahsa},
  title =               {Infinite Synchronizing Words for Probabilistic
                         Automata},
  editor =              {Murlak, Filip and Sankovski, Piotr},
  booktitle =           {{P}roceedings of the 36th {I}nternational
                         {S}ymposium on {M}athematical {F}oundations of
                         {C}omputer {S}cience ({MFCS}'13)},
  acronym =             {{MFCS}'11},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6907},
  pages =               {278-289},
  year =                {2011},
  month =               aug,
  doi =                 {10.1007/978-3-642-22993-0_27},
}

@techreport{mfcs2011-DMS-erratum,
  author =              {Doyen, Laurent and Massart, {\relax Th}ierry and
                         Shirmohammadi, Mahsa},
  title =               {Infinite Synchronizing Words for Probabilistic
                         Automata (erratum)},
  number =              {1206.0995},
  year =                {2012},
  month =               jun,
  institution =         {arXiv},
  type =                {Research Report},
}

@inproceedings{fossacs2014-DMS,
  author =              {Doyen, Laurent and Massart, {\relax Th}ierry and
                         Shirmohammadi, Mahsa},
  title =               {Limit synchronization in {M}arkov decision
                         processes},
  editor =              {Muscholl, Anca},
  booktitle =           {{P}roceedings of the 17th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'14)},
  acronym =             {{FoSSaCS}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8412},
  pages =               {58-72},
  year =                {2014},
  month =               apr,
  doi =                 {10.1007/978-3-642-54830-7_4},
}

@article{jcss100()-DMS,
  author =              {Doyen, Laurent and Massart, {\relax Th}ierry and
                         Shirmohammadi, Mahsa},
  title =               {The complexity of synchronizing {M}arkov decision
                         processes},
  publisher =           {Elsevier},
  journal =             {Journal of Computer and System Sciences},
  volume =              {100},
  pages =               {96-129},
  year =                {2019},
  month =               mar,
  doi =                 {10.1016/j.jcss.2018.09.004},
}

@article{ijfcs18(1)-DN,
  author =              {Demri, St{\'e}phane and Nowak, David},
  title =               {Reasoning about Transfinite Sequences},
  journal =             {International Journal of Foundations of Computer
                         Science},
  volume =              {18},
  number =              {1},
  pages =               {87-112},
  year =                {2007},
  month =               feb,
  doi =                 {10.1142/S0129054107004589},
}

@inproceedings{wcet2010-DOTHL,
  author =              {Dalsgaard, Andreas E. and Olesen, Mads Chr. and
                         Toft, Martin and Hansen, Ren{\'e} R. and Larsen, Kim
                         Guldstrand},
  title =               {METAMOC: Modular Execution Time Analysis using Model
                         Checking},
  editor =              {Lisper, Bj{\"o}rn},
  booktitle =           {{P}roceedings of the 10th {I}nternational {W}orkshop
                         on {W}orst-{C}ase {E}xecution {T}ime {A}nalysis
                         ({WCET}'10)},
  acronym =             {{WCET}'10},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {OpenAccess Series in Informatics},
  volume =              {15},
  pages =               {113-123},
  year =                {2010},
  month =               jul,
}

@inproceedings{hscc1995-DOTY,
  author =              {Daws, Conrado and Olivero, Alfredo and Tripakis,
                         Stavros and Yovine, Sergio},
  title =               {The tool {\scshape {K}ronos}},
  editor =              {Alur, Rajeev and Henzinger, Thomas A. and Sontag,
                         Eduardo D.},
  booktitle =           {{H}ybrid {S}ystems~{III}: {V}erification and
                         {C}ontrol ({HSCC}'95)},
  acronym =             {{HSCC}'95},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1066},
  pages =               {208-219},
  year =                {1996},
  confyear =            {1995},
  confmonth =           {10},
}

@phdthesis{phd-doyen,
  author =              {Doyen, Laurent},
  title =               {Algorithmic Analysis of Complex Semantics for Timed
                         and Hybrid Automata},
  year =                {2006},
  month =               jun,
  school =              {D{\'e}partement d'Informatique, Universit{\'e} Libre
                         de Bruxelles, Belgium},
  type =                {Th\`ese de doctorat},
}

@article{ipl102(5)-Doy,
  author =              {Doyen, Laurent},
  title =               {Robust parametric reachability for timed automata},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {102},
  number =              {5},
  pages =               {208-213},
  year =                {2007},
  month =               may,
  doi =                 {10.1016/j.ipl.2006.11.018},
}

@phdthesis{hdr-doyen,
  author =              {Doyen, Laurent},
  title =               {Games and Automata: From Boolean to Quantitative
                         Verification},
  year =                {2012},
  month =               mar,
  school =              {{\'E}cole Normale Sup{\'e}rieure de Cachan, France},
  type =                {M\'emoire d'habilitation},
}

@techreport{IISc-CSA-TR-2005-7-DP,
  author =              {D'Souza, Deepak and Prabhakar, Pavithra},
  title =               {On the Expressiveness of {MTL} in the Pointwise and
                         Continuous Semantics},
  number =              {IISc-CSA-TR-2005-7},
  year =                {2005},
  month =               may,
  institution =         {Indian Institute of Science, Bangalore, India},
  type =                {Technical Report},
}

@article{sttt9(1)-DP,
  author =              {D'Souza, Deepak and Prabhakar, Pavithra},
  title =               {On the Expressiveness of {MTL} in the Pointwise and
                         Continuous Semantics},
  publisher =           {Springer-Verlag},
  journal =             {International Journal on Software Tools for
                         Technology Transfer},
  volume =              {9},
  number =              {1},
  pages =               {1-4},
  year =                {2007},
  month =               feb,
  doi =                 {10.1007/s10009-005-0214-9},
}

@article{ejor183(2)-APP,
  author =              {D{'}Ariano, Andrea and Pacciarelli, Dario and
                         Pranzo, Marco},
  title =               {A~branch-and-bound algorithm for scheduling trains
                         in a railway network},
  publisher =           {Elsevier},
  journal =             {European Journal of Operational Research},
  volume =              {183},
  number =              {2},
  pages =               {643-657},
  year =                {2007},
  month =               dec,
  doi =                 {10.1016/j.ejor.2006.10.034},
}

@book{DPV06,
  author =              {Dasgupta, Sanjoy and Papadimitriou, {\relax
                         Ch}ristos H. and Vazirani, Vijay V.},
  title =               {Algorithms},
  publisher =           {McGraw-Hill},
  year =                {2006},
}

@book{BoT-DR,
  author =              {Diekert, Volker and Rozenberg, Grzegorz},
  title =               {The Book of Traces},
  publisher =           {World Scientific},
  year =                {1995},
}

@inproceedings{tacas2010-DR,
  author =              {Doyen, Laurent and Raskin, Jean-Fran{\c c}ois},
  title =               {Antichain Algorithms for Finite Automata},
  editor =              {Esparza, Javier and Majumdar, Rupak},
  booktitle =           {{P}roceedings of the 16th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'10)},
  acronym =             {{TACAS}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6015},
  pages =               {2-22},
  year =                {2010},
  month =               mar,
}

@article{sttt5(2-3)-DRV,
  author =              {Delzanno, Giorgio and Raskin, Jean-Fran{\c c}ois and
                         Van{~}Begin, Laurent},
  title =               {Covering sharing trees: a compact data structure for
                         parameterized verification},
  publisher =           {Springer-Verlag},
  journal =             {International Journal on Software Tools for
                         Technology Transfer},
  volume =              {5},
  number =              {2-3},
  pages =               {268-297},
  year =                {2004},
}

@inproceedings{stacs1998-DS,
  author =              {Demri, St{\'e}phane and Schnoebelen, {\relax
                         Ph}ilippe},
  title =               {The Complexity of Propositional Linear Temporal
                         Logics in Simple Cases (extended abstract)},
  editor =              {Morvan, Michel and Meinel, {\relax Ch}ristoph and
                         Krob, Daniel},
  booktitle =           {{P}roceedings of the 15th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'98)},
  acronym =             {{STACS}'98},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1373},
  pages =               {61-72},
  year =                {1998},
  month =               feb,
}

@article{icomp174(1)-DS,
  author =              {Demri, St{\'e}phane and Schnoebelen, {\relax
                         Ph}ilippe},
  title =               {The Complexity of Propositional Linear Temporal
                         Logics in Simple Cases},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {174},
  number =              {1},
  pages =               {84-103},
  year =                {2002},
  month =               apr,
}

@article{fundi53(1)-DS,
  author =              {Demri, St{\'e}phane and Sattler, Ulrike},
  title =               {Automata-Theoretic Decision Procedures for
                         Information Logics},
  publisher =           {IOS Press},
  journal =             {Fundamenta Informaticae},
  volume =              {53},
  number =              {1},
  pages =               {1-22},
  year =                {2002},
}

@inproceedings{stacs01-DSPK,
  author =              {Dang, Zhe and San{~}Pietro, Pierluigi and Kemmerer,
                         Richard A.},
  title =               {On {P}resburger Liveness of Discrete Timed Automata},
  editor =              {Ferreira, Afonso and Reichel, Horst},
  booktitle =           {{P}roceedings of the 18th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'01)},
  acronym =             {{STACS}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2010},
  pages =               {132-143},
  year =                {2001},
  month =               feb,
}

@inproceedings{cav2015-DSQBE,
  author =              {Desai, Ankush and Seshia,Sanjit A. and Qadeer, Shaz
                         and Broman, David and Eidson, John C.},
  title =               {Approximate synchrony: An abstraction for
                         distributed almost-synchronous systems},
  editor =              {Kroening, Daniel and Pasareanu, Corina S.},
  booktitle =           {{P}roceedings of the 27th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'15)},
  acronym =             {{CAV}'15},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9206},
  pages =               {429-448},
  year =                {2015},
  month =               jul,
  doi =                 {10.1007/978-3-319-21668-3_25},
}

@inproceedings{fsttcs12-DSTZ,
  author =              {Delzanno, Giorgio and Sangnier, Arnaud and Traverso,
                         Riccardo and Zavattaro, Gianluigi},
  title =               {On~the Complexity of Parameterized Reachability in
                         Reconfigurable Broadcast Networks},
  editor =              {D'Souza, Deepak and Kavitha, Telikepalli and
                         Radhakrishnan, Jaikumar},
  booktitle =           {{P}roceedings of the 32nd {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'12)},
  acronym =             {{FSTTCS}'12},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {18},
  pages =               {289-300},
  year =                {2012},
  month =               dec,
  doi =                 {LIPIcs.FSTTCS.2012.289},
}

@inproceedings{concur2010-DSZ,
  author =              {Delzanno, Giorgio and Sangnier, Arnaud and
                         Zavattaro, Gianluigi},
  title =               {Parameterized Verification of Ad~Hoc Networks},
  editor =              {Gastin, Paul and Laroussinie, Fran{\c c}ois},
  booktitle =           {{P}roceedings of the 21st {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'10)},
  acronym =             {{CONCUR}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6269},
  pages =               {313-327},
  year =                {2010},
  month =               sep,
  doi =                 {10.1007/978-3-642-15375-4_22},
}

@inproceedings{forte2012-DSZ,
  author =              {Delzanno, Giorgio and Sangnier, Arnaud and
                         Zavattaro, Gianluigi},
  title =               {Verification of Ad~Hoc Networks with Node and
                         Communication Failures},
  editor =              {Giese, Holger and Ro{\c{s}}u, Grigore},
  booktitle =           {{P}roceedings of the {J}oint 14th {IFIP} {WG~6.1}
                         {I}nternational {C}onference on {F}ormal {M}ethods
                         for {O}pen {O}bject-{B}ased {D}istributed {S}ystems
                         ({FMOODS}'12) and 32nd {IFIP} {WG~6.1}
                         {I}nternational {C}onference on {F}ormal
                         {T}echniques for {N}etworked and {D}istributed
                         {S}ystems ({FORTE}'12)},
  acronym =             {{FMOODS/FORTE}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7273},
  pages =               {313-327},
  year =                {2012},
  month =               jun,
  doi =                 {10.1007/978-3-642-15375-4_22},
}

@inproceedings{tacas1998-DT,
  author =              {Daws, Conrado and Tripakis, Stavros},
  title =               {Model Checking of Real-Time Reachability Properties
                         Using Abstractions},
  editor =              {Steffen, Bernhard},
  booktitle =           {{P}roceedings of the 4th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'98)},
  acronym =             {{TACAS}'98},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1384},
  pages =               {313-329},
  year =                {1998},
  month =               mar,
  doi =                 {10.1007/BFb0054180},
}

@inproceedings{formats2004-DT,
  author =              {D'Souza, Deepak and Tabareau, Nicolas},
  title =               {On~Timed Automata with Input-Determined Guards},
  editor =              {Lakhnech, Yassine and Yovine, Sergio},
  booktitle =           {{P}roceedings of the {J}oint {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'04) and {F}ormal
                         {T}echniques in {R}eal-Time and {F}ault-Tolerant
                         {S}ystems ({FTRTFT}'04)},
  acronym =             {{FORMATS-FTRTFT}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3253},
  pages =               {68-83},
  year =                {2004},
  month =               sep,
  doi =                 {10.1007/978-3-540-30206-3_7},
}

@techreport{arxiv11-DT,
  author =              {Dima, C{\u a}t{\u a}lin and {\c T}iplea, Ferucio
                         Lauren{\c t}iu},
  title =               {Model-checking {ATL} under Imperfect Information and
                         Perfect Recall Semantics is Undecidable},
  number =              {1102.4225},
  year =                {2011},
  month =               feb,
  institution =         {arXiv},
  type =                {Research Report},
}

@phdthesis{phd-duflot,
  author =              {Duflot, Marie},
  title =               {Algorithmes distribu{\'e}s sur des anneaux
                         param{\'e}tr{\'e}s : preuves de convergence
                         probabiliste et d{\'e}terministe},
  year =                {2003},
  month =               sep,
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {Th\`ese de doctorat},
}

@inproceedings{ijcai2013-DGV,
  author =              {De{~}Giacomo, Giuseppe and Vardi, Moshe Y.},
  title =               {Linear Temporal Logic and Linear Dynamic Logic on
                         Finite Traces},
  editor =              {Rossi, Francesca},
  booktitle =           {{P}roceedings of the 23rd {I}nternational {J}oint
                         {C}onference on {A}rtificial {I}ntelligence
                         ({IJCAI}'13)},
  acronym =             {{IJCAI}'13},
  publisher =           {IJCAI organization},
  pages =               {854-860},
  year =                {2013},
  month =               aug,
}

@inproceedings{icalp1999-DW,
  author =              {Dickh{\"o}fer, Martin and Wilke, Thomas},
  title =               {Timed Alternating Tree Automata: The Automata
                         Theoretic Solution to the {TCTL} Model Checking
                         Problem},
  editor =              {Wiedermann, Jir{\'\i} and van Emde Boas, Peter and
                         Nielsen, Mogens},
  booktitle =           {{P}roceedings of the 26th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'99)},
  acronym =             {{ICALP}'99},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1644},
  pages =               {281-290},
  year =                {1999},
  month =               jul,
}

@inproceedings{rtss1995-DY,
  author =              {Daws, Conrado and Yovine, Sergio},
  title =               {Two examples of verification of multirate timed
                         automata with {K}ronos},
  booktitle =           {{P}roceedings of the 16th {S}ymposium on {R}eal-Time
                         {S}ystems ({RTSS}'95)},
  acronym =             {{RTSS}'95},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {66-75},
  year =                {1995},
  month =               dec,
}