2010
[BCM10] Patricia Bouyer, Fabrice Chevalier, and Nicolas Markey. On the Expressiveness of TPTL and MTL. Information and Computation 208(2):97-116. Elsevier, February 2010.
Abstract

TPTL and MTL are two classical timed extensions of LTL. In this paper, we prove the 20-year-old conjecture that TPTL is strictly more expressive than MTL. But we show that, surprisingly, the TPTL formula proposed by Alur and Henzinger for witnessing this conjecture can be expressed in MTL. More generally, we show that TPTL formulae using only modality F can be translated into MTL.

@article{icomp208(2)-BCM,
  author =              {Bouyer, Patricia and Chevalier, Fabrice and Markey,
                         Nicolas},
  title =               {On the Expressiveness of {TPTL} and {MTL}},
  publisher =           {Elsevier},
  journal =             {Information and Computation},
  volume =              {208},
  number =              {2},
  pages =               {97-116},
  year =                {2010},
  month =               feb,
  doi =                 {10.1016/j.ic.2009.10.004},
  abstract =            {TPTL and MTL are two classical timed extensions
                         of~LTL. In~this paper, we prove the 20-year-old
                         conjecture that TPTL is strictly more expressive
                         than~MTL. But we show that, surprisingly, the
                         TPTL~formula proposed by Alur and Henzinger for
                         witnessing this conjecture \emph{can} be expressed
                         in~MTL. More generally, we show that TPTL formulae
                         using only modality~F can be translated into~MTL.},
}
[BJL+10] Thomas Brihaye, Marc Jungers, Samson Lasaulce, Nicolas Markey, and Ghassan Oreiby. Using Model Checking for Analyzing Distributed Power Control Problems. EURASIP Journal on Wireless Communications and Networking 2010(861472). Hindawi Publishing Corp., June 2010.
Abstract

Model checking (MC) is a formal verification technique which has been known and still knows a resounding success in the computer science community. Realizing that the distributed power control (PC) problem can be modeled by a timed game between a given transmitter and its environment, the authors wanted to know whether this approach can be applied to distributed PC. It turns out that it can be applied successfully and allows one to analyze realistic scenarios including the case of discrete transmit powers and games with incomplete information. The proposed methodology is as follows. We state some objectives a transmitter-receiver pair would like to reach. The network is modeled by a game where transmitters are considered as timed automata interacting with each other. The objectives are then translated into timed alternating-time temporal logic formulae and MC is exploited to know whether the desired properties are verified and determine a winning strategy.

@article{jwcn2010(861472)-BJLMO,
  author =              {Brihaye, {\relax Th}omas and Jungers, Marc and
                         Lasaulce, Samson and Markey, Nicolas and Oreiby,
                         Ghassan},
  title =               {Using Model Checking for Analyzing Distributed Power
                         Control Problems},
  publisher =           {Hindawi Publishing Corp.},
  journal =             {EURASIP Journal on Wireless Communications and
                         Networking},
  volume =              {2010},
  number =              {861472},
  year =                {2010},
  month =               jun,
  doi =                 {10.1155/2010/861472},
  abstract =            {Model checking~(MC) is a formal verification
                         technique which has been known and still knows a
                         resounding success in the computer science
                         community. Realizing that the distributed power
                         control~(PC) problem can be modeled by a timed game
                         between a given transmitter and its environment, the
                         authors wanted to know whether this approach can be
                         applied to distributed~PC. It~turns out that it can
                         be applied successfully and allows one to analyze
                         realistic scenarios including the case of discrete
                         transmit powers and games with incomplete
                         information. The proposed methodology is as follows.
                         We state some objectives a transmitter-receiver pair
                         would like to reach. The network is modeled by a
                         game where transmitters are considered as timed
                         automata interacting with each other. The objectives
                         are then translated into timed alternating-time
                         temporal logic formulae and MC is exploited to know
                         whether the desired properties are verified and
                         determine a winning strategy.},
}
[BBM10] Patricia Bouyer, Romain Brenguier, and Nicolas Markey. Nash Equilibria for Reachability Objectives in Multi-player Timed Games. In CONCUR'10, Lecture Notes in Computer Science 6269, pages 192-206. Springer-Verlag, September 2010.
Abstract

We propose a procedure for computing Nash equilibria in multi-player timed games with reachability objectives. Our procedure is based on the construction of a finite concurrent game, and on a generic characterization of Nash equilibria in (possibly infinite) concurrent games. Along the way, we use our characterization to compute Nash equilibria in finite concurrent games.

@inproceedings{concur2010-BBM,
  author =              {Bouyer, Patricia and Brenguier, Romain and Markey,
                         Nicolas},
  title =               {{N}ash Equilibria for Reachability Objectives in
                         Multi-player Timed Games},
  editor =              {Gastin, Paul and Laroussinie, Fran{\c c}ois},
  booktitle =           {{P}roceedings of the 21st {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'10)},
  acronym =             {{CONCUR}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6269},
  pages =               {192-206},
  year =                {2010},
  month =               sep,
  doi =                 {10.1007/978-3-642-15375-4_14},
  abstract =            {We propose a procedure for computing Nash equilibria
                         in multi-player timed games with reachability
                         objectives. Our procedure is based on the
                         construction of a finite concurrent game, and on a
                         generic characterization of Nash equilibria in
                         (possibly infinite) concurrent games. Along the way,
                         we~use our characterization to compute Nash
                         equilibria in finite concurrent games.},
}
[BBM10] Patricia Bouyer, Romain Brenguier, and Nicolas Markey. Computing Equilibria in Two-Player Timed Games via Turn-Based Finite Games. In FORMATS'10, Lecture Notes in Computer Science 6246, pages 62-76. Springer-Verlag, September 2010.
Abstract

We study two-player timed games where the objectives of the two players are not opposite. We focus on the standard notion of Nash equilibrium and propose a series of transformations that builds two finite turn-based games out of a timed game, with a precise correspondence between Nash equilibria in the original and in final games. This provides us with an algorithm to compute Nash equilibria in two-player timed games for large classes of properties.

@inproceedings{formats2010-BBM,
  author =              {Bouyer, Patricia and Brenguier, Romain and Markey,
                         Nicolas},
  title =               {Computing Equilibria in Two-Player Timed Games
                         {\textit{via}}~Turn-Based Finite Games},
  editor =              {Chatterjee, Krishnendu and Henzinger, Thomas A.},
  booktitle =           {{P}roceedings of the 8th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'10)},
  acronym =             {{FORMATS}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6246},
  pages =               {62-76},
  year =                {2010},
  month =               sep,
  doi =                 {10.1007/978-3-642-15297-9_7},
  abstract =            {We study two-player timed games where the objectives
                         of the two players are not opposite. We focus on the
                         standard notion of Nash equilibrium and propose a
                         series of transformations that builds two finite
                         turn-based games out of a timed game, with a precise
                         correspondence between Nash equilibria in the
                         original and in final games. This provides us with
                         an algorithm to compute Nash equilibria in
                         two-player timed games for large classes of
                         properties.},
}
[BFL+10] Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, and Nicolas Markey. Timed Automata with Observers under Energy Constraints. In HSCC'10, pages 61-70. ACM Press, April 2010.
Abstract

In this paper, we study one-clock priced timed automata in which prices can grow linearly (dp/dt=k) or exponentially (dp/dt=kp), with discontinuous updates on edges. We propose EXPTIME algorithms to decide the existence of controllers that ensure existence of infinite runs or reachability of some goal location with non-negative observer value all along the run. These algorithms consist in computing the optimal delays that should be elapsed in each location along a run, so that the final observer value is maximized (and never goes below zero).

@inproceedings{hscc2010-BFLM,
  author =              {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim
                         Guldstrand and Markey, Nicolas},
  title =               {Timed Automata with Observers under Energy
                         Constraints},
  editor =              {Johansson, Karl Henrik and Yi, Wang},
  booktitle =           {{P}roceedings of the 13th {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
                         ({HSCC}'10)},
  acronym =             {{HSCC}'10},
  publisher =           {ACM Press},
  pages =               {61-70},
  year =                {2010},
  month =               apr,
  doi =                 {10.1145/1755952.1755963},
  abstract =            {In this paper, we study one-clock priced timed
                         automata in which prices can grow linearly
                         (\(\frac{dp}{dt}=k\)) or exponentially
                         (\(\frac{dp}{dt}=kp\)), with discontinuous updates
                         on edges. We propose EXPTIME algorithms to decide
                         the existence of controllers that ensure existence
                         of infinite runs or reachability of some goal
                         location with non-negative observer value all along
                         the run. These algorithms consist in computing the
                         optimal delays that should be elapsed in each
                         location along a run, so that the final observer
                         value is maximized (and never goes below zero).},
}
[DLM10] Arnaud Da Costa, François Laroussinie, and Nicolas Markey. ATL with strategy contexts: Expressiveness and Model Checking. In FSTTCS'10, Leibniz International Proceedings in Informatics 8, pages 120-132. Leibniz-Zentrum für Informatik, December 2010.
Abstract

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

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

@inproceedings{fsttcs2010-DLM,
  author =              {Da{~}Costa, Arnaud and Laroussinie, Fran{\c c}ois
                         and Markey, Nicolas},
  title =               {{ATL} with strategy contexts: Expressiveness and
                         Model Checking},
  editor =              {Lodaya, Kamal and Mahajan, Meena},
  booktitle =           {{P}roceedings of the 30th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'10)},
  acronym =             {{FSTTCS}'10},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {8},
  pages =               {120-132},
  year =                {2010},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2010.120},
  abstract =            {We study the alternating-time temporal logics
                         \(\textsf{ATL}\) and~\(\textsf{ATL}^{*}\) extended
                         with strategy contexts: these make agents commit to
                         their strategies during the evaluation of formulas,
                         contrary to plain \(\textsf{ATL}\)
                         and~\(\textsf{ATL}^{*}\) where strategy quantifiers
                         reset previously selected strategies.\par We
                         illustrate the important expressive power of
                         strategy contexts by proving that they make the
                         extended logics, namely
                         \(\textsf{ATL}_{\textsf{sc}}\)
                         and~\(\textsf{ATL}_{\textsf{sc}}^{*}\), equally
                         expressive: any~formula
                         in~\(\textsf{ATL}_{\textsf{sc}}^{*}\) can be
                         translated into an equivalent, linear-size
                         \(\textsf{ATL}_{\textsf{sc}}\) formula. Despite the
                         high expressiveness of these logics, we prove that
                         they remain decidable by designing a
                         tree-automata-based algorithm for model-checking
                         \(\textsf{ATL}_{\textsf{sc}}\) on the full class of
                         \(n\)-player concurrent game structures.},
}
[HBM+10] Paul Hunter, Patricia Bouyer, Nicolas Markey, Joël Ouaknine, and James Worrell. Computing Rational Radical Sums in Uniform TC0. In FSTTCS'10, Leibniz International Proceedings in Informatics 8, pages 308-316. Leibniz-Zentrum für Informatik, December 2010.
Abstract

A fundamental problem in numerical computation and computational geometry is to determine the sign of arithmetic expressions in radicals. Here we consider the simpler problem of deciding whether ∑i=1m Ci . AiXi is zero for given rational numbers Ai, Ci, Xi. It has been known for almost twenty years that this can be decided in polynomial time. In this paper we improve this result by showing membership in uniform TC0. This requires several significant departures from Blömer's polynomial-time algorithm as the latter crucially relies on primitives, such as gcd computation and binary search, that are not known to be in TC0.

@inproceedings{fsttcs2010-HBMOW,
  author =              {Hunter, Paul and Bouyer, Patricia and Markey,
                         Nicolas and Ouaknine, Jo{\"e}l and Worrell, James},
  title =               {Computing Rational Radical Sums in Uniform
                         {TC\textsuperscript{0}}},
  editor =              {Lodaya, Kamal and Mahajan, Meena},
  booktitle =           {{P}roceedings of the 30th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'10)},
  acronym =             {{FSTTCS}'10},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {8},
  pages =               {308-316},
  year =                {2010},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2010.308},
  abstract =            {A~fundamental problem in numerical computation and
                         computational geometry is to determine the sign of
                         arithmetic expressions in radicals. Here we consider
                         the simpler problem of deciding whether
                         \(\sum_{i=1}^m C_i \cdot A_i^{X_i}\) is zero for
                         given rational numbers~\(A_i\), \(C_i\),~\(X_i\).
                         It~has been known for almost twenty years that this
                         can be decided in polynomial time. In this paper we
                         improve this result by showing membership in uniform
                         \(\textsf{TC}^0\). This requires several significant
                         departures from Bl{\"o}mer's polynomial-time
                         algorithm as the latter crucially relies on
                         primitives, such as gcd computation and binary
                         search, that are not known to be
                         in~\(\textsf{TC}^0\).},
}
[MW10] Nicolas Markey and Jef Wijsen (eds.) Proceedings of the 17th International Symposium on Temporal Representation and Reasoning (TIME'10). IEEE Comp. Soc. Press, September 2010. 
@proceedings{time2010-MW,
  title =               {{P}roceedings of the 17th {I}nternational
                         {S}ymposium on {T}emporal {R}epresentation and
                         {R}easoning ({TIME}'10)},
  editor =              {Markey, Nicolas and Wijsen, Jef},
  booktitle =           {{P}roceedings of the 17th {I}nternational
                         {S}ymposium on {T}emporal {R}epresentation and
                         {R}easoning ({TIME}'10)},
  acronym =             {{TIME}'10},
  publisher =           {IEEE Comp. Soc. Press},
  year =                {2010},
  month =               sep,
  doi =                 {10.1109/TIME.2010.4},
  url =                 {http://ieeexplore.ieee.org/xpl/ tocresult.jsp?
                         reload=true&isnumber=5601852},
}
[ACS10] Tesnim Abdellatif, Jacques Combaz, and Joseph Sifakis. Model-based implementation of real-time applications. In EMSOFT'10, pages 229-238. ACM Press, October 2010. 
@inproceedings{emsoft2010-ACS,
  author =              {Abdellatif, Tesnim and Combaz, Jacques and Sifakis,
                         Joseph},
  title =               {Model-based implementation of real-time
                         applications},
  editor =              {Carloni, Luca P. and Tripakis, Stavros},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {C}onference on {E}mbedded {S}oftware ({EMSOFT}'10)},
  acronym =             {{EMSOFT}'10},
  publisher =           {ACM Press},
  pages =               {229-238},
  year =                {2010},
  month =               oct,
}
[AKY10] Parosh Aziz Abdulla, Pavel Krčál, and Wang Yi. Sampled Semantics of Timed Automata. Logical Methods in Computer Science 6(3). September 2010. 
@article{lmcs6(3)-AJ,
  author =              {Abdulla, Parosh Aziz and Kr{\v{c}}{\'a}l, Pavel and
                         Yi, Wang},
  title =               {Sampled Semantics of Timed Automata},
  journal =             {Logical Methods in Computer Science},
  volume =              {6},
  number =              {3},
  year =                {2010},
  month =               sep,
  doi =                 {10.2168/LMCS-6(3:14)2010},
}
[ALN+10] Natasha Alechina, Brian Logan, Nguyen Hoang Nga, and Abdur Rakib. Resource-bounded alternating-time temporal logic. In AAMAS'10, pages 481-488. International Foundation for Autonomous Agents and Multiagent Systems, May 2010. 
@inproceedings{aamas2010-ALHNR,
  author =              {Alechina, Natasha and Logan, Brian and Nga, Nguyen
                         Hoang and Rakib, Abdur},
  title =               {Resource-bounded alternating-time temporal logic},
  editor =              {van der Hoek, Wiebe and Kaminka, Gal A. and
                         Lesp{\'e}rance, Yves and Luck, Michael and Sen,
                         Sandeep},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference on {A}utonomous {A}gents and
                         {M}ultiagent {S}ystems ({AAMAS}'10)},
  acronym =             {{AAMAS}'10},
  publisher =           {International Foundation for Autonomous Agents and
                         Multiagent Systems},
  pages =               {481-488},
  year =                {2010},
  month =               may,
}
[BBC10] Albert Benveniste, Anne Bouillard, and Paul Caspi. A unifying view of loosely time-triggered architectures. In EMSOFT'10, pages 189-198. ACM Press, October 2010. 
@inproceedings{emsoft2010-BBC,
  author =              {Benveniste, Albert and Bouillard, Anne and Caspi,
                         Paul},
  title =               {A~unifying view of loosely time-triggered
                         architectures},
  editor =              {Carloni, Luca P. and Tripakis, Stavros},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {C}onference on {E}mbedded {S}oftware ({EMSOFT}'10)},
  acronym =             {{EMSOFT}'10},
  publisher =           {ACM Press},
  pages =               {189-198},
  year =                {2010},
  month =               oct,
  doi =                 {10.1145/1879021.1879047},
}
[BC10] Luboš Brim and Jakub Chaloupka. Using Strategy Improvement to Stay Alive. Technical Report FIMU-RS-2010-03, Faculty of Informatics, Masaryk University, Brno, Czech Republic, March 2010. 
@techreport{FIMU-RS-2010-03-BC,
  author =              {Brim, Lubo{\v s} and Chaloupka, Jakub},
  title =               {Using Strategy Improvement to Stay Alive},
  number =              {FIMU-RS-2010-03},
  year =                {2010},
  month =               mar,
  institution =         {Faculty of Informatics, Masaryk University, Brno,
                         Czech Republic},
}
[BJ10] Nils Bulling and Wojciech Jamroga. Model Checking Agents with Memory Is Harder than It Seemed. In AAMAS'10, pages 633-640. International Foundation for Autonomous Agents and Multiagent Systems, May 2010. 
@inproceedings{aamas2010-BJ,
  author =              {Bulling, Nils and Jamroga, Wojciech},
  title =               {Model Checking Agents with Memory Is Harder than It
                         Seemed},
  editor =              {van der Hoek, Wiebe and Kaminka, Gal A. and
                         Lesp{\'e}rance, Yves and Luck, Michael and Sen,
                         Sandeep},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference on {A}utonomous {A}gents and
                         {M}ultiagent {S}ystems ({AAMAS}'10)},
  acronym =             {{AAMAS}'10},
  publisher =           {International Foundation for Autonomous Agents and
                         Multiagent Systems},
  pages =               {633-640},
  year =                {2010},
  month =               may,
}
[BJK10] Tomáš Brázdil, Petr Jančar, and Antonín Kučera. Reachability Games on Extended Vector Addition Systems with States. In ICALP'10, Lecture Notes in Computer Science 6199, pages 478-489. Springer-Verlag, July 2010. 
@inproceedings{icalp2010-BJK,
  author =              {Br{\'a}zdil, Tom{\'a}{\v s} and Jan{\v c}ar, Petr
                         and Ku{\v c}era, Anton{\'\i}n},
  title =               {Reachability Games on Extended Vector Addition
                         Systems with States},
  editor =              {Abramsky, Samson and Gavoille, Cyril and Kirchner,
                         Claude and Meyer auf der Heide, Friedhelm and
                         Spirakis, Paul G.},
  booktitle =           {{P}roceedings of the 37th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'10)~-- Part~{II}},
  acronym =             {{ICALP}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6199},
  pages =               {478-489},
  year =                {2010},
  month =               jul,
  doi =                 {10.1007/978-3-642-14162-1_40},
}
[BJV10] Jasper Berendsen, David N. Jansen, and Frits Vaandrager. Fortuna: model checking priced probabilistic timed automata. In QEST'10, pages 273-281. IEEE Comp. Soc. Press, September 2010. 
@inproceedings{qest2010-BJV,
  author =              {Berendsen, Jasper and Jansen, David N. and
                         Vaandrager, Frits},
  title =               {Fortuna: model checking priced probabilistic timed
                         automata},
  booktitle =           {{P}roceedings of the 7th {I}nternational
                         {C}onference on {Q}uantitative {E}valuation of
                         {S}ystems ({QEST}'10)},
  acronym =             {{QEST}'10},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {273-281},
  year =                {2010},
  month =               sep,
}
[BMP10] Laura Bozzelli, Aniello Murano, and Adriano Peron. Pushdown module checking. Formal Methods in System Design 36(1):65-95. Springer-Verlag, February 2010. 
@article{fmsd36(1)-BMP,
  author =              {Bozzelli, Laura and Murano, Aniello and Peron,
                         Adriano},
  title =               {Pushdown module checking},
  publisher =           {Springer-Verlag},
  journal =             {Formal Methods in System Design},
  volume =              {36},
  number =              {1},
  pages =               {65-95},
  year =                {2010},
  month =               feb,
}
[CD10] Krishnendu Chatterjee and Laurent Doyen. Energy Parity Games. In ICALP'10, Lecture Notes in Computer Science 6199, pages 599-610. Springer-Verlag, July 2010. 
@inproceedings{icalp2010-CD,
  author =              {Chatterjee, Krishnendu and Doyen, Laurent},
  title =               {Energy Parity Games},
  editor =              {Abramsky, Samson and Gavoille, Cyril and Kirchner,
                         Claude and Meyer auf der Heide, Friedhelm and
                         Spirakis, Paul G.},
  booktitle =           {{P}roceedings of the 37th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'10)~-- Part~{II}},
  acronym =             {{ICALP}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6199},
  pages =               {599-610},
  year =                {2010},
  month =               jul,
}
[CDH10] Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Quantitative Languages. ACM Transactions on Computational Logic 11(4). ACM Press, July 2010. 
@article{tocl11(4)-CDH,
  author =              {Chatterjee, Krishnendu and Doyen, Laurent and
                         Henzinger, Thomas A.},
  title =               {Quantitative Languages},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {11},
  number =              {4},
  year =                {2010},
  month =               jul,
  doi =                 {10.1145/1805950.1805953},
}
[CDH+10] Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. Generalized Mean-payoff and Energy Games. In FSTTCS'10, Leibniz International Proceedings in Informatics 8, pages 505-516. Leibniz-Zentrum für Informatik, December 2010. 
@inproceedings{fsttcs2010-CDHR,
  author =              {Chatterjee, Krishnendu and Doyen, Laurent and
                         Henzinger, Thomas A. and Raskin, Jean-Fran{\c c}ois},
  title =               {Generalized Mean-payoff and Energy Games},
  editor =              {Lodaya, Kamal and Mahajan, Meena},
  booktitle =           {{P}roceedings of the 30th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'10)},
  acronym =             {{FSTTCS}'10},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {8},
  pages =               {505-516},
  year =                {2010},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2010.505},
}
[CHP10] Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. Strategy Logic. Information and Computation 208(6):677-693. Elsevier, June 2010. 
@article{icomp208(6)-CHP,
  author =              {Chatterjee, Krishnendu and Henzinger, Thomas A. and
                         Piterman, Nir},
  title =               {Strategy Logic},
  publisher =           {Elsevier},
  journal =             {Information and Computation},
  volume =              {208},
  number =              {6},
  pages =               {677-693},
  year =                {2010},
  month =               jun,
  doi =                 {10.1016/j.ic.2009.07.004},
}
[DBM+10] Kun Deng, Prabir Barooah, Prashant G. Mehta, and Sean P. Meyn. Building thermal model reduction via aggregation of states. In ACC'10, pages 5118-5123. IEEE Comp. Soc. Press, June 2010. 
@inproceedings{acc2010-DBMM,
  author =              {Deng, Kun and Barooah, Prabir and Mehta, Prashant G.
                         and Meyn, Sean P.},
  title =               {Building thermal model reduction via aggregation of
                         states},
  booktitle =           {Proceedings of the 2010 American Control Conference
                         ({ACC}'10)},
  acronym =             {{ACC}'10},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {5118-5123},
  year =                {2010},
  month =               jun,
  doi =                 {10.1109/ACC.2010.5530470},
}
[DDG+10] Aldric Degorre, Laurent Doyen, Raffaella Gentilini, Jean-François Raskin, and Szymon Toruńczyk. Energy and Mean-Payoff Games with Imperfect Information. In CSL'10, Lecture Notes in Computer Science 6247, pages 260-274. Springer-Verlag, August 2010. 
@inproceedings{csl2010-DDGRT,
  author =              {Degorre, Aldric and Doyen, Laurent and Gentilini,
                         Raffaella and Raskin, Jean-Fran{\c c}ois and
                         Toru{\'n}czyk, Szymon},
  title =               {Energy and Mean-Payoff Games with Imperfect
                         Information},
  editor =              {Dawar, Anuj and Veith, Helmut},
  booktitle =           {{P}roceedings of the 24th {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'10)},
  acronym =             {{CSL}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6247},
  pages =               {260-274},
  year =                {2010},
  month =               aug,
  doi =                 {10.1007/978-3-642-15205-4_22},
}
[DGR+10] Barbara Di Giampaolo, Gilles Geeraerts, Jean-François Raskin, and Tali Sznajder. Safraless procedures for timed specifications. In FORMATS'10, Lecture Notes in Computer Science 6246, pages 2-22. Springer-Verlag, September 2010. 
@inproceedings{formats2010-DGRS,
  author =              {Di{~}Giampaolo, Barbara and Geeraerts, Gilles and
                         Raskin, Jean-Fran{\c c}ois and Sznajder, Tali},
  title =               {Safraless procedures for timed specifications},
  editor =              {Chatterjee, Krishnendu and Henzinger, Thomas A.},
  booktitle =           {{P}roceedings of the 8th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'10)},
  acronym =             {{FORMATS}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6246},
  pages =               {2-22},
  year =                {2010},
  month =               sep,
}
[DLL+10] Alexandre David, Kim Guldstrand Larsen, Shuhao Li, Marius Mikučionis, and Brian Nielsen. Testing Real-Time Systems under Uncertainty. In FMCO'10, Lecture Notes in Computer Science 6957, pages 352-371. Springer-Verlag, December 2010. 
@inproceedings{fmco2010-DLLMN,
  author =              {David, Alexandre and Larsen, Kim Guldstrand and Li,
                         Shuhao and Miku{\v{c}}ionis, Marius and Nielsen,
                         Brian},
  title =               {Testing Real-Time Systems under Uncertainty},
  booktitle =           {{R}evised {P}apers of the 13th {I}nternational
                         {C}onference on {F}ormal {M}ethods for {C}omponents
                         and {O}bjects ({FMCO}'10)},
  acronym =             {{FMCO}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6957},
  pages =               {352-371},
  year =                {2010},
  month =               dec,
  doi =                 {10.1007/978-3-642-25271-6_19},
}
[DLS10] Stéphane Demri, Ranko Lazić, and Arnaud Sangnier. Model checking memoryful linear-time logics over one-counter automata. Theoretical Computer Science 411(22-24):2298-2316. Elsevier, May 2010. 
@article{tcs411(22-24)-DLS,
  author =              {Demri, St{\'e}phane and Lazi{\'c}, Ranko and
                         Sangnier, Arnaud},
  title =               {Model checking memoryful linear-time logics over
                         one-counter automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {411},
  number =              {22-24},
  pages =               {2298-2316},
  year =                {2010},
  month =               may,
  doi =                 {10.1016/j.tcs.2010.02.021},
}
[DOT+10] Andreas E. Dalsgaard, Mads Chr. Olesen, Martin Toft, René R. Hansen, and Kim Guldstrand Larsen. METAMOC: Modular Execution Time Analysis using Model Checking. In WCET'10, OpenAccess Series in Informatics 15, pages 113-123. Leibniz-Zentrum für Informatik, July 2010. 
@inproceedings{wcet2010-DOTHL,
  author =              {Dalsgaard, Andreas E. and Olesen, Mads Chr. and
                         Toft, Martin and Hansen, Ren{\'e} R. and Larsen, Kim
                         Guldstrand},
  title =               {METAMOC: Modular Execution Time Analysis using Model
                         Checking},
  editor =              {Lisper, Bj{\"o}rn},
  booktitle =           {{P}roceedings of the 10th {I}nternational {W}orkshop
                         on {W}orst-{C}ase {E}xecution {T}ime {A}nalysis
                         ({WCET}'10)},
  acronym =             {{WCET}'10},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {OpenAccess Series in Informatics},
  volume =              {15},
  pages =               {113-123},
  year =                {2010},
  month =               jul,
}
[DR10] Laurent Doyen and Jean-François Raskin. Antichain Algorithms for Finite Automata. In TACAS'10, Lecture Notes in Computer Science 6015, pages 2-22. Springer-Verlag, March 2010. 
@inproceedings{tacas2010-DR,
  author =              {Doyen, Laurent and Raskin, Jean-Fran{\c c}ois},
  title =               {Antichain Algorithms for Finite Automata},
  editor =              {Esparza, Javier and Majumdar, Rupak},
  booktitle =           {{P}roceedings of the 16th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'10)},
  acronym =             {{TACAS}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6015},
  pages =               {2-22},
  year =                {2010},
  month =               mar,
}
[DSZ10] Giorgio Delzanno, Arnaud Sangnier, and Gianluigi Zavattaro. Parameterized Verification of Ad Hoc Networks. In CONCUR'10, Lecture Notes in Computer Science 6269, pages 313-327. Springer-Verlag, September 2010. 
@inproceedings{concur2010-DSZ,
  author =              {Delzanno, Giorgio and Sangnier, Arnaud and
                         Zavattaro, Gianluigi},
  title =               {Parameterized Verification of Ad~Hoc Networks},
  editor =              {Gastin, Paul and Laroussinie, Fran{\c c}ois},
  booktitle =           {{P}roceedings of the 21st {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'10)},
  acronym =             {{CONCUR}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6269},
  pages =               {313-327},
  year =                {2010},
  month =               sep,
  doi =                 {10.1007/978-3-642-15375-4_22},
}
[EFG+10] Rüdiger Ehlers, Daniel Fass, Michael Gerke, and Hans-Jörg Peter. Fully Symbolic Timed Model Checking Using Constraint Matrix Diagrams. In RTSS'10, pages 360-371. IEEE Comp. Soc. Press, November 2010. 
@inproceedings{rtss2010-EFGP,
  author =              {Ehlers, R{\"u}diger and Fass, Daniel and Gerke,
                         Michael and Peter, Hans-J{\"o}rg},
  title =               {Fully Symbolic Timed Model Checking Using Constraint
                         Matrix Diagrams},
  booktitle =           {{P}roceedings of the 31st {IEEE} {S}ymposium on
                         {R}eal-Time {S}ystems ({RTSS}'10)},
  acronym =             {{RTSS}'10},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {360-371},
  year =                {2010},
  month =               nov,
  doi =                 {10.1109/RTSS.2010.36},
}
[EJT10] Michael Elberfeld, Andreas Jakoby, and Till Tantau. Logspace Versions of the Theorems of Bodlaender and Courcelle. In FOCS'10, pages 143-152. IEEE Comp. Soc. Press, October 2010. 
@inproceedings{focs2010-EJT,
  author =              {Elberfeld, Michael and Jakoby, Andreas and Tantau,
                         Till},
  title =               {Logspace Versions of the Theorems of {B}odlaender
                         and {C}ourcelle},
  booktitle =           {{P}roceedings of the 51st {A}nnual {S}ymposium on
                         {F}oundations of {C}omputer {S}cience ({FOCS}'10)},
  acronym =             {{FOCS}'10},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {143-152},
  year =                {2010},
  month =               oct,
  doi =                 {10.1109/FOCS.2010.21},
}
[EMP10] Rüdiger Ehlers, Robert Mattmüller, and Hans-Jörg Peter. Combining Symbolic Representations for Solving Timed Games. In FORMATS'10, Lecture Notes in Computer Science 6246, pages 107-212. Springer-Verlag, September 2010. 
@inproceedings{formats2010-EMP,
  author =              {Ehlers, R{\"u}diger and Mattm{\"u}ller, Robert and
                         Peter, Hans-J{\"o}rg},
  title =               {Combining Symbolic Representations for Solving Timed
                         Games},
  editor =              {Chatterjee, Krishnendu and Henzinger, Thomas A.},
  booktitle =           {{P}roceedings of the 8th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'10)},
  acronym =             {{FORMATS}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6246},
  pages =               {107-212},
  year =                {2010},
  month =               sep,
  doi =                 {10.1007/978-3-642-15297-9_10},
}
[FKL10] Dana Fisman, Orna Kupferman, and Yoad Lustig. Rational synthesis. In TACAS'10, Lecture Notes in Computer Science 6015, pages 190-204. Springer-Verlag, March 2010. 
@inproceedings{tacas2010-FKL,
  author =              {Fisman, Dana and Kupferman, Orna and Lustig, Yoad},
  title =               {Rational synthesis},
  editor =              {Esparza, Javier and Majumdar, Rupak},
  booktitle =           {{P}roceedings of the 16th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'10)},
  acronym =             {{TACAS}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6015},
  pages =               {190-204},
  year =                {2010},
  month =               mar,
  doi =                 {10.1007/978-3-642-12002-2_16},
}
[FLR10] Emmanuel Filiot, Tristan Le Gall, and Jean-François Raskin. Iterated Regret Minimization in Game Graphs. In MFCS'10, Lecture Notes in Computer Science 6281, pages 342-354. Springer-Verlag, August 2010. 
@inproceedings{mfcs2010-FLR,
  author =              {Filiot, Emmanuel and Le{~}Gall, Tristan and Raskin,
                         Jean-Fran{\c c}ois},
  title =               {Iterated Regret Minimization in Game Graphs},
  editor =              {Hlin{\v{e}}n{\'y}, Petr and Ku{\v c}era,
                         Anton{\'\i}n},
  booktitle =           {{P}roceedings of the 35th {I}nternational
                         {S}ymposium on {M}athematical {F}oundations of
                         {C}omputer {S}cience ({MFCS}'10)},
  acronym =             {{MFCS}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6281},
  pages =               {342-354},
  year =                {2010},
  month =               aug,
}
[GC10] Arie Gurfinkel and Marsha Chechik. Robust Vacuity for Branching Temporal Logic. Research Report cs.LO/1002.4616, arXiv, February 2010. 
@techreport{arxiv-cs.LO/1002.4616,
  author =              {Gurfinkel, Arie and Chechik, Marsha},
  title =               {Robust Vacuity for Branching Temporal Logic},
  number =              {cs.LO/1002.4616},
  year =                {2010},
  month =               feb,
  institution =         {arXiv},
  type =                {Research Report},
}
[GH10] Hugo Gimbert and Florian Horn. Solving simple stochastic tail games. In SODA'10, pages 847-862. Society for Industrial and Applied Math., January 2010. 
@inproceedings{soda2010-GH,
  author =              {Gimbert, Hugo and Horn, Florian},
  title =               {Solving simple stochastic tail games},
  booktitle =           {{P}roceedings of the 21st {A}nnual {ACM}-{SIAM}
                         {S}ymposium on {D}iscrete {A}lgorithms ({SODA}'10)},
  acronym =             {{SODA}'10},
  publisher =           {Society for Industrial and Applied Math.},
  pages =               {847-862},
  year =                {2010},
  month =               jan,
  doi =                 {10.1137/1.9781611973075.69},
}
[GHO+10] Stefan Göller, Christoph Haase, Joël Ouaknine, and James Worrell. Model Checking Succinct and Parametric One-Counter Automata. In ICALP'10, Lecture Notes in Computer Science 6199, pages 575-586. Springer-Verlag, July 2010. 
@inproceedings{icalp2010-GHOW,
  author =              {G{\"o}ller, Stefan and Haase, Christoph and
                         Ouaknine, Jo{\"e}l and Worrell, James},
  title =               {Model Checking Succinct and Parametric One-Counter
                         Automata},
  editor =              {Abramsky, Samson and Gavoille, Cyril and Kirchner,
                         Claude and Meyer auf der Heide, Friedhelm and
                         Spirakis, Paul G.},
  booktitle =           {{P}roceedings of the 37th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'10)~-- Part~{II}},
  acronym =             {{ICALP}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6199},
  pages =               {575-586},
  year =                {2010},
  month =               jul,
  doi =                 {10.1007/978-3-642-14162-1_48},
}
[GL10] Stefan Göller and Markus Lohrey. Branching-time model checking of one-counter processes. In STACS'10, Leibniz International Proceedings in Informatics 20, pages 405-416. Leibniz-Zentrum für Informatik, February 2010. 
@inproceedings{stacs2010-GL,
  author =              {G{\"o}ller, Stefan and Lohrey, Markus},
  title =               {Branching-time model checking of one-counter
                         processes},
  editor =              {Marion, Jean-Yves and Schwentick, Thomas},
  booktitle =           {{P}roceedings of the 27th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'10)},
  acronym =             {{STACS}'10},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {20},
  pages =               {405-416},
  year =                {2010},
  month =               feb,
}
[GP10] Alwyn Goodloe and Lee Pike. Monitoring distributed real-time systems: a survey and future directions. Technical Report NASA/CR-2010-216724, NASA, July 2010. 
@techreport{NASACR10-216724-GP,
  author =              {Goodloe, Alwyn and Pike, Lee},
  title =               {Monitoring distributed real-time systems: a~survey
                         and future directions},
  number =              {NASA/CR-2010-216724},
  year =                {2010},
  month =               jul,
  institution =         {NASA},
  type =                {Technical Report},
}
[GRT10] James Gross, Frank G. Radmacher, and Wolfgang Thomas. A Game-Theoretic Approach to Routing under Adversarial Conditions. In IFIPTCS'10, IFIP Conference Proceedings 323, pages 355-370. Springer-Verlag, September 2010. 
@inproceedings{ifiptcs2010-GRT,
  author =              {Gross, James and Radmacher, Frank G. and Thomas,
                         Wolfgang},
  title =               {A~Game-Theoretic Approach to Routing under
                         Adversarial Conditions},
  editor =              {Calude, Cristian S. and Sassone, Vladimiro},
  booktitle =           {{P}roceedings of the 6th {IFIP} {I}nternational
                         {C}onference on {T}heoretical {C}omputer {S}cience
                         ({IFIPTCS}'10)},
  acronym =             {{IFIPTCS}'10},
  publisher =           {Springer-Verlag},
  series =              {IFIP Conference Proceedings},
  volume =              {323},
  pages =               {355-370},
  year =                {2010},
  month =               sep,
}
[GRV10] Gilles Geeraerts, Jean-François Raskin, and Laurent Van Begin. On the Efficient Computation of the Minimal Coverability Set of Petri Nets. International Journal of Foundations of Computer Science 21(2):135-165. April 2010. 
@article{ijfcs21(2)-GRV,
  author =              {Geeraerts, Gilles and Raskin, Jean-Fran{\c c}ois and
                         Van{~}Begin, Laurent},
  title =               {On the Efficient Computation of the Minimal
                         Coverability Set of {P}etri Nets},
  journal =             {International Journal of Foundations of Computer
                         Science},
  volume =              {21},
  number =              {2},
  pages =               {135-165},
  year =                {2010},
  month =               apr,
}
[HKT10] Michael Holtmann, łukasz Kaiser, and Wolfgang Thomas. Degrees of Lookahead in Regular Infinite Games. In FoSSaCS'10, Lecture Notes in Computer Science 6014, pages 252-266. Springer-Verlag, March 2010. 
@inproceedings{fossacs2010-HKT,
  author =              {Holtmann, Michael and Kaiser, {\L}ukasz and Thomas,
                         Wolfgang},
  title =               {Degrees of Lookahead in Regular Infinite Games},
  editor =              {Ong, Luke},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'10)},
  acronym =             {{FoSSaCS}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6014},
  pages =               {252-266},
  year =                {2010},
  month =               mar,
}
[HLR+10] Holger Hermanns, Kim Guldstrand Larsen, Jean-François Raskin, and Jan Tretmans. Quantitative system validation in model driven design. In EMSOFT'10, pages 301-302. ACM Press, October 2010. 
@inproceedings{emsoft2010-HLRT,
  author =              {Hermanns, Holger and Larsen, Kim Guldstrand and
                         Raskin, Jean-Fran{\c c}ois and Tretmans, Jan},
  title =               {Quantitative system validation in model driven
                         design},
  editor =              {Carloni, Luca P. and Tripakis, Stavros},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {C}onference on {E}mbedded {S}oftware ({EMSOFT}'10)},
  acronym =             {{EMSOFT}'10},
  publisher =           {ACM Press},
  pages =               {301-302},
  year =                {2010},
  month =               oct,
}
[HZH+10] Fei He, He Zhu, William N. N. Hung, Xiaoyu Song, and Ming Gu. Compositional Abstraction Refinement for Timed Systems. In TASE'10, pages 168-176. IEEE Comp. Soc. Press, August 2010. 
@inproceedings{tase2010-HZHSG,
  author =              {He, Fei and Zhu, He and Hung, William N. N. and
                         Song, Xiaoyu and Gu, Ming},
  title =               {Compositional Abstraction Refinement for Timed
                         Systems},
  editor =              {Liu, Jing and Peled, Doron A. and Wang, Bow-Yaw and
                         Wang, Farn},
  booktitle =           {{P}roceedings of the 4th {I}nternational {S}ymposium
                         on {T}heoretical {A}spects of {S}oftware
                         {E}ngineering ({TASE}'10)},
  acronym =             {{TASE}'10},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {168-176},
  year =                {2010},
  month =               aug,
  doi =                 {10.1109/TASE.2010.27},
}
[Mar10] Pavel V. Martyugin. Complexity of Problems Concerning Carefully Synchronizing Words for PFA and Directing Words for NFA. In CSR'10, Lecture Notes in Computer Science 6072, pages 288-302. Springer-Verlag, June 2010. 
@inproceedings{csr2010-Mar,
  author =              {Martyugin, Pavel V.},
  title =               {Complexity of Problems Concerning Carefully
                         Synchronizing Words for~{PFA} and Directing Words
                         for~{NFA}},
  editor =              {Ablayev, Farid M. and Mayr, Ernst W.},
  booktitle =           {{P}roceedings of the 5th {I}nternational {C}omputer
                         {S}cience {S}ymposium in {R}usia ({CSR}'10)},
  acronym =             {{CSR}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6072},
  pages =               {288-302},
  year =                {2010},
  month =               jun,
  doi =                 {10.1007/978-3-642-13182-0_27},
}
[Mar10] Manuel Biscaia Martins. Supervisory Control of Petri Nets using Linear Temporal Logic. Thèse de doctorat, Instituto Superior Técnico, Universidade Técnica de Lisboa, Portugal, January 2010. 
@phdthesis{phd-mbmartins,
  author =              {Martins, Manuel Biscaia},
  title =               {Supervisory Control of {P}etri Nets using Linear
                         Temporal Logic},
  year =                {2010},
  month =               jan,
  school =              {Instituto Superior T\'ecnico, Universidade T\'ecnica
                         de Lisboa, Portugal},
  type =                {Th\`ese de doctorat},
}
[MMV10] Fabio Mogavero, Aniello Murano, and Moshe Y. Vardi. Reasoning about strategies. In FSTTCS'10, Leibniz International Proceedings in Informatics 8, pages 133-144. Leibniz-Zentrum für Informatik, December 2010. 
@inproceedings{fsttcs2010-MMV,
  author =              {Mogavero, Fabio and Murano, Aniello and Vardi, Moshe
                         Y.},
  title =               {Reasoning about strategies},
  editor =              {Lodaya, Kamal and Mahajan, Meena},
  booktitle =           {{P}roceedings of the 30th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'10)},
  acronym =             {{FSTTCS}'10},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {8},
  pages =               {133-144},
  year =                {2010},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2010.133},
}
[MMV10] Fabio Mogavero, Aniello Murano, and Moshe Y. Vardi. Relentful Strategic Reasoning in Alternating-Time Temporal Logic. In LPAR'10, Lecture Notes in Artificial Intelligence 6355, pages 371-386. Springer-Verlag, April 2010. 
@inproceedings{lpar2010(dakar)-MMV,
  author =              {Mogavero, Fabio and Murano, Aniello and Vardi, Moshe
                         Y.},
  title =               {Relentful Strategic Reasoning in Alternating-Time
                         Temporal Logic},
  editor =              {Clarke, Edmund M. and Voronkov, Andrei},
  booktitle =           {{P}roceedings of the 16th {I}nternational
                         {C}onference {L}ogic {P}rogramming and {A}utomated
                         {R}easoning ({LPAR}'10)},
  acronym =             {{LPAR}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Artificial Intelligence},
  volume =              {6355},
  pages =               {371-386},
  year =                {2010},
  month =               apr,
}
[MN10] Janusz Malinowski and Peter Niebert. SAT Based Bounded Model Checking with Partial Order Semantics for Timed Automata. In TACAS'10, Lecture Notes in Computer Science 6015, pages 405-419. Springer-Verlag, March 2010. 
@inproceedings{tacas2010-MN,
  author =              {Malinowski, Janusz and Niebert, Peter},
  title =               {{SAT} Based Bounded Model Checking with Partial
                         Order Semantics for Timed Automata},
  editor =              {Esparza, Javier and Majumdar, Rupak},
  booktitle =           {{P}roceedings of the 16th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'10)},
  acronym =             {{TACAS}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6015},
  pages =               {405-419},
  year =                {2010},
  month =               mar,
}
[NOK10] Takeshi Nagaoka, Kozo Okano, and Shinji Kusumoto. An abstraction refinement technique for timed automata based on counterexample-guided abstraction refinement loop. IEICE Transactions on Information and Systems 5(5):994-1005. Institute of Electronics, Information and Communication Engineers, May 2010. 
@article{IEICEtransinfE93D(5)-NOK,
  author =              {Nagaoka, Takeshi and Okano, Kozo and Kusumoto,
                         Shinji},
  title =               {An abstraction refinement technique for timed
                         automata based on counterexample-guided abstraction
                         refinement loop},
  publisher =           {Institute of Electronics, Information and
                         Communication Engineers},
  journal =             {IEICE Transactions on Information and Systems},
  volume =              {5},
  number =              {5},
  pages =               {994-1005},
  year =                {2010},
  month =               may,
  doi =                 {10.1587/transinf.E93.D.994},
}
[OW10] Joël Ouaknine and James Worrell. Towards a theory of time-bounded verification. In ICALP'10, Lecture Notes in Computer Science 6199, pages 22-37. Springer-Verlag, July 2010. 
@inproceedings{icalp2010-ORW,
  author =              {Ouaknine, Jo{\"e}l and Worrell, James},
  title =               {Towards a theory of time-bounded verification},
  editor =              {Abramsky, Samson and Gavoille, Cyril and Kirchner,
                         Claude and Meyer auf der Heide, Friedhelm and
                         Spirakis, Paul G.},
  booktitle =           {{P}roceedings of the 37th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'10)~-- Part~{II}},
  acronym =             {{ICALP}'10},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {6199},
  pages =               {22-37},
  year =                {2010},
  month =               jul,
}
[PS10] Soumya Paul and Sunil Simon. Nash Equilibrium in Generalised Muller Games. In FSTTCS'09, Leibniz International Proceedings in Informatics 4, pages 335-346. Leibniz-Zentrum für Informatik, December 2010. 
@inproceedings{fsttcs2009-PS,
  author =              {Paul, Soumya and Simon, Sunil},
  title =               {{N}ash Equilibrium in Generalised {M}uller Games},
  editor =              {Kannan, Ravi and Narayan Kumar, K.},
  booktitle =           {{P}roceedings of the 29th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'09)},
  acronym =             {{FSTTCS}'09},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {4},
  pages =               {335-346},
  year =                {2010},
  month =               dec,
}
[Rey10] Mark Reynolds. The Complexity of Temporal Logic over the Reals. Annals of Pure and Applied Logic 161(8):1063-1096. Elsevier, May 2010. 
@article{apal161(8)-Rey,
  author =              {Reynolds, Mark},
  title =               {The Complexity of Temporal Logic over the Reals},
  publisher =           {Elsevier},
  journal =             {Annals of Pure and Applied Logic},
  volume =              {161},
  number =              {8},
  pages =               {1063-1096},
  year =                {2010},
  month =               may,
}
[RJL+10] Christopher Thomas Ryan, Albert Xin Jiang, and Kevin Leyton-Brown. Symmetric Games with Piecewise Linear Utilities. In BQGT'10. ACM Press, May 2010. 
@inproceedings{bqgt10-RJL,
  author =              {Ryan, Christopher Thomas and Jiang, Albert Xin and
                         Leyton-Brown, Kevin},
  title =               {Symmetric Games with Piecewise Linear Utilities},
  editor =              {Dror, Moshe and So{\v{s}}i{\'c}, Greys},
  booktitle =           {{P}roceedings of the {B}ehavioral and {Q}uantitative
                         {G}ame {T}heory: {C}onference on {F}uture
                         {D}irections ({BQGT}'10)},
  acronym =             {{BQGT}'10},
  publisher =           {ACM Press},
  year =                {2010},
  month =               may,
  doi =                 {10.1145/1807406.1807447},
}
[San10] Ocan Sankur. Model-checking robuste des automates temporisés via les machines à canaux. Mémoire de master, Lab. Spécification & Vérification, ENS Cachan, France, 2010. 
@mastersthesis{master10-sankur,
  author =              {Sankur, Ocan},
  title =               {Model-checking robuste des automates temporis{\'e}s
                         via les machines {\`a} canaux},
  year =                {2010},
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {M\'emoire de master},
}
[Spe10] Heike Sperber. How to find Nash equilibria with extreme total latency in network congestion games?. Mathematical Methods of Operations Research 71(2):245-265. Springer-Verlag, April 2010. 
@article{mmor71(2)-Spe,
  author =              {Sperber, Heike},
  title =               {How to find {N}ash equilibria with extreme total
                         latency in network congestion games?},
  publisher =           {Springer-Verlag},
  journal =             {Mathematical Methods of Operations Research},
  volume =              {71},
  number =              {2},
  pages =               {245-265},
  year =                {2010},
  month =               apr,
  doi =                 {10.1007/s00186-009-0293-6},
}
[SW10] Chrstoffer Sloth and Rafael Wisniewski. Timed Game Abstraction of Control Systems. Technical Report 1012.5113, arXiv, December 2010. 
@techreport{arxiv1012.5113-SW,
  author =              {Sloth, Chrstoffer and Wisniewski, Rafael},
  title =               {Timed Game Abstraction of Control Systems},
  number =              {1012.5113},
  year =                {2010},
  month =               dec,
  institution =         {arXiv},
}
[TFL10] Claus Thrane, Uli Fahrenberg, and Kim Guldstrand Larsen. Quantitative Analysis of Weighted Transition Systems. Journal of Logic and Algebraic Programming 79(7):689-703. Elsevier, October 2010. 
@article{jlap79(7)-TFL,
  author =              {Thrane, Claus and Fahrenberg, Uli and Larsen, Kim
                         Guldstrand},
  title =               {Quantitative Analysis of Weighted Transition
                         Systems},
  publisher =           {Elsevier},
  journal =             {Journal of Logic and Algebraic Programming},
  volume =              {79},
  number =              {7},
  pages =               {689-703},
  year =                {2010},
  month =               oct,
}
[Umm10] Michael Ummels. Stochastic multiplayer games: theory and algorithms. PhD thesis, RWTH Aachen, Germany, January 2010. 
@phdthesis{phd10-Umm,
  author =              {Ummels, Michael},
  title =               {Stochastic multiplayer games: theory and algorithms},
  year =                {2010},
  month =               jan,
  school =              {RWTH Aachen, Germany},
}
[WBB+10] Ralf Wimmer, Bettina Braitling, Bernd Becker, Pepijn Crouzen, Holger Hermanns, Abhishek Dhama, and Oliver E. Theel. Symblicit calculation of long-run averages for concurrent probabilistic systems. In QEST'10, pages 27-36. IEEE Comp. Soc. Press, September 2010. 
@inproceedings{qest2010-WBBHCHDT,
  author =              {Wimmer, Ralf and Braitling, Bettina and Becker,
                         Bernd and Crouzen, Pepijn and Hermanns, Holger and
                         Dhama, Abhishek and Theel, Oliver E.},
  title =               {Symblicit calculation of long-run averages for
                         concurrent probabilistic systems},
  booktitle =           {{P}roceedings of the 7th {I}nternational
                         {C}onference on {Q}uantitative {E}valuation of
                         {S}ystems ({QEST}'10)},
  acronym =             {{QEST}'10},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {27-36},
  year =                {2010},
  month =               sep,
}
List of authors