2007
[BLM07] Patricia Bouyer, Kim Guldstrand Larsen et Nicolas Markey. Model Checking One-clock Priced Timed Automata. In FoSSaCS'07, Lecture Notes in Computer Science 4423, pages 108-122. Springer-Verlag, mars 2007.
Résumé

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.},
}
[BLM+07] Thomas Brihaye, François Laroussinie, Nicolas Markey et Ghassan Oreiby. Timed Concurrent Game Structures. In CONCUR'07, Lecture Notes in Computer Science 4703, pages 445-459. Springer-Verlag, septembre 2007.
Résumé

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.}},
}
[BM07] Patricia Bouyer et Nicolas Markey. Costs are Expensive!. In FORMATS'07, Lecture Notes in Computer Science 4763, pages 53-68. Springer-Verlag, octobre 2007.
Résumé

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.},
}
[BMO+07] Patricia Bouyer, Nicolas Markey, Joël Ouaknine et James Worrell. The Cost of Punctuality. In LICS'07, pages 109-118. IEEE Comp. Soc. Press, juillet 2007.
Résumé

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.},
}
[LMO07] François Laroussinie, Nicolas Markey et Ghassan Oreiby. On the Expressiveness and Complexity of ATL. In FoSSaCS'07, Lecture Notes in Computer Science 4423, pages 243-257. Springer-Verlag, mars 2007.
Résumé

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.},
}
[AAE+07] Dana Angluin, James Aspnes, David Eisenstat et Eric Ruppert. The computational power of population protocols. Distributed Computing 20(4):279-304. Springer-Verlag, mars 2007. 
@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},
}
[AGJ07] Thomas Ågotnes, Valentin Goranko et Wojciech Jamroga. Alternating-time Temporal Logics with Irrevocable Strategies. In TARK'07, pages 15-24. Juin 2007. 
@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,
}
[dAH+07] Luca de Alfaro, Thomas A. Henzinger et Orna Kupferman. Concurrent Reachability Games. Theoretical Computer Science 386(3):188-217. Elsevier, novembre 2007. 
@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},
}
[ASY07] Eugene Asarin, Gerardo Schneider et Sergio Yovine. Algorithmic analysis of polygonal hybrid systems, part I: Reachability. Theoretical Computer Science 379(1-2):231-265. Elsevier, juin 2007. 
@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,
}
[BBB+07] Christel Baier, Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye et Marcus Größer. Probabilistic and Topological Semantics for Timed Automata. In FSTTCS'07, Lecture Notes in Computer Science 4855, pages 179-191. Springer-Verlag, décembre 2007. 
@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,
}
[BBB+07] Éric Badouel, Marek Bednarczyk, Andrzej Borzyszkowski, Benoît Caillaud et Philippe Darondeau. Concurrent secrets. Discrete Event Dynamic Systems 17(4):425-446. Kluwer Academic, décembre 2007. 
@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},
}
[BBB+07] Patricia Bouyer, Thomas Brihaye, Véronique Bruyère et Jean-François Raskin. On the Optimal Reachability Problem of Weighted Timed Automata. Formal Methods in System Design 31(2):135-175. Springer-Verlag, octobre 2007. 
@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},
}
[BBG+07] Christel Baier, Tomáš Brázdil, Marcus Größer et Antonín Kučera. Stochastic Game Logic. In QEST'07, pages 227-236. IEEE Comp. Soc. Press, septembre 2007. 
@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,
}
[BCD+07] Gerd Behrmann, Agnès Cougnard, Alexandre David, Emmanuel Fleury, Kim Guldstrand Larsen et Didier Lime. UPPAAL-Tiga: Time for Playing Games!. In CAV'07, Lecture Notes in Computer Science 4590, pages 121-125. Springer-Verlag, juillet 2007. 
@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,
}
[BHP+07] Thomas Brihaye, Thomas A. Henzinger, Vinayak S. Prabhu et Jean-François Raskin. Minimum-Time Reachability in Timed Games. In ICALP'07, Lecture Notes in Computer Science 4596, pages 825-837. Springer-Verlag, juillet 2007. 
@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,
}
[BHT07] Dirk Beyer, Thomas A. Henzinger et Grégory Théoduloz. Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis. In CAV'07, Lecture Notes in Computer Science 4590. Springer-Verlag, juillet 2007. 
@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},
}
[BV07] Henrik Björklund et Sergei Vorobyov. A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games. Discrete Applied Mathematics 155(2):210-229. Elsevier, janvier 2007. 
@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},
}
[CDL+07] Franck Cassez, Alexandre David, Kim Guldstrand Larsen, Didier Lime et Jean-François Raskin. Timed Control with Observation Based and Stuttering Invariant Strategies. In ATVA'07, Lecture Notes in Computer Science 4762, pages 192-206. Springer-Verlag, octobre 2007. 
@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},
}
[Cha07] Krishnendu Chatterjee. Stochastic ω-regular games. PhD thesis, University of Califormia at Berkeley, USA, 2007. 
@phdthesis{phd-chatterjee,
  author =              {Chatterjee, Krishnendu},
  title =               {Stochastic {\(\omega\)}-regular games},
  year =                {2007},
  school =              {University of Califormia at Berkeley, USA},
}
[CHP07] Krishnendu Chatterjee, Thomas A. Henzinger et Nir Piterman. Generalized Parity Games. In FoSSaCS'07, Lecture Notes in Computer Science 4423, pages 153-167. Springer-Verlag, mars 2007. 
@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,
}
[CHP07] Krishnendu Chatterjee, Thomas A. Henzinger et Nir Piterman. Strategy Logic. In CONCUR'07, Lecture Notes in Computer Science 4703, pages 59-73. Springer-Verlag, septembre 2007. 
@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},
}
[CL07] Taolue Chen et Jian Lu. Probabilistic Alternating-time Temporal Logic and Model Checking Algorithm. In FSKD'07, pages 35-39. IEEE Comp. Soc. Press, août 2007. 
@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},
}
[CR07] Olivier Carton et Chloé Rispal. Complementation of rational sets on scattered linear orderings of finite rank. Theoretical Computer Science 382(2):109-119. Elsevier, août 2007. 
@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,
}
[DDG07] Stéphane Demri, Deepak D'Souza et Régis Gascon. Decidable Temporal Logic with Repeating Values. In LFCS'07, Lecture Notes in Computer Science 4514, pages 180-194. Springer-Verlag, juin 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,
}
[DG07] Manfred Droste et Paul Gastin. Weighted automata and weighted logics. Theoretical Computer Science 380(1-2):69-86. Elsevier, juin 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,
}
[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, octobre 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,
}
[DKL07] Henning Dierks, Sebastian Kupferschmid et Kim Guldstrand Larsen. Automatic abstraction refinement for timed automata. In FORMATS'07, Lecture Notes in Computer Science 4763, pages 114-129. Springer-Verlag, octobre 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},
}
[DN07] Stéphane Demri et David Nowak. Reasoning about Transfinite Sequences. International Journal of Foundations of Computer Science 18(1):87-112. Février 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},
}
[Doy07] Laurent Doyen. Robust parametric reachability for timed automata. Information Processing Letters 102(5):208-213. Elsevier, mai 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},
}
[DP07] Deepak D'Souza et 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, février 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 et Marco Pranzo. A branch-and-bound algorithm for scheduling trains in a railway network. European Journal of Operational Research 183(2):643-657. Elsevier, décembre 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},
}
[EY07] Kousha Etessami et Mihalis Yannakakis. On the Complexity of Nash Equilibria and Other Fixed Points (Extended Abstract). In FOCS'07, pages 113-123. IEEE Comp. Soc. Press, octobre 2007. 
@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,
}
[FMR07] Tim French, John C. McCabe-Dansted et Mark Reynolds. A Temporal Logic of Robustness. In FroCoS'07, Lecture Notes in Artificial Intelligence 4720, pages 193-205. Springer-Verlag, septembre 2007. 
@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},
}
[FPR07] Carlo A. Furia, Matteo Pradella et Matteo Rossi. Dense-Time MTL Verification Through Sampling. Research Report 2007-37, Dipartimento di Elettronica ed Informazione, Politecnico di Milano, Italy, avril 2007. 
@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},
}
[FR07] Carlo A. Furia et Matteo Rossi. On the Expressiveness of MTL Variants over Dense Time. In FORMATS'07, Lecture Notes in Computer Science 4763, pages 163-178. Springer-Verlag, octobre 2007. 
@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},
}
[GMP07] Villiam Geffert, Carlo Mereghetti et Giovanni Pighizzini. Complementing Two-way Finite Automata. Information and Computation 205(8):1173-1187. Elsevier, août 2007. 
@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,
}
[HMB07] Michael R. Hansen, Jan Madsen et Aske Wiid Brekling. Semantics and Verification of a Language for Modelling Hardware Architectures. In Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bjørner and Chaochen Zhou on the Occasion of Their 70th Birthdays, Lecture Notes in Computer Science 4700, pages 300-319. Springer-Verlag, septembre 2007. 
@inproceedings{BZbday07-HMB,
  author =              {Hansen, Michael R. and Madsen, Jan and Brekling,
                         Aske Wiid},
  title =               {Semantics and Verification of a Language for
                         Modelling Hardware Architectures},
  editor =              {Jones, Cliff B. and Liu, Zhiming and Woodcock, Jim},
  booktitle =           {Formal Methods and Hybrid Real-Time Systems, Essays
                         in Honor of Dines~Bj{\o}rner and Chaochen~Zhou on
                         the Occasion of Their 70th Birthdays},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4700},
  pages =               {300-319},
  year =                {2007},
  month =               sep,
  doi =                 {10.1007/978-3-540-75221-9_13},
}
[HR07] Yoram Hirshfeld et Alexander Rabinovich. Expressiveness of Metric modalities for continuous time. Logical Methods in Computer Science 3(1). Mars 2007. 
@article{lmcs3(1)-HR,
  author =              {Hirshfeld, Yoram and Rabinovich, Alexander},
  title =               {Expressiveness of Metric modalities for continuous
                         time},
  journal =             {Logical Methods in Computer Science},
  volume =              {3},
  number =              {1},
  year =                {2007},
  month =               mar,
  doi =                 {10.2168/LMCS-3(1:3)2007},
}
[JLS07] Marcin Jurdziński, François Laroussinie et Jeremy Sproston. Model Checking Probabilistic Timed Automata with One or Two Clocks. In TACAS'07, Lecture Notes in Computer Science 4424, pages 170-184. Springer-Verlag, mars 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},
}
[JMO07] Jacques Julliand, Hassan Mountassir et Émilie Oudot. VeSTA: A Tool to Verify the Correct Integration of a Component in a Composite Timed System. In ICFEM'07, Lecture Notes in Computer Science 4789, pages 116-135. Springer-Verlag, novembre 2007. 
@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},
}
[JRL+07] Jan J. Jensen, Jacob Illum Rasmussen, Kim Guldstrand Larsen et Alexandre David. Guided Controller Synthesis for Climate Controller Using UPPAAL Tiga. In FORMATS'07, Lecture Notes in Computer Science 4763, pages 227-240. Springer-Verlag, octobre 2007. 
@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,
}
[JS07] Petr Jančar et Zdeněk Sawa. A note on Emptiness for Alternating Finite Automata with a One-letter Alphabet. Information Processing Letters 104(5):164-167. Elsevier, novembre 2007. 
@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,
}
[KDH+07] Sebastian Kupferschmid, Klaus Dräger, Jörg Hoffmann, Bernd Finkbeiner, Henning Dierks, Andreas Podelski et Gerd Behrmann. Uppaal/DMC – Abstraction-Based Heuristics for Directed Model Checking. In TACAS'07, Lecture Notes in Computer Science 4424, pages 679-682. Springer-Verlag, mars 2007. 
@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,
}
[Lan07] Martin Lange. Linear-Time Logics Around PSL: Complexity, Expressiveness, and a Little Bit of Succinctness. In CONCUR'07, Lecture Notes in Computer Science 4703, pages 90-104. Springer-Verlag, septembre 2007. 
@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,
}
[LP07] Yuri M. Lifshits et Dmitri S. Pavlov. Potential Theory for Mean Payoff Games. Journal of Mathematical Science 145(3):4967-4974. Springer-Verlag, septembre 2007. 
@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,
}
[LWW07] Carsten Lutz, Dirk Walther et Frank Wolter. Quantitative temporal logics over the reals: PSPACE and below. Information and Computation 205(1):99-123. Elsevier, janvier 2007. 
@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},
}
[MO07] Maura Mazzarello et Ennio Ottaviani. A traffic management system for real-time traffic optimisation in railways. Transportation Research Part B: Methodological 41(2):246-274. Elsevier, février 2007. 
@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},
}
[MS07] Marios Mavronicolas et Paul G. Spirakis. The price of selfish routing. Algorithmica 48(1):91-126. Springer-Verlag, mai 2007. 
@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},
}
[NB07] Sriram Narasimhan et Gautam Biswas. Model-Based Diagnosis of Hybrid Systems. IEEE Transactions on Systems, Man, and Cybernetics – Part A: Systems and Humans 37(3):348-361. IEEE, mai 2007. 
@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},
}
[NRT+07] Noam Nisan, Tim Roughgarden, Éva Tardos et Vijay V. Vazirani. Algorithmic Game Theory. Cambridge University Press, 2007. 
@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},
}
[OW07] Joël Ouaknine et James Worrell. On the Decidability and Complexity of Metric Temporal Logic over Finite Words. Logical Methods in Computer Science 3(1). Mars 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},
}
[Pap07] Christos H. Papadimitriou. The complexity of finding Nash equilibria. In Noam Nisan, Tim Roughgarden, Éva Tardos et Vijay V. Vazirani (eds.), Algorithmic Game Theory. Cambridge University Press, 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},
}
[Pin07] Sophie Pinchinat. A Generic constructive Solution for Concurrent Games with Expressive Constraints on Strategies. In ATVA'07, Lecture Notes in Computer Science 4762, pages 253-267. Springer-Verlag, octobre 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,
}
[Pin07] Sophie Pinchinat. Quantified Mu-Calculus with Decision Modalities for Concurrent Game Structures. Technical Report TR-CS-07-02, The Australian National University, Australia, janvier 2007. 
@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},
}
[Pin07] Sophie Pinchinat. Quantified Mu-Calculus with Decision Modalities for Concurrent Game Structures. Technical Report TR-CS-07-02, The Australian National University, Australia, janvier 2007. 
@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},
}
[RBL07] Jacob Illum Rasmussen, Gerd Behrmann et Kim Guldstrand Larsen. Complexity in Simplicity: Flexible Agent-Based State Space Exploration. In TACAS'07, Lecture Notes in Computer Science 4424, pages 231-245. Springer-Verlag, mars 2007. 
@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},
}
[Rey07] Pierre-Alain Reynier. Vérification de systèmes temporisés et distribués : modèles, algorithmes et implémentabilité. PhD thesis, Lab. Spécification & Vérification, ENS Cachan, France, Juin 2007. 
@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},
}
[Rou07] Tim Roughgarden. Routing games. In Noam Nisan, Tim Roughgarden, Éva Tardos et Vijay V. Vazirani (eds.), Algorithmic Game Theory. Cambridge University Press, 2007. 
@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},
}
[RRD+07] Talal Rahwan, Sarvapali D. Ramchurn, Viet Dung Dang, Andrea Giovannucci et Nicholas R. Jennings. Anytime Optimal Coalition Structure Generation. In AAAI-IAAI'07, pages 1184-1190. AAAI Press, juillet 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,
}
[SF07] Sven Schewe et Bernd Finkbeiner. Synthesis of Asynchronous Systems. In LOPSTR'06, Lecture Notes in Computer Science 4407, pages 127-142. Springer-Verlag, 2007. 
@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},
}
[SF07] Mani Swaminathan et Martin Fränzle. A Symbolic Decision Procedure for Robust Safety of Timed Systems. In TIME'07, pages 192. IEEE Comp. Soc. Press, juin 2007. 
@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,
}
[STZ07] Subhash Suri, Csaba D. Tóth et Yunhong Zhou. Selfish Load Balancing and Atomic Congestion Games. Algorithmica 47(1):79-96. Springer-Verlag, janvier 2007. 
@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},
}
[Vaa07] Jouko Väänänen. Dependence Logic: A New Approach to Independence-Friendly Logic. London Mathematical Society Student Texts 70. Cambridge University Press, 2007. 
@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},
}
[Var07] Moshe Y. Vardi. The Büchi Complementation Saga. In STACS'07, Lecture Notes in Computer Science 4393, pages 12-22. Springer-Verlag, février 2007. 
@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,
}
[WvdH+07] Dirk Walther, Wiebe van der Hoek et Michael Wooldridge. Alternating-time Temporal Logic with Explicit Strategies. In TARK'07, pages 269-278. Juin 2007. 
@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},
}
[WS07] Volker Weber et Thomas Schwentick. Dynamic Complexity Theory Revisited. Theory of Computing Systems 40(4):355-377. Springer-Verlag, juin 2007. 
@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,
}
Liste des auteurs