Nicolas Markey

Abstract

We consider the model of priced (a.k.a. weighted) timed automata, an extension of timed automata with cost information on both locations and transitions. We prove that model-checking this class of models against the logic WCTL, CTL with cost-constrained modalities, is PSPACE-complete under the "single-clock" assumption. In contrast, it has been recently proved that the model-checking problem is undecidable for this model as soon as the system has three clocks. We also prove that the model-checking of WCTL becomes undecidable, even under this "single-clock" assumption.

@inproceedings{fossacs2007-BLM,
  author =              {Bouyer, Patricia and Larsen, Kim Guldstrand and
                         Markey, Nicolas},
  title =               {Model Checking One-clock Priced Timed Automata},
  editor =              {Seidl, Helmut},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'07)},
  acronym =             {{FoSSaCS}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4423},
  pages =               {108-122},
  year =                {2007},
  month =               mar,
  doi =                 {10.1007/978-3-540-71389-0_9},
  abstract =            {We consider the model of priced (a.k.a.~weighted)
                         timed automata, an extension of timed automata with
                         cost information on both locations and transitions.
                         We prove that model-checking this class of models
                         against the logic~WCTL, CTL~with cost-constrained
                         modalities, is PSPACE-complete under the
                         {"}single-clock{"} assumption. In~contrast, it~has
                         been recently proved that the model-checking problem
                         is undecidable for this model as soon as the system
                         has three clocks. We also prove that the
                         model-checking of~WCTL becomes undecidable, even
                         under this {"}single-clock{"} assumption.},
}

Abstract

We propose a new model for timed games, based on concurrent game structures (CGSs). Compared to the classical timed game automata of Asarin et al., our timed CGSs are "more concurrent", in the sense that they always allow all the agents to act on the system, independently of the delay they want to elapse before their action. Timed CGSs weaken the "element of surprise" of timed game automata reported by de Alfaro et al.

We prove that our model has nice properties, in particular that model-checking timed CGSs against timed ATL is decidable via region abstraction, and in particular that strategies are "region-stable" if winning objectives are. We also propose a new extension of TATL, containing ATL*, which we call TALTL. We prove that model-checking this logic remains decidable on timed CGSs. Last, we explain how our algorithms can be adapted in order to rule out Zeno (co-)strategies, based on the ideas of Henzinger et al.

@inproceedings{concur2007-BLMO,
  author =              {Brihaye, {\relax Th}omas and Laroussinie, Fran{\c
                         c}ois and Markey, Nicolas and Oreiby, Ghassan},
  title =               {Timed Concurrent Game Structures},
  editor =              {Caires, Lu{\'\i}s and Vasconcelos, Vasco T.},
  booktitle =           {{P}roceedings of the 18th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'07)},
  acronym =             {{CONCUR}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4703},
  pages =               {445-459},
  year =                {2007},
  month =               sep,
  doi =                 {10.1007/978-3-540-74407-8_30},
  abstract =            {We propose a new model for timed games, based on
                         concurrent game structures~(CGSs). Compared to the
                         classical \emph{timed game automata} of~Asarin
                         \emph{et~al.}, our timed~CGSs are {"}more
                         concurrent{"}, in the sense that they always allow
                         all the agents to act on the system, independently
                         of the delay they want to elapse before their
                         action. Timed CGSs weaken the {"}element of
                         surprise{"} of timed game automata reported by
                         de~Alfaro \emph{et~al.}\par We prove that our model
                         has nice properties, in particular that
                         model-checking timed CGSs against timed
                         \(\textsf{ATL}\) is decidable \emph{via} region
                         abstraction, and in particular that strategies are
                         {"}region-stable{"} if winning objectives are. We
                         also propose a new extension of \(\textsf{TATL}\),
                         containing~\(\textsf{ATL}^{*}\), which we
                         call~\(\textsf{TALTL}\). We~prove that
                         model-checking this logic remains decidable on timed
                         CGSs. Last, we explain how our algorithms can be
                         adapted in order to rule out Zeno (co-)strategies,
                         based on the ideas of Henzinger \emph{et~al.}},
}

Abstract

We study the model-checking problem for WMTL, a cost-extension of the linear-time timed temporal logic MTL, that is interpreted over weighted timed automata. We draw a complete picture of the decidability for that problem: it is decidable only for the class of one-clock weighted timed automata with a restricted stopwatch cost, and any slight extension of this model leads to undecidability. We finally give some consequences on the undecidability of linear hybrid automata.

@inproceedings{formats2007-BM,
  author =              {Bouyer, Patricia and Markey, Nicolas},
  title =               {Costs are Expensive!},
  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 =               {53-68},
  year =                {2007},
  month =               oct,
  doi =                 {10.1007/978-3-540-75454-1_6},
  abstract =            {We study the model-checking problem for WMTL,
                         a~cost-extension of the linear-time timed temporal
                         logic MTL, that is interpreted over weighted timed
                         automata. We~draw a complete picture of the
                         decidability for that problem: it~is decidable only
                         for the class of one-clock weighted timed automata
                         with a restricted stopwatch cost, and any slight
                         extension of this model leads to undecidability.
                         We~finally give some consequences on the
                         undecidability of linear hybrid automata.},
}

Abstract

In an influential paper titled "The Benefits of Relaxing Punctuality", Alur, Feder, and Henzinger introduced Metric Interval Temporal Logic (MITL) as a fragment of the real-time logic Metric Temporal Logic (MTL) in which exact or punctual timing constraints are banned. Their main result showed that model checking and satisfiability for MITL are both EXPSPACE-Complete.

Until recently, it was widely believed that admitting even the simplest punctual specifications in any linear-time temporal logic would automatically lead to undecidability. Although this was recently disproved, until now no punctual fragment of MTL was known to have even primitive recursive complexity (with certain decidable fragments having provably non-primitive recursive complexity).

In this paper we identify a `co-flat' subset of MTL that is capable of expressing a large class of punctual specifications and for which model checking (although not satisfiability) has no complexity cost over MITL. Our logic is moreover qualitatively different from MITL in that it can express properties that are not timed-regular. Correspondingly, our decision procedures do not involve translating formulas into finite-state automata, but rather into certain kinds of reversal-bounded Turing machines. Using this translation we show that the model checking problem for our logic is EXPSPACE-Complete, and is even PSPACE-Complete if timing constraints are encoded in unary.

@inproceedings{lics2007-BMOW,
  author =              {Bouyer, Patricia and Markey, Nicolas and Ouaknine,
                         Jo{\"e}l and Worrell, James},
  title =               {The Cost of Punctuality},
  booktitle =           {{P}roceedings of the 22nd {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'07)},
  acronym =             {{LICS}'07},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {109-118},
  year =                {2007},
  month =               jul,
  doi =                 {10.1109/LICS.2007.49},
  abstract =            {In an influential paper titled {"}The Benefits of
                         Relaxing Punctuality{"}, Alur, Feder, and~Henzinger
                         introduced Metric Interval Temporal Logic~(MITL) as
                         a fragment of the real-time logic Metric Temporal
                         Logic~(MTL) in which exact or punctual timing
                         constraints are banned. Their main result showed
                         that model checking and satisfiability for~MITL are
                         both EXPSPACE-Complete.\par Until recently, it was
                         widely believed that admitting even the simplest
                         punctual specifications in any linear-time temporal
                         logic would automatically lead to undecidability.
                         Although this was recently disproved, until now no
                         punctual fragment of~MTL was known to have even
                         primitive recursive complexity (with certain
                         decidable fragments having provably non-primitive
                         recursive complexity).\par In this paper we identify
                         a `co-flat' subset of~MTL that is capable of
                         expressing a large class of punctual specifications
                         and for which model checking (although not
                         satisfiability) has no complexity cost over~MITL.
                         Our logic is moreover qualitatively different
                         from~MITL in that it can express properties that are
                         not timed-regular. Correspondingly, our decision
                         procedures do not involve translating formulas into
                         finite-state automata, but rather into certain kinds
                         of reversal-bounded Turing machines. Using this
                         translation we show that the model checking problem
                         for our logic is EXPSPACE-Complete, and is even
                         PSPACE-Complete if timing constraints are encoded in
                         unary.},
}

Abstract

ATL is a temporal logic geared towards the specification and verification of properties in multi-agents systems. It allows to reason on the existence of strategies for coalitions of agents in order to enforce a given property. We prove that the standard definition of ATL (built on modalities "Next", "Always" and "Until") has to be completed in order to express the duals of its modalities: it is necessary to add the modality "Release". We then precisely characterize the complexity of ATL model-checking when the number of agents is not fixed. We prove that it is Δ2P and Δ3P-complete, depending on the underlying multi-agent model (ATS and CGS, resp.). We also prove that ATL+ model-checking is Δ3P-complete over both models, even with a fixed number of agents.

@inproceedings{fossacs2007-LMO,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
                         Oreiby, Ghassan},
  title =               {On the Expressiveness and Complexity of~{ATL}},
  editor =              {Seidl, Helmut},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'07)},
  acronym =             {{FoSSaCS}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4423},
  pages =               {243-257},
  year =                {2007},
  month =               mar,
  doi =                 {10.1007/978-3-540-71389-0_18},
  abstract =            {ATL is a temporal logic geared towards the
                         specification and verification of properties in
                         multi-agents systems. It allows to reason on the
                         existence of strategies for coalitions of agents in
                         order to enforce a given property. We prove that the
                         standard definition of~ATL (built on modalities
                         {"}Next{"}, {"}Always{"} and~{"}Until{"}) has to be
                         completed in order to express the duals of its
                         modalities: it~is necessary to add the modality
                         {"}Release{"}. We~then precisely characterize the
                         complexity of ATL model-checking when the number of
                         agents is not fixed. We prove that it is
                         \(\Delta_{2}^{P}\) and \(\Delta_{3}^{P}\)-complete,
                         depending on the underlying multi-agent model (ATS
                         and CGS,~resp.). We also prove that~ATL\({}^{+}\)
                         model-checking is \(\Delta_{3}^{P}\)-complete over
                         both models, even with a fixed number of agents.},
}

@article{discomp20(4)-AAER,
  author =              {Angluin, Dana and Aspnes, James and Eisenstat, David
                         and Ruppert, Eric},
  title =               {The computational power of population protocols},
  publisher =           {Springer-Verlag},
  journal =             {Distributed Computing},
  volume =              {20},
  number =              {4},
  pages =               {279-304},
  year =                {2007},
  month =               mar,
  doi =                 {10.1007/s00446-007-0040-2},
}

@inproceedings{tark2007-AGJ,
  author =              {{\AA}gotnes, Thomas and Goranko, Valentin and
                         Jamroga, Wojciech},
  title =               {Alternating-time Temporal Logics with Irrevocable
                         Strategies},
  editor =              {Samet, Dov},
  booktitle =           {{P}roceedings of the 11th {C}onference on
                         {T}heoretical {A}spects of {R}ationality and
                         {K}nowledge ({TARK}'07)},
  acronym =             {{TARK}'07},
  pages =               {15-24},
  year =                {2007},
  month =               jun,
}

@article{tcs386(3)-AHK,
  author =              {de Alfaro, Luca and Henzinger, Thomas A. and
                         Kupferman, Orna},
  title =               {Concurrent Reachability Games},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {386},
  number =              {3},
  pages =               {188-217},
  year =                {2007},
  month =               nov,
  doi =                 {10.1016/j.tcs.2007.07.008},
}

@article{tcs379(1-2)-ASY,
  author =              {Asarin, Eugene and Schneider, Gerardo and Yovine,
                         Sergio},
  title =               {Algorithmic analysis of polygonal hybrid systems,
                         part~{I}: Reachability},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {379},
  number =              {1-2},
  pages =               {231-265},
  year =                {2007},
  month =               jun,
}

@inproceedings{fsttcs2007-BBBBG,
  author =              {Baier, {\relax Ch}ristel and Bertrand, Nathalie and
                         Bouyer, Patricia and Brihaye, {\relax Th}omas and
                         Gr{\"o}{\ss}er, Marcus},
  title =               {Probabilistic and Topological Semantics for Timed
                         Automata},
  editor =              {Arvind, Vikraman and Prasad, Sanjiva},
  booktitle =           {{P}roceedings of the 27th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'07)},
  acronym =             {{FSTTCS}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4855},
  pages =               {179-191},
  year =                {2007},
  month =               dec,
}

@article{deds17(4)-BBBCD,
  author =              {Badouel, {\'E}ric and Bednarczyk, Marek and
                         Borzyszkowski, Andrzej and Caillaud, Beno{\^\i}t and
                         Darondeau, Philippe},
  title =               {Concurrent secrets},
  publisher =           {Kluwer Academic},
  journal =             {Discrete Event Dynamic Systems},
  volume =              {17},
  number =              {4},
  pages =               {425-446},
  year =                {2007},
  month =               dec,
  doi =                 {10.1007/s10626-007-0020-5},
}

@article{fmsd31(2)-BBBR,
  author =              {Bouyer, Patricia and Brihaye, {\relax Th}omas and
                         Bruy{\`e}re, V{\'e}ronique and Raskin, Jean-Fran{\c
                         c}ois},
  title =               {On the Optimal Reachability Problem of Weighted
                         Timed Automata},
  publisher =           {Springer-Verlag},
  journal =             {Formal Methods in System Design},
  volume =              {31},
  number =              {2},
  pages =               {135-175},
  year =                {2007},
  month =               oct,
  doi =                 {10.1007/s10703-007-0035-4},
}

@inproceedings{qest2007-BBGK,
  author =              {Baier, {\relax Ch}ristel and Br{\'a}zdil,
                         Tom{\'a}{\v s} and Gr{\"o}{\ss}er, Marcus and Ku{\v
                         c}era, Anton{\'\i}n},
  title =               {Stochastic Game Logic},
  booktitle =           {{P}roceedings of the 4th {I}nternational
                         {C}onference on {Q}uantitative {E}valuation of
                         {S}ystems ({QEST}'07)},
  acronym =             {{QEST}'07},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {227-236},
  year =                {2007},
  month =               sep,
}

@inproceedings{cav2007-BCDFLL,
  author =              {Behrmann, Gerd and Cougnard, Agn{\`e}s and David,
                         Alexandre and Fleury, Emmanuel and Larsen, Kim
                         Guldstrand and Lime, Didier},
  title =               {{UPPAAL-Tiga}: Time for Playing Games!},
  editor =              {Damm, Werner and Hermanns, Holger},
  booktitle =           {{P}roceedings of the 19th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'07)},
  acronym =             {{CAV}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4590},
  pages =               {121-125},
  year =                {2007},
  month =               jul,
}

@inproceedings{icalp2007-BHPR,
  author =              {Brihaye, {\relax Th}omas and Henzinger, Thomas A.
                         and Prabhu, Vinayak S. and Raskin, Jean-Fran{\c
                         c}ois},
  title =               {Minimum-Time Reachability in Timed Games},
  editor =              {Arge, Lars and Cachin, Christian and Jurdzi{\'n}ski,
                         Tomasz and Tarlecki, Andrzej},
  booktitle =           {{P}roceedings of the 34th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'07)},
  acronym =             {{ICALP}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4596},
  pages =               {825-837},
  year =                {2007},
  month =               jul,
}

@inproceedings{cav2007-BHT,
  author =              {Beyer, Dirk and Henzinger, Thomas A. and
                         Th{\'e}oduloz, Gr{\'e}gory},
  title =               {Configurable Software Verification: Concretizing the
                         Convergence of Model Checking and Program Analysis},
  editor =              {Damm, Werner and Hermanns, Holger},
  booktitle =           {{P}roceedings of the 19th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'07)},
  acronym =             {{CAV}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4590},
  year =                {2007},
  month =               jul,
  doi =                 {10.1007/978-3-540-73368-3_51},
}

@article{dam155(2)-BV,
  author =              {Bj{\"o}rklund, Henrik and Vorobyov, Sergei},
  title =               {A combinatorial strongly subexponential strategy
                         improvement algorithm for mean payoff games},
  publisher =           {Elsevier},
  journal =             {Discrete Applied Mathematics},
  volume =              {155},
  number =              {2},
  pages =               {210-229},
  year =                {2007},
  month =               jan,
  doi =                 {10.1016/j.dam.2006.04.029},
}

@inproceedings{atva2007-CDLLR,
  author =              {Cassez, Franck and David, Alexandre and Larsen, Kim
                         Guldstrand and Lime, Didier and Raskin, Jean-Fran{\c
                         c}ois},
  title =               {Timed Control with Observation Based and Stuttering
                         Invariant Strategies},
  editor =              {Namjoshi, Kedar and Yoneda, Tomohiro and Higashino,
                         Teruo and Okamura, Yoshio},
  booktitle =           {{P}roceedings of the 5th {I}nternational {S}ymposium
                         on {A}utomated {T}echnology for {V}erification and
                         {A}nalysis ({ATVA}'07)},
  acronym =             {{ATVA}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4762},
  pages =               {192-206},
  year =                {2007},
  month =               oct,
  doi =                 {10.1007/978-3-540-75596-8_15},
}

@phdthesis{phd-chatterjee,
  author =              {Chatterjee, Krishnendu},
  title =               {Stochastic {\(\omega\)}-regular games},
  year =                {2007},
  school =              {University of Califormia at Berkeley, USA},
}

@inproceedings{fossacs2007-CHP,
  author =              {Chatterjee, Krishnendu and Henzinger, Thomas A. and
                         Piterman, Nir},
  title =               {Generalized Parity Games},
  editor =              {Seidl, Helmut},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'07)},
  acronym =             {{FoSSaCS}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4423},
  pages =               {153-167},
  year =                {2007},
  month =               mar,
}

@inproceedings{concur2007-CHP,
  author =              {Chatterjee, Krishnendu and Henzinger, Thomas A. and
                         Piterman, Nir},
  title =               {Strategy Logic},
  editor =              {Caires, Lu{\'\i}s and Vasconcelos, Vasco T.},
  booktitle =           {{P}roceedings of the 18th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'07)},
  acronym =             {{CONCUR}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4703},
  pages =               {59-73},
  year =                {2007},
  month =               sep,
  doi =                 {10.1007/978-3-540-74407-8_5},
}

@inproceedings{fskd2007-CL,
  author =              {Chen, Taolue and Lu, Jian},
  title =               {Probabilistic Alternating-time Temporal Logic and
                         Model Checking Algorithm},
  editor =              {Lei, J.},
  booktitle =           {{P}roceedings of the 4th {I}nternational
                         {C}onference on {F}uzzy {S}ystems and {K}nowledge
                         {D}iscovery ({FSKD}'07)},
  acronym =             {{FSKD}'07},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {35-39},
  year =                {2007},
  month =               aug,
  doi =                 {10.1109/FSKD.2007.458},
}

@article{tcs382(2)-CR,
  author =              {Carton, Olivier and Rispal, Chlo{\'e}},
  title =               {Complementation of rational sets on scattered linear
                         orderings of finite rank},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {382},
  number =              {2},
  pages =               {109-119},
  year =                {2007},
  month =               aug,
}

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

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

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

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

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

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

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

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

@inproceedings{focs2007-EY,
  author =              {Etessami, Kousha and Yannakakis, Mihalis},
  title =               {On the Complexity of {N}ash Equilibria and Other
                         Fixed Points (Extended Abstract)},
  booktitle =           {{P}roceedings of the 48th {A}nnual {S}ymposium on
                         {F}oundations of {C}omputer {S}cience ({FOCS}'07)},
  acronym =             {{FOCS}'07},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {113-123},
  year =                {2007},
  month =               oct,
}

@inproceedings{frocos2007-FMR,
  author =              {French, Tim and McCabe{-}Dansted, John C. and
                         Reynolds, Mark},
  title =               {A Temporal Logic of Robustness},
  editor =              {Konev, Boris and Wolter, Frank},
  booktitle =           {{P}roceedings of the 6th {I}nternational {W}orkshop
                         on {F}rontiers of {C}ombining {S}ystems
                         ({FroCoS}'07)},
  acronym =             {{FroCoS}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Artificial Intelligence},
  volume =              {4720},
  pages =               {193-205},
  year =                {2007},
  month =               sep,
  doi =                 {10.1007/978-3-540-74621-8_13},
}

@techreport{DEI-2007-37-FPR,
  author =              {Furia, Carlo A. and Pradella, Matteo and Rossi,
                         Matteo},
  title =               {Dense-Time {MTL} Verification Through Sampling},
  number =              {2007-37},
  year =                {2007},
  month =               apr,
  institution =         {Dipartimento di Elettronica ed Informazione,
                         Politecnico di Milano, Italy},
  type =                {Research Report},
}

@inproceedings{formats07-FR,
  author =              {Furia, Carlo A. and Rossi, Matteo},
  title =               {On the Expressiveness of {MTL} Variants over Dense
                         Time},
  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 =               {163-178},
  year =                {2007},
  month =               oct,
  doi =                 {10.1007/978-3-540-75454-1_13},
}

@article{icomp205(8)-GMP,
  author =              {Geffert, Villiam and Mereghetti, Carlo and
                         Pighizzini, Giovanni},
  title =               {Complementing Two-way Finite Automata},
  publisher =           {Elsevier},
  journal =             {Information and Computation},
  volume =              {205},
  number =              {8},
  pages =               {1173-1187},
  year =                {2007},
  month =               aug,
}

@inproceedings{BZbday07-HMB,
  author =              {Hansen, Michael R. and Madsen, Jan and Brekling,
                         Aske Wiid},
  title =               {Semantics and Verification of a Language for
                         Modelling Hardware Architectures},
  editor =              {Jones, Cliff B. and Liu, Zhiming and Woodcock, Jim},
  booktitle =           {Formal Methods and Hybrid Real-Time Systems, Essays
                         in Honor of Dines~Bj{\o}rner and Chaochen~Zhou on
                         the Occasion of Their 70th Birthdays},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4700},
  pages =               {300-319},
  year =                {2007},
  month =               sep,
  doi =                 {10.1007/978-3-540-75221-9_13},
}

@article{lmcs3(1)-HR,
  author =              {Hirshfeld, Yoram and Rabinovich, Alexander},
  title =               {Expressiveness of Metric modalities for continuous
                         time},
  journal =             {Logical Methods in Computer Science},
  volume =              {3},
  number =              {1},
  year =                {2007},
  month =               mar,
  doi =                 {10.2168/LMCS-3(1:3)2007},
}

@inproceedings{tacas2007-JLS,
  author =              {Jurdzi{\'n}ski, Marcin and Laroussinie, Fran{\c
                         c}ois and Sproston, Jeremy},
  title =               {Model Checking Probabilistic Timed Automata with One
                         or Two Clocks},
  editor =              {Grumberg, Orna and Huth, Michael},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'07)},
  acronym =             {{TACAS}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4424},
  pages =               {170-184},
  year =                {2007},
  month =               mar,
  doi =                 {10.1007/978-3-540-71209-1_15},
}

@inproceedings{icfem2007-JMO,
  author =              {Julliand, Jacques and Mountassir, Hassan and Oudot,
                         {\'E}milie},
  title =               {{V}e{STA}: A~Tool to Verify the Correct Integration
                         of a Component in a Composite Timed System},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference on {F}ormal {E}ngineering {M}ethods
                         ({ICFEM}'07)},
  acronym =             {{ICFEM}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4789},
  pages =               {116-135},
  year =                {2007},
  month =               nov,
  doi =                 {10.1007/978-3-540-76650-6_8},
}

@inproceedings{formats2007-JRLD,
  author =              {Jensen, Jan J. and Rasmussen, Jacob Illum and
                         Larsen, Kim Guldstrand and David, Alexandre},
  title =               {Guided Controller Synthesis for Climate Controller
                         Using {UPPAAL} {T}iga},
  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 =               {227-240},
  year =                {2007},
  month =               oct,
}

@article{ipl104(5)-JS,
  author =              {Jan{\v c}ar, Petr and Sawa, Zden{\v{e}}k},
  title =               {A note on Emptiness for Alternating Finite Automata
                         with a One-letter Alphabet},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {104},
  number =              {5},
  pages =               {164-167},
  year =                {2007},
  month =               nov,
}

@inproceedings{tacas2007-KDHFDPB,
  author =              {Kupferschmid, Sebastian and Dr{\"a}ger, Klaus and
                         Hoffmann, J{\"o}rg and Finkbeiner, Bernd and Dierks,
                         Henning and Podelski, Andreas and Behrmann, Gerd},
  title =               {{U}ppaal{\slash}{DMC}~-- Abstraction-Based
                         Heuristics for Directed Model Checking},
  editor =              {Grumberg, Orna and Huth, Michael},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'07)},
  acronym =             {{TACAS}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4424},
  pages =               {679-682},
  year =                {2007},
  month =               mar,
}

@inproceedings{concur2007-Lan,
  author =              {Lange, Martin},
  title =               {Linear-Time Logics Around~{PSL}: Complexity,
                         Expressiveness, and a Little Bit of Succinctness},
  editor =              {Caires, Lu{\'\i}s and Vasconcelos, Vasco T.},
  booktitle =           {{P}roceedings of the 18th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'07)},
  acronym =             {{CONCUR}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4703},
  pages =               {90-104},
  year =                {2007},
  month =               sep,
}

@article{jms145(3)-LP,
  author =              {Lifshits, Yuri M. and Pavlov, Dmitri S.},
  title =               {Potential Theory for Mean Payoff Games},
  publisher =           {Springer-Verlag},
  journal =             {Journal of Mathematical Science},
  volume =              {145},
  number =              {3},
  pages =               {4967-4974},
  year =                {2007},
  month =               sep,
}

@article{lww-icomp2007,
  author =              {Lutz, Carsten and Walther, Dirk and Wolter, Frank},
  title =               {Quantitative temporal logics over the reals:
                         {PSPACE} and below},
  publisher =           {Elsevier},
  journal =             {Information and Computation},
  volume =              {205},
  number =              {1},
  pages =               {99-123},
  year =                {2007},
  month =               jan,
  doi =                 {10.1016/j.ic.2006.08.006},
}

@article{transpB41(2)-MO,
  author =              {Mazzarello, Maura and Ottaviani, Ennio},
  title =               {A~traffic management system for real-time traffic
                         optimisation in railways},
  publisher =           {Elsevier},
  journal =             {Transportation Research Part B: Methodological},
  volume =              {41},
  number =              {2},
  pages =               {246-274},
  year =                {2007},
  month =               feb,
  doi =                 {10.1016/j.trb.2006.02.005},
}

@article{alga48(1)-MS,
  author =              {Mavronicolas, Marios and Spirakis, Paul G.},
  title =               {The price of selfish routing},
  publisher =           {Springer-Verlag},
  journal =             {Algorithmica},
  volume =              {48},
  number =              {1},
  pages =               {91-126},
  year =                {2007},
  month =               may,
  doi =                 {10.1007/s00453-006-0056-1},
}

@article{tsmcA37(3)-NB,
  author =              {Narasimhan, Sriram and Biswas, Gautam},
  title =               {Model-Based Diagnosis of Hybrid Systems},
  publisher =           {IEEE},
  journal =             {IEEE Transactions on Systems, Man, and
                         Cybernetics~-- Part~A: Systems and Humans},
  volume =              {37},
  number =              {3},
  pages =               {348-361},
  year =                {2007},
  month =               may,
  doi =                 {10.1109/TSMCA.2007.893487},
}

@book{agt2007-NRTV,
  title =               {Algorithmic Game Theory},
  editor =              {Nisan, Noam and Roughgarden, Tim and Tardos, {\'E}va
                         and Vazirani, Vijay V.},
  booktitle =           {Algorithmic Game Theory},
  publisher =           {Cambridge University Press},
  year =                {2007},
}

@article{lmcs3(1)-OW,
  author =              {Ouaknine, Jo{\"e}l and Worrell, James},
  title =               {On the Decidability and Complexity of Metric
                         Temporal Logic over Finite Words},
  journal =             {Logical Methods in Computer Science},
  volume =              {3},
  number =              {1},
  year =                {2007},
  month =               mar,
  doi =                 {10.2168/LMCS-3(1:8)2007},
}

@incollection{agt2007-Pap,
  author =              {Papadimitriou, {\relax Ch}ristos H.},
  title =               {The complexity of finding {N}ash equilibria},
  editor =              {Nisan, Noam and Roughgarden, Tim and Tardos, {\'E}va
                         and Vazirani, Vijay V.},
  booktitle =           {Algorithmic Game Theory},
  publisher =           {Cambridge University Press},
  pages =               {29-51},
  chapter =             {2},
  year =                {2007},
}

@inproceedings{atva2007-Pin,
  author =              {Pinchinat, Sophie},
  title =               {A Generic constructive Solution for Concurrent Games
                         with Expressive Constraints on Strategies},
  editor =              {Namjoshi, Kedar and Yoneda, Tomohiro and Higashino,
                         Teruo and Okamura, Yoshio},
  booktitle =           {{P}roceedings of the 5th {I}nternational {S}ymposium
                         on {A}utomated {T}echnology for {V}erification and
                         {A}nalysis ({ATVA}'07)},
  acronym =             {{ATVA}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4762},
  pages =               {253-267},
  year =                {2007},
  month =               oct,
}

@techreport{TRCS0702-Pin,
  author =              {Pinchinat, Sophie},
  title =               {Quantified Mu-Calculus with Decision Modalities for
                         Concurrent Game Structures},
  number =              {TR-CS-07-02},
  year =                {2007},
  month =               jan,
  institution =         {The Australian National University, Australia},
}

@techreport{TRCS0702-Pin,
  author =              {Pinchinat, Sophie},
  title =               {Quantified Mu-Calculus with Decision Modalities for
                         Concurrent Game Structures},
  number =              {TR-CS-07-02},
  year =                {2007},
  month =               jan,
  institution =         {The Australian National University, Australia},
}

@inproceedings{tacas2007-RBL,
  author =              {Rasmussen, Jacob Illum and Behrmann, Gerd and
                         Larsen, Kim Guldstrand},
  title =               {Complexity in Simplicity: Flexible Agent-Based State
                         Space Exploration},
  editor =              {Grumberg, Orna and Huth, Michael},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'07)},
  acronym =             {{TACAS}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4424},
  pages =               {231-245},
  year =                {2007},
  month =               mar,
  doi =                 {10.1007/978-3-540-71209-1_19},
}

@phdthesis{phd-reynier,
  author =              {Reynier, Pierre-Alain},
  title =               {V{\'e}rification de syst{\`e}mes temporis{\'e}s et
                         distribu{\'e}s~: mod{\`e}les, algorithmes et
                         impl{\'e}mentabilit{\'e}},
  year =                {2007},
  month =               jun,
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
}

@incollection{agt2007-ch18-Rou,
  author =              {Roughgarden, Tim},
  title =               {Routing games},
  editor =              {Nisan, Noam and Roughgarden, Tim and Tardos, {\'E}va
                         and Vazirani, Vijay V.},
  booktitle =           {Algorithmic Game Theory},
  publisher =           {Cambridge University Press},
  pages =               {461-486},
  chapter =             {18},
  year =                {2007},
}

@inproceedings{aaai2007-RRDGJ,
  author =              {Rahwan, Talal and Ramchurn, Sarvapali D. and Dung
                         Dang, Viet and Giovannucci, Andrea and Jennings,
                         Nicholas R.},
  title =               {Anytime Optimal Coalition Structure Generation},
  booktitle =           {{P}roceedings of the 22nd {N}ational {C}onference on
                         {A}rtificial {I}ntelligence ({AAAI}'07) and 19th
                         {I}nnovative {A}pplications of {A}rtificial
                         {I}ntelligence {C}onference ({IAAI}'07)},
  acronym =             {{AAAI-IAAI}'07},
  publisher =           {AAAI Press},
  pages =               {1184-1190},
  year =                {2007},
  month =               jul,
}

@inproceedings{lopstr2006-SF,
  author =              {Schewe, Sven and Finkbeiner, Bernd},
  title =               {Synthesis of Asynchronous Systems},
  editor =              {Puebla, Germ{\'a}n},
  booktitle =           {{R}evised {S}elected {P}apers of the 16th
                         {I}nternational {S}ymposium on {L}ogic-{B}ased
                         {P}rogram {S}ynthesis and {T}ransformation
                         ({LOPSTR}'06)},
  acronym =             {{LOPSTR}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4407},
  pages =               {127-142},
  year =                {2007},
  confyear =            {2006},
  confmonth =           {7},
}

@inproceedings{time2007-SF,
  author =              {Swaminathan, Mani and Fr{\"a}nzle, Martin},
  title =               {A Symbolic Decision Procedure for Robust Safety of
                         Timed Systems},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {S}ymposium on {T}emporal {R}epresentation and
                         {R}easoning ({TIME}'07)},
  acronym =             {{TIME}'07},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {192},
  year =                {2007},
  month =               jun,
}

@article{alga2007-STZ,
  author =              {Suri, Subhash and T{\'o}th, Csaba D. and Zhou,
                         Yunhong},
  title =               {Selfish Load Balancing and Atomic Congestion Games},
  publisher =           {Springer-Verlag},
  journal =             {Algorithmica},
  volume =              {47},
  number =              {1},
  pages =               {79-96},
  year =                {2007},
  month =               jan,
  doi =                 {10.1007/s00453-006-1211-4},
}

@book{DL07-Vaa,
  author =              {V{\"a}{\"a}n{\"a}nen, Jouko},
  title =               {Dependence Logic: A~New Approach to
                         Independence-Friendly Logic},
  publisher =           {Cambridge University Press},
  series =              {London Mathematical Society Student Texts},
  volume =              {70},
  year =                {2007},
  doi =                 {10.1017/CBO9780511611193},
}

@inproceedings{stacs2007-Var,
  author =              {Vardi, Moshe Y.},
  title =               {The {B}{\"u}chi Complementation Saga},
  editor =              {Thomas, Wolfgang and Weil, Pascal},
  booktitle =           {{P}roceedings of the 24th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'07)},
  acronym =             {{STACS}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4393},
  pages =               {12-22},
  year =                {2007},
  month =               feb,
}

@inproceedings{tark2007-WHW,
  author =              {Walther, Dirk and van der Hoek, Wiebe and
                         Wooldridge, Michael},
  title =               {Alternating-time Temporal Logic with Explicit
                         Strategies},
  editor =              {Samet, Dov},
  booktitle =           {{P}roceedings of the 11th {C}onference on
                         {T}heoretical {A}spects of {R}ationality and
                         {K}nowledge ({TARK}'07)},
  acronym =             {{TARK}'07},
  pages =               {269-278},
  year =                {2007},
  month =               jun,
  doi =                 {10.1145/1324249.1324285},
}

@article{tcsyst40(4)-WS,
  author =              {Weber, Volker and Schwentick, Thomas},
  title =               {Dynamic Complexity Theory Revisited},
  publisher =           {Springer-Verlag},
  journal =             {Theory of Computing Systems},
  volume =              {40},
  number =              {4},
  pages =               {355-377},
  year =                {2007},
  month =               jun,
}