D
[vD03] Govert van Drimmelen. Satisfiability in Alternating-time Temporal Logic. In LICS'03, pages 208-217. IEEE Comp. Soc. Press, June 2003.
@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,
}
[Da11] Arnaud Da Costa. Propriétés de jeux multi-agents. Thèse de doctorat, Lab. Spécification & Vérification, ENS Cachan, France, September 2011.
@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},
}
[Dam94] Mads Dam. Temporal Logic, Automata and Classical Theories. In ESSLLI'94. August 1994.
@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,
}
[Dam94] Dennis René Dams. CTL* and ECTL* as fragments of the modal μ-calculus. Theoretical Computer Science 126(1):77-96. Elsevier, April 1994.
@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,
}
[Dam99] Dennis René Dams. Flat Fragments of CTL and CTL*: Separating the Expressive and Distinguishing Powers. Logic Journal of the IGPL 7(1):55-78. Oxford University Press, January 1999.
@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,
}
[Dan03] Zhe Dang. Pushdown Timed Automata: A Binary Reachability Characterization and Safety Verification. Theoretical Computer Science 302(1-3):93-121. Elsevier, June 2003.
@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,
}
[DBM+10] Kun Deng, Prabir Barooah, Prashant G. Mehta, and Sean P. Meyn. Building thermal model reduction via aggregation of states. In ACC'10, pages 5118-5123. IEEE Comp. Soc. Press, June 2010.
@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},
}
[DBR67] George B. Dantzig, W. O. Blattner, and M. R. Rao. Finding a Cycle in a Graph with Minimum Cost to Time Ratio with Application to a Ship Routing Problem. In Pierre Rosenstiehl (eds.), Theory of Graphs. Gordon and Breach Science Publishers, 1967.
@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},
}
[DCM+04] Jenifer Davoren, Vaughan Coulthard, Nicolas Markey, and Thomas Moor. Non-deterministic Temporal Logics for General Flow Systems. In HSCC'04, Lecture Notes in Computer Science 2993, pages 280-295. Springer-Verlag, March 2004.
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.

@inproceedings{hscc2004-DCMM,
  author =              {Davoren, Jenifer and Coulthard, Vaughan and Markey,
                         Nicolas and Moor, {\relax Th}omas},
  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.},
}
[DD03] Stéphane Demri and Deepak D'Souza. An Automata-Theoretic Approach to Constraint LTL. Research Report LSV-03-11, Lab. Spécification & Vérification, ENS Cachan, France, August 2003.
@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},
}
[DDD+12] Werner Damm, Henning Dierks, Stefan Disch, Willem Hagemann, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, and Boris Wirtz. Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces. Science of Computer Programming 77(10-11):1122-1150. Elsevier, September 2012.
@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},
}
[DDG07] Stéphane Demri, Deepak D'Souza, and Régis Gascon. Decidable Temporal Logic with Repeating Values. In LFCS'07, Lecture Notes in Computer Science 4514, pages 180-194. Springer-Verlag, June 2007.
@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,
}
[DDG+10] Aldric Degorre, Laurent Doyen, Raffaella Gentilini, Jean-François Raskin, and Szymon Toruńczyk. Energy and Mean-Payoff Games with Imperfect Information. In CSL'10, Lecture Notes in Computer Science 6247, pages 260-274. Springer-Verlag, August 2010.
@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,
}
[DDL+13] Alexandre David, Dehui Du, Kim Guldstrand Larsen, Axel Legay, and Marius Mikučionis. Optimizing Control Strategy Using Statistical Model Checking. In NFM'13, Lecture Notes in Computer Science 7871, pages 352-367. Springer-Verlag, May 2013.
@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},
}
[DDM+04] Martin De Wulf, Laurent Doyen, Nicolas Markey, and Jean-François Raskin. Robustness and Implementability of Timed Automata. In FORMATS-FTRTFT'04, Lecture Notes in Computer Science 3253, pages 118-133. Springer-Verlag, September 2004.
Abstract

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.},
}
[DDM+08] Martin De Wulf, Laurent Doyen, Nicolas Markey, and Jean-François Raskin. Robust Safety of Timed Automata. Formal Methods in System Design 33(1-3):45-84. Springer-Verlag, December 2008.
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 Δ>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.},
}
[DDR04] Martin De Wulf, Laurent Doyen, and Jean-François Raskin. Almost ASAP Semantics: From Timed Models to Timed Implementations. In HSCC'04, Lecture Notes in Computer Science 2993, pages 296-310. Springer-Verlag, March 2004.
@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,
}
[DDR05] Martin De Wulf, Laurent Doyen, and Jean-François Raskin. Almost ASAP Semantics: From Timed Models to Timed Implementations. Formal Aspects of Computing 17(3):319-341. Springer-Verlag, 2005.
@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},
}
[De94] Sergio De Agostino. P-complete problems in data compression. Theoretical Computer Science 127(1):181-186. Elsevier, May 1994.
@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,
}
[De00] Sergio De Agostino. Erratum to "P-complete Problems in Data Compression". Theoretical Computer Science 234(1-2):325-326. Elsevier, March 2000.
@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,
}
[De06] Martin De Wulf. From Timed Models to Timed Implementations. Thèse de doctorat, Département d'Informatique, Université Libre de Bruxelles, Belgium, December 2006.
@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},
}
[DEG+15] Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, and Rupak Majumdar. Model Checking Parameterized Asynchronous Shared-Memory Systems. In CAV'15, Lecture Notes in Computer Science 9206, pages 67-84. Springer-Verlag, July 2015.
@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},
}
[DFF+04] Erik D. Demaine, Rudolf Fleischer, Aviezri S. Fraenkel, and Richard J. Nowakowski. Appendix B: Open Problems at the 2002 Dagstuhl Seminar on Algebraic Combinatorial Game Theory. Theoretical Computer Science 313(3):539-543. Elsevier, February 2004.
@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,
}
[DG00] Volker Diekert and Paul Gastin. LTL is Expressively Complete for Mazurkiewicz Traces. In ICALP'00, Lecture Notes in Computer Science 1853, pages 211-222. Springer-Verlag, July 2000.
@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,
}
[DG02] Jenifer Davoren and Rajeev Prabhakar Gore. Bimodal Logics for Reasoning about Continuous Dynamics. In AIML'00. World Scientific, 2002.
@inproceedings{aiml2000-DG,
  author =              {Davoren, Jenifer 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},
}
[DG07] Manfred Droste and Paul Gastin. Weighted automata and weighted logics. Theoretical Computer Science 380(1-2):69-86. Elsevier, June 2007.
@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,
}
[DG08] Anuj Dawar and Erich Grädel. The Descriptive Complexity of Parity Games. In CSL'08, Lecture Notes in Computer Science 5213, pages 354-368. Springer-Verlag, September 2008.
@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},
}
[DG08] Volker Diekert and Paul Gastin. First-order definable languages. In Jörg Flum, Erich Grädel, and Thomas Wilke (eds.), Logic and Automata: History and Perspectives, Texts in Logic and Games 2, pages 261-306. Amsterdam University Press, 2008.
@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},
}
[DG09] Stéphane Demri and Régis Gascon. The Effects of Bounding Syntactic Resources on Presburger LTL. Journal of Logic and Computation 19(6):1541-1575. Oxford University Press, December 2009.
@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},
}
[DGP09] Constantinos Daskalakis, Paul W. Goldberg, and Christos H. Papadimitriou. The complexity of computing a Nash equilibrium. SIAM Journal on Computing 39(1):195-259. Society for Industrial and Applied Math., 2009.
@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},
}
[DGR09] Laurent Doyen, Raffaella Gentilini, and Jean-François Raskin. Faster Pseudo-Polynomial Algorithms for Mean-Payoff Games. Technical Report 2009-121, CFV, 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},
}
[DGR+09] Laurent Doyen, Gilles Geeraerts, Jean-François Raskin, and Julien Reichert. Realizability of Real-Time Logics. In FORMATS'09, Lecture Notes in Computer Science 5813, pages 133-148. Springer-Verlag, September 2009.
@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,
}
[DGR+10] Barbara Di Giampaolo, Gilles Geeraerts, Jean-François Raskin, and Tali Sznajder. Safraless procedures for timed specifications. In FORMATS'10, Lecture Notes in Computer Science 6246, pages 2-22. Springer-Verlag, September 2010.
@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,
}
[DGV99] Marco Daniele, Fausto Giunchiglia, and Moshe Y. Vardi. Improved Automata Generation for Linear Temporal Logic. In CAV'99, Lecture Notes in Computer Science 1633, pages 249-260. Springer-Verlag, July 1999.
@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,
}
[DH00] Giovanna D'Agostino and Marco Hollenberg. Logical Questions Concerning the μ-Calculus: Interpolation, Lyndon and łoś-Tarski. Journal of Symbolic Logic 65(1):310-332. Association for Symbolic Logic, March 2000.
@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},
}
[DHL+06] Alexandre David, John Håkansson, Kim Guldstrand Larsen, and Paul Pettersson. Model Checking Timed Automata with Priorities Using DBM Subtraction. In FORMATS'06, Lecture Notes in Computer Science 4202, pages 128-142. Springer-Verlag, September 2006.
@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},
}
[Die01] Henning Dierks. PLC-automata: a new class of implementable real-time automata. Theoretical Computer Science 253(1):61-93. Elsevier, February 2001.
@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,
}
[Die05] Henning Dierks. Finding Optimal Plans for Domains with Continuous Effects with UPPAAL Cora. In VV&PS'05. June 2005.
@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,
}
[Dij59] Edsger W. Dijkstra. A note on two problems in connexion with graphs. Numerische Mathematik 1:269–271. Springer-Verlag, 1959.
@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},
}
[Dil90] David L. Dill. Timing Assumptions and Verification of Finite-State Concurrent Systems. In AVMFSS'89, Lecture Notes in Computer Science 407, pages 197-212. Springer-Verlag, 1990.
@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},
}
[Dim00] Cătălin Dima. Real-Time Automata and the Kleene Algebra of Sets of Real Numbers. In STACS'00, Lecture Notes in Computer Science 1770, pages 279-289. Springer-Verlag, March 2000.
@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,
}
[Dim02] Cătălin Dima. Computing Reachability Relations in Timed Automata. In LICS'02, pages 177-186. IEEE Comp. Soc. Press, July 2002.
@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,
}
[Dim07] Cătălin Dima. Dynamical Properties of Timed Automata Revisited. In FORMATS'07, Lecture Notes in Computer Science 4763, pages 130-146. Springer-Verlag, October 2007.
@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,
}
[DJJ+03] Piotr Dembinski, Agata Janowska, Paweł Janowski, Wojciech Penczek, Agata Pólrola, Maciej Szreter, Bożna Woźna, and Andrzej Zbrzezny. Verics: A Tool for Verifying Timed Automata and Estelle Specifications. In TACAS'03, Lecture Notes in Computer Science 2619, pages 278-283. Springer-Verlag, April 2003.
@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,
}
[DJL+13] Stéphane Demri, Marcin Jurdziński, Oded Lachish, and Ranko Lazić. The covering and boundedness problems for branching vector addition systems. Journal of Computer and System Sciences 79(1):23-38. Elsevier, February 2013.
@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},
}
[DJL+14] Laurent Doyen, Line Juhl, Kim Guldstrand Larsen, Nicolas Markey, and Mahsa Shrimohammadi. Synchronizing words for weighted and timed automata. In FSTTCS'14, Leibniz International Proceedings in Informatics 29, pages 121-132. Leibniz-Zentrum für Informatik, December 2014.
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.

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 Shrimohammadi,
                         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.},
}
[DJL+15] Alexandre David, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marius Mikučionis, and Jakob Haar Taankvist. Uppaal Stratego. In TACAS'15, Lecture Notes in Computer Science 9035, pages 206-211. Springer-Verlag, April 2015.
@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},
}
[DJW97] Stefan Dziembowski, Marcin Jurdziński, and Igor Walukiewicz. How Much Memory is Needed to Win Infinite Games. In LICS'97, pages 99-110. IEEE Comp. Soc. Press, June 1997.
@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,
}
[DK06] Conrado Daws and Piotr Kordy. Symbolic robustness analysis of timed automata. In FORMATS'06, Lecture Notes in Computer Science 4202, pages 143-155. Springer-Verlag, September 2006.
@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,
}
[DKL07] Henning Dierks, Sebastian Kupferschmid, and Kim Guldstrand Larsen. Automatic abstraction refinement for timed automata. In FORMATS'07, Lecture Notes in Computer Science 4763, pages 114-129. Springer-Verlag, October 2007.
@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},
}
[DKL09] Christian Dax, Felix Klaedtke, and Martin Lange. On Regular Temporal Logics with Past. In ICALP'09, Lecture Notes in Computer Science 5556, pages 175-187. Springer-Verlag, July 2009.
@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},
}
[DKM+15] Samir Datta, Raghav Kulkarni, Anish Mukherjee, Thomas Schwentick, and Thomas Zeume. Reachability is in DynFO. In ICALP'15, Lecture Notes in Computer Science 9135, pages 159-170. Springer-Verlag, July 2015.
@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},
}
[DKP91] Nachum Dershowitz, Stéphane Kaplan, and David A. Plaisted. Rewrite, Rewrite, Rewrite, Rewrite, Rewrite, .... Theoretical Computer Science 83(1):71-96. Elsevier, 1991.
@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},
}
[DKV09] Manfred Droste, Werner Kuich, and Walter Vogler. Handbook of Weighted Automata. Springer-Verlag, 2009.
@book{hwa-DKV,
  title =               {Handbook of Weighted Automata},
  editor =              {Droste, Manfred and Kuich, Werner and Vogler,
                         Walter},
  publisher =           {Springer-Verlag},
  year =                {2009},
}
[DL94] Giuseppe De Giacomo and Maurizio Lenzerini. Concept Language with Number Restrictions and Fixpoints, and its Relationship with Mu-Calculus. In ECAI'94, pages 411-415. John Wiley & Sons, August 1994.
@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,
}
[DLF+16] Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibault Michaud, Étienne Renault, and Laurent Xu. Spot 2.0 – A Framework for LTL and ω-Automata Manipulation. In ATVA'16, Lecture Notes in Computer Science 9938, pages 122-129. Springer-Verlag, October 2016.
@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},
}
[DLL+12] Alexandre David, Kim Guldstrand Larsen, Axel Legay, and Marius Mikučionis. Schedulability of Herschel-Planck Revisited Using Statistical Model Checking. In ISoLA'12, Lecture Notes in Computer Science 7610, pages 293-307. Springer-Verlag, October 2012.
@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},
}
[DLL+10] Alexandre David, Kim Guldstrand Larsen, Shuhao Li, Marius Mikučionis, and Brian Nielsen. Testing Real-Time Systems under Uncertainty. In FMCO'10, Lecture Notes in Computer Science 6957, pages 352-371. Springer-Verlag, December 2010.
@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},
}
[DLL+11] Alexandre David, Kim Guldstrand Larsen, Axel Legay, Marius Mikučionis, Danny Bøgsted Poulsen, Jonas van Vliet, and Zheng Wang. Statistical Model Checking for Networks of Priced Timed Automata. In FORMATS'11, Lecture Notes in Computer Science 6919, pages 80-96. Springer-Verlag, September 2011.
@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,
}
[DLL+11] Alexandre David, Kim Guldstrand Larsen, Axel Legay, Marius Mikučionis, and Zheng Wang. Time for Statistical Model Checking of Real-Time Systems. In CAV'11, Lecture Notes in Computer Science 6806, pages 349-355. Springer-Verlag, July 2011.
@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},
}
[DLL+08] Alexandre David, Kim Guldstrand Larsen, Shuhao Li, and Brian Nielsen. A Game-Theoretic Approach to Real-Time System Testing. In DATE'00, pages 486-491. IEEE Comp. Soc. Press, March 2008.
@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 2000 {D}esign, {A}utomation and
                         {T}est in {E}urope ({DATE}'00)},
  acronym =             {{DATE}'00},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {486-491},
  year =                {2008},
  month =               mar,
}
[DLL+13] Alexandre David, Kim Guldstrand Larsen, Axel Legay, and Danny Bøgsted Poulsen. Statistical Model Checking of Dynamic Networks of Stochastic Hybrid Automata. In AVOCS'13, Electronic Communications of the EASST 10. European Association of Software Science and Technology, September 2013.
@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,
}
[DLM10] Arnaud Da Costa, François Laroussinie, and Nicolas Markey. ATL with strategy contexts: Expressiveness and Model Checking. In FSTTCS'10, Leibniz International Proceedings in Informatics 8, pages 120-132. Leibniz-Zentrum für Informatik, December 2010.
Abstract

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.},
}
[DLM12] Arnaud Da Costa, François Laroussinie, and Nicolas Markey. Quantified CTL: Expressiveness and Model Checking. In CONCUR'12, Lecture Notes in Computer Science 7454, pages 177-192. Springer-Verlag, September 2012.
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.

@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.},
}
[DLM16] Amélie David, François Laroussinie, and Nicolas Markey. On the expressiveness of QCTL. In CONCUR'16, Leibniz International Proceedings in Informatics 59, pages 28:1-28:15. Leibniz-Zentrum für Informatik, August 2016.
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 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).},
}
[DLM+13] Peter H. Dalsgaard, Thibault Le Guilly, Daniel Middelhede, Petur Olsen, Thomas Pedersen, Anders P. Ravn, and Arne Skou. A Toolchain for Home Automation Controller Development. In SEAA'13, pages 122-129. September 2013.
@inproceedings{HLMOPRS-seaa2013,
  author =              {Dalsgaard, Peter H. and Le{~}Guilly, {\relax
                         Th}ibault 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,
}
[DLR+09] Alexandre David, Kim Guldstrand Larsen, Jacob Illum Rasmussen, and Arne Skou. Model-based framework for schedulability analysis using UPPAAL 4.1. In Gabriela Nicolescu and Pieter J. Mosterman (eds.), Model-Based Design for Embedded Systems, Computational Analysis, Synthesis, and Design of Dynamic Systems, pages 93-119. CRC Press, 2009.
@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},
}
[DLS02] Stéphane Demri, François Laroussinie, and Philippe Schnoebelen. A Parametric Analysis of the State Explosion Problem in Model Checking (Extended Abstract). In STACS'02, Lecture Notes in Computer Science 2285, pages 620-631. Springer-Verlag, March 2002.
@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,
}
[DLS10] Stéphane Demri, Ranko Lazić, and Arnaud Sangnier. Model checking memoryful linear-time logics over one-counter automata. Theoretical Computer Science 411(22-24):2298-2316. Elsevier, May 2010.
@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},
}
[DM86] Partha Dasgupta and Eric Maskin. The Existence of Equilibrium in Discontinuous Economic Games, 1: Theory. The Review of Economic Studies 53(1):1-26. Oxford University Press, January 1986.
@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,
}
[DM86] Partha Dasgupta and Eric Maskin. The Existence of Equilibrium in Discontinuous Economic Games, 2: Applications. The Review of Economic Studies 53(1):27-41. Oxford University Press, January 1986.
@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,
}
[DM02] Deepak D'Souza and Parthasarathy Madhusudan. Timed Control Synthesis for External Specifications. In STACS'02, Lecture Notes in Computer Science 2285, pages 571-582. Springer-Verlag, March 2002.
@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,
}
[DM18] Dario Della Monica and Aniello Murano. Parity-energy ATL for Qualitative and Quantitative Reasoning in MAS. In AAMAS'18, pages 1441-1449. International Foundation for Autonomous Agents and Multiagent Systems, July 2018.
@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,
}
[DMS11] Laurent Doyen, Thierry Massart, and Mahsa Shrimohammadi. Infinite Synchronizing Words for Probabilistic Automata. In MFCS'11, Lecture Notes in Computer Science 6907, pages 278-289. Springer-Verlag, August 2011.
@inproceedings{mfcs2011-DMS,
  author =              {Doyen, Laurent and Massart, {\relax Th}ierry and
                         Shrimohammadi, 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},
}
[DN07] Stéphane Demri and David Nowak. Reasoning about Transfinite Sequences. International Journal of Foundations of Computer Science 18(1):87-112. February 2007.
@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},
}
[DOT+10] Andreas E. Dalsgaard, Mads Chr. Olesen, Martin Toft, René R. Hansen, and Kim Guldstrand Larsen. METAMOC: Modular Execution Time Analysis using Model Checking. In WCET'10, OpenAccess Series in Informatics 15, pages 113-123. Leibniz-Zentrum für Informatik, July 2010.
@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,
}
[DOT+96] Conrado Daws, Alfredo Olivero, Stavros Tripakis, and Sergio Yovine. The tool Kronos. In HSCC'95, Lecture Notes in Computer Science 1066, pages 208-219. Springer-Verlag, 1996.
@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},
}
[Doy06] Laurent Doyen. Algorithmic Analysis of Complex Semantics for Timed and Hybrid Automata. Thèse de doctorat, Département d'Informatique, Université Libre de Bruxelles, Belgium, June 2006.
@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},
}
[Doy07] Laurent Doyen. Robust parametric reachability for timed automata. Information Processing Letters 102(5):208-213. Elsevier, May 2007.
@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},
}
[Doy12] Laurent Doyen. Games and Automata: From Boolean to Quantitative Verification. Mémoire d'habilitation, École Normale Supérieure de Cachan, France, March 2012.
@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},
}
[DP05] Deepak D'Souza and Pavithra Prabhakar. On the Expressiveness of MTL in the Pointwise and Continuous Semantics. Technical Report IISc-CSA-TR-2005-7, Indian Institute of Science, Bangalore, India, May 2005.
@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},
}
[DP07] Deepak D'Souza and Pavithra Prabhakar. On the Expressiveness of MTL in the Pointwise and Continuous Semantics. International Journal on Software Tools for Technology Transfer 9(1):1-4. Springer-Verlag, February 2007.
@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},
}
[DPP07] Andrea D'Ariano, Dario Pacciarelli, and Marco Pranzo. A branch-and-bound algorithm for scheduling trains in a railway network. European Journal of Operational Research 183(2):643-657. Elsevier, December 2007.
@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},
}
[DR95] Volker Diekert and Grzegorz Rozenberg. The Book of Traces. World Scientific, 1995.
@book{BoT-DR,
  author =              {Diekert, Volker and Rozenberg, Grzegorz},
  title =               {The Book of Traces},
  publisher =           {World Scientific},
  year =                {1995},
}
[DR10] Laurent Doyen and Jean-François Raskin. Antichain Algorithms for Finite Automata. In TACAS'10, Lecture Notes in Computer Science 6015, pages 2-22. Springer-Verlag, March 2010.
@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,
}
[DRV04] Giorgio Delzanno, Jean-François Raskin, and Laurent Van Begin. Covering sharing trees: a compact data structure for parameterized verification. International Journal on Software Tools for Technology Transfer 5(2-3):268-297. Springer-Verlag, 2004.
@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},
}
[DS98] Stéphane Demri and Philippe Schnoebelen. The Complexity of Propositional Linear Temporal Logics in Simple Cases (extended abstract). In STACS'98, Lecture Notes in Computer Science 1373, pages 61-72. Springer-Verlag, February 1998.
@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,
}
[DS02] Stéphane Demri and Philippe Schnoebelen. The Complexity of Propositional Linear Temporal Logics in Simple Cases. Information and Computation 174(1):84-103. Academic Press, April 2002.
@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,
}
[DS02] Stéphane Demri and Ulrike Sattler. Automata-Theoretic Decision Procedures for Information Logics. Fundamenta Informaticae 53(1):1-22. IOS Press, 2002.
@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},
}
[DSK01] Zhe Dang, Pierluigi San Pietro, and Richard A. Kemmerer. On Presburger Liveness of Discrete Timed Automata. In STACS'01, Lecture Notes in Computer Science 2010, pages 132-143. Springer-Verlag, February 2001.
@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,
}
[DSQ+15] Ankush Desai, Sanjit A. Seshia, Shaz Qadeer, David Broman, and John C. Eidson. Approximate synchrony: An abstraction for distributed almost-synchronous systems. In CAV'15, Lecture Notes in Computer Science 9206, pages 429-448. Springer-Verlag, July 2015.
@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},
}
[DST+12] Giorgio Delzanno, Arnaud Sangnier, Riccardo Traverso, and Gianluigi Zavattaro. On the Complexity of Parameterized Reachability in Reconfigurable Broadcast Networks. In FSTTCS'12, Leibniz International Proceedings in Informatics 18, pages 289-300. Leibniz-Zentrum für Informatik, December 2012.
@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},
}
[DSZ10] Giorgio Delzanno, Arnaud Sangnier, and Gianluigi Zavattaro. Parameterized Verification of Ad Hoc Networks. In CONCUR'10, Lecture Notes in Computer Science 6269, pages 313-327. Springer-Verlag, September 2010.
@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},
}
[DSZ12] Giorgio Delzanno, Arnaud Sangnier, and Gianluigi Zavattaro. Verification of Ad Hoc Networks with Node and Communication Failures. In FMOODS/FORTE'12, Lecture Notes in Computer Science 7273, pages 313-327. Springer-Verlag, June 2012.
@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},
}
[DT98] Conrado Daws and Stavros Tripakis. Model Checking of Real-Time Reachability Properties Using Abstractions. In TACAS'98, Lecture Notes in Computer Science 1384, pages 313-329. Springer-Verlag, March 1998.
@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},
}
[DT04] Deepak D'Souza and Nicolas Tabareau. On Timed Automata with Input-Determined Guards. In FORMATS-FTRTFT'04, Lecture Notes in Computer Science 3253, pages 68-83. Springer-Verlag, September 2004.
@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},
}
[DT11] Cătălin Dima and Ferucio Laurenţiu Ţiplea. Model-checking ATL under Imperfect Information and Perfect Recall Semantics is Undecidable. Research Report 1102.4225, arXiv, February 2011.
@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},
}
[Duf03] Marie Duflot. Algorithmes distribués sur des anneaux paramétrés : preuves de convergence probabiliste et déterministe. Thèse de doctorat, Lab. Spécification & Vérification, ENS Cachan, France, September 2003.
@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},
}
[DW99] Martin Dickhöfer and Thomas Wilke. Timed Alternating Tree Automata: The Automata Theoretic Solution to the TCTL Model Checking Problem. In ICALP'99, Lecture Notes in Computer Science 1644, pages 281-290. Springer-Verlag, July 1999.
@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,
}
[DY95] Conrado Daws and Sergio Yovine. Two examples of verification of multirate timed automata with Kronos. In RTSS'95, pages 66-75. IEEE Comp. Soc. Press, December 1995.
@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,
}