Nicolas Markey

Abstract

We investigate a number of problems related to infinite runs of weighted timed automata (with a single weight variable), subject to lower-bound constraints on the accumulated weight. Closing an open problem from an earlier paper, we show that the existence of an infinite lower-bound-constrained run is–for us somewhat unexpectedly–undecidable for weighted timed automata with four or more clocks.

This undecidability result assumes a fixed and known initial credit. We show that the related problem of existence of an initial credit for which there exists a feasible run is decidable in PSPACE. We also investigate the variant of these problems where only bounded-duration runs are considered, showing that this restriction makes our original problem decidable in NEXPTIME. We prove that the universal versions of all those problems (i.e, checking that all the considered runs satisfy the lower-bound constraint) are decidable in PSPACE.

Finally, we extend this study to multi-weighted timed automata: the existence of a feasible run becomes undecidable even for bounded duration, but the existence of initial credits remains decidable (in PSPACE).

@article{peva73()-BLM,
  author =              {Bouyer, Patricia and Larsen, Kim Guldstrand and
                         Markey, Nicolas},
  title =               {Lower-Bound Constrained Runs in Weighted Timed
                         Automata},
  publisher =           {Elsevier},
  journal =             {Performance Evaluation},
  volume =              {73},
  pages =               {91-109},
  year =                {2014},
  month =               mar,
  doi =                 {10.1016/j.peva.2013.11.002},
  abstract =            {We investigate a number of problems related to
                         infinite runs of weighted timed automata (with a
                         single weight variable), subject to lower-bound
                         constraints on the accumulated weight. Closing an
                         open problem from an earlier paper, we show that the
                         existence of an infinite lower-bound-constrained run
                         is--for us somewhat unexpectedly--undecidable for
                         weighted timed automata with four or more
                         clocks.\par This undecidability result assumes a
                         fixed and known initial credit. We show that the
                         related problem of existence of an initial credit
                         for which there exists a feasible run is decidable
                         in PSPACE. We also investigate the variant of these
                         problems where only bounded-duration runs are
                         considered, showing that this restriction makes our
                         original problem decidable in NEXPTIME. We prove
                         that the universal versions of all those problems
                         (i.e, checking that all the considered runs satisfy
                         the lower-bound constraint) are decidable in
                         PSPACE.\par Finally, we extend this study to
                         multi-weighted timed automata: the existence of a
                         feasible run becomes undecidable even for bounded
                         duration, but the existence of initial credits
                         remains decidable (in~PSPACE).},
}

Abstract

While it was defined long ago, the extension of CTL with quantification over atomic propositions has never been studied extensively. Considering two different semantics (depending whether propositional quantification refers to the Kripke structure or to its unwinding tree), we study its expressiveness (showing in particular that QCTL coincides with Monadic Second-Order Logic for both semantics) and characterise the complexity of its model-checking and satisfiability problems, depending on the number of nested propositional quantifiers (showing that the structure semantics populates the polynomial hierarchy while the tree semantics populates the exponential hierarchy).

@article{lmcs10(4)-LM,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas},
  title =               {Quantified~{CTL}: expressiveness and complexity},
  journal =             {Logical Methods in Computer Science},
  volume =              {10},
  number =              {4},
  year =                {2014},
  month =               dec,
  doi =                 {10.2168/LMCS-10(4:17)2014},
  abstract =            {While it was defined long ago, the extension of CTL
                         with quantification over atomic propositions has
                         never been studied extensively. Considering two
                         different semantics (depending whether propositional
                         quantification refers to the Kripke structure or to
                         its unwinding tree), we~study its expressiveness
                         (showing in particular that QCTL coincides with
                         Monadic Second-Order Logic for both semantics) and
                         characterise the complexity of its model-checking
                         and satisfiability problems, depending on the number
                         of nested propositional quantifiers (showing that
                         the structure semantics populates the polynomial
                         hierarchy while the tree semantics populates the
                         exponential hierarchy).},
}

Abstract

We define and study a new approach to the implementability of timed automata, where the semantics is perturbed by imprecisions and finite frequency of the hardware. In order to circumvent these effects, we introduce parametric shrinking of clock constraints, which corresponds to tightening the guards. We propose symbolic procedures to decide the existence of (and then compute) parameters under which the shrunk version of a given timed automaton is non-blocking and can time-abstract simulate the exact semantics. We then define an implementation semantics for timed automata with a digital clock and positive reaction times, and show that for shrinkable timed automata, non-blockingness and time-abstract simulation are preserved in implementation.

@article{icomp234()-SBM,
  author =              {Sankur, Ocan and Bouyer, Patricia and Markey,
                         Nicolas},
  title =               {Shrinking Timed Automata},
  publisher =           {Elsevier},
  journal =             {Information and Computation},
  volume =              {234},
  pages =               {107-132},
  year =                {2014},
  month =               feb,
  doi =                 {10.1016/j.ic.2014.01.002},
  abstract =            {We define and study a new approach to the
                         implementability of timed automata, where the
                         semantics is perturbed by imprecisions and finite
                         frequency of the hardware. In order to circumvent
                         these effects, we introduce \emph{parametric
                         shrinking} of clock constraints, which corresponds
                         to tightening the guards. We propose symbolic
                         procedures to decide the existence of (and then
                         compute) parameters under which the shrunk version
                         of a given timed automaton is non-blocking and can
                         time-abstract simulate the exact semantics. We then
                         define an implementation semantics for timed
                         automata with a digital clock and positive reaction
                         times, and show that for shrinkable timed automata,
                         non-blockingness and time-abstract simulation are
                         preserved in implementation.},
}

Abstract

Extending formal verification techniques to handle quantitative aspects, both for the models and for the properties to be checked, has become a central research topic over the last twenty years. Following several recent works, we study model checking for (one-dimensional) weighted Kripke structures with positive and negative weights, and temporal logics constraining the total and/or average weight. We prove decidability when only accumulated weight is constrained, while allowing average-weight constraints alone already is undecidable.

@inproceedings{atva2014-BGM,
  author =              {Bouyer, Patricia and Gardy, Patrick and Markey,
                         Nicolas},
  title =               {Quantitative verification of weighted {K}ripke
                         structures},
  editor =              {Cassez, Franck and Raskin, Jean-Fran{\c c}ois},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {S}ymposium on {A}utomated {T}echnology for
                         {V}erification and {A}nalysis ({ATVA}'14)},
  acronym =             {{ATVA}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8837},
  pages =               {64-80},
  year =                {2014},
  month =               nov,
  doi =                 {10.1007/978-3-319-11936-6_6},
  abstract =            {Extending formal verification techniques to handle
                         quantitative aspects, both for the models and for
                         the properties to be checked, has become a central
                         research topic over the last twenty years. Following
                         several recent works, we study model checking for
                         (one-dimensional) weighted Kripke structures with
                         positive and negative weights, and temporal logics
                         constraining the total and/or average weight. We
                         prove decidability when only accumulated weight is
                         constrained, while allowing average-weight
                         constraints alone already is undecidable.},
}

Abstract

For the accurate analysis of computerized systems, powerful quantitative formalisms have been designed, together with efficient verification algorithms. However, verification has mostly remained boolean—either a property is true, or it is false. We believe that this is too crude in a context where quantitative information and constraints are crucial: correctness should be quantified!

In a recent line of works, several authors have proposed quantitative semantics for temporal logics, using e.g. discounting modalities (which give less importance to distant events). In the present paper, we define and study a quantitative semantics of LTL with averaging modalities, either on the long run or within an until modality. This, in a way, relaxes the classical Boolean semantics of LTL, and provides a measure of certain properties of a model. We prove that computing and even approximating the value of a formula in this logic is undecidable.

@inproceedings{concur2014-BMM,
  author =              {Bouyer, Patricia and Markey, Nicolas and
                         Matteplackel, Raj~Mohan},
  title =               {Averaging in~{LTL}},
  editor =              {Baldan, Paolo and Gorla, Daniele},
  booktitle =           {{P}roceedings of the 25th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'14)},
  acronym =             {{CONCUR}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8704},
  pages =               {266-280},
  year =                {2014},
  month =               sep,
  doi =                 {10.1007/978-3-662-44584-6_19},
  abstract =            {For the accurate analysis of computerized systems,
                         powerful quantitative formalisms have been designed,
                         together with efficient verification algorithms.
                         However, verification has mostly remained
                         boolean---either a property is~true, or it~is false.
                         We~believe that this is too crude in a context where
                         quantitative information and constraints are
                         crucial: correctness should be quantified!\par In a
                         recent line of works, several authors have proposed
                         quantitative semantics for temporal logics, using
                         e.g. \emph{discounting} modalities (which give less
                         importance to distant events). In~the present paper,
                         we define and study a quantitative semantics of~LTL
                         with \emph{averaging} modalities, either on the long
                         run or within an until modality. This, in a way,
                         relaxes the classical Boolean semantics of~LTL, and
                         provides a measure of certain properties of a model.
                         We~prove that computing and even approximating the
                         value of a formula in this logic is undecidable.},
}

Abstract

We study mixed-strategy Nash equilibria in multiplayer deterministic concurrent games played on graphs, with terminal-reward payoffs (that is, absorbing states with a value for each player). We show undecidability of the existence of a constrained Nash equilibrium (the constraint requiring that one player should have maximal payoff), with only three players and 0/1-rewards (i.e., reachability objectives). This has to be compared with the undecidability result by Ummels and Wojtczak for turn-based games which requires 14 players and general rewards. Our proof has various interesting consequences: (i) the undecidability of the existence of a Nash equilibrium with a constraint on the social welfare; (ii) the undecidability of the existence of an (unconstrained) Nash equilibrium in concurrent games with terminal-reward payoffs.

@inproceedings{fsttcs2014-BMS,
  author =              {Bouyer, Patricia and Markey, Nicolas and Stan,
                         Daniel},
  title =               {Mixed {N}ash Equilibria in Concurrent Games},
  editor =              {Raman, Venkatesh and Suresh, S. P.},
  booktitle =           {{P}roceedings of the 34th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'14)},
  acronym =             {{FSTTCS}'14},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {29},
  pages =               {351-363},
  year =                {2014},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2014.351},
  abstract =            {We study mixed-strategy Nash equilibria in
                         multiplayer deterministic concurrent games played on
                         graphs, with terminal-reward payoffs (that is,
                         absorbing states with a value for each player). We
                         show undecidability of the existence of a
                         constrained Nash equilibrium (the constraint
                         requiring that one player should have maximal
                         payoff), with only three players and 0/1-rewards
                         (i.e., reachability objectives). This has to be
                         compared with the undecidability result by Ummels
                         and Wojtczak for turn-based games which requires 14
                         players and general rewards. Our proof has various
                         interesting consequences: (i)~the~undecidability of
                         the existence of a Nash equilibrium with a
                         constraint on the social welfare;
                         (ii)~the~undecidability of the existence of an
                         (unconstrained) Nash equilibrium in concurrent games
                         with terminal-reward payoffs.},
}

Abstract

We investigate a model for representing large multiplayer games, which satisfy strong symmetry properties. This model is made of multiple copies of an arena; each player plays in his own arena, and can partially observe what the other players do. Therefore, this game has partial information and symmetry constraints, which make the computation of Nash equilibria difficult. We show several undecidability results, and for bounded-memory strategies, we precisely characterize the complexity of computing pure Nash equilibria (for qualitative objectives) in this game model.

@inproceedings{sr2014-BMV,
  author =              {Bouyer, Patricia and Markey, Nicolas and Vester,
                         Steen},
  title =               {Nash Equilibria in Symmetric Games with Partial
                         Observation},
  booktitle =           {{P}roceedings of the 2nd {I}nternational {W}orkshop
                         on {S}trategic {R}easoning ({SR}'14)},
  acronym =             {{SR}'14},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {146},
  pages =               {49-55},
  year =                {2014},
  month =               mar,
  doi =                 {10.4204/EPTCS.146.7},
  abstract =            {We investigate a model for representing large
                         multiplayer games, which satisfy strong symmetry
                         properties. This model is made of multiple copies of
                         an arena; each player plays in his own arena, and
                         can partially observe what the other players do.
                         Therefore, this game has partial information and
                         symmetry constraints, which make the computation of
                         Nash equilibria difficult. We show several
                         undecidability results, and for bounded-memory
                         strategies, we precisely characterize the complexity
                         of computing pure Nash equilibria (for qualitative
                         objectives) in this game model.},
}

Abstract

The problem of synchronizing automata is concerned with the existence of a word that sends all states ofM the automaton to one and the same state. This problem has classically been studied for complete deterministic finite automata, with the existence problem being NLOGSPACE-complete.

In this paper we consider synchronizing-word problems for weighted and timed automata. We consider the synchronization problem in several variants and combinations of these, including deterministic and non-deterministic timed and weighted automata, synchronization to unique location with possibly different clock valuations or accumulated weights, as well as synchronization with a safety condition forbidding the automaton to visit states outside a safety-set during synchronization (e.g. energy constraints). For deterministic weighted automata, the synchronization problem is proven PSPACE-complete under energy constraints, and in 3-EXPSPACE under general safety constraints. For timed automata the synchronization problems are shown to be PSPACE-complete in the deterministic case, and undecidable in the non-deterministic case.

@inproceedings{fsttcs2014-DJLMS,
  author =              {Doyen, Laurent and Juhl, Line and Larsen, Kim
                         Guldstrand and Markey, Nicolas and Shirmohammadi,
                         Mahsa},
  title =               {Synchronizing words for weighted and timed automata},
  editor =              {Raman, Venkatesh and Suresh, S. P.},
  booktitle =           {{P}roceedings of the 34th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'14)},
  acronym =             {{FSTTCS}'14},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {29},
  pages =               {121-132},
  year =                {2014},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2014.121},
  abstract =            {The problem of synchronizing automata is concerned
                         with the existence of a word that sends all states
                         ofM the automaton to one and the same state. This
                         problem has classically been studied for complete
                         deterministic finite automata, with the existence
                         problem being NLOGSPACE-complete.\par In this paper
                         we consider synchronizing-word problems for weighted
                         and timed automata. We consider the synchronization
                         problem in several variants and combinations of
                         these, including deterministic and non-deterministic
                         timed and weighted automata, synchronization to
                         unique location with possibly different clock
                         valuations or accumulated weights, as well as
                         synchronization with a safety condition forbidding
                         the automaton to visit states outside a safety-set
                         during synchronization (e.g. energy constraints).
                         For deterministic weighted automata, the
                         synchronization problem is proven PSPACE-complete
                         under energy constraints, and in 3-EXPSPACE under
                         general safety constraints. For timed automata the
                         synchronization problems are shown to be
                         PSPACE-complete in the deterministic case, and
                         undecidable in the non-deterministic case.},
}

Abstract

Symmetry reductions have been applied extensively for the verification of finite-state concurrent systems and hardware designs using model-checking of temporal logics such as LTL, CTL and CTL*, as well as real-time and probabilistic-system model-checking. In this paper we extend the technique to handle infinite-state games on graphs with finite branching where the objectives of the players can be very general. As particular applications, it is shown that the technique can be applied to reduce the state space in parity games as well as when doing model-checking of the temporal logic ATL*.

@inproceedings{atva2014-MV,
  author =              {Markey, Nicolas and Vester, Steen},
  title =               {Symmetry Reduction in Infinite Games with Finite
                         Branching},
  editor =              {Cassez, Franck and Raskin, Jean-Fran{\c c}ois},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {S}ymposium on {A}utomated {T}echnology for
                         {V}erification and {A}nalysis ({ATVA}'14)},
  acronym =             {{ATVA}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8837},
  pages =               {281-296},
  year =                {2014},
  month =               nov,
  doi =                 {10.1007/978-3-319-11936-6_21},
  abstract =            {Symmetry reductions have been applied extensively
                         for the verification of finite-state concurrent
                         systems and hardware designs using model-checking of
                         temporal logics such as LTL, CTL and
                         CTL\textsuperscript{*}, as well as real-time and
                         probabilistic-system model-checking. In this paper
                         we extend the technique to handle infinite-state
                         games on graphs with finite branching where the
                         objectives of the players can be very general. As
                         particular applications, it is shown that the
                         technique can be applied to reduce the state space
                         in parity games as well as when doing model-checking
                         of the temporal logic ATL\textsuperscript{*}.},
}

Abstract

Formal methods (e.g. Timed Automata or Linear Hybrid Automata) can be used to analyse a real-time system by performing a reachability analysis on the model. The advantage of using formal methods is that they are more expressive than classical analytic models used in schedulability analysis. For example, it is possible to express state-dependent behaviour, arbitrary activation patterns, etc.

In this paper we use the formalism of Linear Hybrid Automata to encode a hierarchical scheduling system. In particular, we model a dynamic server algorithm and the tasks contained within, abstracting away the rest of the system, thus enabling component-based scheduling analysis. We prove the correctness of the model and the decidability of the reachability analysis for the case of periodic tasks. Then, we compare the results of our model against classical schedulability analysis techniques, showing that our analysis performs better than analytic methods in terms of resource utilisation. We further present two case studies: a component with state-dependent tasks, and a simplified model of a real avionics system. Finally, through extensive tests with various configurations, we demonstrate that this approach is usable for medium size components.

@inproceedings{rtcsa2014-SLSFM,
  author =              {Sun, Youcheng and Lipari, Giuseppe and Soulat,
                         Romain and Fribourg, Laurent and Markey, Nicolas},
  title =               {Component-Based Analysis of Hierarchical Scheduling
                         using Linear Hybrid Automata},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {C}onference on {R}eal-{T}ime {C}omputing {S}ystems
                         and {A}pplications ({RTCSA}'14)},
  acronym =             {{RTCSA}'14},
  publisher =           {IEEE Comp. Soc. Press},
  year =                {2014},
  month =               aug,
  doi =                 {10.1109/RTCSA.2014.6910502},
  abstract =            {Formal methods (e.g. Timed Automata or Linear Hybrid
                         Automata) can be used to analyse a real-time system
                         by performing a reachability analysis on the model.
                         The advantage of using formal methods is that they
                         are more expressive than classical analytic models
                         used in schedulability analysis. For example, it is
                         possible to express state-dependent behaviour,
                         arbitrary activation patterns,~etc.\par In this
                         paper we use the formalism of Linear Hybrid Automata
                         to encode a hierarchical scheduling system. In
                         particular, we model a dynamic server algorithm and
                         the tasks contained within, abstracting away the
                         rest of the system, thus enabling component-based
                         scheduling analysis. We prove the correctness of the
                         model and the decidability of the reachability
                         analysis for the case of periodic tasks. Then, we
                         compare the results of our model against classical
                         schedulability analysis techniques, showing that our
                         analysis performs better than analytic methods in
                         terms of resource utilisation. We further present
                         two case studies: a~component with state-dependent
                         tasks, and a simplified model of a real avionics
                         system. Finally, through extensive tests with
                         various configurations, we demonstrate that this
                         approach is usable for medium size components.},
}

@inproceedings{tacas2014-ABK,
  author =              {Almagor, Shaull and Boker, Udi and Kupferman, Orna},
  title =               {Discounting in~{LTL}},
  editor =              {{\'A}brah{\'a}m, Erikz and Havelund, Klaus},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'14)},
  acronym =             {{TACAS}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8413},
  pages =               {424-439},
  year =                {2014},
  month =               apr,
  doi =                 {10.1007/978-3-642-54862-8_37},
}

@inproceedings{vmcai2014-AJKR,
  author =              {Aminof, Benjamin and Jacobs, Swen and Khalimov,
                         Ayrat and Rubin, Sasha},
  title =               {Parametrized Model Checking of Token-Passing
                         Systems},
  editor =              {McMillan, Kenneth L. and Rival, Xavier},
  booktitle =           {{P}roceedings of the 15th {I}nternational {W}orkshop
                         on {V}erification, {M}odel {C}hecking, and
                         {A}bstract {I}nterpretation ({VMCAI}'14)},
  acronym =             {{VMCAI}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8318},
  pages =               {262-281},
  year =                {2014},
  month =               jan,
  doi =                 {10.1007/978-3-642-54013-4_15},
}

@inproceedings{concur2014-AKRSV,
  author =              {Aminof, Benjamin and Kotek, Tomer and Rubin, Sasha
                         and Spegni, Francesco and Veith, Helmut},
  title =               {Parameterized Model Checking of Rendezvous Systems},
  editor =              {Baldan, Paolo and Gorla, Daniele},
  booktitle =           {{P}roceedings of the 25th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'14)},
  acronym =             {{CONCUR}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8704},
  pages =               {109-124},
  year =                {2014},
  month =               sep,
  doi =                 {10.1007/978-3-662-44584-6_9},
}

@inproceedings{sr2014-AR,
  author =              {Aminof, Benjamin and Rubin, Sasha},
  title =               {First Cycle Games},
  booktitle =           {{P}roceedings of the 2nd {I}nternational {W}orkshop
                         on {S}trategic {R}easoning ({SR}'14)},
  acronym =             {{SR}'14},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {146},
  pages =               {83-90},
  year =                {2014},
  month =               mar,
  doi =                 {10.4204/EPTCS.146.11},
}

@article{lmcs10(4)-BBBMBGJ,
  author =              {Bertrand, Nathalie and Bouyer, Patricia and Brihaye,
                         {\relax Th}omas and Menet, Quentin and Baier,
                         {\relax Ch}ristel and Gr{\"o}{\ss}er, Marcus and
                         Jurdzi{\'n}ski, Marcin},
  title =               {Stochastic Timed Automata},
  journal =             {Logical Methods in Computer Science},
  volume =              {10},
  number =              {4},
  year =                {2014},
  month =               dec,
  doi =                 {10.2168/LMCS-10(4:6)2014},
}

@article{tcsyst54(2)-BBD,
  author =              {Brihaye, {\relax Th}omas and Bruy{\`e}re,
                         V{\'e}ronique and De{~}Pril, Julie},
  title =               {On Equilibria in Quantitative Games with
                         Reachability{{\slash}}Safety Objectives},
  publisher =           {Springer-Verlag},
  journal =             {Theory of Computing Systems},
  volume =              {54},
  number =              {2},
  pages =               {150-189},
  year =                {2014},
  month =               feb,
}

@inproceedings{BBJKNN-isola2014,
  author =              {Bohlender, Dimitri and Bruintjes, Harold and Junges,
                         Sebastian and Katelaan, Jens and Nguyen, Viet Yen
                         and Noll, Thomas},
  title =               {A~Review of Statistical Model Checking Pitfalls on
                         Real-Time Stochastic Models},
  editor =              {Margaria, Tiziana and Steffen, Bernhard},
  booktitle =           {{P}roceedings of the 6th {I}nternational {S}ymposium
                         on {L}everaging {A}pplications of {F}ormal
                         {M}ethods, {V}erification and {V}alidation
                         ({IS}o{LA}'14)~-- {P}art~{II}: {S}pecialized
                         {T}echniques and {A}pplications},
  acronym =             {{IS}o{LA}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8803},
  pages =               {177-192},
  year =                {2014},
  month =               oct,
  doi =                 {10.1007/978-3-662-45231-8_13},
}

@article{tocl15(4)-BCHK,
  author =              {Boker, Udi and Chatterjee, Krishnendu and Henzinger,
                         Thomas A. and Kupferman, Orna},
  title =               {Temporal Specifications with Accumulative Values},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {15},
  number =              {4},
  pages =               {27:1-27:25},
  year =                {2014},
  month =               aug,
  doi =                 {10.1145/2629686},
}

@article{acta51(3-4)-BDLL,
  author =              {Bulychev, Peter and David, Alexandre and Larsen, Kim
                         Guldstrand and Li, Guangyuan},
  title =               {Efficient Controller Synthesis for a fragment of
                         {{\(\textsf{MTL}_{0,\infty}\)}}},
  publisher =           {Springer-Verlag},
  journal =             {Acta Informatica},
  volume =              {51},
  number =              {3-4},
  pages =               {165-192},
  year =                {2014},
  month =               jun,
  doi =                 {10.1007/s00236-013-0189-z},
}

@inproceedings{fossacs2014-BFS,
  author =              {Bertrand, Nathalie and Fournier, Paulin and
                         Sangnier, Arnaud},
  title =               {Playing with Probabilities in Reconfigurable
                         Broadcast Networks},
  editor =              {Muscholl, Anca},
  booktitle =           {{P}roceedings of the 17th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'14)},
  acronym =             {{FoSSaCS}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8412},
  pages =               {134-148},
  year =                {2014},
  month =               apr,
  doi =                 {10.1007/978-3-642-54830-7_9},
}

@inproceedings{concur2014-BGKMMT,
  author =              {Brihaye, {\relax Th}omas and Geeraerts, Gilles and
                         Narayanan Krishna, Shankara and Manasa, Lakshmi and
                         Monmege, Benjamin and Trivedi, Ashutosh},
  title =               {Adding negative prices to priced timed games},
  editor =              {Baldan, Paolo and Gorla, Daniele},
  booktitle =           {{P}roceedings of the 25th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'14)},
  acronym =             {{CONCUR}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8704},
  pages =               {560-575},
  year =                {2014},
  month =               sep,
  doi =                 {10.1007/978-3-662-44584-6_38},
}

@inproceedings{rp2014-BGS,
  author =              {Bollig, Benedikt and Gastin, Paul and Schubert,
                         Jana},
  title =               {Parameterized verification of communicating automata
                         under context bounds},
  editor =              {Ouaknine, Jo{\"e}l and Potapov, Igor and Worrell,
                         James},
  booktitle =           {{P}roceedings of the 8th {W}orkshop on
                         {R}eachability {P}roblems in {C}omputational
                         {M}odels ({RP}'14)},
  acronym =             {{RP}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8762},
  pages =               {45-57},
  year =                {2014},
  month =               sep,
  doi =                 {10.1007/978-3-319-11439-2_4},
}

@inproceedings{fsttcs2014-BHL,
  author =              {Bertrand, Nathalie and Haddad, Serge and Lefaucheux,
                         Engel},
  title =               {Foundation of Diagnosis and Predictability in
                         Probabilistic Systems},
  editor =              {Raman, Venkatesh and Suresh, S. P.},
  booktitle =           {{P}roceedings of the 34th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'14)},
  acronym =             {{FSTTCS}'14},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {29},
  pages =               {417-429},
  year =                {2014},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2014.417},
}

@inproceedings{atva2014-BHM,
  author =              {Boigelot, Bernard and Herbreteau, Fr{\'e}d{\'e}ric
                         and Mainz, Isabelle},
  title =               {Acceleration of Affine Hybrid Transformations},
  editor =              {Cassez, Franck and Raskin, Jean-Fran{\c c}ois},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {S}ymposium on {A}utomated {T}echnology for
                         {V}erification and {A}nalysis ({ATVA}'14)},
  acronym =             {{ATVA}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8837},
  pages =               {31-46},
  year =                {2014},
  month =               nov,
  doi =                 {10.1007/978-3-319-11936-6_4},
}

@inproceedings{cav2014-BKKN,
  author =              {Br{\'a}zdil, Tom{\'a}{\v s} and Kla{\v{s}}ka, David
                         and Ku{\v c}era, Anton{\'\i}n and Novotn{\'y}, Petr},
  title =               {Minimizing Running Costs in Consumption Systems},
  editor =              {Biere, Armin and Bloem, Roderick},
  booktitle =           {{P}roceedings of the 26th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'14)},
  acronym =             {{CAV}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8559},
  pages =               {457-472},
  year =                {2014},
  month =               jul,
}

@inproceedings{csllics2014-BMR,
  author =              {Bruy{\`e}re, V{\'e}ronique and Meunier, No{\"e}mie
                         and Raskin, Jean-Fran{\c c}ois},
  title =               {Secure Equilibria in Weighted Games},
  booktitle =           {{P}roceedings of the Joint Meeting of the 23rd
                         {EACSL} {A}nnual {C}onference on {C}omputer
                         {S}cience {L}ogic and the 29th {A}nnual {ACM\slash
                         IEEE} {S}ymposium on {L}ogic {I}n {C}omputer
                         {S}cience ({CSL\slash LICS}'14)},
  acronym =             {{CSL\slash LICS}'14},
  publisher =           {ACM Press},
  chapter =             {26},
  year =                {2014},
  month =               jul,
  doi =                 {10.1145/2603088.2603109},
}

@inproceedings{csllics2014-BRS,
  author =              {Brenguier, Romain and Raskin, Jean-Fran{\c c}ois and
                         Sassolas, Mathieu},
  title =               {The complexity of admissibility in omega-regular
                         games},
  booktitle =           {{P}roceedings of the Joint Meeting of the 23rd
                         {EACSL} {A}nnual {C}onference on {C}omputer
                         {S}cience {L}ogic and the 29th {A}nnual {ACM\slash
                         IEEE} {S}ymposium on {L}ogic {I}n {C}omputer
                         {S}cience ({CSL\slash LICS}'14)},
  acronym =             {{CSL\slash LICS}'14},
  publisher =           {ACM Press},
  pages =               {23:1-23:10},
  year =                {2014},
  month =               jul,
  doi =                 {10.1145/2603088.2603143},
}

@inproceedings{vmcai2014-CDFR,
  author =              {Chatterjee, Krishnendu and Doyen, Laurent and
                         Filiot, Emmanuel and Raskin, Jean-Fran{\c c}ois},
  title =               {Doomsday Equilibria for Omega-Regular Games},
  editor =              {McMillan, Kenneth L. and Rival, Xavier},
  booktitle =           {{P}roceedings of the 15th {I}nternational {W}orkshop
                         on {V}erification, {M}odel {C}hecking, and
                         {A}bstract {I}nterpretation ({VMCAI}'14)},
  acronym =             {{VMCAI}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8318},
  pages =               {78-97},
  year =                {2014},
  month =               jan,
  doi =                 {10.1007/978-3-642-54013-4_5},
}

@mastersthesis{master14-Cer,
  author =              {{\v{C}}erm{\'a}k, Petr},
  title =               {A~Model Checker for Strategy Logic},
  year =                {2014},
  month =               jun,
  school =              {Dept. of Computing, Imperial College London, UK},
}

@techreport{arxiv1402.3199,
  author =              {Chaturvedi, Namit and Gelderie, Marcus},
  title =               {Weak {{\(\omega\)}}-Regular Trace Languages},
  number =              {1402.3199},
  year =                {2014},
  month =               feb,
  institution =         {arXiv},
  type =                {Research Report},
}

@inproceedings{rp2014-CH,
  author =              {Carayol, Arnaud and Hague, Matthew},
  title =               {Regular Strategies In Pushdown Reachability Games},
  editor =              {Ouaknine, Jo{\"e}l and Potapov, Igor and Worrell,
                         James},
  booktitle =           {{P}roceedings of the 8th {W}orkshop on
                         {R}eachability {P}roblems in {C}omputational
                         {M}odels ({RP}'14)},
  acronym =             {{RP}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8762},
  pages =               {58-71},
  year =                {2014},
  month =               sep,
  doi =                 {10.1007/978-3-319-11439-2_5},
}

@inproceedings{icalp2014-Cha,
  author =              {Chaturvedi, Namit},
  title =               {Toward a structure theory of regular infinitary
                         trace languages},
  editor =              {Esparza, Javier and Fraigniaud, Pierre and
                         Koutsoupias, Elias},
  booktitle =           {{P}roceedings of the 41st {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'14)~-- Part~{II}},
  acronym =             {{ICALP}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8573},
  pages =               {134-145},
  year =                {2014},
  month =               jul,
  doi =                 {10.1007/978-3-662-43951-7_12},
}

@techreport{AIB-2014-04,
  author =              {Chaturvedi, Namit},
  title =               {Languages of Infinite Traces and Deterministic
                         Asynchronous Automata},
  number =              {AIB-2014-004},
  year =                {2014},
  month =               feb,
  institution =         {RWTH Aachen, Germany},
  type =                {Research Report},
}

@inproceedings{cav2014-CLMM,
  author =              {{\v{C}}erm{\'a}k, Petr and Lomuscio, Alessio and
                         Mogavero, Fabio and Murano, Aniello},
  title =               {{MCMAS-SLK}: A~Model Checker for the Verification of
                         Strategy Logic Specifications},
  editor =              {Biere, Armin and Bloem, Roderick},
  booktitle =           {{P}roceedings of the 26th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'14)},
  acronym =             {{CAV}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8559},
  pages =               {525-532},
  year =                {2014},
  month =               jul,
  doi =                 {10.1007/978-3-319-08867-9_34},
}

@article{acta51(3-4)-CRR,
  author =              {Chatterjee, Krishnendu and Randour, Mickael and
                         Raskin, Jean-Fran{\c c}ois},
  title =               {Strategy Synthesis for Multi-dimensional
                         Quantitative Objectives},
  publisher =           {Springer-Verlag},
  journal =             {Acta Informatica},
  volume =              {51},
  number =              {3-4},
  pages =               {129-163},
  year =                {2014},
  month =               jun,
  doi =                 {10.1007/s00236-013-0182-6},
}

@inproceedings{fossacs2014-DMS,
  author =              {Doyen, Laurent and Massart, {\relax Th}ierry and
                         Shirmohammadi, Mahsa},
  title =               {Limit synchronization in {M}arkov decision
                         processes},
  editor =              {Muscholl, Anca},
  booktitle =           {{P}roceedings of the 17th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'14)},
  acronym =             {{FoSSaCS}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8412},
  pages =               {58-72},
  year =                {2014},
  month =               apr,
  doi =                 {10.1007/978-3-642-54830-7_4},
}

@inproceedings{stacs2014-Esp,
  author =              {Esparza, Javier},
  title =               {Keeping a Crowd Safe: On the Complexity of
                         Parameterized Verification (Invited Talk)},
  editor =              {Mayr, Ernst W. and Portier, Natacha},
  booktitle =           {{P}roceedings of the 31st {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'14)},
  acronym =             {{STACS}'14},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {25},
  pages =               {1-10},
  year =                {2014},
  month =               mar,
  doi =                 {10.4230/LIPIcs.STACS.2014.1},
}

@article{tocl15(4)-FPS,
  author =              {Frigeri, Achille and Pasquale, Liliana and
                         Spoletini, Paola},
  title =               {Fuzzy Time in Linear Temporal Logic},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {15},
  number =              {4},
  pages =               {30:1-30:22},
  year =                {2014},
  month =               aug,
}

@phdthesis{phd-gelderie,
  author =              {Gelderie, Marcus},
  title =               {Strategy Machines~-- Representation and Complexity
                         of Strategies in Infinite Games},
  year =                {2014},
  month =               feb,
  school =              {RWTH Aachen, Germany},
  type =                {{PhD} thesis},
}

@inproceedings{cav2014-HLLNS,
  author =              {Hansen, Henri and Lin, Shang{-}Wei and Liu, Yang and
                         Nguyen, Truong Khanh and Sun, Jun},
  title =               {Diamonds Are a Girl's Best Friend: Partial Order
                         Reduction for Timed Automata with Abstractions},
  editor =              {Biere, Armin and Bloem, Roderick},
  booktitle =           {{P}roceedings of the 26th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'14)},
  acronym =             {{CAV}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8559},
  pages =               {391-406},
  year =                {2014},
  month =               jul,
  doi =                 {10.1007/978-3-319-08867-9_26},
}

@inproceedings{fsttcs2014-HR,
  author =              {Hunter, Paul and Raskin, Jean-Fran{\c c}ois},
  title =               {Quantitative games with interval objectives},
  editor =              {Raman, Venkatesh and Suresh, S. P.},
  booktitle =           {{P}roceedings of the 34th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'14)},
  acronym =             {{FSTTCS}'14},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {29},
  pages =               {365-377},
  year =                {2014},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2014.365},
}

@inproceedings{nasaFM2014-JLSST,
  author =              {Jensen, Peter Gj{\o}l and Larsen, Kim Guldstrand and
                         Srba, Ji{\v r}{\'\i} and S{\o}rensen, Mathias Grund
                         and Taankvist, Jakob Haar},
  title =               {Memory Efficient Data Structures for Explicit
                         Verification of Timed Systems},
  editor =              {Badger, Julia M. and Rozier, Kristin Yvonne},
  booktitle =           {{P}roceedings of the 6th {NASA} {F}ormal {M}ethods
                         {S}ymposium ({NFM}'14)},
  acronym =             {{NFM}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8430},
  pages =               {307-312},
  year =                {2014},
  month =               apr,
  doi =                 {10.1007/978-3-319-06200-6_26},
}

@article{tcs515-LLTW,
  author =              {Larsen, Kim Guldstrand and Legay, Axel and
                         Traonouez, Louis-Marie and W{\k a}sowski, Andrzej},
  title =               {Robust synthesis for real-time systems},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {515},
  pages =               {96-122},
  year =                {2014},
  month =               jan,
}

@inproceedings{icra2014-LP,
  author =              {Liu, Jun and Prabhakar, Pavithra},
  title =               {Switching control of dynamical systems from metric
                         temporal logic specifications},
  booktitle =           {{P}roceedings of the 2014 {IEEE} {I}nternational
                         {C}onference on {R}obotics and {A}utomation
                         ({ICRA}'14)},
  acronym =             {{ICRA}'01},
  publisher =           {IEEE Robotics~\& Automation Soc.},
  pages =               {5333-5338},
  year =                {2014},
  month =               may,
  doi =                 {10.1109/ICRA.2014.6907643},
}

@article{ercimnews97-Mar,
  author =              {Markey, Nicolas},
  title =               {Cassting: Synthesizing Complex Systems Using
                         Non-Zero-Sum Games},
  publisher =           {European Research Consortium for Informatics and
                         Mathematics},
  journal =             {ERCIM News},
  volume =              {97},
  pages =               {25-26},
  year =                {2014},
  month =               apr,
  url =                 {http://ercim-news.ercim.eu/en97/special/
  cassting-synthesizing-complex-systems-using-non-zero-sum-games},
}

@article{tocl15(4)-MMPV,
  author =              {Mogavero, Fabio and Murano, Aniello and Perelli,
                         Giuseppe and Vardi, Moshe Y.},
  title =               {Reasoning About Strategies: On the Model-Checking
                         Problem},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {15},
  number =              {4},
  pages =               {34:1-34:47},
  year =                {2014},
  month =               aug,
  doi =                 {10.1145/2631917},
}

@inproceedings{clima2014-MMS,
  author =              {Mogavero, Fabio and Murano, Aniello and Sauro,
                         Luigi},
  title =               {A Behavioral Hierarchy of Strategy Logic},
  editor =              {Bulling, Nils and van der Torre, Leendert W. N. and
                         Villata, Serena and Jamroga, Wojciech and
                         Vasconcelos, Wamberto Weber},
  booktitle =           {{P}roceedings of the 15th {I}nternational {W}orkshop
                         on {C}omputational {L}ogic in {M}ulti-{A}gent
                         {S}ystems ({CLIMA}'14)},
  acronym =             {{CLIMA}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Artificial Intelligence},
  volume =              {8624},
  pages =               {148-165},
  year =                {2014},
  month =               aug,
  doi =                 {10.1007/978-3-319-09764-0_10},
}

@inproceedings{concur2014-ORS,
  author =              {Oualhadj, Youssouf and Reynier, Pierre-Alain and
                         Sankur, Ocan},
  title =               {Probabilistic Robust Timed Games},
  editor =              {Baldan, Paolo and Gorla, Daniele},
  booktitle =           {{P}roceedings of the 25th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'14)},
  acronym =             {{CONCUR}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8704},
  pages =               {203-217},
  year =                {2014},
  month =               sep,
  doi =                 {10.1007/978-3-662-44584-6_15},
}

@phdthesis{phd-shirmohammadi,
  author =              {Shirmohammadi, Mahsa},
  title =               {Qualitative analysis of synchronizing probabilistic
                         systems},
  year =                {2014},
  month =               dec,
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France and D{\'e}partement d'Informatique,
                         Universit{\'e} Libre de Bruxelles, Belgium},
  type =                {Th\`ese de doctorat},
}

@mastersthesis{sorensen-master14,
  author =              {S{\o}rensen, Mathias Grund},
  title =               {Controller synthesis for home automation},
  year =                {2014},
  school =              {Computer Science Department, Aalborg University,
                         Denmark},
}

@inproceedings{atva2014-WJ,
  author =              {Wang, Weifeng and Jiao, Li},
  title =               {Trace Abstraction Refinement for Timed Automata},
  editor =              {Cassez, Franck and Raskin, Jean-Fran{\c c}ois},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {S}ymposium on {A}utomated {T}echnology for
                         {V}erification and {A}nalysis ({ATVA}'14)},
  acronym =             {{ATVA}'14},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {8837},
  pages =               {396-410},
  year =                {2014},
  month =               nov,
  doi =                 {10.1007/978-3-319-11936-6_28},
}