Nicolas Markey

Résumé

We define and study a slight variation on the semantics of Strategy Logic: while in the classical semantics, all strategies are shifted during the evaluation of temporal modalities, we propose to only shift the strategies that have been assigned to a player, thus matching the intuition that we can assign the very same strategy to the players at different points in time. We prove that surprisingly, this renders the model-checking problem undecidable.

@article{ipl116(2)-BGM,
  author =              {Bouyer, Patricia and Gardy, Patrick and Markey,
                         Nicolas},
  title =               {On the semantics of Strategy Logic},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {116},
  number =              {2},
  pages =               {75-79},
  year =                {2016},
  month =               feb,
  doi =                 {10.1016/j.ipl.2015.10.004},
  abstract =            {We define and study a slight variation on the
                         semantics of Strategy Logic: while in the classical
                         semantics, all strategies are shifted during the
                         evaluation of temporal modalities, we propose to
                         only shift the strategies that have been assigned to
                         a player, thus matching the intuition that we can
                         assign the very same strategy to the players at
                         different points in time. We prove that
                         surprisingly, this renders the model-checking
                         problem undecidable.},
}

Résumé

Weighted timed automata have been defined in the early 2000's for modelling resource-consumption or -allocation problems in real-time systems. Optimal reachability is decidable in weighted timed automata, and a symbolic forward algorithm has been developed to solve that problem. This algorithm uses so-called priced zones, an extension of standard zones with cost functions. In order to ensure termination, the algorithm requires clocks to be bounded. For unpriced timed automata, much work has been done to develop sound abstractions adapted to the forward exploration of timed automata, ensuring termination of the model-checking algorithm without bounding the clocks. In this paper, we take advantage of recent developments on abstractions for timed automata, and propose an algorithm allowing for symbolic analysis of all weighted timed automata, without requiring bounded clocks.

@inproceedings{cav2016-BCM,
  author =              {Bouyer, Patricia and Colange, Maximilien and Markey,
                         Nicolas},
  title =               {Symbolic Optimal Reachability in Weighted Timed
                         Automata},
  editor =              {Chaudhuri, Swarat and Farzan, Azadeh},
  booktitle =           {{P}roceedings of the 28th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'16)},
  acronym =             {{CAV}'16},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9779},
  pages =               {513-530},
  year =                {2016},
  month =               jul,
  doi =                 {10.1007/978-3-319-41528-4_28},
  url =                 {http://arxiv.org/abs/1602.00481},
  abstract =            {Weighted timed automata have been defined in the
                         early 2000's for modelling resource-consumption or
                         -allocation problems in real-time systems. Optimal
                         reachability is decidable in weighted timed
                         automata, and a symbolic forward algorithm has been
                         developed to solve that problem. This algorithm uses
                         so-called priced zones, an extension of standard
                         zones with cost functions. In order to ensure
                         termination, the algorithm requires clocks to be
                         bounded. For unpriced timed automata, much work has
                         been done to develop sound abstractions adapted to
                         the forward exploration of timed automata, ensuring
                         termination of the model-checking algorithm without
                         bounding the clocks. In this paper, we take
                         advantage of recent developments on abstractions for
                         timed automata, and propose an algorithm allowing
                         for symbolic analysis of all weighted timed
                         automata, without requiring bounded clocks.},
}

Résumé

We study the almost-sure reachability problem in a distributed system obtained as the asynchronous composition of N copies (called processes) of the same automaton (called protocol), that can communicate via a shared register with finite domain. The automaton has two types of transitions: write-transitions update the value of the register, while read-transitions move to a new state depending on the content of the register. Non-determinism is resolved by a stochastic scheduler. Given a protocol, we focus on almost-sure reachability of a target state by one of the processes. The answer to this problem naturally depends on the number N of processes. However, we prove that our setting has a cut-off property : the answer to the almost-sure reachability problem is constant when N is large enough; we then develop an EXPSPACE algorithm deciding whether this constant answer is positive or negative.

@inproceedings{icalp2016-BMRSS,
  author =              {Bouyer, Patricia and Markey, Nicolas and Randour,
                         Mickael and Sangnier, Arnaud and Stan, Daniel},
  title =               {Reachability in Networks of Register Protocols under
                         Stochastic Schedulers},
  editor =              {Chatzigiannakis, Ioannis and Mitzenmacher, Michael
                         and Rabani, Yuval and Sangiorgi, Davide},
  booktitle =           {{P}roceedings of the 43rd {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'16)~-- Part~{II}},
  acronym =             {{ICALP}'16},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {55},
  pages =               {106:1-106:14},
  year =                {2016},
  month =               jul,
  doi =                 {10.4230/LIPIcs.ICALP.2016.106},
  abstract =            {We study the almost-sure reachability problem in a
                         distributed system obtained as the asynchronous
                         composition of~\(N\) copies (called
                         \emph{processes}) of the same automaton (called
                         \emph{protocol}), that can communicate via a shared
                         register with finite domain. The automaton has two
                         types of transitions: write-transitions update the
                         value of the register, while read-transitions move
                         to a new state depending on the content of the
                         register. Non-determinism is resolved by a
                         stochastic scheduler. Given a protocol, we focus on
                         almost-sure reachability of a target state by one of
                         the processes. The answer to this problem naturally
                         depends on the number~\(N\) of processes. However,
                         we prove that our setting has a cut-off property :
                         the answer to the almost-sure reachability problem
                         is constant when \(N\) is large enough; we~then
                         develop an EXPSPACE algorithm deciding whether this
                         constant answer is positive or negative.},
}

Résumé

We study the existence of mixed-strategy equilibria in concurrent games played on graphs. While existence is guaranteed with safety objectives for each player, Nash equilibria need not exist when players are given arbitrary terminal-reward objectives, and their existence is undecidable with qualitative reachability objectives (and only three players). However, these results rely on the fact that the players can enforce infinite plays while trying to improve their payoffs. In this paper, we introduce a relaxed notion of equilibria, where deviations are imprecise. We prove that contrary to Nash equilibria, such (stationary) equilibria always exist, and we develop a PSPACE algorithm to compute one.

@inproceedings{gandalf2016-BMS,
  author =              {Bouyer, Patricia and Markey, Nicolas and Stan,
                         Daniel},
  title =               {Stochastic Equilibria under Imprecise Deviations in
                         Terminal-Reward Concurrent Games},
  editor =              {Cantone, Domenico and Delzanno, Giorgio},
  booktitle =           {{P}roceedings of the 7th {I}nternational {S}ymposium
                         on {G}ames, {A}utomata, {L}ogics and {F}ormal
                         {V}erification ({GandALF}'16)},
  acronym =             {{GandALF}'16},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {226},
  pages =               {61-75},
  year =                {2016},
  month =               sep,
  doi =                 {10.4204/EPTCS.226.5},
  abstract =            {We study the existence of mixed-strategy equilibria
                         in concurrent games played on graphs. While
                         existence is guaranteed with safety objectives for
                         each player, Nash equilibria need not exist when
                         players are given arbitrary terminal-reward
                         objectives, and their existence is undecidable with
                         qualitative reachability objectives (and~only three
                         players). However, these results rely on the fact
                         that the players can enforce infinite plays while
                         trying to improve their payoffs. In this paper, we
                         introduce a relaxed notion of equilibria, where
                         deviations are imprecise. We prove that contrary to
                         Nash equilibria, such (stationary) equilibria always
                         exist, and we develop a PSPACE algorithm to compute
                         one.},
}

Résumé

QCTL extends the temporal logic CTL with quantification over atomic propositions. While the algorithmic questions for QCTL and its fragments with limited quantification depth are well-understood (e.g. satisfiability of QCTLk, with at most k nested blocks of quantifiers, is k+1-EXPTIME-complete), very few results are known about the expressiveness of this logic. We address such expressiveness questions in this paper. We first consider the distinguishing power of these logics (i.e., their ability to separate models), their relationship with behavioural equivalences, and their ability to capture the behaviours of finite Kripke structures with so-called characteristic formulas. We then consider their expressive power (i.e., their ability to express a property), showing that in terms of expressiveness the hierarchy QCTLk collapses at level 2 (in other terms, any QCTL formula can be expressed using at most two nested blocks of quantifiers).

@inproceedings{concur2016-DLM,
  author =              {David, Am{\'e}lie and Laroussinie, Fran{\c c}ois and
                         Markey, Nicolas},
  title =               {On~the expressiveness of~{QCTL}},
  editor =              {Desharnais, Jules and Jagadeesan, Radha},
  booktitle =           {{P}roceedings of the 27th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'16)},
  acronym =             {{CONCUR}'16},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {59},
  pages =               {28:1-28:15},
  year =                {2016},
  month =               aug,
  doi =                 {10.4230/LIPIcs.CONCUR.2016.28},
  abstract =            {QCTL extends the temporal logic CTL with
                         quantification over atomic propositions. While the
                         algorithmic questions for QCTL and its fragments
                         with limited quantification depth are
                         well-understood (e.g. satisfiability of
                         QCTL\textsuperscript{\(k\)}, with at most \(k\)
                         nested blocks of quantifiers, is
                         \(k+1\)-EXPTIME-complete), very few results are
                         known about the expressiveness of this logic.
                         We~address such expressiveness questions in this
                         paper. We first consider the \emph{distinguishing
                         power} of these logics (i.e.,~their ability to
                         separate models), their relationship with
                         behavioural equivalences, and their ability to
                         capture the behaviours of finite Kripke structures
                         with so-called characteristic formulas. We then
                         consider their \emph{expressive power} (i.e.,~their
                         ability to express a property), showing that in
                         terms of expressiveness the hierarchy
                         QCTL\textsuperscript{\(k\)} collapses at level~2
                         (in~other terms, any~QCTL formula can be expressed
                         using at most two nested blocks of quantifiers).},
}

Résumé

Switched systems are a convenient formalism for modeling physical processes interacting with a digital controller. Unfortunately, the formalism does not capture the distributed nature encountered e.g. in cyber-physical systems, which are organized as networks of elements interacting with each other and with local controllers. Most current methods for control synthesis can only produce a centralized controller, which is assumed to have complete knowledge of all the component states and can interact with all of them. In this paper, we consider a controller synthesis method based on state space decomposition, and propose a game-based approach in order to extend it within a distributed framework.

@inproceedings{syncop2015-FKM,
  author =              {Fribourg, Laurent and K{\"u}hne, Ulrich and Markey,
                         Nicolas},
  title =               {Game-based Synthesis of Distributed Controllers for
                         Sampled Switched Systems},
  editor =              {Andr{\'e}, {\'E}tienne and Frehse, Goran},
  booktitle =           {{P}roceedings of the 2nd {I}nternational {W}orkshop
                         on {S}ynthesis of {C}omplex {P}arameters
                         ({S}yn{C}o{P}'15)},
  acronym =             {{S}yn{C}o{P}'15},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {OpenAccess Series in Informatics},
  volume =              {44},
  pages =               {47-61},
  year =                {2016},
  month =               apr,
  doi =                 {10.4230/OASIcs.SynCoP.2015.48},
  abstract =            {Switched systems are a convenient formalism for
                         modeling physical processes interacting with a
                         digital controller. Unfortunately, the formalism
                         does not capture the distributed nature encountered
                         e.g. in cyber-physical systems, which are organized
                         as networks of elements interacting with each other
                         and with local controllers. Most current methods for
                         control synthesis can only produce a centralized
                         controller, which is assumed to have complete
                         knowledge of all the component states and can
                         interact with all of them. In~this paper,
                         we~consider a controller synthesis method based on
                         state space decomposition, and propose a game-based
                         approach in order to extend it within a distributed
                         framework.},
}

Résumé

We present a correct-by-design method of state-dependent control synthesis for linear discrete-time switching systems. Given an objective region R of the state space, the method builds a capture set S and a control which steers any element of S into R. The method works by iterated backward reachability from R. More precisely, S is given as a parametric extension of R, and the maximum value of the parameter is solved by linear programming. The method can also be used to synthesize a stability control which maintains indefinitely within R all the states starting at R. We explain how the synthesis method can be performed in a distributed manner. The method has been implemented and successfully applied to the synthesis of a distributed control of a concrete floor heating system with 11 rooms and 211 = 2048 switching modes.

@inproceedings{rp2016-LFMDC,
  author =              {Le{~}Co{\"e}nt, Adrien and Fribourg, Laurent and
                         Markey, Nicolas and De{~}Vuyst, Florian and Chamoin,
                         Ludovic},
  title =               {Distributed Synthesis of State-Dependent Switching
                         Control},
  editor =              {Larsen, Kim Guldstrand and Srba, Ji{\v r}{\'\i}},
  booktitle =           {{P}roceedings of the 10th {W}orkshop on
                         {R}eachability {P}roblems in {C}omputational
                         {M}odels ({RP}'16)},
  acronym =             {{RP}'16},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9899},
  pages =               {119-133},
  year =                {2016},
  month =               sep,
  doi =                 {10.1007/978-3-319-45994-3_9},
  abstract =            {We present a correct-by-design method of
                         state-dependent control synthesis for linear
                         discrete-time switching systems. Given an objective
                         region~\(R\) of the state space, the method builds a
                         capture set~\(S\) and a control which steers any
                         element of~\(S\) into~\(R\). The method works by
                         iterated backward reachability from~\(R\). More
                         precisely, \(S\)~is given as a parametric extension
                         of~\(R\), and the maximum value of the parameter is
                         solved by linear programming. The method can also be
                         used to synthesize a stability control which
                         maintains indefinitely within~\(R\) all the states
                         starting at~\(R\). We~explain how the synthesis
                         method can be performed in a distributed manner. The
                         method has been implemented and successfully applied
                         to the synthesis of a distributed control of a
                         concrete floor heating system with 11 rooms and
                         \(2^{11} = 2048\) switching modes.},
}

@proceedings{cassting-syncop2016-DJMS,
  title =               {{P}roceedings of the {C}assting Workshop on {G}ames
                         for the {S}ynthesis of {C}omplex {S}ystems
                         ({C}assting'16) and of the 3rd {I}nternational
                         {W}orkshop on {S}ynthesis of {C}omplex {P}arameters
                         ({S}yn{C}o{P}'16)},
  editor =              {Brihaye, {\relax Th}omas and Delahaye, Beno{\^\i}t
                         and Jezequel, Lo{\"\i}g and Markey, Nicolas and
                         Srba, Ji{\v r}{\'\i}},
  booktitle =           {{P}roceedings of the {C}assting Workshop on {G}ames
                         for the {S}ynthesis of {C}omplex {S}ystems
                         ({C}assting'16) and of the 3rd {I}nternational
                         {W}orkshop on {S}ynthesis of {C}omplex {P}arameters
                         ({S}yn{C}o{P}'16)},
  acronym =             {{C}assting{{\slash}}{S}yn{C}o{P}'16},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {220},
  year =                {2016},
  month =               jul,
  confyear =            {2016},
  confmonth =           {4},
  doi =                 {10.4204/EPTCS.220},
  url =                 {http://eptcs.web.cse.unsw.edu.au/
                         content.cgi?CASSTINGSynCoP2016},
}

@proceedings{formats2016-FM,
  title =               {{P}roceedings of the 14th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'16)},
  editor =              {Fr{\"a}nzle, Martin and Markey, Nicolas},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'16)},
  acronym =             {{FORMATS}'16},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9884},
  year =                {2016},
  month =               aug,
  doi =                 {10.1007/978-3-319-44878-7},
  url =                 {http://link.springer.com/book/10.1007/978-3-319-44878-7},
}

@inproceedings{usenixsec2016-ABBDE,
  author =              {Almeida, Jos{\'e} Bacelar and Barbosa, Manuel and
                         Barthe, Gilles and Dupressoir, Fran{\c c}ois and
                         Emmi, Michael},
  title =               {Verifying Constant-Time Implementations},
  editor =              {Holz, Thorsten and Savage, Stefan},
  booktitle =           {{P}roceedings of the 25th {USENIX} {S}ecurity
                         {S}ymposium ({USENIX} {S}ecurity'16)},
  acronym =             {{USENIX} {S}ecurity'16},
  publisher =           {Usenix Association},
  pages =               {53-70},
  year =                {2016},
  month =               aug,
}

@article{jacm63(3)-ABK,
  author =              {Almagor, Shaull and Boker, Udi and Kupferman, Orna},
  title =               {Formally Reasoning about Quality},
  publisher =           {ACM Press},
  journal =             {Journal of the~ACM},
  volume =              {63},
  number =              {3},
  pages =               {24:1-24:56},
  year =                {2016},
  month =               sep,
  doi =                 {10.1145/2875421},
}

@inproceedings{concur2016-AGK,
  author =              {Akshay, S. and Gastin, Paul and Krishna, Shankara
                         Narayanan},
  title =               {Analyzing Timed Systems Using Tree Automata},
  editor =              {Desharnais, Jules and Jagadeesan, Radha},
  booktitle =           {{P}roceedings of the 27th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'16)},
  acronym =             {{CONCUR}'16},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {59},
  pages =               {27:1-27:14},
  year =                {2016},
  month =               aug,
  doi =                 {10.4230/LIPIcs.CONCUR.2016.27},
}

@inproceedings{sagt2016-AHK,
  author =              {Avni, Guy and Henzinger, Thomas A. and Kupferman,
                         Orna},
  title =               {Dynamic Resource Allocation Games},
  booktitle =           {{P}roceedings of the 9th {I}nternational {S}ymposium
                         on {A}lgorithmic {G}ame {T}heory ({SAGT}'16)},
  acronym =             {{SAGT}'16},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9928},
  pages =               {153-166},
  year =                {2016},
  month =               sep,
  doi =                 {10.1007/978-3-662-53354-3_13},
}

@inproceedings{vmcai2016-AJK,
  author =              {Au{\ss}erlechner, Simon and Jacobs, Swen and
                         Khalimov, Ayrat},
  title =               {Tight Cutoffs for Guarded Protocols with Fairness},
  editor =              {Jobstmann, Barbara and Leino, K. Rustan M.},
  booktitle =           {{P}roceedings of the 17th {I}nternational {W}orkshop
                         on {V}erification, {M}odel {C}hecking, and
                         {A}bstract {I}nterpretation ({VMCAI}'16)},
  acronym =             {{VMCAI}'16},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9583},
  pages =               {476-494},
  year =                {2016},
  month =               jan,
  doi =                 {10.1007/978-3-662-49122-5_23},
}

@inproceedings{csl2016-AK,
  author =              {Almagor, Shaull and Kupferman, Orna},
  title =               {High-Quality Synthesis Against Stochastic
                         Environments},
  editor =              {Talbot, Jean-Marc and Regnier, Laurent},
  booktitle =           {{P}roceedings of the 25th {EACSL} {A}nnual
                         {C}onference on {C}omputer {S}cience {L}ogic
                         ({CSL}'16)},
  acronym =             {{CSL}'16},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {62},
  pages =               {28:1-28:17},
  year =                {2016},
  month =               sep,
  doi =                 {10.4230/LIPIcs.CSL.2016.28},
}

@inproceedings{aamas2016-AMMR,
  author =              {Aminof, Benjamin and Malvone, Vadim and Murano,
                         Aniello and Rubin, Sasha},
  title =               {Graded Strategy Logic: Reasoning about Uniqueness of
                         Nash Equilibria},
  editor =              {Jonker, Catholijn M. and Marsella, Stacy and
                         Thangarajah, John and Tuyls, Karl},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {A}utonomous {A}gents and
                         {M}ultiagent {S}ystems ({AAMAS}'16)},
  acronym =             {{AAMAS}'16},
  publisher =           {International Foundation for Autonomous Agents and
                         Multiagent Systems},
  pages =               {698-706},
  year =                {2016},
  month =               may,
}

@book{BO16-CSAPP,
  author =              {Bryant, Randal E. and O'Hallaron, David R.},
  title =               {Computer Systems~-- A~programmer's perspective},
  publisher =           {Pearson},
  year =                {2016},
}

@inproceedings{fsttcs2016-BPRS,
  author =              {Brenguier, Romain and P{\'e}rez, Guillermo A. and
                         Raskin, Jean-Fran{\c c}ois and Sassolas, Mathieu},
  title =               {Admissibility in Quantitative Graph Games},
  editor =              {Akshay, S. and Lal, Akash and Saurabh, Saket and
                         Sen, Sandeep},
  booktitle =           {{P}roceedings of the 36th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'16)},
  acronym =             {{FSTTCS}'16},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  pages =               {42:1-42:14},
  year =                {2016},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2016.42},
}

@inproceedings{concur2016-Bre,
  author =              {Brenguier, Romain},
  title =               {Optimal Assumptions for Synthesis},
  editor =              {Desharnais, Jules and Jagadeesan, Radha},
  booktitle =           {{P}roceedings of the 27th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'16)},
  acronym =             {{CONCUR}'16},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {59},
  pages =               {8:1-8:15},
  year =                {2016},
  month =               aug,
  doi =                 {10.4230/LIPIcs.CONCUR.2016.8},
}

@inproceedings{icalp2016-CD,
  author =              {Chatterjee, Krishnendu and Doyen, Laurent},
  title =               {Computation Tree Logic for Synchronization
                         Properties},
  editor =              {Chatzigiannakis, Ioannis and Mitzenmacher, Michael
                         and Rabani, Yuval and Sangiorgi, Davide},
  booktitle =           {{P}roceedings of the 43rd {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'16)~-- Part~{II}},
  acronym =             {{ICALP}'16},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {55},
  pages =               {98:1-98:14},
  year =                {2016},
  month =               jul,
  doi =                 {10.4230/LIPIcs.ICALP.2016.98},
}

@inproceedings{icalp2016-CFGR,
  author =              {Condurache, Rodica and Filiot, Emmanuel and
                         Gentilini, Raffaella and Raskin, Jean-Fran{\c c}ois},
  title =               {The Complexity of Rational Synthesis},
  editor =              {Chatzigiannakis, Ioannis and Mitzenmacher, Michael
                         and Rabani, Yuval and Sangiorgi, Davide},
  booktitle =           {{P}roceedings of the 43rd {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'16)~-- Part~{II}},
  acronym =             {{ICALP}'16},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {55},
  pages =               {121:1-121:15},
  year =                {2016},
  month =               jul,
  doi =                 {10.4230/LIPIcs.ICALP.2016.121},
}

@inproceedings{atva2016-DLFMRX,
  author =              {Duret{-}Lutz, Alexandre and Lewkowicz, Alexandre and
                         Fauchille, Amaury and Michaud, Thibault and Renault,
                         {\'E}tienne and Xu, Laurent},
  title =               {Spot~2.0~-- {A}~Framework for {LTL} and
                         {{\(\omega\)}}-Automata Manipulation},
  editor =              {Artho, Cyrille and Legay, Axel and Peled, Doron A.},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {S}ymposium on {A}utomated {T}echnology for
                         {V}erification and {A}nalysis ({ATVA}'16)},
  acronym =             {{ATVA}'16},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9938},
  pages =               {122-129},
  year =                {2016},
  month =               oct,
  doi =                 {10.1007/978-3-319-46520-3_8},
}

@inproceedings{fsttcs2016-EGLM,
  author =              {Esparza, Javier and Ganty, Pierre and Leroux,
                         J{\'e}r{\^o}me and Majumdar, Rupak},
  title =               {Model checking Population Protocols},
  editor =              {Akshay, S. and Lal, Akash and Saurabh, Saket and
                         Sen, Sandeep},
  booktitle =           {{P}roceedings of the 36th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'16)},
  acronym =             {{FSTTCS}'16},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  pages =               {27:1-27:14},
  year =                {2016},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2016.27},
}

@article{scp123()-FJMP,
  author =              {Falcone, Yli{\`e}s and J{\'e}ron, Thierry and
                         Marchand, Herv{\'e} and Pinisetty, Srinivas},
  title =               {Runtime enforcement of regular timed properties by
                         suppressing and delaying events},
  publisher =           {Elsevier},
  journal =             {Science of Computer Programming},
  volume =              {123},
  pages =               {2-41},
  year =                {2016},
  month =               jul,
  doi =                 {10.1016/j.scico.2016.02.008},
}

@inproceedings{pn2016-HK,
  author =              {H{\'e}lou{\"e}t, Lo{\"\i}c and Kecir, Karim},
  title =               {Realizability of Schedules by Stochastic Time
                         {P}etri Nets with Blocking Semantics},
  editor =              {Kordon, Fabrice and Moldt, Daniel},
  booktitle =           {{P}roceedings of the 37th {I}nternational
                         {C}onference on {A}pplications and {T}heory of
                         {P}etri Nets and {C}oncurrency ({PETRI NETS}'16)},
  acronym =             {{PETRI~NETS}'16},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9698},
  pages =               {155-175},
  year =                {2016},
  month =               jun,
  doi =                 {10.1007/978-3-319-39086-4_11},
}

@inproceedings{fsttcs2016-HSTW,
  author =              {Herbreteau, Fr{\'e}d{\'e}ric and Srivathsan, B. and
                         Tran, Thanh-Tung and Walukiewicz, Igor},
  title =               {Why liveness for timed automata is hard, and what we
                         can do about~it},
  editor =              {Akshay, S. and Lal, Akash and Saurabh, Saket and
                         Sen, Sandeep},
  booktitle =           {{P}roceedings of the 36th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'16)},
  acronym =             {{FSTTCS}'16},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  pages =               {48:1-48:14},
  year =                {2016},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2016.48},
}

@article{icomp251()-HSW,
  author =              {Herbreteau, Fr{\'e}d{\'e}ric and Srivathsan, B. and
                         Walukiewicz, Igor},
  title =               {Efficient emptiness check for timed {B}{\"u}chi
                         automata},
  publisher =           {Elsevier},
  journal =             {Information and Computation},
  volume =              {251},
  pages =               {67-90},
  year =                {2016},
  month =               dec,
  doi =                 {10.1016/j.ic.2016.07.004},
}

@inproceedings{aamas2016-JKP,
  author =              {Jamroga, Wojciech and Konikowska, Beata and Penczek,
                         Wojciech},
  title =               {Multi-Valued Verification of Strategic Ability},
  editor =              {Jonker, Catholijn M. and Marsella, Stacy and
                         Thangarajah, John and Tuyls, Karl},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {A}utonomous {A}gents and
                         {M}ultiagent {S}ystems ({AAMAS}'16)},
  acronym =             {{AAMAS}'16},
  publisher =           {International Foundation for Autonomous Agents and
                         Multiagent Systems},
  pages =               {1180-1189},
  year =                {2016},
  month =               may,
}

@inproceedings{fossacs2016-KMP,
  author =              {Krishna, Shankara Narayanan and Madnani, Khushraj
                         and Pandya, Paritosh K.},
  title =               {Metric Temporal Logic with Counting},
  editor =              {Jacobs, Bart and L{\"o}ding, Christof},
  booktitle =           {{P}roceedings of the 19th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'16)},
  acronym =             {{FoSSaCS}'16},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9634},
  pages =               {335-352},
  year =                {2016},
  month =               apr,
  doi =                 {10.1007/978-3-662-49630-5_20},
}

@article{amai78(1)-KPV,
  author =              {Kupferman, Orna and Perelli, Giuseppe and Vardi,
                         Moshe Y.},
  title =               {Synthesis with rational environments},
  publisher =           {Kluwer Academic},
  journal =             {Annals of Mathematics and Artificial Intelligence},
  volume =              {78},
  number =              {1},
  pages =               {3-20},
  year =                {2016},
  month =               sep,
  doi =                 {10.1007/s10472-016-9508-8},
}

@inproceedings{cav2016-LR,
  author =              {Lin, Anthony W. and R{\"u}mmer, Philipp},
  title =               {Liveness of Randomised Parameterised Systems under
                         Arbitrary Schedulers},
  editor =              {Chaudhuri, Swarat and Farzan, Azadeh},
  booktitle =           {{P}roceedings of the 28th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'16)},
  acronym =             {{CAV}'16},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9779},
  pages =               {112-133},
  year =                {2016},
  month =               jul,
  doi =                 {10.1007/978-3-319-41540-6_7},
}

@inproceedings{sac2016-PPTJFM,
  author =              {Pinisetty, Srinivas and Preoteasa, Viorel and
                         Tripakis, Stavros and J{\'e}ron, Thierry and
                         Falcone, Yli{\`e}s and Marchand, Herv{\'e}},
  title =               {Predictive Runtime Enforcement},
  editor =              {Ossowski, Sascha},
  booktitle =           {{P}roceedings of the 31st {A}nnual {ACM} {S}ymposium
                         on {A}pplied {C}omputing ({SAC}'16)},
  acronym =             {{SAC}'16},
  publisher =           {ACM Press},
  pages =               {1628-1633},
  year =                {2016},
  month =               apr,
  doi =                 {10.1145/2851613.2851827},
}

@article{scl96()-PS,
  author =              {Perrin, Nicolas and Schlehuber{-}Caissier, Philipp},
  title =               {Fast diffeomorphic matching to learn globally
                         asymptotically stable nonlinear dynamical systems},
  publisher =           {Elsevier},
  journal =             {Systems~\& Control Letters},
  volume =              {96},
  pages =               {51-59},
  year =                {2016},
  month =               oct,
  doi =                 {10.1016/j.sysconle.2016.06.018},
}

@article{fundi143(3-4)-Rei,
  author =              {Reichert, Julien},
  title =               {On The Complexity of Counter Reachability Games},
  publisher =           {IOS Press},
  journal =             {Fundamenta Informaticae},
  volume =              {143},
  number =              {3-4},
  pages =               {415-436},
  year =                {2016},
  doi =                 {10.3233/FI-2016-1320},
}

@article{toct8(1)-Sch,
  author =              {Schmitz, Sylvain},
  title =               {Complexity Hierarchies Beyond Elementary},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computation Theory},
  volume =              {8},
  number =              {1},
  pages =               {3:1-3:36},
  year =                {2016},
  month =               feb,
  doi =                 {10.1145/2858784},
}

@phdthesis{phd-vdb2016,
  author =              {Van{~}den{ }Bogaard, Marie},
  title =               {Motifs de flot d'information dans les jeux {\`a}
                         information imparfaite},
  year =                {2016},
  month =               dec,
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {Th\`ese de doctorat},
}