Nicolas Markey

Abstract

We consider the model of priced (a.k.a. weighted) timed automata, an extension of timed automata with cost information on both locations and transitions, and we study various model-checking problems for that model based on extensions of classical temporal logics with cost constraints on modalities. We prove that, under the assumption that the model has only one clock, model-checking this class of models against the logic WCTL, CTL with cost-constrained modalities, is PSPACE-complete (while it has been shown undecidable as soon as the model has three clocks). We also prove that model checking WMTL (LTL with cost-constrained modalities) is decidable only if there is a single clock in the model and a single stopwatch cost variable (i.e., whose slopes lie in {0,1}).

@article{lmcs4(2)-BLM,
  author =              {Bouyer, Patricia and Larsen, Kim Guldstrand and
                         Markey, Nicolas},
  title =               {Model Checking One-clock Priced Timed Automata},
  journal =             {Logical Methods in Computer Science},
  volume =              {4},
  number =              {2},
  year =                {2008},
  month =               may,
  doi =                 {10.2168/LMCS-4(2:9)2008},
  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,
                         and we study various model-checking problems for
                         that model based on extensions of classical temporal
                         logics with cost constraints on modalities. We prove
                         that, under the assumption that the model has only
                         one clock, model-checking this class of models
                         against the logic~WCTL, CTL with cost-constrained
                         modalities, is PSPACE-complete (while it has been
                         shown undecidable as soon as the model has three
                         clocks). We~also prove that model checking WMTL (LTL
                         with cost-constrained modalities) is decidable only
                         if there is a single clock in the model and a single
                         stopwatch cost variable (\textit{i.e.}, whose slopes
                         lie in~\(\{0,1\}\)).},
}

Abstract

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

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

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

Abstract

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

@article{lmcs4(2)-LMO,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
                         Oreiby, Ghassan},
  title =               {On the Expressiveness and Complexity of~{ATL}},
  journal =             {Logical Methods in Computer Science},
  volume =              {4},
  number =              {2},
  year =                {2008},
  month =               may,
  doi =                 {10.2168/LMCS-4(2:7)2008},
  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.},
}

Abstract

In [Baier et al., Probabilistic and Topological Semantics for Timed Automata, FSTTCS'07] a probabilistic semantics for timed automata has been defined in order to rule out unlikely (sequences of) events. The qualitative model-checking problem for LTL properties has been investigated, where the aim is to check whether a given LTL property holds with probability 1 in a timed automaton, and solved for the class of single-clock timed automata.

In this paper, we consider the quantitative model-checking problem for ω-regular properties: we aim at computing the exact probability that a given timed automaton satisfies an ω-regular property. We develop a framework in which we can compute a closed-form expression for this probability; we furthermore give an approximation algorithm, and finally prove that we can decide the threshold problem in that framework.

@inproceedings{qest2008-BBBM,
  author =              {Bertrand, Nathalie and Bouyer, Patricia and Brihaye,
                         {\relax Th}omas and Markey, Nicolas},
  title =               {Quantitative Model-Checking of One-Clock Timed
                         Automata under Probabilistic Semantics},
  booktitle =           {{P}roceedings of the 5th {I}nternational
                         {C}onference on {Q}uantitative {E}valuation of
                         {S}ystems ({QEST}'08)},
  acronym =             {{QEST}'08},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {55-64},
  year =                {2008},
  month =               sep,
  doi =                 {10.1109/QEST.2008.19},
  abstract =            {In [Baier \emph{et~al.}, \textit{Probabilistic and
                         Topological Semantics for Timed Automata},
                         FSTTCS'07] a probabilistic semantics for timed
                         automata has been defined in order to rule out
                         unlikely (sequences of) events. The qualitative
                         model-checking problem for LTL properties has been
                         investigated, where the aim is to check whether a
                         given LTL property holds with probability~\(1\) in a
                         timed automaton, and solved for the class of
                         single-clock timed automata.\par In this paper, we
                         consider the quantitative model-checking problem for
                         \(\omega\)-regular properties: we aim at computing
                         the exact probability that a given timed automaton
                         satisfies an \(\omega\)-regular property. We develop
                         a framework in which we can compute a closed-form
                         expression for this probability; we furthermore give
                         an approximation algorithm, and finally prove that
                         we can decide the threshold problem in that
                         framework.},
}

Abstract

We study the problems of existence and construction of infinite schedules for finite weighted automata and one-clock weighted timed automata, subject to boundary constraints on the accumulated weight. More specifically, we consider automata equipped with positive and negative weights on transitions and locations, corresponding to the production and consumption of some resource (e.g. energy). We ask the question whether there exists an infinite path for which the accumulated weight for any finite prefix satisfies certain constraints (e.g. remains between 0 and some given upper-bound). We also consider a game version of the above, where certain transitions may be uncontrollable.

@inproceedings{formats2008-BFLMS,
  author =              {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim
                         Guldstrand and Markey, Nicolas and Srba, Ji{\v
                         r}{\'\i}},
  title =               {Infinite Runs in Weighted Timed Automata with Energy
                         Constraints},
  editor =              {Cassez, Franck and Jard, Claude},
  booktitle =           {{P}roceedings of the 6th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'08)},
  acronym =             {{FORMATS}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5215},
  pages =               {33-47},
  year =                {2008},
  month =               sep,
  doi =                 {10.1007/978-3-540-85778-5_4},
  abstract =            {We~study the problems of existence and construction
                         of infinite schedules for finite weighted automata
                         and one-clock weighted timed automata, subject to
                         boundary constraints on the accumulated weight. More
                         specifically, we~consider automata equipped with
                         positive and negative weights on transitions and
                         locations, corresponding to the production and
                         consumption of some resource (\emph{e.g.}~energy).
                         We~ask the question whether there exists an infinite
                         path for which the accumulated weight for any finite
                         prefix satisfies certain constraints
                         (\emph{e.g.}~remains between~\(0\) and some given
                         upper-bound). We~also consider a game version of the
                         above, where certain transitions may be
                         uncontrollable.},
}

Abstract

We focus on the problem of finding (the size of) a minimal winning coalition in a multi-player game. More precisely, we prove that deciding whether there is a winning coalition of size at most k is NP-complete, while deciding whether k is the optimal size is DP-complete. We also study different variants of our original problem: the function problem, where the aim is to effectively compute the coalition; more succinct encoding of the game; and richer families of winning objectives.

@inproceedings{time2008-BGMR,
  author =              {Brihaye, {\relax Th}omas and Ghannem, Mohamed and
                         Markey, Nicolas and Rieg, Lionel},
  title =               {Good friends are hard to find!},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {S}ymposium on {T}emporal {R}epresentation and
                         {R}easoning ({TIME}'08)},
  acronym =             {{TIME}'08},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {32-40},
  year =                {2008},
  month =               jun,
  doi =                 {10.1109/TIME.2008.10},
  abstract =            {We focus on the problem of finding (the~size of)
                         a~minimal winning coalition in a multi-player game.
                         More precisely, we~prove that deciding whether there
                         is a winning coalition of size at most~\(k\) is
                         NP-complete, while deciding whether \(k\) is the
                         optimal size is DP-complete. We~also study different
                         variants of our original problem: the function
                         problem, where the aim is to effectively compute the
                         coalition; more succinct encoding of the game; and
                         richer families of winning objectives.},
}

Abstract

A channel machine consists of a finite controller together with several fifo channels; the controller can read messages from the head of a channel and write messages to the tail of a channel. In this paper, we focus on channel machines with insertion errors, i.e., machines in whose channels messages can spontaneously appear. Such devices have been previously introduced in the study of Metric Temporal Logic. We consider the termination problem: are all the computations of a given insertion channel machine finite? We show that this problem has non-elementary, yet primitive recursive complexity.

@inproceedings{stacs2008-BMOSW,
  author =              {Bouyer, Patricia and Markey, Nicolas and Ouaknine,
                         Jo{\"e}l and Schnoebelen, {\relax Ph}ilippe and
                         Worrell, James},
  title =               {On Termination for Faulty Channel Machines},
  editor =              {Albers, Susanne and Weil, Pascal},
  booktitle =           {{P}roceedings of the 25th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'08)},
  acronym =             {{STACS}'08},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {1},
  pages =               {121-132},
  year =                {2008},
  month =               feb,
  doi =                 {10.4230/LIPIcs.STACS.2008.1339},
  abstract =            {A channel machine consists of a finite controller
                         together with several fifo channels; the controller
                         can read messages from the head of a channel and
                         write messages to the tail of a channel. In this
                         paper, we focus on channel machines with
                         \emph{insertion errors}, \textit{i.e.}, machines in
                         whose channels messages can spontaneously appear.
                         Such devices have been previously introduced in the
                         study of Metric Temporal Logic. We~consider the
                         termination problem: are all the computations of a
                         given insertion channel machine finite? We~show that
                         this problem has non-elementary, yet primitive
                         recursive complexity.},
}

Abstract

Metric Interval Temporal Logic (MITL) is a popular formalism for expressing real-time specifications. This logic achieves decidability by restricting the precision of timing constraints, in particular, by banning so-called punctual specifications. In this paper we introduce a significantly more expressive logic that can express a wide variety of punctual specifications, but whose model-checking problem has the same complexity as that of MITL. We conclude that for model checking the most commonly occurring specifications, such as invariance and bounded response, punctuality can be accommodated at no cost.

@inproceedings{icalp2008-BMOW,
  author =              {Bouyer, Patricia and Markey, Nicolas and Ouaknine,
                         Jo{\"e}l and Worrell, James},
  title =               {On Expressiveness and Complexity in Real-time Model
                         Checking},
  editor =              {Aceto, Luca and Damg{\aa}rd, Ivan and Goldberg,
                         Leslie Ann and Halld{\'o}rsson, Magn{\'u}s M. and
                         Ing{\'o}lfsd{\'o}ttir, Anna and Walukiewicz, Igor},
  booktitle =           {{P}roceedings of the 35th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'08)~-- Part~{II}},
  acronym =             {{ICALP}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5126},
  pages =               {124-135},
  year =                {2008},
  month =               jul,
  doi =                 {10.1007/978-3-540-70583-3_11},
  abstract =            {Metric Interval Temporal Logic (MITL) is a popular
                         formalism for expressing real-time specifications.
                         This logic achieves decidability by restricting the
                         precision of timing constraints, in particular, by
                         banning so-called \emph{punctual} specifications.
                         In~this paper we~introduce a significantly more
                         expressive logic that can express a wide variety of
                         punctual specifications, but whose model-checking
                         problem has the same complexity as that of~MITL.
                         We~conclude that for model checking the most
                         commonly occurring specifications, such as
                         invariance and bounded response, punctuality can be
                         accommodated at no cost.},
}

Abstract

Whereas formal verification of timed systems has become a very active field of research, the idealised mathematical semantics of timed automata cannot be faithfully implemented. Several works have thus focused on a modified semantics of timed automata which ensures implementability, and robust model-checking algorithms for safety, and later LTL properties have been designed. Recently, a new approach has been proposed, which reduces (standard) model-checking of timed automata to other verification problems on channel machines. Thanks to a new encoding of the modified semantics as a network of timed systems, we propose an original combination of both approaches, and prove that robust model-checking for coFlat-MTL, a large fragment of MTL, is EXPSPACE-Complete.

@inproceedings{fossacs2008-BMR,
  author =              {Bouyer, Patricia and Markey, Nicolas and Reynier,
                         Pierre-Alain},
  title =               {Robust Analysis of Timed Automata via Channel
                         Machines},
  editor =              {Amadio, Roberto},
  booktitle =           {{P}roceedings of the 11th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'08)},
  acronym =             {{FoSSaCS}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4962},
  pages =               {157-171},
  year =                {2008},
  month =               mar,
  doi =                 {10.1007/978-3-540-78499-9_12},
  abstract =            {Whereas formal verification of timed systems has
                         become a very active field of research, the
                         idealised mathematical semantics of timed automata
                         cannot be faithfully implemented. Several works have
                         thus focused on a modified semantics of timed
                         automata which ensures implementability, and robust
                         model-checking algorithms for safety, and later LTL
                         properties have been designed. Recently, a~new
                         approach has been proposed, which reduces (standard)
                         model-checking of timed automata to other
                         verification problems on channel machines. Thanks to
                         a new encoding of the modified semantics as a
                         network of timed systems, we propose an original
                         combination of both approaches, and prove that
                         robust model-checking for coFlat-MTL, a large
                         fragment of~MTL, is EXPSPACE-Complete.},
}

@incollection{afsec2008-CM,
  author =              {Cassez, Franck and Markey, Nicolas},
  title =               {Contr{\^o}le des syst{\`e}mes temporis{\'e}s},
  editor =              {Roux, Olivier H. and Jard, Claude},
  booktitle =           {Approches formelles des syst{\`e}mes embarqu{\'e}s
                         communicants},
  publisher =           {Herm{\`e}s},
  pages =               {105-144},
  chapter =             {4},
  year =                {2008},
  month =               oct,
  url =                 {http://e.lavoisier.fr/produit/9782746243156},
}

@inproceedings{ABGMN-concur08,
  author =              {Akshay, S. and Bollig, Benedikt and Gastin, Paul and
                         Mukund, Madhavan and Narayan Kumar, K.},
  title =               {Distributed Timed Automata with Independently
                         Evolving Clocks},
  editor =              {van Breugel, Franck and Chechik, Marsha},
  booktitle =           {{P}roceedings of the 19th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'08)},
  acronym =             {{CONCUR}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5201},
  pages =               {82-97},
  year =                {2008},
  month =               aug,
}

@article{siamcomp38(4)-ADKTWR,
  author =              {Anshelevich, Elliot and Dasgupta, Anirban and
                         Kleinberg, Jon and Tardos, {\'E}va and Wexler, Tom
                         and Roughgarden, Tim},
  title =               {The~Price of Stability for Network Design with Fair
                         Cost Allocation},
  publisher =           {Society for Industrial and Applied Math.},
  journal =             {SIAM Journal on Computing},
  volume =              {38},
  number =              {4},
  pages =               {1602-1623},
  year =                {2008},
  doi =                 {10.1137/070680096},
}

@inproceedings{sas2008-AGG,
  author =              {Allamigeon, Xavier and Gaubert, St{\'e}phane and
                         Goubault, {\'E}ric},
  title =               {Inferring Min and Max Invariants Using Max-Plus
                         Polyhedra},
  editor =              {Alpuente, Mar{\'\i}a and Vidal, Germ{\'a}n},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {S}ymposium on {S}tatic {A}nalysis ({SAS}'08)},
  acronym =             {{SAS}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5079},
  pages =               {189-204},
  year =                {2008},
  month =               jul,
}

@techreport{clausthal0801-AGJ,
  author =              {{\AA}gotnes, Thomas and Goranko, Valentin and
                         Jamroga, Wojciech},
  title =               {Strategic Commitment and Release in Logics for
                         Multi-Agent Systems (Extended abstract)},
  number =              {08-01},
  year =                {2008},
  institution =         {Clausthal University of Technology, Germany},
}

@inproceedings{lics2008-BBBBG,
  author =              {Baier, {\relax Ch}ristel and Bertrand, Nathalie and
                         Bouyer, Patricia and Brihaye, {\relax Th}omas and
                         Gr{\"o}{\ss}er, Marcus},
  title =               {Almost-sure Model Checking of Infinite Paths in
                         One-clock Timed Automata},
  booktitle =           {{P}roceedings of the 23rd {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'08)},
  acronym =             {{LICS}'08},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {217-226},
  year =                {2008},
  month =               jun,
  doi =                 {10.1109/LICS.2008.25},
}

@article{fmsd32(1)-BBL,
  author =              {Bouyer, Patricia and Brinksma, Ed and Larsen, Kim
                         Guldstrand},
  title =               {Optimal infinite scheduling for multi-priced timed
                         automata},
  publisher =           {Springer-Verlag},
  journal =             {Formal Methods in System Design},
  volume =              {32},
  number =              {1},
  pages =               {2-23},
  year =                {2008},
  month =               feb,
}

@article{jlap77(1-2)-BHM,
  author =              {Brekling, Aske Wiid and Hansen, Michael R. and
                         Madsen, Jan},
  title =               {Models and formal verification of multiprocessor
                         system-on-chips},
  publisher =           {Elsevier},
  journal =             {Journal of Logic and Algebraic Programming},
  volume =              {77},
  number =              {1-2},
  pages =               {1-19},
  year =                {2008},
  month =               oct,
}

@book{PoMC2008-BK,
  author =              {Baier, {\relax Ch}ristel and Katoen, Joost-Pieter},
  title =               {Principles of Model-Checking},
  publisher =           {MIT Press},
  year =                {2008},
  month =               may,
}

@inproceedings{jtres2008-BKOTL,
  author =              {B{\o}gholm, Thomas and Kargh{-}hansen, Henrik and
                         Olsen, Petur and Thomsen, Bent and Larsen, Kim
                         Guldstrand},
  title =               {Model-based schedulability analysis of safety
                         critical hard real-time Java programs},
  editor =              {Bollella, Gregory and Locke, C. Douglas},
  booktitle =           {{P}roceedings of the 6th {I}nternational {W}orkshop
                         on {J}ava {T}echnologies for {R}eal-time and
                         {E}mbedded {S}ystems ({JTRES}'08)},
  acronym =             {{JTRES}'08},
  publisher =           {ACM Press},
  series =              {ACM International Conference Proceeding Series},
  volume =              {343},
  pages =               {106-114},
  year =                {2008},
  month =               sep,
  doi =                 {10.1145/1434790.1434807},
}

@inproceedings{fossacs2008-Boj,
  author =              {Boja{\'n}czyk, Miko{\l}aj},
  title =               {The Common Fragment of {ACTL} and~{LTL}},
  editor =              {Amadio, Roberto},
  booktitle =           {{P}roceedings of the 11th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'08)},
  acronym =             {{FoSSaCS}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4962},
  pages =               {172-185},
  year =                {2008},
  month =               mar,
}

@inproceedings{fossacs2008-Boz,
  author =              {Bozzelli, Laura},
  title =               {The complexity of CTL\textsuperscript{*} + Linear
                         Past},
  editor =              {Amadio, Roberto},
  booktitle =           {{P}roceedings of the 11th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'08)},
  acronym =             {{FoSSaCS}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4962},
  pages =               {186-200},
  year =                {2008},
  month =               mar,
}

@inproceedings{csl2008-CDH,
  author =              {Chatterjee, Krishnendu and Doyen, Laurent and
                         Henzinger, Thomas A.},
  title =               {Quantitative Languages},
  editor =              {Kaminski, Michael and Martini, Simone},
  booktitle =           {{P}roceedings of the 22nd {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'08)},
  acronym =             {{CSL}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5213},
  pages =               {385-400},
  year =                {2008},
  month =               sep,
  doi =                 {10.1007/978-3-540-87531-4_28},
}

@techreport{corr0805.2620-CHP,
  author =              {Chatterjee, Krishnendu and Henzinger, Thomas A. and
                         Piterman, Nir},
  title =               {Algorithms for {B}{\"u}chi games},
  number =              {0805.2620},
  year =                {2008},
  month =               may,
  institution =         {arXiv},
  type =                {Research Report},
}

@inproceedings{hscc2008-CMH,
  author =              {Chatterjee, Krishnendu and Majumdar, Rupak and
                         Henzinger, Thomas A.},
  title =               {Controller Synthesis with Budget Constraints},
  editor =              {Egerstedt, Magnus and Mishra, Bud},
  booktitle =           {{P}roceedings of the 11th {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
                         ({HSCC}'08)},
  acronym =             {{HSCC}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4981},
  year =                {2008},
  month =               apr,
}

@article{lmcs4(2)-CPJ,
  author =              {Comon, Hubert and Perrin, Nicolas and Jacquemard,
                         Florent},
  title =               {Visibly Tree Automata with Memory and Constraints},
  journal =             {Logical Methods in Computer Science},
  volume =              {4},
  number =              {2},
  year =                {2008},
  month =               may,
  doi =                 {10.2168/LMCS-4(2:8)2008},
}

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

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

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

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

@inproceedings{qapl2008-FLS,
  author =              {Faella, Marco and Legay, Axel and Stoelinga,
                         Mari{\"e}lle},
  title =               {Model Checking Quantitative Linear Time Logic},
  editor =              {Aldini, Alessandro and Baier, {\relax Ch}ristel},
  booktitle =           {{P}roceedings of the 6th {W}orkshop on
                         {Q}uantitative {A}spects of {P}rogramming
                         {L}anguages ({QAPL}'08)},
  acronym =             {{QAPL}'08},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {220},
  number =              {3},
  pages =               {61-77},
  year =                {2008},
  month =               mar,
}

@inproceedings{sagt2008-Fot,
  author =              {Fotakis, Dimitris},
  title =               {Congestion games with linearly-independent paths:
                         convergence time and price of anarchy},
  editor =              {Monien, Burkhard and Schroeder, Ulf-Peter},
  booktitle =           {{P}roceedings of the 1st {I}nternational {S}ymposium
                         on {A}lgorithmic {G}ame {T}heory ({SAGT}'08)},
  acronym =             {{SAGT}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4997},
  pages =               {33-45},
  year =                {2008},
  month =               apr,
  doi =                 {10.1007/978-3-540-79309-0_5},
}

@inproceedings{wine2008-GHKSW,
  author =              {Gassner, Elisabeth and Hatzl, Johannes and Krumke,
                         Sven O. and Sperber, Heike and Woeginger, Gerhard
                         J.},
  title =               {How hard is it to find extreme {N}ash equilibria in
                         network congestion games?},
  editor =              {Papadimitriou, {\relax Ch}ristos H. and Zhang,
                         Shuzhong},
  booktitle =           {{P}roceedings of the 4th {I}nternational {W}orkshop
                         on {I}nternet and {N}etwork {E}conomics ({WINE}'08)},
  acronym =             {{WINE}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5385},
  pages =               {82-93},
  year =                {2008},
  month =               dec,
  doi =                 {10.1007/978-3-540-92185-1_17},
}

@phdthesis{phd-grinchtein,
  author =              {Grinchtein, Olga},
  title =               {Learning of Timed Systems},
  year =                {2008},
  school =              {Deparment of Information Technology, Uppsala
                         University, Sweden},
}

@article{icomp206(12)-HR,
  author =              {Hirshfeld, Yoram and Rabinovich, Alexander},
  title =               {Decidable Metric Logics},
  publisher =           {Elsevier},
  journal =             {Information and Computation},
  volume =              {206},
  number =              {12},
  pages =               {1425-1442},
  year =                {2008},
  month =               dec,
  doi =                 {10.1016/j.ic.2008.08.004},
}

@inproceedings{formats2008-IKYBGVVSS,
  author =              {Igna, Georgeta and Kannan, Vankatesh and Yang, Yang
                         and Basten, Twan and Geilen, Marc C.W. and
                         Vaandrager, Frits and Voorhoeve, Marc and de Smet,
                         Sebastian and Somers, Lou J.},
  title =               {Formal Modeling and Scheduling of Datapaths of
                         Digital Document Printers},
  editor =              {Cassez, Franck and Jard, Claude},
  booktitle =           {{P}roceedings of the 6th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'08)},
  acronym =             {{FORMATS}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5215},
  pages =               {170-187},
  year =                {2008},
  month =               sep,
}

@article{tocsys42(3)-JD,
  author =              {Jamroga, Wojciech and Dix, J{\"u}rgen},
  title =               {Model Checking Abilities of Agents: A Closer Look},
  publisher =           {Springer-Verlag},
  journal =             {Theory of Computing Systems},
  volume =              {42},
  number =              {3},
  pages =               {366-410},
  year =                {2008},
  month =               apr,
  doi =                 {10.1007/s00224-007-9080-z},
}

@article{tcsyst43(2)-KBBEGRZ,
  author =              {Khachiyan, Leonid and Boros, Endre and Borys, Konrad
                         and Elbassioni, Khaled and Gurvich, Vladimir and
                         Rudolf, Gabor and Zhao, Jihui},
  title =               {On short paths interdiction problems: Total and
                         node-wise limited interdiction},
  publisher =           {Springer-Verlag},
  journal =             {Theory of Computing Systems},
  volume =              {43},
  number =              {2},
  pages =               {204-233},
  year =                {2008},
  month =               aug,
  doi =                 {10.1007/s00224-007-9025-6},
}

@inproceedings{tacas2008-KHL,
  author =              {Kupferschmid, Sebastian and Hoffmann, J{\"o}rg and
                         Larsen, Kim Guldstrand},
  title =               {Fast Directed Model Checking Via Russian Doll
                         Abstraction},
  editor =              {Ramakrishnan, C. R. and Rehof, Jakob},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'08)},
  acronym =             {{TACAS}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4963},
  pages =               {203-217},
  year =                {2008},
  month =               mar,
}

@article{doklady78(1)-KSC,
  author =              {Kuzmin, Egor V. and Sokolov, Valery A. and Chaly,
                         Dmitry Y.},
  title =               {Boundedness Problems for {M}insky Counter Machines},
  publisher =           {Pleiades Publishing},
  journal =             {Doklady Mathematics},
  volume =              {78},
  number =              {1},
  pages =               {604-606},
  year =                {2008},
}

@inproceedings{cav2008KWNP,
  author =              {Kupferschmid, Sebastian and Wehrle, Martin and
                         Nebel, Bernhard and Podelski, Andreas},
  title =               {Faster Than {U}ppaal?},
  editor =              {Gupta, Aarti and Malik, Sharad},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'08)},
  acronym =             {{CAV}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5123},
  pages =               {552-555},
  year =                {2008},
  month =               jul,
}

@article{ipl108(5)-Lan,
  author =              {Lange, Martin},
  title =               {A purely model-theoretic proof of the exponential
                         succinctness gap between {CTL\(^{+}\)} and {CTL}},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {108},
  number =              {5},
  pages =               {308-312},
  year =                {2008},
  month =               nov,
}

@article{tcs390(2-3)-LR,
  author =              {Larsen, Kim Guldstrand and Rasmussen, Jacob Illum},
  title =               {Optimal Conditional reachability for Multi-Priced
                         Timed Automata},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {390},
  number =              {2-3},
  pages =               {197-213},
  year =                {2008},
  month =               jan,
}

@techreport{arxiv-cs.GT/0806.2923,
  author =              {Luttenberger, Michael},
  title =               {Strategy Iteration using Non-Deterministic
                         Strategies for Solving Parity Games},
  number =              {cs.GT/0806.2923},
  year =                {2008},
  month =               jun,
  institution =         {arXiv},
  type =                {Research Report},
}

@article{tocl9(2)-LW,
  author =              {Lasota, S{\l}awomir and Walukiewicz, Igor},
  title =               {Alternating Timed Automata},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {9},
  number =              {2},
  year =                {2008},
  month =               mar,
}

@inproceedings{fmsb2008-MB,
  author =              {Maler, Oded and Batt, Gr{\'e}gory},
  title =               {Approximating continuous systems by timed automata},
  editor =              {Fisher, Jasmin},
  booktitle =           {{P}roceedings of the 1st {I}nternational {W}okshop
                         on {F}ormal {M}ethods in {S}ystems {B}iology
                         ({FMSB}'08)},
  acronym =             {{FMSB}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Bioinformatics},
  volume =              {5054},
  pages =               {77-89},
  year =                {2008},
  month =               jun,
  doi =                 {10.1007/978-3-540-68413-8_6},
}

@inproceedings{mmtv-rp08,
  author =              {Meier, Arne and Mundhenk, Martin and Thomas, Michael
                         and Vollmer, Heribert},
  title =               {The Complexity of Satisfiability for Fragmentf of
                         {CTL} and {CTL}\(^{*}\)},
  editor =              {Halava, Vesa and Potapov, Igor},
  booktitle =           {{P}roceedings of the 2nd {W}orkshop on
                         {R}eachability {P}roblems in {C}omputational
                         {M}odels ({RP}'08)},
  acronym =             {{RP}'08},
  pages =               {201-213},
  year =                {2008},
  month =               sep,
}

@inproceedings{lpar2008-Mon,
  author =              {Monniaux, David},
  title =               {A~Quantifier Elimination Algorithm for Linear Real
                         Arithmetic},
  editor =              {Cervesato, Iliano and Veith, Helmutand Voronkov,
                         Andrei},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference {L}ogic {P}rogramming and {A}utomated
                         {R}easoning ({LPAR}'08)},
  acronym =             {{LPAR}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5330},
  pages =               {243-257},
  year =                {2008},
  month =               nov,
  doi =                 {10.1007/978-3-540-89439-1_18},
}

@phdthesis{phd-nickovic,
  author =              {Nickovic, Dejan},
  title =               {Checking Timed and Hybrid Properties: Theory and
                         Applications},
  year =                {2008},
  month =               oct,
  school =              {Lab. VERIMAG, Grenoble, France},
}

@phdthesis{phd-oreiby,
  author =              {Oreiby, Ghassan},
  title =               {Logiques temporelles pour le contr{\^o}le
                         temporis{\'e}},
  year =                {2008},
  month =               dec,
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {Th\`ese de doctorat},
}

@mastersthesis{diplom08-Rab,
  author =              {Rabinovich, Roman},
  title =               {Complexity Measures for Directed Graphs},
  year =                {2008},
  month =               aug,
  school =              {RWTH Aachen, Germany},
  type =                {Diplomarbeit},
}

@inproceedings{kr2008-RS,
  author =              {Ramanujam, R. and Simon, Sunil},
  title =               {Dynamic Logic on Games with Structured Strategies},
  editor =              {Brewka, Gerhard and Lang, J{\'e}r{\^o}me},
  booktitle =           {{P}roceedings of the 11th {I}nternational
                         {C}onference on {P}rinciples of {K}nowledge
                         {R}epresentation and {R}easoning ({KR}'08)},
  acronym =             {{KR}'08},
  publisher =           {AAAI Press},
  pages =               {49-58},
  year =                {2008},
  month =               sep,
}

@inproceedings{veras2007-RT,
  author =              {Radmacher, Frank G. and Thomas, Wolfgang},
  title =               {A~Game Theoretic Approach to the Analysis of Dynamic
                         Networks},
  editor =              {Ballis, Demis and Escobar, Santiago and Marchiori,
                         Massimo},
  booktitle =           {{P}roceedings of the 1st {W}orkshop on
                         {V}erification of {A}daptive {S}ystems ({VerAS}'07)},
  acronym =             {{VerAS}'07},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {200(2)},
  pages =               {21-37},
  year =                {2008},
  month =               feb,
  confyear =            {2007},
}

@inproceedings{icalp2008-Sch,
  author =              {Schewe, Sven},
  title =               {{ATL}{\(^*\)} Satisfiability Is 2{EXPTIME}-Complete},
  editor =              {Aceto, Luca and Damg{\aa}rd, Ivan and Goldberg,
                         Leslie Ann and Halld{\'o}rsson, Magn{\'u}s M. and
                         Ing{\'o}lfsd{\'o}ttir, Anna and Walukiewicz, Igor},
  booktitle =           {{P}roceedings of the 35th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'08)~-- Part~{II}},
  acronym =             {{ICALP}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5126},
  pages =               {373-385},
  year =                {2008},
  month =               jul,
}

@phdthesis{phd-schewe,
  author =              {Schewe, Sven},
  title =               {Synthesis of Distributed Systems},
  year =                {2008},
  month =               jul,
  school =              {Saarland University, Germany},
}

@inproceedings{ifiptcs2008-SFK,
  author =              {Swaminathan, Mani and Fr{\"a}nzle, Martin and
                         Katoen, Joost-Pieter},
  title =               {The Surprising Robustness of (Closed) Timed Automata
                         against Clock-Drift},
  editor =              {Karhum{\"a}ki, Juhani and Ong, Luke},
  booktitle =           {{P}roceedings of the 5th {IFIP} {I}nternational
                         {C}onference on {T}heoretical {C}omputer {S}cience
                         ({IFIPTCS}'08)},
  acronym =             {{IFIPTCS}'08},
  publisher =           {Springer-Verlag},
  series =              {IFIP Conference Proceedings},
  volume =              {273},
  pages =               {537-553},
  year =                {2008},
  month =               sep,
}

@article{cacm51(8)-Sho,
  author =              {Shoham, Yoav},
  title =               {Computer Science and Game Theory},
  publisher =           {ACM Press},
  journal =             {Communications of the ACM},
  volume =              {51},
  number =              {8},
  pages =               {74-79},
  year =                {2008},
  month =               aug,
  doi =                 {10.1145/1378704.1378721},
}

@inproceedings{formats2008-SPNM,
  author =              {Suman, P. Vijay and Pandya, Paritosh K. and
                         Narayanan Krishna, Shankara and Manasa, Lakshmi},
  title =               {Timed Automata with Integer Resets: Language
                         Inclusion and Expressiveness},
  editor =              {Cassez, Franck and Jard, Claude},
  booktitle =           {{P}roceedings of the 6th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'08)},
  acronym =             {{FORMATS}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5215},
  pages =               {78-92},
  year =                {2008},
  month =               sep,
}

@inproceedings{fossacs2008-Umm,
  author =              {Ummels, Michael},
  title =               {The Complexity of {N}ash Equilibria in Infinite
                         Multiplayer Games},
  editor =              {Amadio, Roberto},
  booktitle =           {{P}roceedings of the 11th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'08)},
  acronym =             {{FoSSaCS}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4962},
  pages =               {20-34},
  year =                {2008},
  month =               mar,
}

@inproceedings{lata2008-Vol,
  author =              {Volkov, Mikhail V.},
  title =               {Synchronizing Automata and the {{\v{C}}}ern{\'y}
                         Conjecture},
  editor =              {Mart{\'\i}n-Vide, Carlos and Otto, Friedrich and
                         Fernau, Henning},
  booktitle =           {{R}evised {P}apers of the 2nd {I}nternational
                         {C}onference on {L}anguage and {A}utomata {T}heory
                         and {A}pplications ({LATA}'08)},
  acronym =             {{LATA}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5196},
  pages =               {11-27},
  year =                {2008},
  month =               mar,
}

@inproceedings{formats2008-VPKM,
  author =              {Vijay{ }Suman, P. and Pandya, Paritosh K. and
                         Krishna, Shankara Narayanan and Manasa, Lakshmi},
  title =               {Timed Automata with Integer Resets: Language
                         Inclusion and Expressiveness},
  editor =              {Cassez, Franck and Jard, Claude},
  booktitle =           {{P}roceedings of the 6th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'08)},
  acronym =             {{FORMATS}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5215},
  pages =               {78-92},
  year =                {2008},
  month =               sep,
  doi =                 {10.1007/978-3-540-85778-5_7},
}

@incollection{la2008-ala-VW,
  author =              {Vardi, Moshe Y. and Wilke, Thomas},
  title =               {Automata: from logics to algorithms},
  editor =              {Flum, J{\"o}rg and Gr{\"a}del, Erich and Wilke,
                         Thomas},
  booktitle =           {Logic and Automata: History and Perspectives},
  publisher =           {Amsterdam University Press},
  series =              {Texts in Logic and Games},
  volume =              {2},
  pages =               {629-736},
  year =                {2008},
}

@inproceedings{rts2008-Wan,
  author =              {Wang, Farn},
  title =               {Efficient Model-Checking of Dense-Time Systems with
                         Time-Convexity Analysis},
  booktitle =           {{P}roceedings of the 29th {S}ymposium on {R}eal-Time
                         {S}ystems ({RTSS}'08)},
  acronym =             {{RTSS}'08},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {195-205},
  year =                {2008},
  month =               nov,
  doi =                 {10.1109/RTSS.2008.53},
}

@inproceedings{tacas2008-WBE,
  author =              {Wahl, Thomas and Blanc, Nicolas and Emerson, E.
                         Allen},
  title =               {{SVISS}: Symbolic Verification of Symmetric Systems},
  editor =              {Ramakrishnan, C. R. and Rehof, Jakob},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'08)},
  acronym =             {{TACAS}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4963},
  pages =               {459-462},
  year =                {2008},
  month =               mar,
  doi =                 {10.1007/978-3-540-78800-3_34},
}

@article{rts38(1)-WH,
  author =              {Waszniowski, Libor and Hanz{\'a}lek, Zden{\v{e}}k},
  title =               {Formal verification of multitasking applications
                         based on timed automata model},
  publisher =           {Kluwer Academic},
  journal =             {Real-Time Systems},
  volume =              {38},
  number =              {1},
  pages =               {39-65},
  year =                {2008},
  month =               jan,
}