@inproceedings{FFLRS-fsfma14, address = {Singapore}, month = may, year = 2014, volume = 156, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Lin, Shang{-}Wei and Petrucci, Laure}, acronym = {{FSFMA}'14}, booktitle = {{P}roceedings of the 2nd {F}rench-{S}ingaporean {W}orkshop on {F}ormal {M}ethods and {A}pplications ({FSFMA}'14)}, author = {Feld, Gilles and Fribourg, Laurent and Labrousse, Denis and Revol, Bertrand and Soulat, Romain}, title = {Correct-by-design Control Synthesis for Multilevel Converters using State Space Decomposition}, pages = {5-16}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FFLRS-fsfma14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FFLRS-fsfma14.pdf}, doi = {10.4204/EPTCS.156.5}, abstract = {High-power converters based on elementary switching cells are more and more used in the industry of power electronics owing to various advantages such as lower voltage stress and reduced power loss. However, the complexity of controlling such converters is a major challenge that the power manufacturing industry has to face with. The synthesis of industrial switching controllers relies today on heuristic rules and empiric simulation. The state of the system is not guaranteed to stay within the limits that are admissible for its correct electrical behavior. We show here how to apply a formal method in order to synthesize a correct-by-design control that guarantees that the power converter will always stay within a predefined safe zone of variations for its input parameters. The method is applied in order to synthesize a correct-by-design control for 5-level and 7-level power converters with a flying capacitor topology. We check the validity of our approach by numerical simulations for 5 and 7 levels. We also perform physical experimentations using a prototype built by SATIE laboratory for 5 levels} }

@misc{cassting-D24, author = {Markey, Nicolas and Chaturvedi, Namit and Geeraerts, Gilles and Srba, Ji{\v{r}}{\'\i}}, title = {Efficient strategy synthesis for complex objectives}, howpublished = {Cassting deliverable~D2.4 (FP7-ICT-601148)}, month = oct, year = {2014}, note = {20~pages}, type = {Contract Report}, url = {http://www.cassting-project.eu/wp-content/uploads/2014/10/deliv-24.pdf}, pdf = {http://www.cassting-project.eu/wp-content/uploads/2014/10/deliv-24.pdf} }

@inproceedings{JLMX-mfps30, address = {Ithaca, New~York, USA}, month = jun, year = 2014, volume = 308, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier Science Publishers}, editor = {Jacobs, Bart and Silva, Alexandra and Staton, Sam}, acronym = {{MFPS}'14}, booktitle = {{P}roceedings of the 30th {C}onference on {M}athematical {F}oundations of {P}rogramming {S}emantics ({MFPS}'14)}, author = {Jaziri, Samy and Larsen, Kim G. and Mardare, Radu and Xue, Bingtian}, title = {Adequacy and Complete Axiomatization for Timed Modal Logic}, pages = {183-210}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/JLMX-mfps14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JLMX-mfps14.pdf}, doi = {10.1016/j.entcs.2014.10.011}, abstract = {In this paper we develop the metatheory for Timed Modal Logic~(TML), which is the modal logic used for the analysis of timed transition systems~(TTSs). We solve a series of long-standing open problems related to~TML. Firstly, we prove that TML enjoys the Hennessy-Milner property and solve one of the open questions in the field. Secondly, we prove that the set of validities are not recursively enumerable. Nevertheless, we develop a strongly-complete proof system for~TML. Since the logic is not compact, the proof system contains infinitary rules, but only with countable sets of instances. Thus, we~can involve topological results regarding Stone spaces, such as the Rasiowa-Sikorski lemma, to complete the proofs.} }

@article{CDGH-ic15, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Chatterjee, Krishnendu and Doyen, Laurent and Gimbert, Hugo and Henzinger, Thomas A.}, title = {Randomness for free}, volume = {245}, month = dec, year = 2015, pages = {3-16}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDGH-ic15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDGH-ic15.pdf}, doi = {10.1016/j.ic.2015.06.003}, abstract = {We consider two-player zero-sum games on finite-state graphs. These games can be classified on the basis of the information of the players and on the mode of interaction between them. On the basis of information the classification is as follows: (a)~partial-observation (both players have partial view of the game); (b)~one-sided complete-observation (one player has complete observation); and (c)~complete-observation (both players have complete view of the game). On~the basis of mode of interaction we have the following classification: (a)~concurrent (players interact simultaneously); and (b)~turn-based (players interact in turn). The~two sources of randomness in these games are randomness in the transition function and randomness in the strategies. In general, randomized strategies are more powerful than deterministic strategies, and probabilistic transitions give more general classes of games. We present a complete characterization for the classes of games where randomness is not helpful~in: (a)~the transition function (probabilistic transitions can be simulated by deterministic transitions); and (b)~strategies (pure strategies are as powerful as randomized strategies). As~a consequence of our characterization we obtain new undecidability results for these games.} }

@article{LM-ic14, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas}, title = {Augmenting {ATL} with strategy contexts}, volume = {245}, month = dec, year = 2015, pages = {98-123}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2014-05.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/rr-lsv-2014-05.pdf}, doi = {10.1016/j.ic.2014.12.020}, abstract = {We study the extension of the alternating-time temporal logic (ATL) with strategy contexts: contrary to the original semantics, in this semantics the strategy quantifiers do not reset the previously selected strategies.\par We show that our extension ATLsc is very expressive, but that its decision problems are quite hard: model checking is \(k\)-EXPTIME-complete when the formula has k nested strategy quantifiers; satisfiability is undecidable, but we prove that it is decidable when restricting to turn-based games. Our algorithms are obtained through a very convenient translation to QCTL (the~computation-tree logic CTL extended with atomic quantification), which we show also applies to Strategy Logic, as well as when strategy quantification ranges over memoryless strategies.} }

@inproceedings{DJLMS-fsttcs14, address = {New~Dehli, India}, month = dec, year = 2014, volume = {29}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Raman, Venkatesh and Suresh, S.~P.}, acronym = {{FSTTCS}'14}, 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)}, author = {Doyen, Laurent and Juhl, Line and Larsen, Kim G. and Markey, Nicolas and Shirmohammadi, Mahsa}, title = {Synchronizing words for weighted and timed automata}, pages = {121-132}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DJLMS-fsttcs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DJLMS-fsttcs14.pdf}, 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 of 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.} }

@inproceedings{BMS-fsttcs14, address = {New~Dehli, India}, month = dec, year = 2014, volume = {29}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Raman, Venkatesh and Suresh, S.~P.}, acronym = {{FSTTCS}'14}, 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)}, author = {Bouyer, Patricia and Markey, Nicolas and Stan, Daniel}, title = {Mixed {N}ash Equilibria in Concurrent Games}, pages = {351-363}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-fsttcs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-fsttcs14.pdf}, 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.} }

@article{BBBMBGJ-lmcs14, journal = {Logical Methods in Computer Science}, author = {Bertrand, Nathalie and Bouyer, Patricia and Brihaye, {\relax Th}omas and Menet, Quentin and Baier, Christel and Gr{\"o}{\ss}er, Marcus and Jurdzi{\'n}ski, Marcin}, title = {Stochastic Timed Automata}, volume = 10, number = {4:6}, nopages = {}, month = dec, year = 2014, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBMBGJ-mfcs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBMBGJ-mfcs14.pdf}, doi = {10.2168/LMCS-10(4:6)2014}, abstract = {A~stochastic timed automaton is a purely stochastic process defined on a timed automaton, in which both delays and discrete choices are made randomly. We study the almost-sure model-checking problem for this model, that is, given a stochastic timed automaton~\(\mathcal{A}\) and a property~\(\varphi\), we want to decide whether \(\mathcal{A}\) satisfies~\(\varphi\) with probability~\(1\). In this paper, we identify several classes of automata and of properties for which this can be decided. The proof relies on the construction of a finite abstraction, called the thick graph, that we interpret as a finite Markov chain, and for which we can decide the almost-sure model-checking problem. Correctness of the abstraction holds when automata are almost-surely fair, which we show, is the case for two large classes of systems, single-clock automata and so-called weak-reactive automata. Techniques employed in this article gather tools from real-time verification and probabilistic verification, as well as topological games played on timed automata.} }

@article{BMS-tcs14, publisher = {Elsevier Science Publishers}, journal = {Theoretical Computer Science}, author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan}, title = {Robust Reachability in Timed Automata and Games: A~Game-based Approach}, volume = 563, year = {2015}, month = jan, pages = {43-74}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-tcs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-tcs14.pdf}, doi = {10.1016/j.tcs.2014.08.014 }, abstract = {Reachability checking is one of the most basic problems in verification. By solving this problem in a game, one can synthesize a strategy that dictates the actions to be performed for ensuring that the target location is reached. In this work, we are interested in synthesizing {"}robust{"} strategies for ensuring reachability of a location in timed automata. By robust, we mean that it must still ensure reachability even when the delays are perturbed by the environment. We model this perturbed semantics as a game between the controller and its environment, and solve the parameterized robust reachability problem: we show that the existence of an upper bound on the perturbations under which there is a strategy reaching a target location is EXPTIME-complete. We also extend our algorithm, with the same complexity, to turn-based timed games, where the successor state is entirely determined by the environment in some locations.} }

@article{FKS-fmsd14, publisher = {Springer}, journal = {Formal Methods in System Design}, author = {Fribourg, Laurent and K{\"u}hne, Ulrich and Soulat, Romain}, title = {Finite Controlled Invariants for Sampled Switched Systems}, year = 2014, month = dec, volume = 45, number = 3, pages = {303-329}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FKS-fmsd14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FKS-fmsd14.pdf}, doi = {10.1007/s10703-014-0211-2}, abstract = {We consider in this paper switched systems, a class of hybrid systems recently used with success in various domains such as automotive industry and power electronics. We propose a state-dependent control strategy which makes the trajectories of the analyzed system converge to finite cyclic sequences of points. Our method relies on a technique of decomposition of the state space into local regions where the control is uniform. We have implemented the procedure using zonotopes, and applied it successfully to several examples of the literature and industrial case studies in power electronics.} }

@inproceedings{SLAF-syncop14, address = {Grenoble, France}, volume = 145, series = {Electronic Proceedings in Theoretical Computer Science}, month = apr, year = 2014, editor = {Andr{\'e}, {\'E}tienne and Frehse, Goran}, acronym = {{SYNCOP}'14}, booktitle = {{P}roceedings of the 1st {I}nternational {W}orkshop on {S}ynthesis of {C}ontinuous {P}arameters ({SYNCOP}'14)}, author = {Sun, Youcheng and Lipari, Giuseppe and Andr{\'e}, {\'E}tienne and Fribourg, Laurent}, title = {Toward Parametric Timed Interfaces for Real-Time Components}, pages = {49-64}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/SLAF-syncop14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SLAF-syncop14.pdf}, doi = {10.4204/EPTCS.145.6}, abstract = {We propose here a framework to model real-time components consisting of concurrent real-time tasks running on a single processor, using parametric timed automata. Our framework is generic and modular, so as to be easily adapted to different schedulers and more complex task models. We first perform a parametric schedulability analysis of the components using the inverse method. We show that the method unfortunately does not provide satisfactory results when the task periods are considered as parameters. After identifying and explaining the problem, we present a solution adapting the model by making use of the worst-case scenario in schedulability analysis. We show that the analysis with the inverse method always converges on the modified model when the system load is strictly less than~\(100\%\). Finally, we show how to use our parametric analysis for the generation of timed interfaces in compositional system design.} }

@inproceedings{BGM-atva14, address = {Sydney, Australia}, month = nov, year = {2014}, volume = 8837, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Cassez, Franck and Raskin, Jean-Fran{\c{c}}ois}, acronym = {{ATVA}'14}, booktitle = {{P}roceedings of the 12th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'14)}, author = {Bouyer, Patricia and Gardy, Patrick and Markey, Nicolas}, title = {Quantitative verification of weighted {K}ripke structures}, pages = {64-80}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-atva14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-atva14.pdf}, 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.} }

@inproceedings{MV-atva14, address = {Sydney, Australia}, month = nov, year = {2014}, volume = 8837, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Cassez, Franck and Raskin, Jean-Fran{\c{c}}ois}, acronym = {{ATVA}'14}, booktitle = {{P}roceedings of the 12th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'14)}, author = {Markey, Nicolas and Vester, Steen}, title = {Symmetry Reduction in Infinite Games with Finite Branching}, pages = {281-296}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/MV-atva14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/MV-atva14.pdf}, 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{*}.} }

@inproceedings{DMS-concur14, address = {Rome, Italy}, month = sep, year = 2014, volume = 8704, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Baldan, Paolo and Gorla, Daniele}, acronym = {{CONCUR}'14}, booktitle = {{P}roceedings of the 25th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'14)}, author = {Doyen, Laurent and Massart, {\relax Th}ierry and Shirmohammadi, Mahsa}, title = {Robust Synchronization in {M}arkov Decision Processes}, pages = {234-248}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DMS-concur14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DMS-concur14.pdf}, doi = {10.1007/978-3-662-44584-6_17}, abstract = {We consider synchronizing properties of Markov decision processes (MDP), viewed as generators of sequences of probability distributions over states. A~probability distribution is \(p\)-synchronizing if the probability mass is at least~\(p\) in some state, and a sequence of probability distributions is weakly \(p\)-synchronizing, or strongly \(p\)-synchronizing if respectively infinitely many, or all but finitely many distributions in the sequence are \(p\)-synchronizing.\par For each synchronizing mode, an MDP can be \textit{(i)}~sure winning if there is a strategy that produces a \(1\)-synchronizing sequence; \textit{(ii)}~almost-sure winning if there is a strategy that produces a sequence that is, for all \(\epsilon>0\), a \((1-\epsilon)\)-synchronizing sequence; \textit{(iii)}~limit-sure winning if for all \(\epsilon>0\), there is a strategy that produces a \((1-\epsilon)\)-synchronizing sequence.\par For each synchronizing and winning mode, we consider the problem of deciding whether an MDP is winning, and we establish matching upper and lower complexity bounds of the problems, as well as the optimal memory requirement for winning strategies: \textit{(a)}~for all winning modes, we show that the problems are PSPACE-complete for weakly synchronizing, and PTIME-complete for strongly synchronizing; \textit{(b)}~we~show that for weakly synchronizing, exponential memory is sufficient and may be necessary for sure winning, and infinite memory is necessary for almost-sure winning; for strongly synchronizing, linear-size memory is sufficient and may be necessary in all modes; \textit{(c)}~we~show a robustness result that the almost-sure and limit-sure winning modes coincide for both weakly and strongly synchronizing.} }

@inproceedings{BMM-concur14, address = {Rome, Italy}, month = sep, year = 2014, volume = 8704, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Baldan, Paolo and Gorla, Daniele}, acronym = {{CONCUR}'14}, booktitle = {{P}roceedings of the 25th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'14)}, author = {Bouyer, Patricia and Markey, Nicolas and Matteplackel, Raj~Mohan}, title = {Averaging in~{LTL}}, pages = {266-280}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMM-concur14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMM-concur14.pdf}, 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.} }

@article{BBMU-lmcs14, journal = {Logical Methods in Computer Science}, author = {Bouyer, Patricia and Brenguier, Romain and Markey, Nicolas and Ummels, Michael}, title = {Pure {N}ash Equilibria in Concurrent Games}, volume = {11}, number = {2:9}, nopages = {}, month = jun, year = 2015, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBMU-lmcs15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBMU-lmcs15.pdf}, doi = {10.2168/LMCS-11(2:9)2015}, abstract = {We study pure-strategy Nash equilibria in multiplayer concurrent games, for a variety of omega-regular objectives. For simple objectives (e.g. reachability, B{\"u}chi objectives), we transform the problem of deciding the existence of a Nash equilibrium in a given concurrent game into that of deciding the existence of a winning strategy in a turn-based two-player game (with a refined objective). We use that transformation to design algorithms for computing Nash equilibria, which in most cases have optimal worst-case complexity. For automata-defined objectives, we extend the above algorithms using a simulation relation which allows us to consider the product of the game with the automata defining the objectives. Building on previous algorithms for simple qualitative objectives, we define and study a semi-quantitative framework, where all players have several boolean objectives equipped with a preorder; a player may for instance want to satisfy all her objectives, or to maximise the number of objectives that she achieves. In most cases, we prove that the algorithms we obtain match the complexity of the problem they address.} }

@article{LM-lmcs14, journal = {Logical Methods in Computer Science}, author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas}, title = {Quantified {CTL}: Expressiveness and Complexity}, volume = 10, number = {4:17}, nopages = {}, month = dec, year = 2014, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LM-lmcs14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LM-lmcs14.pdf}, 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).} }

@phdthesis{mahsa-phd2014, author = {Shirmohammadi, Mahsa}, title = {Qualitative Analysis of Synchronizing Probabilistic Systems}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France and Universit\'e Libre de Bruxelles, Belgium}, type = {Th{\`e}se de doctorat}, year = 2014, month = dec, url = {http://www.lsv.fr/Publis/PAPERS/PDF/mahsa-phd14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/mahsa-phd14.pdf} }

@misc{cassting-D13, author = {Markey, Nicolas and Doyen, Laurent and Berwanger, Dietmar}, title = {Models for large-scale systems}, howpublished = {Cassting deliverable~D1.3 (FP7-ICT-601148)}, month = sep, year = {2015}, note = {17~pages}, type = {Contract Report}, url = {http://www.cassting-project.eu/wp-content/uploads/deliv-13.pdf}, pdf = {http://www.cassting-project.eu/wp-content/uploads/deliv-13.pdf} }

@misc{cassting-D21, author = {Geeraerts, Gilles and Dehouck, Samuel and Markey, Nicolas and Larsen, Kim G.}, title = {Efficient algorithms for multi-player games with quantitative aspects}, howpublished = {Cassting deliverable~D2.1 (FP7-ICT-601148)}, month = mar, year = {2015}, note = {22~pages}, type = {Contract Report}, url = {http://www.cassting-project.eu/wp-content/uploads/deliv-21.pdf}, pdf = {http://www.cassting-project.eu/wp-content/uploads/deliv-21.pdf} }

@misc{cassting-D63, author = {Markey, Nicolas and Delaborde, Arthur}, title = {Annual report for Year~2}, howpublished = {Cassting deliverable~D6.3 (FP7-ICT-601148)}, month = may, year = {2015}, note = {34~pages}, type = {Contract Report}, nourlnote = {confidentiel} }

@article{BGM-ipl15, publisher = {Elsevier Science Publishers}, journal = {Information Processing Letters}, author = {Bouyer, Patricia and Gardy, Patrick and Markey, Nicolas}, title = {On~the semantics of Strategy Logic}, volume = {116}, number = {2}, pages = {75-79}, month = feb, year = {2016}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-ipl15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-ipl15.pdf}, 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.} }

@inproceedings{BV-fsttcs15, address = {Bangalore, India}, month = dec, year = 2015, volume = {45}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Harsha, Prahladh and Ramalingam, G.}, acronym = {{FSTTCS}'15}, booktitle = {{P}roceedings of the 35th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'15)}, author = {Berwanger, Dietmar and Van{ }den{ }Bogaard, Marie}, title = {Games with Delays. A~{F}rankenstein Approach}, pages = {307-319}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BV-fsttcs15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BV-fsttcs15.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2015.307}, abstract = {We investigate infinite games on finite graphs where the information flow is perturbed by non-deterministic signalling delays. It is known that such perturbations make synthesis problems virtually unsolvable, in the general case. On the classical model where signals are attached to states, tractable cases are rare and difficult to identify. In this paper, we propose a model where signals are detached from control states, and we identify a subclass on which equilibrium outcomes can be preserved, even if signals are delivered with a delay that is finitely bounded. To offset the perturbation, our solution procedure combines responses from a collection of virtual plays following an equilibrium strategy in the instant-signalling game to synthesise, in a Dr.~Frankenstein manner, an equivalent equilibrium strategy for the delayed-signalling game.} }

@inproceedings{BGM-fsttcs15, address = {Bangalore, India}, month = dec, year = 2015, volume = {45}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Harsha, Prahladh and Ramalingam, G.}, acronym = {{FSTTCS}'15}, booktitle = {{P}roceedings of the 35th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'15)}, author = {Bouyer, Patricia and Gardy, Patrick and Markey, Nicolas}, title = {Weighted strategy logic with boolean goals over one-counter games}, pages = {69-83}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-fsttcs15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGM-fsttcs15.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2015.69}, abstract = {Strategy Logic is a powerful specification language for expressing non-zero-sum properties of multi-player games. SL conveniently extends the logic ATL with explicit quantification and assignment of strategies. In this paper, we consider games over one-counter automata, and a quantitative extension 1cSL of SL with assertions over the value of the counter. We prove two results: we first show that, if decidable, model checking the so-called Boolean-goal fragment of 1cSL has non-elementary complexity; we actually prove the result for the Boolean-goal fragment of SL over finite-state games, which was an open question in (Mogavero \emph{et~al.} Reasoning about strategies: On the model-checking problem. 2014). As a first step towards proving decidability, we then show that the Boolean-goal fragment of 1cSL over one-counter games enjoys a nice periodicity property.} }

@inproceedings{ncma2015-bou, address = {Porto, Portugal}, month = aug, year = 2015, volume = 318, series = {books@ocg.at}, publisher = {Austrian Computer Society}, editor = {Freund, Rudolf and Holzer, Markus and Moreira, Nelma and Reis, Rog{\'e}rio}, acronym = {{NCMA}'15}, booktitle = {{P}roceedings of the 7th {W}orkshop on {N}on-{C}lassical {M}odels of {A}utomata and {A}pplications ({NCMA}'15)}, author = {Bouyer, Patricia}, title = {On the optimal reachability problem in weighted timed automata and games}, pages = {11-36}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ncma15-bou.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ncma15-bou.pdf}, abstract = {In these notes, we survey works made on the models of weighted timed automata and games, and more specifically on the optimal reachability problem.} }

@phdthesis{reichert-phd15, author = {Reichert, Julien}, title = {D{\'e}cidabilit{\'e} et complexit{\'e} de jeux d'accessibilit{\'e} sur des syst{\`e}mes {\`a} compteurs}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2015, month = jul, url = {http://www.lsv.fr/Publis/PAPERS/PDF/reichert-phd15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/reichert-phd15.pdf} }

@inproceedings{FGMMP-rp15, address = {Warsaw, Poland}, month = sep, year = 2015, volume = {9328}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Boja{\'n}czyk, Miko{\l}aj and Lasota, S{\l}awomir and Potapov, Igor}, acronym = {{RP}'15}, booktitle = {{P}roceedings of the 9th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'15)}, author = {Fribourg, Laurent and Goubault, {\'E}ric and Mohamed, Sameh and Mrozek, Marian and Putot, Sylvie}, title = {A~Topological Method for Finding Invariants of Continuous Systems}, pages = {63-75}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FGMMP-rp15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FGMMP-rp15.pdf}, doi = {10.1007/978-3-319-24537-9_7}, abstract = {A~usual way to find positive invariant sets of ordinary differential equations is to restrict the search to predefined finitely generated shapes, such as linear templates, or ellipsoids as in classical quadratic Lyapunov function based approaches. One then looks for generators or parameters for which the corresponding shape has the property that the flow of the ODE goes inwards on its border. But for non-linear systems, where the structure of invariant sets may be very complicated, such simple predefined shapes are generally not well suited. The present work proposes a more general approach based on a topological property, namely Wa\.{z}ewski's property. Even for complicated non-linear dynamics, it is possible to successfully restrict the search for isolating blocks of simple shapes, that are bound to contain non-empty invariant sets. This approach generalizes the Lyapunov-like approaches, by allowing for inwards and outwards flow on the boundary of these shapes, with extra topological conditions. We developed and implemented an algorithm based on Wa\.{z}ewski's property, SOS optimization and some extra combinatorial and algebraic properties, that shows very nice results on a number of classical polynomial dynamical systems.} }

@inproceedings{BFM-avocs15, address = {Edinburgh, UK}, month = sep, year = {2015}, volume = 72, series = {Electronic Communications of the EASST}, publisher = {European Association of Software Science and Technology}, editor = {Grov, Gudmund and Ireland, Andrew}, acronym = {{AVoCS}'15}, booktitle = {{P}roceedings of the 15th {I}nternational {W}orkshop on {A}utomated {V}erification of {C}ritical {S}ystems ({AVoCS}'15)}, author = {Bouyer, Patricia and Fang, Erwin and Markey, Nicolas}, title = {Permissive strategies in timed automata and games}, nopages = {263-277}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFM-avocs15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFM-avocs15.pdf}, doi = {10.14279/tuj.eceasst.72.1015}, abstract = {Timed automata are a convenient framework for modelling and reasoning about real-time systems. While these models are now very well-understood, they do not offer a convenient way of taking timing imprecisions into account. Several solutions (e.g. parametric guard enlargement) have recently been proposed over the last ten years to take such imprecisions into account. In this paper, we propose a new approach for handling robust reachability, based on permissive strategies. While classical strategies propose to play an action at an exact point in time, permissive strategies return an interval of possible dates when to play the selected action. With such a permissive strategy, we associate a penalty, which is the inverse of the length of the proposed interval, and accumulates along the run. We show that in that setting, optimal strategies can be computed in polynomial time for one-clock timed automata.} }

@inproceedings{BMRLL-gandalf15, address = {Genova, Italy}, month = sep, year = 2015, volume = {193}, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Esparza, Javier and Tronci, Enrico}, acronym = {{GandALF}'15}, booktitle = {{P}roceedings of the 6th {I}nternational {S}ymposium on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification ({GandALF}'15)}, author = {Bouyer, Patricia and Markey, Nicolas and Randour, Mickael and Larsen, Kim G. and Laursen, Simon}, title = {Average-energy games}, pages = {1-15}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMRLL-gandalf15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMRLL-gandalf15.pdf}, doi = {10.4204/EPTCS.193.1}, abstract = {Two-player quantitative zero-sum games provide a natural framework to synthesize controllers with performance guarantees for reactive systems within an uncontrollable environment. Classical settings include mean-payoff games, where the objective is to optimize the long-run average gain per action, and energy games, where the system has to avoid running out of energy.\par We study \emph{average-energy} games, where the goal is to optimize the long-run average of the accumulated energy. We show that this objective arises naturally in several applications, and that it yields interesting connections with previous concepts in the literature. We prove that deciding the winner in such games is in \textsf{NP}{{\(\cap\)}}\textsf{coNP} and at least as hard as solving mean-payoff games, and we establish that memoryless strategies suffice to win. We also consider the case where the system has to minimize the average-energy while maintaining the accumulated energy within predefined bounds at all times: this corresponds to operating with a finite-capacity storage for energy. We give results for one-player and two-player games, and establish complexity bounds and memory requirements.} }

@inproceedings{LMS-gandalf15, address = {Genova, Italy}, month = sep, year = 2015, volume = {193}, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Esparza, Javier and Tronci, Enrico}, acronym = {{GandALF}'15}, booktitle = {{P}roceedings of the 6th {I}nternational {S}ymposium on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification ({GandALF}'15)}, author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas and Sangnier, Arnaud}, title = {{{\(\textsf{ATL}_{\textsf{sc}}\)}} with partial observation}, pages = {43-57}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LMS-gandalf15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LMS-gandalf15.pdf}, doi = {10.4204/EPTCS.193.4}, abstract = {Alternating-time temporal logic with strategy contexts ({{\(\textsf{ATL}_{\textsf{sc}}\)}}) is a powerful formalism for expressing properties of multi-agent systems: it~extends \textsf{CTL} with \emph{strategy quantifiers}, offering a convenient way of expressing both collaboration and antagonism between several agents. Incomplete observation of the state space is a desirable feature in such a framework, but it quickly leads to undecidable verification problems. In this paper, we prove that \emph{uniform} incomplete observation (where all players have the same observation) preserves decidability of the model checking problem, even for very expressive logics such as {{\(\textsf{ATL}_{\textsf{sc}}\)}}.} }

@inproceedings{BV-dlt15, address = {Liverpool, UK}, month = jul, year = 2015, volume = {9168}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Potapov, Igor}, acronym = {{DLT}'15}, booktitle = {{P}roceedings of the 19th {I}nternational {C}onference on {D}evelopments in {L}anguage {T}heory ({DLT}'15)}, author = {Berwanger, Dietmar and Van{ }den{ }Bogaard, Marie}, title = {Consensus Game Acceptors}, pages = {108-119}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BV-dlt15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BV-dlt15.pdf}, doi = {10.1007/978-3-319-21500-6_8}, abstract = {We study a game for recognising formal languages, in which two players with imperfect information need to coordinate on a common decision, given private input strings correlated by a finite graph. The players have a joint objective to avoid an inadmissible decision, in spite of the uncertainty induced by the input.\par We show that the acceptor model based on consensus games characterises context-sensitive languages, and conversely, that winning strategies in such games can be described by context-sensitive languages. We also discuss consensus game acceptors with a restricted observation pattern that describe nondeterministic linear-time languages.} }

@inproceedings{BMV-atva15, address = {Shanghai, China}, month = oct, year = {2015}, volume = {9364}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Finkbeiner, Bernd and Pu, Geguang and Zhang, Lijun}, acronym = {{ATVA}'15}, booktitle = {{P}roceedings of the 13th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'15)}, author = {Berwanger, Dietmar and Mathew, Anup Basil and Van{ }den{ }Bogaard, Marie}, title = {Hierarchical Information Patterns and Distributed Strategy Synthesis}, pages = {378-393}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMV-atva15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMV-atva15.pdf}, doi = {10.1007/978-3-319-24953-7_28}, abstract = {Infinite games with imperfect information tend to be undecidable unless the information flow is severely restricted. One fundamental decidable case occurs when there is a total ordering among players, such that each player has access to all the information that the following ones receive.\par In this paper we consider variations of this hierarchy principle for synchronous games with perfect recall, and identify new decidable classes for which the distributed synthesis problem is solvable with finite-state strategies. In particular, we show that decidability is maintained when the information hierarchy may change along the play, or when transient phases without hierarchical information are allowed.} }

@article{CLMT-dagstuhl15, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, journal = {Dagstuhl Reports}, editor = {Chatterjee, Krishnendu and Lafortune, St{\'e}phane and Markey, Nicolas and Thomas, Wolfgang}, author = {Chatterjee, Krishnendu and Lafortune, St{\'e}phane and Markey, Nicolas and Thomas, Wolfgang}, title = {Non-Zero-Sum-Games and Control ({D}agstuhl Seminar~15061)}, pages = {1-25}, year = {2015}, volume = {5}, number = {2}, month = jun, url = {http://drops.dagstuhl.de/opus/volltexte/2015/5042}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CLMT-dagstuhl15.pdf}, doi = {10.4230/DagRep.5.2.1}, abstract = {In this report, the program, research issues, and results of Dagstuhl Seminar 15061 {"}Non-Zero-Sum-Games and Control{"} are described. The area of non-zero-sum games is addressed in a wide range of topics: multi-player games, partial-observation games, quantitative game models, and---as~a special focus---connections with control engineering (supervisory control).} }

@inproceedings{BMPS-formats15, address = {Madrid, Spain}, month = sep, year = 2015, volume = {9268}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Sankaranarayanan, Sriram and Vicario, Enrico}, acronym = {{FORMATS}'15}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'15)}, author = {Bouyer, Patricia and Markey, Nicolas and Perrin, Nicolas and Schlehuber, Philipp}, title = {Timed automata abstraction of switched dynamical systems using control funnels}, pages = {60-75}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMPS-formats15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMPS-formats15.pdf}, doi = {10.1007/978-3-319-22975-1_5}, abstract = {The~development of formal methods for control design is an important challenge with potential applications in a wide range of safety-critical cyber-physical systems. Focusing on switched dynamical systems, we~propose a new abstraction, based on time-varying regions of invariance (the~\emph{control funnels}), that models behaviors of systems as timed automata. The main advantage of this method is that it allows automated verification of formal specifications and reactive controller synthesis without discretizing the evolution of the state of the system. Efficient constructions are possible in the case of linear dynamics. We~demonstrate the potential of our approach with two examples.} }

@inproceedings{AM-formats15, address = {Madrid, Spain}, month = sep, year = 2015, volume = {9268}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Sankaranarayanan, Sriram and Vicario, Enrico}, acronym = {{FORMATS}'15}, booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'15)}, author = {Andr{\'e}, {\'E}tienne and Markey, Nicolas}, title = {Language Preservation Problems in Parametric Timed Automata}, pages = {27-43}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AM-formats15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AM-formats15.pdf}, doi = {10.1007/978-3-319-22975-1_3}, abstract = {Parametric timed automata (PTA) are a powerful formalism to model and reason about concurrent systems with some unknown timing delays. In this paper, we address the (untimed) language- and trace-preservation problems: given a reference parameter valuation, does there exist another parameter valuation with the same untimed language (or trace)? We show that these problems are undecidable both for general PTA, and even for the restricted class of L/U-PTA. On the other hand, we exhibit decidable subclasses: 1-clock PTA, and 1-parameter deterministic L-PTA and U-PTA.} }

@inproceedings{BJM-concur15, address = {Madrid, Spain}, month = sep, year = 2015, volume = {42}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Aceto, Luca and de Frutos-Escrig, David}, acronym = {{CONCUR}'15}, booktitle = {{P}roceedings of the 26th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'15)}, author = {Bouyer, Patricia and Jaziri, Samy and Markey, Nicolas}, title = {On~the Value Problem in Weighted Timed Games}, pages = {311-324}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BJM-concur15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BJM-concur15.pdf}, doi = {10.4230/LIPIcs.CONCUR.2015.311}, abstract = {A~weighted timed game is a timed game with extra quantitative information representing e.g. energy consumption. Optimizing the cost for reaching a target is a natural question, which has been investigated for ten years. Existence of optimal strategies is known to be undecidable in general, and only very restricted classes of games have been described for which optimal cost and almost-optimal strategies can be computed.\par In this paper, we show that the value problem is undecidable in general weighted timed games. The undecidability proof relies on that for the existence of optimal strategies and on a diagonalization construction recently designed in the context of quantitative temporal logics. We then provide an algorithm to compute arbitrary approximations of the value in a game, and almost-optimal strategies. The algorithm applies in a large subclass of weighted timed games, and is the first approximation scheme which is designed in the current context.} }

@inproceedings{CDV-icalp15, address = {Kyoto, Japan}, month = jul, year = 2015, volume = {9135}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Halld{\'o}rsson, Magnus M. and Iwama, Kazuo and Kobayashi, Naoki and Speckmann, Bettina}, acronym = {{ICALP}'15}, booktitle = {{P}roceedings of the 42nd {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'15)~-- {P}art~{II}}, author = {Chatterjee, Krishnendu and Doyen, Laurent and Vardi, Moshe}, title = {The Complexity of Synthesis from Probabilistic Components}, pages = {108-120}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDV-icalp15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDV-icalp15.pdf}, doi = {10.1007/978-3-662-47666-6_9}, abstract = {The synthesis problem asks for the automatic construction of a system from its specification. In the traditional setting, the system is {"}constructed from scratch{"} rather than composed from reusable components. However, this is rare in practice, and almost every non-trivial software system relies heavily on the use of libraries of reusable components. Recently, Lustig and Vardi introduced dataflow and controlflow synthesis from libraries of reusable components. They proved that dataflow synthesis is undecidable, while controlflow synthesis is decidable. The problem of controlflow synthesis from libraries of probabilistic components was considered by Nain, Lustig and Vardi, and was shown to be decidable for qualitative analysis (that asks that the specification be satisfied with probability~1). Our main contribution for controlflow synthesis from probabilistic components is to establish better complexity bounds for the qualitative analysis problem, and to show that the more general quantitative problem is undecidable. For the qualitative analysis, we show that the problem (i)~is EXPTIME-complete when the specification is given as a deterministic parity word automaton, improving the previously known 2EXPTIME upper bound; and (ii)~belongs to UP\(\cap\)coUP and is parity-games hard, when the specification is given directly as a parity condition on the components, improving the previously known EXPTIME upper bound.} }

@article{BFRR-ic15, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Bruy{\`e}re, V{\'e}ronique and Filiot, Emmanuel and Randour, Mickael and Raskin, Jean-Fran{\c{c}}ois}, title = {Meet Your Expectations With Guarantees: Beyond Worst-Case Synthesis in Quantitative Games}, volume = {254}, number = {2}, month = jun, year = 2017, pages = {259-295}, note = {To appear}, doi = {10.1016/j.ic.2016.10.011}, abstract = {Classical analysis of two-player quantitative games involves an adversary (modeling the environment of the system) which is purely antagonistic and asks for strict guarantees while Markov decision processes model systems facing a purely randomized environment: the aim is then to optimize the expected payoff, with no guarantee on individual outcomes. We introduce the beyond worst-case synthesis problem, which is to construct strategies that guarantee some quantitative requirement in the worst-case while providing a higher expected value against a particular stochastic model of the environment given as input. We study the beyond worst-case synthesis problem for two important quantitative settings: the mean-payoff and the shortest path. In both cases, we show how to decide the existence of finite-memory strategies satisfying the problem and how to synthesize one if one exists. We establish algorithms and we study complexity bounds and memory requirements.} }

@inproceedings{RRS-cav15, address = {San Francisco, CA, USA}, month = jul, year = 2015, volume = 9206, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Kroening, Daniel and Pasareanu, Corina}, acronym = {{CAV}'15}, booktitle = {{P}roceedings of the 27th {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'15)~-- Part~{I}}, author = {Randour, Mickael and Raskin, Jean-Fran{\c{c}}ois and Sankur, Ocan}, title = {Percentile Queries in Multi-Dimensional {M}arkov Decision Processes}, pages = {123-139}, url = {http://arxiv.org/abs/1410.4801}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RRS-arxiv14.pdf}, doi = {10.1007/978-3-319-21690-4_8}, abstract = {Multi-dimensional weighted Markov decision processes (MDPs) are useful to analyze systems with multiple objectives that are potentially conflicting and make necessary the analysis of trade-offs. In this paper, we study the complexity of percentile queries in such MDPs and provide algorithms to synthesize strategies that enforce such constraints. Given a multi-dimensional weighted MDP and a quantitative payoff function~\(f\), quantitative thresholds~\(v_i\) (one per dimension), and probability thresholds~\(\alpha_{i}\), we show how to compute a single strategy that enforces that for all dimension~\(i\), the probability that an outcome~\(\rho\) satisfies \(f_{i}(\rho) \geq v_{i}\) is at least~\(\alpha_{i}\). We study this problem for the classical quantitative payoffs studied in the literature (sup, inf, lim sup, lim inf, mean-payoff, truncated sum, discounted sum). So our work can be seen as an extension to the quantitative case of the multi-objective model checking problem on MDPs studied by Etessami et al. in unweighted MDPs.} }

@inproceedings{FKM-syncop15, address = {London, UK}, volume = 44, series = {Open Access Series in Informatics}, month = apr, year = 2015, editor = {Andr{\'e}, {\'E}tienne and Frehse, Goran}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, acronym = {{SYNCOP}'15}, booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {S}ynthesis of {C}ontinuous {P}arameters ({SYNCOP}'15)}, author = {Fribourg, Laurent and K{\"u}hne, Ulrich and Markey, Nicolas}, title = {Game-based Synthesis of Distributed Controllers for Sampled Switched Systems}, pages = {47-61}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FKM-syncop15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FKM-syncop15.pdf}, doi = {10.4230/OASIcs.SynCoP.2015.47}, 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.} }

@inproceedings{LDRCF-syncop15, address = {London, UK}, volume = 44, series = {Open Access Series in Informatics}, month = apr, year = 2015, editor = {Andr{\'e}, {\'E}tienne and Frehse, Goran}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, acronym = {{SYNCOP}'15}, booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {S}ynthesis of {C}ontinuous {P}arameters ({SYNCOP}'15)}, author = {Le{~}Co{\"e}nt, Adrien and De{~}Vuyst, Florian and Rey, {\relax Ch}ristian and Chamoin, Ludovic and Fribourg, Laurent}, title = {Guaranteed control of switched control systems using model order reduction and state-space bisection}, pages = {32-46}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LDCRF-syncop15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LDCRF-syncop15.pdf}, doi = {10.4230/OASIcs.SynCoP.2015.32}, abstract = {This paper considers discrete-time linear systems controlled by a quantized law, i.e., a piecewise constant time function taking a finite set of values. We show how to generate the control by, first, applying model reduction to the original system, then using a {"}state-space bisection{"} method for synthesizing a control at the reduced-order level, and finally computing an upper bound to the deviations between the controlled output trajectories of the reduced-order model and those of the original model. The effectiveness of our approach is illustrated on several examples of the literature.} }

@article{AFG-sif15, publisher = {SIF}, journal = {1024~-- Bulletin de la soci{\'e}t{\'e} informatique de France}, author = {Abiteboul, Serge and Fribourg, Laurent and Goubault{-}Larrecq, Jean}, title = {{G}{\'e}rard {B}erry~: un~informaticien m{\'e}daille d'or du {CNRS}~2014}, volume = 4, pages = {139-142}, month = oct, year = 2014, url = {http://www.lsv.fr/Publis/PAPERS/PDF/AFG-sif15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AFG-sif15.pdf}, abstract = {C'est un chercheur en informatique qui vient de recevoir la m{\'e}daille d'or du CNRS, la plus haute distinction scientifique fran{\c c}aise toutes disciplines confondues. Les informaticiens sont rares {\`a} avoir {\'e}t{\'e} ainsi honor{\'e}s : ce n'est que la seconde fois apr{\`e}s Jacques Stern en~2006.} }

@inproceedings{RRS-vmcai15, address = {Mumbai, India}, month = jan, year = 2015, volume = 8931, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {D'Souza, Deepak and Lal, Akash and Larsen, Kim Guldstrand}, acronym = {{VMCAI}'15}, booktitle = {{P}roceedings of the 16th {I}nternational {C}onference on {V}erification, {M}odel {C}hecking and {A}bstract {I}nterpretation ({VMCAI}'15)}, author = {Randour, Mickael and Raskin, Jean-Fran{\c{c}}ois and Sankur, Ocan}, title = {Variations on the Stochastic Shortest Path Problem}, pages = {1-18}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/RRS-vmcai15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RRS-vmcai15.pdf}, doi = {10.1007/978-3-662-46081-8_1}, abstract = {In this invited contribution, we revisit the stochastic shortest path problem, and show how recent results allow one to improve over the classical solutions: we present algorithms to synthesize strategies with multiple guarantees on the distribution of the length of paths reaching a given target, rather than simply minimizing its expected value. The concepts and algorithms that we propose here are applications of more general results that have been obtained recently for Markov decision processes and that are described in a series of recent papers.} }

@article{VCDHRR-icomp15, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Velner, Yaron and Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, Thomas A. and Rabinovich, Alexander Moshe and Raskin, Jean-Fran{\c{c}}ois}, title = {The complexity of multi-mean-payoff and multi-energy games}, year = 2015, month = apr, volume = 241, pages = {177-196}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDRR-icomp15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDRR-icomp15.pdf}, doi = {10.1016/j.ic.2015.03.001}, abstract = {In mean-payoff games, the objective of the protagonist is to ensure that the limit average of an infinite sequence of numeric weights is nonnegative. In energy games, the objective is to ensure that the running sum of weights is always nonnegative. Multi-mean-payoff and multi-energy games replace individual weights by tuples, and the limit average (resp., running sum) of each coordinate must be (resp.,~remain) nonnegative. We prove finite-memory determinacy of multi-energy games and show inter-reducibility of multi-mean-payoff and multi-energy games for finite-memory strategies. We improve the computational complexity for solving both classes with finite-memory strategies: we prove coNP-completeness improving the previous known \textsf{EXPSPACE} bound. For memoryless strategies, we show that deciding the existence of a winning strategy for the protagonist is NP-complete. We present the first solution of multi-mean-payoff games with infinite-memory strategies: we show that mean-payoff-sup objectives can be decided in \textsf{NP}{{\(\cap\)}}\textsf{coNP}, whereas mean-payoff-inf objectives are coNP-complete.} }

@article{CDRR-icomp15, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Chatterjee, Krishnendu and Doyen, Laurent and Randour, Mickael and Raskin, Jean-Fran{\c{c}}ois}, title = {Looking at Mean-Payoff and Total-Payoff through Windows}, year = 2015, month = jun, volume = 242, pages = {25-52}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/CDRR-icomp15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDRR-icomp15.pdf}, doi = {10.1016/j.ic.2015.03.010}, abstract = {We consider two-player games played on weighted directed graphs with mean-payoff and total-payoff objectives, two classical quantitative objectives. While for single-dimensional games the complexity and memory bounds for both objectives coincide, we show that in contrast to multi-dimensional mean-payoff games that are known to be coNP-complete, multi-dimensional total-payoff games are undecidable. We introduce conservative approximations of these objectives, where the payoff is considered over a local finite window sliding along a play, instead of the whole play. For single dimension, we show that (i)~if the window size is polynomial, deciding the winner takes polynomial time, and (ii)~the existence of a bounded window can be decided in \(\textsf{NP}\cap\textsf{coNP}\), and is at least as hard as solving mean-payoff games. For multiple dimensions, we show that (i)~the problem with fixed window size is EXPTIME-complete, and (ii)~there is no primitive-recursive algorithm to decide the existence of a bounded window.} }

@inproceedings{BJ-fossacs17, address = {Uppsala, Sweden}, month = apr, year = 2017, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Esparza, Javier and Murawski, Andrzej}, acronym = {{FoSSaCS}'17}, booktitle = {{P}roceedings of the 20th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'17)}, author = {Bouyer, Patricia and Jug{\'e}, Vincent}, title = {Dynamic Complexity of the {D}yck Reachability}, pages = {265-280}, url = {https://arxiv.org/abs/1610.07499}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BJ-fossacs17.pdf}, doi = {10.1007/978-3-662-54458-7_16}, abstract = {Dynamic complexity is concerned with updating the output of a problem when the input is slightly changed. We study the dynamic complexity of Dyck reachability problems in directed and undirected graphs, where updates may add or delete edges. We show a strong dichotomy between such problems, based on the size of the Dyck alphabet. Some of them are P-complete (under a strong notion of reduction) while the others lie either in DynFO or in NL.} }

@inproceedings{BHMRZ-fossacs17, address = {Uppsala, Sweden}, month = apr, year = 2017, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Esparza, Javier and Murawski, Andrzej}, acronym = {{FoSSaCS}'17}, booktitle = {{P}roceedings of the 20th {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'17)}, author = {Bouyer, Patricia and Hofman, Piotr and Markey, Nicolas and Randour, Mickael and Zimmermann, Martin}, title = {Bounding Average-energy Games}, pages = {179-195}, url = {https://arxiv.org/abs/1610.07858}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHMRZ-fossacs17.pdf}, doi = {10.1007/978-3-662-54458-7_11}, abstract = {We consider average-energy games, where the goal is to minimize the long-run average of the accumulated energy. Decidability of average-energy games with a lower-bound constraint on the energy level (but no upper bound) is an open problem; in particular, there is no known upper bound on the memory that is required for winning strategies. By reducing average-energy games with lower-bounded energy to infinite-state mean-payoff games and analyzing the frequency of low-energy configurations, we show an almost tight doubly-exponential upper bound on the necessary memory, and that the winner of average-energy games with lower-bounded energy can be determined in doubly-exponential time. We also prove EXPSPACE-hardness of this problem. Finally, we consider multi-dimensional extensions of all types of average-energy games: without bounds, with only a lower bound, and with both a lower and an upper bound on the energy. We show that the fully-bounded version is the only case to remain decidable in multiple dimensions.} }

@article{J-ijac16, publisher = {World Scientific}, journal = {International Journal of Algebra and Computation}, author = {Jug{\'e}, Vincent}, title = {The Relaxation Normal Form of Braids is Regular}, volume = {27}, number = {1}, year = {2017}, pages = {61-106}, month = feb, url = {https://arxiv.org/abs/1507.03248}, doi = {10.1142/S0218196717500059}, abstract = {Braids can be represented geometrically as laminations of punctured disks. The geometric complexity of a braid is the minimal complexity of a lamination that represents it, and tight laminations are representatives of minimal complexity. These laminations give rise to a normal form of braids, via a relaxation algorithm. We study here this relaxation algorithm and the associated normal form. We prove that this normal form is regular and prefix-closed. We provide an effective construction of a deterministic automaton that recognizes this normal form.} }

@phdthesis{mvdb-phd2016, author = {Van{ }den{ }Bogaard, Marie}, title = {Motifs de Flot d'Information dans les Jeux {\`a} Information Imparfaite}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2016, month = nov, url = {http://www.lsv.fr/Publis/PAPERS/PDF/mvdb-phd16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/mvdb-phd16.pdf} }

@article{BMPS-rts16, publisher = {Kluwer Academic Publishers}, journal = {Real-Time Systems}, author = {Bouyer, Patricia and Markey, Nicolas and Perrin, Nicolas and Schlehuber{-}Caissier, Philipp}, title = {Timed automata abstraction of switched dynamical systems using control funnels}, volume = {53}, number = {3}, year = {2017}, pages = {327-353}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMPS-rts16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMPS-rts16.pdf}, doi = {10.1007/s11241-016-9262-3}, abstract = {The development of formal methods for control design is an important challenge with potential applications in a wide range of safety-critical cyber-physical systems. Focusing on switched dynamical systems, we propose a new abstraction, based on time-varying regions of invariance (control funnels), that models behaviors of systems as timed automata. The~main advantage of this method is that it allows for the automated verification and reactive controller synthesis without discretizing the evolution of the state of the system. Efficient and analytic constructions are possible in the case of linear dynamics whereas bounding funnels with conjectured properties based on numerical simulations can be used for general nonlinear dynamics. We~demonstrate the potential of our approach with three examples.} }

@phdthesis{mohamed-PhD16, author = {Mohamed, Sameh}, title = {Une m{\'e}thode topologique pour la recherche d'ensembles invariants de syst{\`e}mes continus et {\`a} commutation}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = {2016}, month = oct, url = {http://www.lsv.fr/Publis/PAPERS/PDF/mohamed-phd16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/mohamed-phd16.pdf} }

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

@proceedings{BDJMS-casstingsyncop16, 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)}, 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}, editor = {Brihaye, {\relax Th}omas and Delahaye, Beno{\^\i}t and Jezequel, Lo{\"\i}g and Markey, Nicolas and Srba, Ji{\v{r}}{\'i}}, doi = {10.4204/EPTCS.220}, url = {http://eptcs.web.cse.unsw.edu.au/content.cgi?CASSTINGSynCoP2016}, series = {Electronic Proceedings in Theoretical Computer Science}, volume = 220, year = 2016, month = jul, address = {Eindhoven, The~Netherlands} }

@incollection{BFLMOW-hmc18, author = {Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim G. and Markey, Nicolas and Ouaknine, Jo{\"e}l and Worrell, James}, title = {Model Checking Real-Time Systems}, booktitle = {Handbook of Model Checking}, editor = {Clarke, Ed and Henzinger, Tom and Veith, Helmut}, publisher = {Springer}, year = 2018, pages = {1001-1046}, nochapter = {29}, doi = {10.1007/978-3-319-10575-8_29}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLMOW-hmc17.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BFLMOW-hmc17.pdf}, isbn = {978-3-319-10574-1}, abstract = {This chapter surveys timed automata as a formalism for model checking real-time systems. We begin with introducing the model, as an extension of finite-state automata with real-valued variables for measuring time. We then present the main model-checking results in this framework, and give a hint about some recent extensions (namely weighted timed automata and timed games).} }

@inproceedings{BMS-gandalf16, address = {Catania, Italy}, month = sep, year = 2016, volume = {226}, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Cantone, Domenico and Delzanno, Giorgio}, acronym = {{GandALF}'16}, booktitle = {{P}roceedings of the 7th {I}nternational {S}ymposium on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification ({GandALF}'16)}, author = {Bouyer, Patricia and Markey, Nicolas and Stan, Daniel}, title = {Stochastic Equilibria under Imprecise Deviations in Terminal-Reward Concurrent Games}, pages = {61-75}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-gandalf16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMS-gandalf16.pdf}, 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.} }

@inproceedings{LFS-rp16, address = {Aalborg, Denmark}, month = sep, year = 2016, volume = {9899}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Larsen, Kim G. and Srba, Ji{\v{r}}{\'\i}}, acronym = {{RP}'16}, booktitle = {{P}roceedings of the 10th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'16)}, author = {Le{~}Co{\"e}nt, Adrien and Fribourg, Laurent and Soulat, Romain}, title = {Compositional analysis of Boolean networks using local fixed-point iterations}, pages = {134-147}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LFS-rp16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LFS-rp16.pdf}, doi = {10.1007/978-3-319-45994-3_10}, abstract = {We present a compositional method which allows to over-approximate the set of attractors and under-approximate the set of basins of attraction of a Boolean network~(BN). This merely consists in replacing a global fixed-point computation by a composition of local fixed-point computations. Once these approximations have been computed, it~becomes much more tractable to generate the exact sets of attractors and basins of attraction. We illustrate the interest of our approach on several examples, among which is a BN modeling a railway interlocking system with 50 nodes and millions of attractors.} }

@inproceedings{LFMDC-rp16, address = {Aalborg, Denmark}, month = sep, year = 2016, volume = {9899}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Larsen, Kim G. and Srba, Ji{\v{r}}{\'\i}}, acronym = {{RP}'16}, booktitle = {{P}roceedings of the 10th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'16)}, 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}, pages = {119-133}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LFMDC-rp16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LFMDC-rp16.pdf}, 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.} }

@article{BMRLL-acta16, publisher = {Springer}, journal = {Acta Informatica}, author = {Bouyer, Patricia and Markey, Nicolas and Randour, Mickael and Larsen, Kim G. and Laursen, Simon}, title = {Average-energy games}, volume = {55}, number = {2}, year = 2018, month = jul, pages = {91-127}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMRLL-acta16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMRLL-acta16.pdf}, doi = {10.1007/s00236-016-0274-1}, abstract = {Two-player quantitative zero-sum games provide a natural framework to synthesize controllers with performance guarantees for reactive systems within an uncontrollable environment. Classical settings include mean-payoff games, where the objective is to optimize the long-run average gain per action, and energy games, where the system has to avoid running out of energy. We study average-energy games, where the goal is to optimize the long-run average of the accumulated energy. We show that this objective arises naturally in several applications, and that it yields interesting connections with previous concepts in the literature. We prove that deciding the winner in such games is in NP coNP and at least as hard as solving mean-payoff games, and we establish that memoryless strategies suffice to win. We also consider the case where the system has to minimize the average-energy while maintaining the accumulated energy within predefined bounds at all times: this corresponds to operating with a finite-capacity storage for energy. We give results for one-player and two-player games, and establish complexity bounds and memory requirements.} }

@inproceedings{Bouyer-mfcs16, address = {Krakow, Poland}, month = aug, year = 2016, volume = {58}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf}, acronym = {{MFCS}'16}, booktitle = {{P}roceedings of the 41st {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'16)}, author = {Bouyer, Patricia}, title = {Optimal Reachability in Weighted Timed Automata and Games}, pages = {3:1-3:3}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/bouyer-mfcs16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bouyer-mfcs16.pdf}, doi = {10.4230/LIPIcs.MFCS.2016.3}, abstract = {This is an overview of the invited talk delivered at the 41st International Symposium on Math- ematical Foundations of Computer Science (MFCS-2016).} }

@inproceedings{ABKMT-mfcs16, address = {Krakow, Poland}, month = aug, year = 2016, volume = {58}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf}, acronym = {{MFCS}'16}, booktitle = {{P}roceedings of the 41st {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'16)}, author = {Akshay, S. and Bouyer, Patricia and Krishna, Shankara Narayanan and Manasa, Lakshmi and Trivedi, Ashutosh }, title = {Stochastic Timed Games Revisited}, pages = {8:1-8:14}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABKMT-mfcs16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABKMT-mfcs16.pdf}, doi = {10.4230/LIPIcs.MFCS.2016.8}, abstract = {Stochastic timed games (STGs), introduced by Bouyer and Forejt, naturally generalize both continuous-time Markov chains and timed automata by providing a partition of the locations between those controlled by two players (Player Box and Player Diamond) with competing objectives and those governed by stochastic laws. Depending on the number of players---2,~1, or~0---subclasses of stochastic timed games are often classified as \(2\frac{1}{2}\)-player, \(1\frac{1}{2}\)-player, and \(\frac{1}{2}\)-player games where the \(\frac{1}{2}\) symbolizes the presence of the stochastic {"}nature{"} player. For STGs with reachability objectives it is known that \(1\frac{1}{2}\)-player one-clock STGs are decidable for qualitative objectives, and that \(2\frac{1}{2}\)-player three-clock STGs are undecidable for quantitative reachability objectives. This paper further refines the gap in this decidability spectrum. We show that quantitative reachability objectives are already undecidable for \(1\frac{1}{2}\)-player four-clock STGs, and even under the time-bounded restriction for \(2\frac{1}{2}\)-player five-clock~STGs. We~also obtain a class of \(1\frac{1}{2}\), \(2\frac{1}{2}\)-player STGs for which the quantitative reachability problem is decidable.} }

@inproceedings{NPR-mfcs16, address = {Krakow, Poland}, month = aug, year = 2016, volume = {58}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf}, acronym = {{MFCS}'16}, booktitle = {{P}roceedings of the 41st {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'16)}, author = {Reino Niskanen and Igor Potapov and Julien Reichert}, title = {Undecidability of Two-dimensional Robot Games}, pages = {73:1-73:13}, url = {http://arxiv.org/abs/1604.08779}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/NPR-mfcs16.pdf}, doi = {10.4230/LIPIcs.MFCS.2016.73}, abstract = {Robot game is a two-player vector addition game played on the integer lattice \(\mathbb{Z}^n\). Both players have sets of vectors and in each turn the vector chosen by a player is added to the current configuration vector of the game. One of the players, called Eve, tries to play the game from the initial configuration to the origin while the other player, Adam, tries to avoid the origin. The problem is to decide whether or not Eve has a winning strategy. In this paper we prove undecidability of the robot game in dimension two answering the question formulated by Doyen and Rabinovich in 2011 and closing the gap between undecidable and decidable cases.} }

@inproceedings{DLM-concur16, address = {Qu{\'e}bec City, Canada}, month = aug, year = 2016, volume = {59}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Desharnais, Jos{\'e}e and Jagadeesan, Radha}, acronym = {{CONCUR}'16}, booktitle = {{P}roceedings of the 27th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'16)}, author = {David, Am{\'e}lie and Laroussinie, Fran{\c{c}}ois and Markey, Nicolas}, title = {On~the expressiveness of~{QCTL}}, pages = {28:1-28:15}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/DLM-concur16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DLM-concur16.pdf}, 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).} }

@article{LDRCF-ijdc16, publisher = {Springer}, journal = {International Journal of Dynamics and Control}, author = {Le{~}Co{\"e}nt, Adrien and De{~}Vuyst, Florian and Rey, Christian and Chamoin, Ludovic and Fribourg, Laurent}, title = {Control of mechanical systems using set-based methods}, pages = {1-17}, year = 2016, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LDRCF-ijdc16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LDRCF-ijdc16.pdf}, doi = {10.1007/s40435-016-0245-y}, abstract = {This paper considers large discrete-time linear systems obtained from discretized partial differential equations, and controlled by a \emph{quantized} law, i.e., a piecewise constant time function taking a finite set of values. We show how to generate the control by, first, applying \emph{model reduction} to the original system, then using a {"}state-space bisection{"} method for synthesizing a control at the reduced-order level, and finally computing an upper bound on the deviations between the controlled output trajectories of the reduced-order model and those of the original model. The effectiveness of our approach is illustrated on several examples of the literature.} }

@inproceedings{LACF-snr16, address = {Vienna, Austria}, month = apr, year = 2016, publisher = {{IEEE} Computer Society Press}, acronym = {{SNR}'16}, booktitle = {{P}roceedings of the 2nd {I}nternational {W}orkshop on {S}ymbolic and {N}umerical {M}ethods for {R}eachability {A}nalysis ({SNR}'16)}, author = {Le{~}Co{\"e}nt, Adrien and Alexandre{ }dit{ }Sandretto, Julien and Chapoutot, Alexandre and Fribourg, Laurent}, title = {Control of Nonlinear Switched Systems Based on Validated Simulation}, pages = {1-6}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/LACF-snr16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LACF-snr16.pdf}, abstract = {We present an algorithm of control synthesis for nonlinear switched systems, based on an existing procedure of state-space bisection and made available for nonlinear systems with the help of validated simulation. The use of validated simulation also permits to take bounded perturbations and varying parameters into account. The whole approach is entirely guaranteed and the induced controllers are correct-by-design.} }

@inproceedings{BBCM-csr16, address = {St~Petersburg, Russia}, month = jun, year = 2016, volume = {9691}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Gerhard J. Woeginger}, acronym = {{CSR}'16}, booktitle = {{P}roceedings of the 11th {I}nternational {C}omputer {S}cience {S}ymposium in {R}ussia ({CSR}'16)}, author = {Bouyer, Patricia and Brihaye, {\relax Th}omas and Carlier, Pierre and Menet, Quentin}, title = {Compositional Design of Stochastic Timed Automata}, pages = {117-130}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBCM-csr16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBCM-csr16.pdf}, doi = {10.1007/978-3-319-34171-2_9}, abstract = {In this paper, we study the model of stochastic timed automata and we target the definition of adequate composition operators that will allow a compositional approach to the design of stochastic systems with hard real-time constraints. This paper achieves the first step towards that goal. Firstly, we define a parallel composition operator that (we~prove) corresponds to the interleaving semantics for that model; we give conditions over probability distributions, which ensure that the operator is well-defined; and we exhibit problematic behaviours when this condition is not satisfied. We furthermore identify a large and natural subclass which is closed under parallel composition. Secondly, we define a bisimulation notion which naturally extends that for continuous-time Markov chains. Finally, we importantly show that the defined bisimulation is a congruence w.r.t. the parallel composition, which is an expected property for a proper modular approach to system design.} }

@inproceedings{BBBC-icalp16, address = {Rome, Italy}, month = jul, year = 2016, volume = {55}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide}, acronym = {{ICALP}'16}, booktitle = {{P}roceedings of the 43rd {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'16)}, author = {Bertrand, Nathalie and Bouyer, Patricia and Brihaye, {\relax Th}omas and Carlier, Pierre}, title = {Analysing Decisive Stochastic Processes}, pages = {101:1-101:14}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBC-icalp16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBBC-icalp16.pdf}, doi = {10.4230/LIPIcs.ICALP.2016.101}, abstract = {In~2007, Abdulla \textit{et~al.} introduced the elegant concept of decisive Markov chain. Intuitively, decisiveness allows one to lift the good properties of finite Markov chains to infinite Markov chains. For instance, the approximate quantitative reachability problem can be solved for decisive Markov chains (enjoying reasonable effectiveness assumptions) including probabilistic lossy channel systems and probabilistic vector addition systems with states. In this paper, we extend the concept of decisiveness to more general stochastic processes. This extension is non trivial as we consider stochastic processes with a potentially continuous set of states and uncountable branching (common features of real-time stochastic processes). This allows us to obtain decidability results for both qualitative and quantitative verification problems on some classes of real-time stochastic processes, including generalized semi-Markov processes and stochastic timed automata.} }

@inproceedings{CD-icalp16, address = {Rome, Italy}, month = jul, year = 2016, volume = {55}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide}, acronym = {{ICALP}'16}, booktitle = {{P}roceedings of the 43rd {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'16)}, author = {Chatterjee, Krishnendu and Doyen, Laurent}, title = {Computation Tree Logic for Synchronization Properties}, pages = {98:1-98:14}, url = {http://arxiv.org/abs/1604.06384}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CD-icalp16.pdf}, doi = {10.4230/LIPIcs.ICALP.2016.98}, abstract = {We present a logic that extends CTL (Computation Tree Logic) with operators that express synchronization properties. A property is synchronized in a system if it holds in all paths of a certain length. The new logic is obtained by using the same path quantifiers and temporal operators as in CTL, but allowing a different order of the quantifiers. This small syntactic variation induces a logic that can express non-regular properties for which known extensions of MSO with equality of path length are undecidable. We show that our variant of CTL is decidable and that the model-checking problem is in \(\Delta_3^P = P^{NP^NP}\), and is DP-hard. We analogously consider quantifier exchange in extensions of CTL, and we present operators defined using basic operators of CTL* that express the occurrence of infinitely many synchronization points. We show that the model-checking problem remains in \(\Delta_3^P\). The distinguishing power of CTL and of our new logic coincide if the Next operator is allowed in the logics, thus the classical bisimulation quotient can be used for state-space reduction before model checking.} }

@article{BMV-ic16, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Bouyer, Patricia and Markey, Nicolas and Vester, Steen}, title = {{N}ash Equilibria in Symmetric Graph Games with Partial Observation}, volume = {254}, number = {2}, month = jun, year = 2017, pages = {238-258}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BMV-ic16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BMV-ic16.pdf}, doi = {10.1016/j.ic.2016.10.010}, 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{BCM-cav16, address = {Toronto, Canada}, month = jul, year = 2016, volume = 9779, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Chaudhuri, Swarat and Farzan, Azadeh}, acronym = {{CAV}'16}, booktitle = {{P}roceedings of the 28th {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'16)~-- {P}art~{I}}, author = {Bouyer, Patricia and Colange, Maximilien and Markey, Nicolas}, title = {Symbolic Optimal Reachability in Weighted Timed Automata}, pages = {513-530}, url = {http://arxiv.org/abs/1602.00481}, doi = {10.1007/978-3-319-41528-4_28}, 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.} }

@inproceedings{BMRSS-icalp16, address = {Rome, Italy}, month = jul, year = 2016, volume = {55}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide}, acronym = {{ICALP}'16}, booktitle = {{P}roceedings of the 43rd {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'16)}, 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}, pages = {106:1-106:14}, url = {http://arxiv.org/abs/1602.05928}, 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.} }

@inproceedings{CD-lics16, address = {New York City, USA}, month = jul, year = 2016, publisher = {ACM Press}, editor = {Grohe, Martin and Koskinen, Eric and Shankar, Natarajan}, acronym = {{LICS}'16}, booktitle = {{P}roceedings of the 31st {A}nnual {ACM\slash IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'16)}, author = {Chatterjee, Krishnendu and Doyen, Laurent}, title = {Perfect-information Stochastic Games with Generalized Mean-Payoff Objectives}, pages = {247-256}, url = {http://arxiv.org/abs/1604.06376}, doi = {10.1145/2933575.2934513}, abstract = {Graph games provide the foundation for modeling and synthesizing reactive processes. In the synthesis of stochastic reactive processes, the traditional model is perfect-information stochastic games, where some transitions of the game graph are controlled by two adversarial players, and the other transitions are executed probabilistically. We consider such games where the objective is the conjunction of several quantitative objectives (specified as mean-payoff conditions), which we refer to as generalized mean-payoff objectives. The basic decision problem asks for the existence of a finite-memory strategy for a player that ensures the generalized mean-payoff objective be satisfied with a desired probability against all strategies of the opponent. A special case of the decision problem is the almost-sure problem where the desired probability is~1. Previous results presented a semi-decision procedure for epsilon-approximations of the almost-sure problem. In this work, we show that both the almost-sure problem as well as the general basic decision problem are coNP-complete, significantly improving the previous results. Moreover, we show that in the case of 1-player stochastic games, randomized memoryless strategies are sufficient and the problem can be solved in polynomial time. In contrast, in two-player stochastic games, we show that even with randomized strategies exponential memory is required in general, and present a matching exponential upper bound. We also study the basic decision problem with infinite-memory strategies and present computational complexity results for the problem. Our results are relevant in the synthesis of stochastic reactive systems with multiple quantitative requirements. } }

@comment{{B-arxiv16, author = Bollig, Benedikt, affiliation = aff-LSVmexico, title = One-Counter Automata with Counter Visibility, institution = Computing Research Repository, number = 1602.05940, month = feb, nmonth = 2, year = 2016, type = RR, axeLSV = mexico, NOcontrat = "", url = http://arxiv.org/abs/1602.05940, PDF = "http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf", lsvdate-new = 20160222, lsvdate-upd = 20160222, lsvdate-pub = 20160222, lsv-category = "rapl", wwwpublic = "public and ccsb", note = 18~pages, abstract = "In a one-counter automaton (OCA), one can read a letter from some finite alphabet, increment and decrement the counter by one, or test it for zero. It is well-known that universality and language inclusion for OCAs are undecidable. We consider here OCAs with counter visibility: Whenever the automaton produces a letter, it outputs the current counter value along with~it. Hence, its language is now a set of words over an infinite alphabet. We show that universality and inclusion for that model are in PSPACE, thus no harder than the corresponding problems for finite automata, which can actually be considered as a special case. In fact, we show that OCAs with counter visibility are effectively determinizable and closed under all boolean operations. As~a~strict generalization, we subsequently extend our model by registers. The general nonemptiness problem being undecidable, we impose a bound on the number of register comparisons and show that the corresponding nonemptiness problem is NP-complete.", }}

@inproceedings{FGMP-hscc16, address = {Vienna, Austria}, month = apr, year = 2016, publisher = {ACM Press}, editor = {Abate, Alessandro and Fainekos, Georgios}, acronym = {{HSCC}'16}, booktitle = {{P}roceedings of the 19th {ACM} {I}nternational {C}onference on {H}ybrid {S}ystems: {C}omputation and {C}ontrol ({HSCC}'16)}, author = {Fribourg, Laurent and Goubault, {\'E}ric and Mohamed, Sameh and Putot, Sylvie}, title = {A~Topological Method for Finding Invariant Sets of Switched Systems}, pages = {61-70}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/FGMP-hscc16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FGMP-hscc16.pdf}, doi = {10.1145/2883817.2883822}, abstract = {We~revisit the problem of finding controlled invariants sets (viability), for a class of differential inclusions, using topological methods based on Wazewski property. In~many ways, this generalizes the Viability Theorem approach, which is itself a generalization of the Lyapunov function approach for systems described by ordinary differential equations. We give a computable criterion based on SoS methods for a class of differential inclusions to have a non-empty viability kernel within some given region. We use this method to prove the existence of (controlled) invariant sets of switched systems inside a region described by a polynomial template, both with time-dependent switching and with state-based switching through a finite set of hypersurfaces. A~Matlab implementation allows us to demonstrate its use.} }

@techreport{BJM-arxiv16, author = {Bouyer, Patricia and Markey, Nicolas and Jug{\'e}, Vincent}, title = {Dynamic Complexity of Parity Games with Bounded Tree-Width}, institution = {Computing Research Repository}, number = {1610.00571}, year = {2016}, url = {https://arxiv.org/abs/1610.00571}, pdf = {https://arxiv.org/abs/1610.00571}, month = oct, type = {Research Report}, note = {33~pages} }

@inproceedings{GBM-stacs18, address = {Caen, France}, month = feb, volume = {96}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Niedermeier, Rolf and Vall{\'e}e, Brigitte}, acronym = {{STACS}'18}, booktitle = {{P}roceedings of the 35th {A}nnual {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'18)}, author = {Gardy, Patrick and Bouyer, Patricia and Markey, Nicolas}, title = {Dependences in Strategy Logic}, pages = {34:1-34:15}, year = {2018}, doi = {10.4230/LIPIcs.STACS.2018.34}, pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/8532/pdf/LIPIcs-STACS-2018-34.pdf}, url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=8532}, abstract = {Strategy Logic (SL) is a very expressive logic for specifying and verifying properties of multi-agent systems: in SL, one can quantify over strategies, assign them to agents, and express properties of the resulting plays. Such a powerful framework has two drawbacks: first, model checking SL has non-elementary complexity; second, the exact semantics of SL is rather intricate, and may not correspond to what is expected. In this paper, we focus on strategy dependences in SL, by tracking how existentially-quantified strategies in a formula may (or may not) depend on other strategies selected in the formula. We study different kinds of dependences, refining the approach of [Mogavero et al., Reasoning about strategies: On the model-checking problem, 2014], and prove that they give rise to different satisfaction relations. In the setting where strategies may only depend on what they have observed, we identify a large fragment of SL for which we prove model checking can be performed in 2-EXPTIME.} }

@incollection{CDH-kimfest17, author = {Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, {\relax Th}omas~A.}, title = {The Cost of Exactness in Quantitative Reachability}, editor = {Aceto, Luca and Bacci, Giorgio and Bacci, Giovani and Ing{\'o}lfsd{\'o}ttir, Anna and Legay, Axel and Mardare, Radu}, booktitle = {Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {10460}, year = {2017}, pages = {367-381}, month = aug, doi = {10.1007/978-3-319-63121-9_18}, abstract = {In the analysis of reactive systems a quantitative objective assigns a real value to every trace of the system. The value decision problem for a quantitative objective requires a trace whose value is at least a given threshold, and the exact value decision problem requires a trace whose value is exactly the threshold. We compare the compu- tational complexity of the value and exact value decision problems for classical quantitative objectives, such as sum, discounted sum, energy, and mean-payoff for two standard models of reactive systems, namely, graphs and graph games.}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDH-2017.pdf} }

@article{CDFR-ic17, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Krishnendu Chatterjee and Laurent Doyen and Emmanuel Filiot and Jean{-}Fran{\c{c}}ois Raskin}, title = {Doomsday equilibria for omega-regular games}, volume = {254}, year = {2017}, pages = {296-315}, doi = {10.1016/j.ic.2016.10.012}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CDFR-ic2017.pdf}, abstract = {Two-player games on graphs provide the theoretical framework for many important problems such as reactive synthesis. While the traditional study of two-player zero-sum games has been extended to multi-player games with several notions of equilibria, they are decidable only for perfect-information games, whereas several applications require imperfect-information games.\par In this paper we propose a new notion of equilibria, called doomsday equilibria, which is a strategy profile such that all players satisfy their own objective, and if any coalition of players deviates and violates even one of the players objective, then the objective of every player is violated.\par We present algorithms and complexity results for deciding the existence of doomsday equilibria for various classes of ?-regular objectives, both for imperfect-information games, and for perfect-information games. We provide optimal complexity bounds for imperfect-information games, and in most cases for perfect- information games.} }

@inproceedings{D-rp17, address = {London, UK}, month = sep, year = 2017, volume = {10506}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Matthew Hague and Igor Potapov}, acronym = {{RP}'17}, booktitle = {{P}roceedings of the 11th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'17)}, author = {Doyen, Laurent}, title = {The Multiple Dimensions of Mean-Payoff Games}, pages = {1-8}, url = {https://doi.org/10.1007/978-3-319-67089-8_1}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Doyen-rp2017.pdf}, doi = {10.1007/978-3-319-67089-8_1}, abstract = {We consider quantitative game models for the design of reactive systems working in resource-constrained environment. The game is played on a finite weighted graph where some resource (e.g., battery) can be consumed or recharged along the edges of the graph.} }

@phdthesis{gardy-phd2017, author = {Gardy, Patrick}, title = {Semantics of {S}trategy {L}ogic}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2017, month = jun, url = {https://tel.archives-ouvertes.fr/tel-01561802}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/gardy-phd17.pdf} }

@inproceedings{GBBLM-gretsi17, address = {Juan-les-Pins, France}, month = sep, year = 2017, publisher = {}, editor = {}, acronym = {{GRETSI}'17}, booktitle = {Actes du XXVI$^{\text{\`eme}}$ colloque GRETSI}, author = {Mauricio Gonz{\'a}lez and Olivier Beaude and Patricia Bouyer and Samson Lasaulce and Nicolas Markey}, title = {Strat{\'e}gies d'ordonnancement de consommation d'{\'e}nergie en pr{\'e}sence d'information imparfaite de pr{\'e}vision}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/GBBLM-gretsi17.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GBBLM-gretsi17.pdf} }

@techreport{BJM-arxiv17, author = {Bouyer, Patricia and Markey, Nicolas and Jug{\'e}, Vincent}, institution = {Computing Research Repository}, month = feb, note = {14~pages}, number = {1702.05183}, type = {Research Report}, title = {Courcelle's Theorem Made Dynamic}, year = {2017}, url = {https://arxiv.org/abs/1702.05183}, pdf = {https://arxiv.org/abs/1702.05183} }

@inproceedings{BHJ-concur17, address = {Berlin, Germany}, month = sep, year = 2017, volume = {85}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Meyer, Roland and Nestmann, Uwe}, acronym = {{CONCUR}'17}, booktitle = {{P}roceedings of the 28th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'17)}, author = {Bouyer, Patricia and Haddad, Serge and Jug{\'e}, Vincent}, title = {Unbounded product-form {P}etri nets}, pages = {31:1--31:16}, url = {http://drops.dagstuhl.de/opus/volltexte/2017/7795}, pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/7795/pdf/LIPIcs-CONCUR-2017-31.pdf}, doi = {10.4230/LIPIcs.CONCUR.2017.31}, abstract = {Computing steady-state distributions in infinite-state stochastic systems is in general a very difficult task. Product-form Petri nets are those Petri nets for which the steady-state distribution can be described as a natural product corresponding, up to a normalising constant, to an exponentiation of the markings. However, even though some classes of nets are known to have a product-form distribution, computing the normalising constant can be hard. The class of (closed) \(\Pi^3\)-nets has been proposed in an earlier work, for which it is shown that one can compute the steady-state distribution efficiently. However these nets are bounded. In this paper, we generalise queuing Markovian networks and closed \(\Pi^3\)-nets to obtain the class of open \(\Pi^3\)-nets, that generate infinite-state systems. We show interesting properties of these nets: (1) we prove that liveness can be decided in polynomial time, and that reachability in live \(\Pi^3\)-nets can be decided in polynomial time; (2) we show that we can decide ergodicity of such nets in polynomial time as well; (3) we provide a pseudo-polynomial time algorithm to compute the normalising constant.} }

@inproceedings{AGKS-concur17, address = {Berlin, Germany}, month = sep, year = 2017, volume = {85}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Meyer, Roland and Nestmann, Uwe}, acronym = {{CONCUR}'17}, booktitle = {{P}roceedings of the 28th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'17)}, author = {Akshay, S. and Gastin, Paul and Krishna, Shankara Narayanan and Sarkar, Ilias}, title = {Towards an Efficient Tree Automata based technique for Timed Systems}, pages = {39:1--39:15}, url = {http://drops.dagstuhl.de/opus/volltexte/2017/7801}, pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/7801/pdf/LIPIcs-CONCUR-2017-39.pdf}, doi = {10.4230/LIPIcs.CONCUR.2017.39}, abstract = {The focus of this paper is the analysis of real-time systems with recursion, through the development of good theoretical techniques which are implementable. Time is modeled using clock variables, and recursion using stacks. Our technique consists of modeling the behaviours of the timed system as graphs, and interpreting these graphs on tree terms by showing a bound on their tree-width. We then build a tree automaton that accepts exactly those tree terms that describe realizable runs of the timed system. The emptiness of the timed system thus boils down to emptiness of a finite tree automaton that accepts these tree terms. This approach helps us in obtaining an optimal complexity, not just in theory (as done in earlier work e.g.[concur16]), but also in going towards an efficient implementation of our technique. To do this, we make several improvements in the theory and exploit these to build a first prototype tool that can analyze timed systems with recursion.} }

@inproceedings{BQS-concur17, address = {Berlin, Germany}, month = sep, year = 2017, volume = {85}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Meyer, Roland and Nestmann, Uwe}, acronym = {{CONCUR}'17}, booktitle = {{P}roceedings of the 28th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'17)}, author = {Bollig, Benedikt and Quaas, Karin and Sangnier, Arnaud}, title = {The Complexity of Flat Freeze LTL}, pages = {33:1--33:16}, url = {http://drops.dagstuhl.de/opus/volltexte/2017/7799}, pdf = {http://drops.dagstuhl.de/opus/volltexte/2017/7799/pdf/LIPIcs-CONCUR-2017-33.pdf}, doi = {10.4230/LIPIcs.CONCUR.2017.33}, abstract = {We consider the model-checking problem for freeze LTL on one-counter automata (OCAs). Freeze LTL extends LTL with the freeze quantifier, which allows one to store different counter values of a run in registers so that they can be compared with one another. As the model-checking problem is undecidable in general, we focus on the flat fragment of freeze LTL, in which the usage of the freeze quantifier is restricted. Recently, Lechner et al. showed that model checking for flat freeze LTL on OCAs with binary encoding of counter updates is decidable and in 2NEXPTIME. In this paper, we prove that the problem is, in fact, NEXPTIME-complete no matter whether counter updates are encoded in unary or binary. Like Lechner et al., we rely on a reduction to the reachability problem in OCAs with parameterized tests (OCAPs). The new aspect is that we simulate OCAPs by alternating two-way automata over words. This implies an exponential upper bound on the parameter values that we exploit towards an NP algorithm for reachability in OCAPs with unary updates. We obtain our main result as a corollary.} }

@inproceedings{BJM-formats17, address = {Berlin, Germany}, month = sep, year = 2017, volume = {10419}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Abate, Alessandro and Geeraerts, Gilles}, acronym = {{FORMATS}'17}, booktitle = {{P}roceedings of the 15th {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'17)}, author = {Bouyer, Patricia and Jaziri, Samy and Markey, Nicolas}, title = {On the Determinization of Timed Systems}, pages = {25-41}, url = {https://hal.archives-ouvertes.fr/hal-01566436/}, doi = {10.1007/978-3-319-65765-3_2}, abstract = {We introduce a new formalism called automata over a timed domain which provides an adequate framework for the determinization of timed systems. In this formalism, determinization w.r.t. timed language is always possible at the cost of changing the timed domain. We give a condition for determinizability of automata over a timed domain without changing the timed domain, which allows us to recover several known determinizable classes of timed systems, such as strongly-non-zeno timed automata, integer-reset timed automata, perturbed timed automata, etc. Moreover in the case of timed automata this condition encompasses most determinizability conditions from the literature.} }

@phdthesis{stan-phd2017, author = {Stan, Daniel}, title = {Randomized Strategies in Concurrent Games}, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {Th{\`e}se de doctorat}, year = 2017, month = mar, url = {https://hal.archives-ouvertes.fr/tel-01519354}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/stan-phd17.pdf} }

@article{ABG-ic17, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Aiswarya, C. and Bollig, Benedikt and Gastin, Paul}, title = {An Automata-Theoretic Approach to the Verification of Distributed Algorithms}, volume = {259}, month = apr, year = {2018}, pages = {305-327}, doi = {10.1016/j.ic.2017.05.006}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABG-ic17.pdf}, abstract = {We introduce an automata-theoretic method for the verification of distributed algorithms running on ring networks. In a distributed algorithm, an arbitrary number of processes cooperate to achieve a common goal (e.g., elect a leader). Processes have unique identifiers (pids) from an infinite, totally ordered domain. An algorithm proceeds in synchronous rounds, each round allowing a process to perform a bounded sequence of actions such as send or receive a pid, store it in some register, and compare register contents wrt. the associated total order. An algorithm is supposed to be correct independently of the number of processes. To specify correctness properties, we introduce a logic that can reason about processes and pids. Referring to leader election, it may say that, at the end of an execution, each process stores the maximum pid in some dedicated register. We show that the verification problem of distributed algorithms can be reduced to satisfiability of a formula from propositional dynamic logic with loop and converse (LCPDL), interpreted over grids over a finite alphabet. This translation is independent of any restriction imposed on the algorithm. However, since the verification problem (and satisfiability for LCPDL) is undecidable, we propose an underapproximation technique, which bounds the number of rounds. This is an appealing approach, as the number of rounds needed by a distributed algorithm to conclude is often exponentially smaller than the number of processes. Using our reduction to LCPDL, we provide an automata-theoretic solution, reducing model checking to emptiness for alternating two-way automata on words. Overall, we show that round-bounded verification of distributed algorithms over rings is PSPACE-complete, provided the number of rounds is given in unary.} }

@inproceedings{FMW-cav17, address = {Heidelberg, Germany}, month = jul, volume = {10427}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Kuncak, Viktor and Majumdar, Rupak}, acronym = {{CAV}'17}, booktitle = {{P}roceedings of the 29th {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'17)}, author = {Fortin, Marie and Muscholl, Anca and Walukiewicz, Igor}, title = {Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systems}, pages = {155-175}, year = {2017}, doi = {10.1007/978-3-319-63390-9_9}, url = {https://arxiv.org/abs/1606.08707}, abstract = {} }

@article{ABH-ijfcs17, publisher = {World Scientific}, journal = {International Journal of Foundations of Computer Science}, author = {Atig, Mohamed Faouzi and Bollig, Benedikt and Habermehl, Peter}, title = {Emptiness of ordered multi-pushdown automata is {2ETIME}-complete}, volume = {28}, number = {8}, year = {2017}, pages = {945-975}, doi = {10.1142/S0129054117500332}, url = {http://www.worldscientific.com/doi/abs/10.1142/S0129054117500332}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABH-ijfcs17.pdf}, abstract = {We consider ordered multi-pushdown automata, a multi-stack extension of pushdown automata that comes with a constraint on stack operations: a pop can only be performed on the first non-empty stack (which implies that we assume a linear ordering on the collection of stacks). We show that the emptiness problem for multi-pushdown automata is 2ETIME-complete. Containment in 2ETIME is shown by translating an automaton into a grammar for which we can check if the generated language is empty. The lower bound is established by simulating the behavior of an alternating Turing machine working in exponential space. We also compare ordered multi-pushdown automata with the model of bounded-phase (visibly) multi-stack pushdown automata, which do not impose an ordering on stacks, but restrict the number of alternations of pop operations on different stacks.} }

@incollection{BLMOW-kimfest17, author = {Bouyer, Patricia and Laroussinie, Fran{\c{c}}ois and Markey, Nicolas and Ouaknine, Jo{\"e}l and Worrell, James}, title = {Timed temporal logics}, editor = {Aceto, Luca and Bacci, Giorgio and Bacci, Giovani and Ing{\'o}lfsd{\'o}ttir, Anna and Legay, Axel and Mardare, Radu}, booktitle = {Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {10460}, year = {2017}, pages = {211-230}, month = aug, doi = {10.1007/978-3-319-65764-6_11}, abstract = {Since the early 1990's, classical temporal logics have been extended with timing constraints. While temporal logics only express contraints on the order of events, their timed extensions can add quantitative constraints on delays between those events. We survey expressiveness and algorithmic results on those logics, and discuss semantic choices that may look unimportant but do have an impact on the questions we consider.}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BLMOW-kimfest17.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BLMOW-kimfest17.pdf} }

@inproceedings{BGMR-gandalf18, address = {Saarbr{\"u}cken, Germany}, month = sep, volume = {277}, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Andrea Orlandini and Martin Zimmermann}, acronym = {{GandALF}'18}, booktitle = {{P}roceedings of the 9th {I}nternational {S}ymposium on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification ({GandALF}'18)}, author = {Bouyer, Patricia and Gonz{\'a}lez, Mauricio and Markey, Nicolas and Randour, Mickael}, title = {Multi-weighted Markov Decision Processes with Reachability Objectives}, pages = {250-264}, year = {2018}, doi = {10.4204/EPTCS.277.18}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGMR-gandalf18.pdf}, url = {http://arxiv.org/abs/1809.03107}, abstract = {In this paper, we are interested in the synthesis of schedulers in double-weighted Markov decision processes, which satisfy both a percentile constraint over a weighted reachability condition, and a quantitative constraint on the expected value of a random variable defined using a weighted reachability condition. This problem is inspired by the modelization of an electric-vehicle charging problem. We study the cartography of the problem, when one parameter varies, and show how a partial cartography can be obtained via two sequences of opimization problems. We discuss completeness and feasability of the method.} }

@inproceedings{BJM-rv18, address = {Limassol, Cyprus}, month = nov, volume = 11237, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Colombo, Christian and Leucker, Martin}, acronym = {{RV}'18}, booktitle = {{P}roceedings of the 18th {W}orkshop on {R}untime {V}erification ({RV}'18)}, author = {Bouyer, Patricia and Jaziri, Samy and Markey, Nicolas}, title = {Efficient Timed Diagnosis Using Automata with Timed Domains}, pages = {205-221}, year = {2018}, doi = {10.1007/978-3-030-03769-7_12}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BJM-rv18.pdf}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BJM-rv18.pdf}, abstract = {We consider the problems of efficiently diagnosing and predicting what did (or will) happen in a partially-observable one-clock timed automaton. We introduce timed sets as a formalism to keep track of the evolution of the reachable configurations over time, and use our previous work on automata over timed domains to build a candidate diagnoser for our timed automaton. We report on our implementation of this approach compared to the approach of [Tripakis, Fault diagnosis for timed automata, 2002].} }

@article{BLMP-jml18, publisher = {World Scientific}, journal = {Journal of Mathematical Logic}, author = {Brattka, Vasco and Le{~}Roux, St{\'e}phane and Miller, Joseph S. and Pauly, Arno}, title = {{Connected Choice and Brouwer's Fixed Point Theorem}}, year = {2018}, note = {To appear} }

@inproceedings{LPR-fsttcs18, address = {Ahmedabad, India}, month = dec, year = 2018, volume = {122}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Sumit Ganguly and Paritosh Pandya}, acronym = {{FSTTCS}'18}, booktitle = {{P}roceedings of the 38th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'18)}, author = {Le{~}Roux, Stephane and Pauly, Arno and Randour, Mickael}, title = {Extending finite-memory determinacy to Boolean combinations of winning conditions}, pages = {38:1-38:20}, url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9937}, pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/9937/pdf/LIPIcs-FSTTCS-2018-38.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2018.38}, abstract = {We study finite-memory (FM) determinacy in games on finite graphs, a central question for applications in controller synthesis, as FM strategies correspond to implementable controllers. We establish general conditions under which FM strategies suffice to play optimally, even in a broad multi-objective setting. We show that our framework encompasses important classes of games from the literature, and permits to go further, using a unified approach. While such an approach cannot match ad-hoc proofs with regard to tightness of memory bounds, it has two advantages: first, it gives a widely-applicable criterion for FM determinacy; second, it helps to understand the cornerstones of FM determinacy, which are often hidden but common in proofs for specific (combinations of) winning conditions.} }

@inproceedings{BLS-atva18, address = {Los Angeles, California, USA}, month = oct, year = {2018}, volume = {11138}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Shuvendu Lahiri and Chao Wang}, acronym = {{ATVA}'18}, booktitle = {{P}roceedings of the 16th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'18)}, author = {Benedikt Bollig and Mathieu Lehaut and Nathalie Sznajder}, title = {Round-Bounded Control of Parameterized Systems}, pages = {370-386}, url = {https://hal.archives-ouvertes.fr/hal-01849206}, doi = {10.1007/978-3-030-01090-4_22}, abstract = {We consider systems with unboundedly many processes that communicate through shared memory. In that context, simple verification questions have a high complexity or, in the case of pushdown processes, are even undecidable. Good algorithmic properties are recovered under round-bounded verification, which restricts the system behavior to a bounded number of round-robin schedules. In this paper, we extend this approach to a game-based setting. This allows one to solve synthesis and control problems and constitutes a further step towards a theory of languages over infinite alphabets.} }

@inproceedings{BBJ-csl18, address = {Birmingham, UK}, month = sep, year = 2018, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Ghica, Dan R. and Jung, Achim}, acronym = {{CSL}'18}, booktitle = {{P}roceedings of the 27th {A}nnual {EACSL} {C}onference on {C}omputer {S}cience {L}ogic ({CSL}'18)}, author = {B{\'e}rard, B{\'e}atrice and Bouyer, Patricia and Jug{\'e}, Vincent}, title = {Finite bisimulations for dynamical systems with overlapping trajectories}, url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9693}, pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/9693/pdf/LIPIcs-CSL-2018-26.pdf}, doi = {10.4230/LIPIcs.CSL.2018.26}, abstract = {Having a finite bisimulation is a good feature for a dynamical system, since it can lead to the decidability of the verification of reachability properties. We investigate a new class of o-minimal dynamical systems with very general flows, where the classical restrictions on trajectory intersections are partly lifted. We identify conditions, that we call Finite and Uniform Crossing: When Finite Crossing holds, the time-abstract bisimulation is computable and, under the stronger Uniform Crossing assumption, this bisimulation is finite and definable.} }

@inproceedings{GMS-concur18, address = {Beijing, China}, month = sep, year = 2018, volume = {118}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Schewe, Sven and Zhang, Lijun}, acronym = {{CONCUR}'18}, booktitle = {{P}roceedings of the 29th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'18)}, author = {Paul Gastin and Sayan Mukherjee and B. Srivathsan}, title = {Reachability in timed automata with diagonal constraints}, pages = {28:1-28:17}, url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9566}, pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/9566/pdf/LIPIcs-CONCUR-2018-28.pdf}, doi = {10.4230/LIPIcs.CONCUR.2018.28}, abstract = {We consider the reachability problem for timed automata having diagonal constraints (like x - y < 5) as guards in transitions. The best algorithms for timed automata proceed by enumerating reachable sets of its configurations, stored in a data structure called ''zones''. Simulation relations between zones are essential to ensure termination and efficiency. The algorithm employs a simulation test Z <= Z' which ascertains that zone Z does not reach more states than zone Z', and hence further enumeration from Z is not necessary. No effective simulations are known for timed automata containing diagonal constraints as guards. We propose a simulation relation <=_{LU}^d for timed automata with diagonal constraints. On the negative side, we show that deciding Z not <=_{LU}^d Z' is NP-complete. On the positive side, we identify a witness for Z not <=_{LU}^d Z' and propose an algorithm to decide the existence of such a witness using an SMT solver. The shape of the witness reveals that the simulation test is likely to be efficient in practice.} }

@inproceedings{BFG-concur18, address = {Beijing, China}, month = sep, year = 2018, volume = {118}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Schewe, Sven and Zhang, Lijun}, acronym = {{CONCUR}'18}, booktitle = {{P}roceedings of the 29th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'18)}, author = {Bollig, Benedikt and Fortin, Marie and Gastin, Paul}, title = {It Is Easy to Be Wise After the Event: Communicating Finite-State Machines Capture First-Order Logic with ''Happened Before''}, pages = {7:1-7:17}, url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9545}, pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/9545/pdf/LIPIcs-CONCUR-2018-7.pdf}, doi = {10.4230/LIPIcs.CONCUR.2018.7}, abstract = {Message sequence charts (MSCs) naturally arise as executions of communicating finite-state machines (CFMs), in which finite-state processes exchange messages through unbounded FIFO channels. We study the first-order logic of MSCs, featuring Lamport's happened-before relation. We introduce a star-free version of propositional dynamic logic (PDL) with loop and converse. Our main results state that (i) every first-order sentence can be transformed into an equivalent star-free PDL sentence (and conversely), and (ii) every star-free PDL sentence can be translated into an equivalent CFM. This answers an open question and settles the exact relation between CFMs and fragments of monadic second-order logic. As a byproduct, we show that first-order logic over MSCs has the three-variable property.} }

@mastersthesis{m2-Gonzalez, author = {Gonz{\'a}lez, Mauricio}, title = {{Constructions d'Information Parfaite pour certains Jeux {\`a} Information Imparfaite. Quelques Algorithmes.}}, school = {Universit{\'e} Pierre et Marie Curie, Paris, France}, type = {Rapport de {M}aster}, year = {2015}, month = dec }

@mastersthesis{m2-Fang, author = {Fang, Erwin}, title = {{Permissive multi-strategies in timed games}}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2013}, month = aug }

@mastersthesis{m2-Fortin, author = {Fortin, Marie}, title = {{Verification of distributed systems with parameterized network topology}}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2015}, month = sep }

@mastersthesis{m2-Jaziri, author = {Jaziri, Samy}, title = {{Robustness issues in priced timed automata}}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2014}, month = sep }

@article{AGK-lmcs18, journal = {Logical Methods in Computer Science}, author = {Akshay, S. and Gastin, Paul and Krishna, Shankara Narayanan}, title = {Analyzing Timed Systems Using Tree Automata}, volume = {14}, number = {2}, pages = {1-35}, year = {2018}, month = may, doi = {10.23638/LMCS-14(2:8)2018}, pdf = {https://lmcs.episciences.org/4489/pdf}, url = {https://lmcs.episciences.org/4489}, abstract = {Timed systems, such as timed automata, are usually analyzed using their operational semantics on timed words. The classical region abstraction for timed automata reduces them to (untimed) finite state automata with the same time-abstract properties, such as state reachability. We propose a new technique to analyze such timed systems using finite tree automata instead of finite word automata. The main idea is to consider timed behaviors as graphs with matching edges capturing timing constraints. When a family of graphs has bounded tree-width, they can be interpreted in trees and MSO-definable properties of such graphs can be checked using tree automata. The technique is quite general and applies to many timed systems. In this paper, as an example, we develop the technique on timed pushdown systems, which have recently received considerable attention. Further, we also demonstrate how we can use it on timed automata and timed multi-stack pushdown systems (with boundedness restrictions).} }

@inproceedings{BBFLMR-fm18, address = {Oxford, UK}, month = jul, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Roscoe, {Bill W.} and Peleska, Jan}, acronym = {{FM}'18}, booktitle = {{P}roceedings of the 22nd {I}nternational {S}ymposium on {F}ormal {M}ethods ({FM}'18)}, author = {Bacci, Giovanni and Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim G. and Markey, Nicolas and Reynier, Pierre-Alain}, title = {Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty}, pages = {203-221}, year = {2018}, doi = {10.1007/978-3-319-95582-7_12}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BBFLMR-fm18.pdf}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BBFLMR-fm18.pdf}, note = {Best paper award}, abstract = {In this paper, we propose a novel framework for the synthesis of robust and optimal energy-aware controllers. The framework is based on energy timed automata, allowing for easy expression of timing-constraints and variable energy-rates. We prove decidability of the energy-constrained infinite-run problem in settings with both certainty and uncertainty of the energy-rates. We also consider the optimization problem of identifying the minimal upper bound that will permit existence of energy-constrained infinite runs. Our algorithms are based on quantifier elimination for linear real arithmetic. Using Mathematica and Mjollnir, we illustrate our framework through a real industrial example of a hydraulic oil pump. Compared with previous approaches our method is completely automated and provides improved results.} }

@article{BBBC-jlamp18, publisher = {Elsevier Science Publishers}, journal = {Journal of Logic and Algebraic Methods in Programming}, author = {Bertrand, Nathalie and Bouyer, Patricia and Brihaye, Thomas and Carlier, Pierre}, title = {When are Stochastic Transition Systems Tameable?}, volume = {99}, pages = {41-96}, year = {2018}, month = oct, doi = {10.1016/j.jlamp.2018.03.004}, pdf = {https://arxiv.org/pdf/1703.04806.pdf}, url = {https://doi.org/10.1016/j.jlamp.2018.03.004}, abstract = {A decade ago, Abdulla, Ben Henda and Mayr introduced the elegant concept of decisiveness for denumerable Markov chains [1]. Roughly speaking, decisiveness allows one to lift most good properties from finite Markov chains to denumerable ones, and therefore to adapt existing verification algorithms to infinite-state models. Decisive Markov chains however do not encompass stochastic real-time systems, and general stochastic transition systems (STSs for short) are needed. In this article, we provide a framework to perform both the qualitative and the quantitative analysis of STSs. First, we define various notions of decisiveness (inherited from [1]), notions of fairness and of attractors for STSs, and make explicit the relationships between them. Then, we define a notion of abstraction, together with natural concepts of soundness and completeness, and we give general transfer properties, which will be central to several verification algorithms on STSs. We further design a generic construction which will be useful for the analysis of ω-regular properties, when a finite attractor exists, either in the system (if it is denumerable), or in a sound denumerable abstraction of the system. We next provide algorithms for qualitative model-checking, and generic approximation procedures for quantitative model-checking. Finally, we instantiate our framework with stochastic timed automata (STA), generalized semi-Markov processes (GSMPs) and stochastic time Petri nets (STPNs), three models combining dense-time and probabilities. This allows us to derive decidability and approximability results for the verification of these models. Some of these results were known from the literature, but our generic approach permits to view them in a unified framework, and to obtain them with less effort. We also derive interesting new approximability results for STA, GSMPs and STPNs.} }

@article{BVdB-ijfcs18, publisher = {World Scientific}, journal = {International Journal of Foundations of Computer Science}, author = {Berwanger, Dietmar and {van den Bogaard}, Marie}, title = {Consensus Game Acceptors and Iterated Transductions}, volume = {29}, number = {02}, pages = {165-185}, year = {2018}, month = feb, doi = {10.1142/S0129054118400026}, url = {https://www.worldscientific.com/doi/abs/10.1142/S0129054118400026}, abstract = {We study a game for recognising formal languages, in which two players with imperfect information should coordinate on a common decision, given private input words correlated by a finite graph. The players have a common objective to avoid an inadmissible decision, in spite of the uncertainty induced by the input. We show that the acceptor model based on consensus games characterises context-sensitive languages. Further, we describe the expressiveness of these games in terms of iterated synchronous transductions and identify a subclass that characterises context-free languages.}, pdf = {http://www.lsv.fr/~dwb/consensus.pdf} }

@article{BM-icomp17, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Berwanger, Dietmar and Mathew, Anup Basil}, title = {Infinite games with finite knowledge gaps}, volume = {254}, pages = {217-237}, year = {2017}, month = jun, url = {https://doi.org/10.1016/j.ic.2016.10.009}, doi = {10.1016/j.ic.2016.10.009}, abstract = {Infinite games where several players seek to coordinate under imperfect information are deemed to be undecidable, unless the information is hierarchically ordered among the players. We identify a class of games for which joint winning strategies can be constructed effectively without restricting the direction of information flow. Instead, our condition requires that the players attain common knowledge about the actual state of the game over and over again along every play. We show that it is decidable whether a given game satisfies the condition, and prove tight complexity bounds for the strategy synthesis problem under ω-regular winning conditions given by deterministic parity automata.}, pdf = {http://lsv.fr/~dwb/rec.pdf} }

@article{BMVdB-acta17, publisher = {Springer}, journal = {Acta Informatica}, author = {Berwanger, Dietmar and Mathew, Anup Basil and {van den Bogaard}, Marie}, title = {Hierarchical information and the synthesis of distributed strategies}, year = {2017}, month = jun, url = {https://doi.org/10.1007/s00236-017-0306-5}, doi = {10.1007/s00236-017-0306-5}, abstract = {Infinite games with imperfect information are known to be undecidable unless the information flow is severely restricted. One fundamental decidable case occurs when there is a total ordering among players, such that each player has access to all the information that the following ones receive. In this paper we consider variations of this hierarchy principle for synchronous games with perfect recall, and identify new decidable classes for which the distributed synthesis problem is solvable with finite-state strategies. In particular, we show that decidability is maintained when the information hierarchy may change along the play, or when transient phases without hierarchical information are allowed. Finally, we interpret our result in terms of distributed system architectures.}, pdf = {http://lsv.fr/~dwb/hi.pdf} }

@inproceedings{BR-sr17, address = {Liverpool, UK}, month = jul, editor = {{van der Hoek}, Wiebe and Maubert, Bastien and Murano, Aniello and Rubin, Sasha}, acronym = {{SR}'17}, booktitle = {{P}roceedings of the 5th International Workshop on Strategic Reasoning ({SR}'17)}, author = {Dietmar Berwanger and R. Ramanujam}, title = {{Deviator Detection under Imperfect Monitoring}}, year = {2017}, url = {https://arxiv.org/abs/1712.09686}, pdf = {https://arxiv.org/pdf/1712.09686.pdf}, abstract = {Grim-trigger strategies are a fundamental mechanism for sustaining equilibria in iterated games: the players cooperate along an agreed path, and as soon as one player deviates, the others form a coalition to play him down to his minmax level. A precondition to triggering such a strategy is that the identity of the deviating player becomes common knowledge among the other players. This can be difficult or impossible to attain in games where the information structure allows only imperfect monitoring of the played actions or of the global state. We study the problem of synthesising finite-state strategies for detecting the deviator from an agreed strategy profile in games played on finite graphs with different information structures. We show that the problem is undecidable in the general case where the global state cannot be monitored. On the other hand, we prove that under perfect monitoring of the global state and imperfect monitoring of actions, the problem becomes decidable, and we present an effective synthesis procedure that covers infinitely repeated games with private monitoring.} }

@inproceedings{DGK-lics18, address = {Oxford, UK}, publisher = {ACM Press}, editor = {Hofmann, Martin and Dawar, Anuj and Gr{\"a}del, Erich}, acronym = {{LICS}'18}, booktitle = {{P}roceedings of the 33rd {A}nnual {ACM\slash IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'18)}, author = {Dave, Vrunda and Gastin, Paul and Krishna, Shankara Narayanan}, month = jul, title = {{Regular Transducer Expressions for Regular Transformations}}, year = {2018}, url = {https://arxiv.org/abs/1802.02094}, pdf = {https://arxiv.org/pdf/1802.02094.pdf}, pages = {315-324}, doi = {10.1145/3209108.3209182}, abstract = {Functional MSO transductions, deterministic two-way transducers, as well as streaming string transducers are all equivalent models for regular functions. In this paper, we show that every regular function, either on finite words or on infinite words, captured by a deterministic two-way transducer, can be described with a regular transducer expression (RTE). For infinite words, the transducer uses Muller acceptance and \(\omega\)-regular look-ahead. RTEs are constructed from constant functions using the combinators if-then-else (deterministic choice), Hadamard product, and unambiguous versions of the Cauchy product, the 2-chained Kleene-iteration and the 2-chained omega-iteration. Our proof works for transformations of both finite and infinite words, extending the result on finite words of Alur et al. in LICS'14. In order to construct an RTE associated with a deterministic two-way Muller transducer with look-ahead, we introduce the notion of transition monoid for such two-way transducers where the look-ahead is captured by some backward deterministic Büchi automaton. Then, we use an unambiguous version of Imre Simon's famous forest factorization theorem in order to derive a ''good'' (\(\omega\)-)regular expression for the domain of the two-way transducer. ''Good'' expressions are unambiguous and Kleene-plus as well as \(\omega\)-iterations are only used on subexpressions corresponding to idempotent elements of the transition monoid. The combinator expressions are finally constructed by structural induction on the ''Good'' (\(\omega\)-)regular expression describing the domain of the transducer.} }

@inproceedings{CGR-automata18, address = {Ghent, Belgium}, month = jun, year = 2018, volume = 10875, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Jan Baetens and Martin Kutrib}, acronym = {{AUTOMATA}'18}, booktitle = {{P}roceedings of the 24th Annual International Workshop on Cellular Automata and Discrete Complex Systems ({AUTOMATA}'18)}, author = {Carton, Olivier and Guillon, Bruno and Reiter, Fabian}, title = {{Counter Machines and Distributed Automata}}, pages = {13-28}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CGR-automata18.pdf}, doi = {10.1007/978-3-319-92675-9\_2}, abstract = {We prove the equivalence of two classes of counter machines and one class of distributed automata. Our counter machines operate on finite words, which they read from left to right while incrementing or decrementing a fixed number of counters. The two classes differ in the extra features they offer: one allows to copy counter values, whereas the other allows to compute copyless sums of counters. Our distributed automata, on the other hand, operate on directed path graphs that represent words. All nodes of a path synchronously execute the same finite-state machine, whose state diagram must be acyclic except for self-loops, and each node receives as input the state of its direct predecessor. These devices form a subclass of linear-time one-way cellular automata.} }

@techreport{BBFHP-hal18, author = {Barbot, Beno{\^i}t and Beccuti, Marco and Franceschinis, Giuliana and Haddad, Serge and Picaronny, Claudine}, institution = {HAL-Inria}, month = mar, number = {hal-01726011}, type = {Research Report}, title = {Bounds Computation for Symmetric Nets}, year = {2018}, url = {https://hal.inria.fr/hal-01726011}, pdf = {https://hal.inria.fr/hal-01726011/file/main.pdf}, abstract = {Monotonicity in Markov chains is the starting point for quantitative abstraction of complex probabilistic systems leading to (upper or lower) bounds for probabilities and mean values relevant to their analysis. While numerous case studies exist in the literature, there is no generic model for which monotonicity is directly derived from its structure. Here we propose such a model and formalize it as a subclass of Stochastic Symmetric (Petri) Nets (SSNs) called Stochastic Monotonic SNs (SMSNs). On this subclass the monotonicity is proven by coupling arguments that can be applied on an abstract description of the state (symbolic marking). Our class includes both process synchronizations and resource sharings and can be extended to model open or cyclic closed systems. Automatic methods for transforming a non monotonic system into a monotonic one matching the MSN pattern, or for transforming a monotonic system with large state space into one with reduced state space are presented. We illustrate the interest of the proposed method by expressing standard monotonic models and modelling a flexible manufacturing system case study.} }

@article{GM-softc18, publisher = {Springer}, journal = {Soft Computing}, author = {Gastin, Paul and Monmege, Benjamin}, title = {{A unifying survey on weighted logics and weighted automata}}, volume = {22}, number = {4}, year = {2018}, month = feb, pages = {1047-1065}, doi = {10.1007/s00500-015-1952-6}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/softc2016-GM.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/softc2016-GM.pdf}, abstract = {Logical formalisms equivalent to weighted automata have been the topic of numerous research papers in the recent years. It started with the seminal result by Droste and Gastin on weighted logics over semirings for words. It has been extended in two dimensions by many authors. First, the weight domain has been extended to valuation monoids, valuation structures, etc. to capture more quantitative properties. Along another dimension, different structures such as ranked or unranked trees, nested words, Mazurkiewicz traces, etc. have been considered. The long and involved proofs of equivalences in all these papers are implicitly based on the same core arguments. This article provides a meta-theorem which unifies these different approaches. Towards this, we first revisit weighted automata by defining a new semantics for them in two phases---an abstract semantics based on multisets of weight structures (independent of particular weight domains) followed by a concrete semantics. Then, we introduce a core weighted logic with a minimal number of features and a simplified syntax, and lift the new semantics to this logic. We show at the level of the abstract semantics that weighted automata and core weighted logic have the same expressive power. Finally, we show how previous results can be recovered from our result by logical reasoning. In this paper, we prove the meta-theorem for words, ranked and unranked trees, showing the robustness of our approach.} }

@phdthesis{Carlier-phd2017, author = {Carlier, Pierre}, title = {{Verification of Stochastic Timed Automata}}, school = {{Ecole Normale Sup{\'e}rieure de Cachan (ENS Paris-Saclay) and Universit{\'e} de Mons}}, type = {Th{\`e}se de doctorat}, year = 2017, month = dec, url = {https://tel.archives-ouvertes.fr/tel-01696130}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/carlier-phd2017.pdf} }

@inproceedings{DLM-pnse16, address = {Torun, Poland}, month = jun, year = 2016, volume = 1591, series = {CEUR Workshop Proceedings}, publisher = {CEUR-WS.org}, editor = {Lawrence Cabac and Lars Michael Kristensen and Heiko R{\"o}lke:}, acronym = {{PNSE}'16}, booktitle = {{P}roceedings of the 10th {I}nternational {W}orkshop on {P}etri {N}ets and {S}oftware {E}ngineering ({PNSE}'16)}, author = {Alban Linard and Beno{\^{\i}}t Barbot and Didier Buchs and Maximilien Colange and Cl{\'{e}}ment D{\'{e}}moulins and Lom{-}Messan Hillah and Alexis Martin}, title = {Layered Data: {A} Modular Formal Definition without Formalisms}, pages = {287-306}, url = {http://ceur-ws.org/Vol-1591/}, pdf = {http://ceur-ws.org/Vol-1591/paper19.pdf}, abstract = {Defining formalisms and models in a modular way is a painful task. Metamodeling tools and languages have usually not been created with this goal in mind. This article proposes a data structure, called layered data, that allows defining easily modular abstract syntax for for- malisms and models. It also shows its use through an exhaustive example. As a side effect, this article discusses the notion of formalism, and asserts that they do not exist as standalone objects, but rather as relations between models.} }

@inproceedings{B-fossacs18, address = {Thessaloniki, Greece}, month = apr, year = 2018, volume = {10803}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Baier, Christel and {Dal Lago}, Ugo}, acronym = {{FoSSaCS}'18}, booktitle = {{P}roceedings of the 21st {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'18)}, author = {Bouyer, Patricia}, title = {Games on graphs with a public signal monitoring}, pages = {530-547}, url = {https://arxiv.org/abs/1710.07163}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/B-fossacs18.pdf}, doi = {10.1007/978-3-319-89366-2_29}, abstract = {We study Nash equilibria in games on graphs with an imperfect monitoring based on a public signal. In such games, deviations and players responsible for those deviations can be hard to detect and track. We propose a generic epistemic game abstraction, which conveniently allows to represent the knowledge of the players about these deviations, and give a characterization of Nash equilibria in terms of winning strategies in the abstraction. We then use the abstraction to develop algorithms for some payoff functions.} }

@inproceedings{BBM-fsttcs19, address = {Bombay, India}, month = dec, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Arkadev Chattopadhyay and Paul Gastin}, acronym = {{FSTTCS}'19}, booktitle = {{P}roceedings of the 39th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'19)}, author = {Nathalie Bertrand and Patricia Bouyer and Anirban Majumdar}, title = {Concurrent parameterized games}, pages = {31:1-31:15}, year = 2019, doi = {10.4230/LIPIcs.FSTTCS.2019.31}, pdf = {https://drops.dagstuhl.de/opus/volltexte/2019/11593/pdf/LIPIcs-FSTTCS-2019-31.pdf}, url = {https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11593}, abstract = {Traditional concurrent games on graphs involve a fixed number of players, who take decisions simultaneously, determining the next state of the game. In this paper, we introduce a parameterized variant of concurrent games on graphs, where the parameter is precisely the number of players. Parameterized concurrent games are described by finite graphs, in which the transitions bear regular languages to describe the possible move combinations that lead from one vertex to another. We consider the problem of determining whether the first player, say Eve, has a strategy to ensure a reachability objective against any strategy profile of her opponents as a coalition. In particular Eve's strategy should be independent of the number of opponents she actually has. Technically, this paper focuses on an a priori simpler setting where the languages labeling transitions only constrain the number of opponents (but not their precise action choices). These constraints are described as semilinear sets, finite unions of intervals, or intervals. We establish the precise complexities of the parameterized reachability game problem, ranging from PTIME-complete to PSPACE-complete, in a variety of situations depending on the contraints (semilinear predicates, unions of intervals, or intervals) and on the presence or not of non-determinism.} }

@article{BQS-lmcs19, journal = {Logical Methods in Computer Science}, author = {Bollig, Benedikt and Quaas, Karin and Sangnier, Arnaud}, title = {The Complexity of Flat Freeze LTL}, volume = {15}, number = {3}, pages = {32:1-32:26}, year = 2019, doi = {10.23638/LMCS-15(3:32)2019}, pdf = {https://lmcs.episciences.org/5795/pdf}, url = {https://arxiv.org/abs/1609.06124}, abstract = {We consider the model-checking problem for freeze LTL on one-counter automata (OCA). Freeze LTL extends LTL with the freeze quantifier, which allows one to store different counter values of a run in registers so that they can be compared with one another. As the model-checking problem is undecidable in general, we focus on the flat fragment of freeze LTL, in which the usage of the freeze quantifier is restricted. In a previous work, Lechner et al. showed that model checking for flat freeze LTL on OCA with binary encoding of counter updates is decidable and in 2NEXPTIME. In this paper, we prove that the problem is, in fact, NEXPTIME-complete no matter whether counter updates are encoded in unary or binary. Like Lechner et al., we rely on a reduction to the reachability problem in OCA with parameterized tests (OCA(P)). The new aspect is that we simulate OCA(P) by alternating two-way automata over words. This implies an exponential upper bound on the parameter values that we exploit towards an NP algorithm for reachability in OCA(P) with unary updates. We obtain our main result as a corollary. As another application, relying on a reduction by Bundala and Ouaknine, one obtains an alternative proof of the known fact that reachability in closed parametric timed automata with one parametric clock is in NEXPTIME.} }

@inproceedings{GMG-dlt19, address = {Warsaw, Poland}, month = aug, volume = {11647}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Piotrek Hofman and Micha\l Skrzypczak}, acronym = {{DLT}'19}, booktitle = {{P}roceedings of the 23th {I}nternational {C}onference on {D}evelopments in {L}anguage {T}heory ({DLT}'19)}, author = {Paul Gastin and Amaldev Manuel and R. Govind}, title = {Logics for Reversible Regular Languages and Semigroups with Involution}, pages = {182-191}, doi = {10.1007/978-3-030-24886-4_13}, year = 2019, pdf = {https://arxiv.org/pdf/1907.01214.pdf}, url = {https://arxiv.org/abs/1907.01214}, abstract = {We present MSO and FO logics with predicates ``between'' and ``neighbour'' that characterise various fragments of the class of regular languages that are closed under the reverse operation. The standard connections that exist between MSO and FO logics and varieties of finite semigroups extend to this setting with semigroups extended with an involution. The case is different for FO with neighbour relation where we show that one needs additional equations to characterise the class.} }

@inproceedings{Gastin-cai19, address = {Ni{\u s}, Serbia}, month = jun, volume = 11545, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Miroslav {\'C}iri{\'c} and Manfred Droste and Jean-{\'E}ric Pin}, acronym = {{CAI}'19}, booktitle = {{P}roceedings of the 8th {I}nternational {C}onference on {A}lgebraic {I}nformatics ({CAI}'19)}, author = {Gastin, Paul}, title = {Modular Descriptions of Regular Functions}, pages = {3-9}, note = {Invited talk}, year = 2019, pdf = {https://arxiv.org/abs/1908.01137}, doi = {10.1007/978-3-030-21363-3_1}, abstract = {We discuss various formalisms to describe string-to-string transformations. Many are based on automata and can be seen as operational descriptions, allowing direct implementations when the input scanner is deterministic. Alternatively, one may use more human friendly descriptions based on some simple basic transformations (e.g., copy, duplicate, erase, reverse) and various combinators such as function com- position or extensions of regular operations.} }

@inproceedings{GMS-cav19, address = {New York, USA}, month = jul, volume = {11561}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Isil Dillig and Serdar Tasiran}, acronym = {{CAV}'19}, booktitle = {{P}roceedings of the 31st {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'19)}, author = {Paul Gastin and Sayan Mukherjee and B. Srivathsan}, title = {Fast algorithms for handling diagonal constraints in timed automata}, pages = {41-59}, year = 2019, doi = {10.1007/978-3-030-25540-4_3}, pdf = {https://arxiv.org/pdf/1904.08590.pdf}, url = {https://arxiv.org/abs/1904.08590} }

@inproceedings{BBM-mfcs19, address = {Aachen, Germany}, month = aug, volume = {138}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Pinar Heggernes and Joost-Pieter Katoen and Peter Rossmanith}, acronym = {{MFCS}'19}, booktitle = {{P}roceedings of the 42nd {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'19)}, author = {Manfred Droste and Paul Gastin}, title = {Aperiodic Weighted Automata and Weighted First-Order Logic}, pages = {76:1-76:15}, year = 2019, doi = {10.4230/LIPIcs.MFCS.2019.76}, pdf = {http://drops.dagstuhl.de/opus/volltexte/2019/11020/pdf/LIPIcs-MFCS-2019-76.pdf}, url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11020} }

@inproceedings{BT-mfcs19, address = {Aachen, Germany}, month = aug, volume = {138}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Pinar Heggernes and Joost-Pieter Katoen and Peter Rossmanith}, acronym = {{MFCS}'19}, booktitle = {{P}roceedings of the 42nd {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'19)}, author = {Patricia Bouyer and Nathan Thomasset}, title = {Nash equilibria in games over graphs equipped with a communication mechanism}, pages = {9:1-9:14}, year = 2019, doi = {10.4230/LIPIcs.MFCS.2019.9}, pdf = {http://drops.dagstuhl.de/opus/volltexte/2019/10953/pdf/LIPIcs-MFCS-2019-9.pdf}, url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=10953} }

@inproceedings{BBM-concur19, address = {Amsterdam, The Netherlands}, month = aug, volume = {140}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Wan Fokkink and Rob {van Glabbeek}}, acronym = {{CONCUR}'19}, booktitle = {{P}roceedings of the 30th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'19)}, author = {Nathalie Bertrand and Patricia Bouyer and Anirban Majumdar}, title = {Reconfiguration and message losses in parameterized broadcast networks}, pages = {32:1-32:15}, year = 2019, doi = {10.4230/LIPIcs.CONCUR.2019.32}, pdf = {http://drops.dagstuhl.de/opus/volltexte/2019/10934/pdf/LIPIcs-CONCUR-2019-32.pdf}, url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=10934} }

@article{GBM-tocsys19, publisher = {Springer}, journal = {Theory of Computing Systems}, author = {Gardy, Patrick and Bouyer, Patricia and Markey, Nicolas}, title = {Dependences in Strategy Logic}, volume = {64}, number = {3}, year = 2020, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GBM-tocsys19.pdf}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GBM-tocsys19.pdf} }

@inproceedings{BKMMMP-ijcai19, futureaddress = {}, month = jul, publisher = {IJCAI organization}, editor = {Kraus, Sarit}, acronym = {{IJCAI}'19}, booktitle = {{P}roceedings of the 28th {I}nternational {J}oint {C}onference on {A}rtificial {I}ntelligence ({IJCAI}'19)}, author = {Bouyer, Patricia and Kupferman, Orna and Markey, Nicolas and Maubert, Bastien and Murano, Aniello and Perelli, Giuseppe}, title = {Reasoning about Quality and Fuzziness of Strategic Behaviours}, pages = {1588-1594}, year = 2019, doi = {10.24963/ijcai.2019/220}, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKMMMP-ijcai19.pdf}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BKMMMP-ijcai19.pdf} }

@inproceedings{Fortin-icalp19, address = {Patras, Greece}, month = jul, volume = {132}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Chatzigiannakis, Ioannis and Merelli, Emanuela}, acronym = {{ICALP}'19}, booktitle = {{P}roceedings of the 46th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'19)}, author = {Fortin, Marie}, title = {FO = FO3 for linear orders with monotone binary relations}, year = 2019, pages = {116:1-116:13}, doi = {10.4230/LIPIcs.ICALP.2019.116}, pdf = {http://drops.dagstuhl.de/opus/volltexte/2019/10692/pdf/LIPIcs-ICALP-2019-116.pdf}, url = {http://drops.dagstuhl.de/opus/volltexte/2019/10692/}, abstract = {We show that over the class of linear orders with additional binary relations satisfying some monotonicity conditions, monadic first-order logic has the three-variable property. This generalizes (and gives a new proof of) several known results, including the fact that monadic first-order logic has the three-variable property over linear orders, as well as over (R, <, +1), and answers some open questions mentioned in a paper from Antonopoulos, Hunter, Raza and Worrell [FoSSaCS 2015]. Our proof is based on a translation of monadic first-order logic formulas into formulas of a star-free variant of Propositional Dynamic Logic, which are in turn easily expressible in monadic first-order logic with three variables.} }

@inproceedings{AGJK-lics19, address = {Vancouver, Canada}, month = jun, publisher = {{IEEE} Press}, editor = {Bouyer, Patricia}, acronym = {{LICS}'19}, booktitle = {{P}roceedings of the 34th {A}nnual {ACM\slash IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'19)}, author = {Akshay, S. and Gastin, Paul and Jug{\'e}, Vincent and Krishna, Shankara Narayanan}, title = {Timed systems through the lens of logic}, pages = {1-13}, year = 2019, doi = {10.1109/LICS.2019.8785684}, pdf = {https://arxiv.org/pdf/1903.03773.pdf}, url = {https://arxiv.org/abs/1903.03773}, abstract = {In this paper, we analyze timed systems with data structures, using a rich interplay of logic and properties of graphs. We start by describing behaviors of timed systems using graphs with timing constraints. Such a graph is called realizable if we can assign time-stamps to nodes or events so that they are consistent with the timing constraints. The logical definability of several graph properties has been a challenging problem, and we show, using a highly non-trivial argument, that the realizability property for collections of graphs with strict timing constraints is logically definable in a class of propositional dynamic logic (EQ-ICPDL), which is strictly contained in MSO. Using this result, we propose a novel, algorithmically efficient and uniform proof technique for the analysis of timed systems enriched with auxiliary data structures, like stacks and queues. Our technique unravels new results (for emptiness checking as well as model checking) for timed systems with richer features than considered so far, while also recovering existing results.} }

@inproceedings{CD-lics19, address = {Vancouver, Canada}, month = jun, publisher = {{IEEE} Press}, editor = {Bouyer, Patricia}, acronym = {{LICS}'19}, booktitle = {{P}roceedings of the 34th {A}nnual {ACM\slash IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'19)}, author = {Chatterjee, Krishnendu and Doyen, Laurent}, title = {Graph Planning with Expected Finite Horizon}, pages = {1-13}, year = 2019, doi = {10.1109/LICS.2019.8785706}, abstract = {Graph planning gives rise to fundamental algorithmic questions such as shortest path, traveling salesman problem, etc. A classical problem in discrete planning is to consider a weighted graph and construct a path that maximizes the sum of weights for a given time horizon T. However, in many scenarios, the time horizon is not fixed, but the stopping time is chosen according to some distribution such that the expected stopping time is T. If the stopping time distribution is not known, then to ensure robustness, the distribution is chosen by an adversary, to represent the worst-case scenario. A stationary plan for every vertex always chooses the same outgoing edge. For fixed horizon or fixed stopping-time distribution, stationary plans are not sufficient for optimality. Quite surprisingly we show that when an adversary chooses the stopping-time distribution with expected stopping time T, then stationary plans are sufficient. While computing optimal stationary plans for fixed horizon is NP-complete, we show that computing optimal stationary plans under adversarial stopping-time distribution can be achieved in polynomial time. Consequently, our polynomial-time algorithm for adversarial stopping time also computes an optimal plan among all possible plans.} }

@inproceedings{BBR-fossacs19, address = {Prague, Czech Republic}, month = apr, year = 2019, volume = {11425}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Boja{\'n}czyk, Mikolaj and Simpson, Alex}, acronym = {{FoSSaCS}'19}, booktitle = {{P}roceedings of the 22nd {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'19)}, author = {Benedikt Bollig and Patricia Bouyer and Fabian Reiter}, title = {Identifiers in Registers - Describing Network Algorithms with Logic}, pages = {115-132}, url = {https://arxiv.org/abs/1811.08197}, pdf = {https://arxiv.org/pdf/1811.08197.pdf}, doi = {10.1007/978-3-030-17127-8}, abstract = {We propose a formal model of distributed computing based on register automata that captures a broad class of synchronous network algorithms. The local memory of each process is represented by a finite-state controller and a fixed number of registers, each of which can store the unique identifier of some process in the network. To underline the naturalness of our model, we show that it has the same expressive power as a certain extension of first-order logic on graphs whose nodes are equipped with a total order. Said extension lets us define new functions on the set of nodes by means of a so-called partial fixpoint operator. In spirit, our result bears close resemblance to a classical theorem of descriptive complexity theory that characterizes the complexity class PSPACE in terms of partial fixpoint logic (a proper superclass of the logic we consider here).} }

@inproceedings{BKMMMP-ecai20, address = {Santiago de Compostela, Spain}, month = sep, optvolume = {??}, optseries = {Frontiers in Artificial Intelligence and Applications}, publisher = {{IOS} Press}, editor = {Lang, J{\'e}r{\^o}me and De Giacomo, Giuseppe and Barro and Sen{\'e}n Barro and O'Sullivan, Barry}, acronym = {{ECAI}'20}, booktitle = {{P}roceedings of the 24th {E}uropean {C}onference on {A}rtificial {I}ntelligence ({ECAI}'20)}, author = {Patricia Bouyer and Orna Kupferman and Nicolas Markey and Bastien Maubert and Aniello Murano and Giuseppe Perelli}, title = {{Reasoning About Quality and Fuzziness of Strategic Behaviours}}, pages = {2887-2888}, year = 2020, pdf = {https://ebooks.iospress.nl/publication/55232}, url = {https://ebooks.iospress.nl/publication/55232}, doi = {10.3233/FAIA200437} }

@techreport{JFA-arxiv20, author = {Jawher Jerray and Laurent Fribourg and {\'E}tienne Andr{\'e}}, institution = {Computing Research Repository}, month = june, number = {2006.09993}, type = {Research Report}, title = {{Guaranteed phase synchronization of hybrid oscillators using symbolic Euler's method: The Brusselator and biped examples}}, year = {2020}, url = {https://arxiv.org/abs/2006.09993}, pdf = {https://arxiv.org/abs/2006.09993} }

@techreport{JFA-arxiv20bis, author = {Jawher Jerray and Laurent Fribourg and {\'E}tienne Andr{\'e}}, institution = {Computing Research Repository}, month = july, number = {2007.13644}, type = {Research Report}, title = {{Robust optimal control using dynamic programming and guaranteed Euler's method}}, year = {2020}, url = {https://arxiv.org/abs/2007.13644}, pdf = {https://arxiv.org/abs/2007.13644} }

@techreport{JF-arxiv20, author = {Jawher Jerray and Laurent Fribourg}, institution = {Computing Research Repository}, month = december, number = {2012.09310}, type = {Research Report}, title = {{Generation of bounded invariants via stroboscopic set-valued maps: Application to the stability analysis of parametric time-periodic systems}}, year = {2020}, url = {https://arxiv.org/abs/2012.09310}, pdf = {https://arxiv.org/abs/2012.09310} }

@inproceedings{LeRoux-cie2020, address = {Fisciano, Italy}, month = june, year = 2020, volume = 12098, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, editor = {Marcella Anselmo and Gianluca Della Vedova and Florin Manea and Arno Pauly }, acronym = {{CiE}'20}, booktitle = {{P}roceedings of the 16th {C}onference on {C}omputability in {E}urope ({CiE 2020})}, author = {Le Roux, St{\'e}phane}, title = {{Time-Aware Uniformization of Winning Strategies}}, pages = {193-204}, url = {https://link.springer.com/chapter/10.1007%2F978-3-030-51466-2_17}, pdf = {https://link.springer.com/chapter/10.1007%2F978-3-030-51466-2_17}, doi = {https://doi.org/10.1007/978-3-030-51466-2_17} }

@article{BLRPR-ic21, author = {Bruy{\`e}re, V{\'e}ronique and Le Roux, St{\'e}phane and Pauly, Arno and Raskin, Jean{-}Fran{\c{c}}ois}, title = {On the existence of weak subgame perfect equilibria}, volume = {276}, year = 2021, doi = {https://doi.org/10.1016/j.ic.2020.104553}, url = {https://www.sciencedirect.com/science/article/pii/S0890540120300419?via%3Dihub} }

@article{BBFLMR-fac21, publisher = {Springer}, journal = {Formal Aspects of Computing}, author = {Bacci, Giovanni and Bouyer, Patricia and Fahrenberg, Uli and Larsen, Kim and Markey, Nicolas and Reynier, Pierre{-}Alain}, title = {Optimal and robust controller synthesis using energy timed automata with uncertainty}, volume = {33}, pages = {3--25}, year = 2021, doi = {10.1007/s00165-020-00521-4}, url = {https://link.springer.com/article/10.1007/s00165-020-00521-4} }

@phdthesis{fortin-phd2020, author = {Fortin, Marie}, title = {{Expressivity of first-order logic, star-free propositional dynamic logic and communicating automata}}, school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France}, type = {Th{\`e}se de doctorat}, year = 2020, month = nov, url = {https://tel.archives-ouvertes.fr/tel-03079438}, pdf = {https://tel.archives-ouvertes.fr/tel-03079438/document} }

@inproceedings{BRS-csl21, address = {Ljubljana, Slovenia}, month = jan, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Baier, Christel and Goubault{-}Larrecq, Jean}, acronym = {{CSL}'21}, booktitle = {{P}roceedings of the 29th {A}nnual {EACSL} {C}onference on {C}omputer {S}cience {L}ogic ({CSL}'21)}, author = {Benedikt Bollig and Fedor Ryabinin and Arnaud Sangnier}, title = {Reachability in Distributed Memory Automata}, pages = {13:1-13:16}, year = {2021}, doi = {10.4230/LIPIcs.CSL.2021.13}, pdf = {https://drops.dagstuhl.de/opus/volltexte/2021/13447/}, url = {https://drops.dagstuhl.de/opus/volltexte/2021/13447/} }

@inproceedings{BBM-fsttcs20, address = {Goa, India}, month = dec, volume = {182}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Nitin Saxena and Sunil Simon}, acronym = {{FSTTCS}'20}, booktitle = {{P}roceedings of the 40th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'20)}, author = {Nathalie Bertrand and Patricia Bouyer and Anirban Majumdar}, title = {Synthesizing safe coalition strategies}, pages = {39:1--39:17}, year = {2020}, doi = {https://doi.org/10.4230/LIPIcs.FSTTCS.2020.39}, pdf = {https://drops.dagstuhl.de/opus/volltexte/2020/13280/pdf/LIPIcs-FSTTCS-2020-39.pdf}, url = {https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=13280} }

@inproceedings{BBRRV-fsttcs20, address = {Goa, India}, month = dec, volume = {182}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Nitin Saxena and Sunil Simon}, acronym = {{FSTTCS}'20}, booktitle = {{P}roceedings of the 40th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'20)}, author = {Paul Gastin and Sayan Mukherjee and B Srivathsan}, title = {Reachability for updatable timed automata made faster and more effective}, pages = {47:1--47:17}, year = {2020}, doi = {https://doi.org/10.4230/LIPIcs.FSTTCS.2020.47}, pdf = {https://drops.dagstuhl.de/opus/volltexte/2020/13288/pdf/LIPIcs-FSTTCS-2020-47.pdf}, url = {https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=13288} }

@inproceedings{AG-fsttcs20, address = {Goa, India}, month = dec, volume = {182}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Nitin Saxena and Sunil Simon}, acronym = {{FSTTCS}'20}, booktitle = {{P}roceedings of the 40th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'20)}, author = {C. Aiswarya and Paul Gastin}, title = {Weighted Tiling Systems for Graphs: Evaluation Complexity}, year = {2020}, doi = {https://doi.org/10.4230/LIPIcs.FSTTCS.2020.34}, pdf = {https://drops.dagstuhl.de/opus/volltexte/2020/13275/pdf/LIPIcs-FSTTCS-2020-34.pdf}, url = {https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=13275} }

@inproceedings{BBRRV-gandalf20, address = {Brussels, Belgium}, month = sep, volume = {326}, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Bresolin, Davide and Raskin, Jean-Fran\c{c}ois}, acronym = {{GandALF}'20}, booktitle = {{P}roceedings of the 11th {I}nternational {S}ymposium on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification ({GandALF}'20)}, author = {Bouyer, Patricia and Brihaye, Thomas and Randour, Mickael and Rivi{\`e}re, C{\'e}dric and Vandenhove, Pierre}, title = {Decisiveness of Stochastic Systems and its Application to Hybrid Models}, pages = {149?165}, year = {2020}, doi = {10.4204/EPTCS.326.10}, pdf = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?GANDALF2020.10.pdf}, url = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?GANDALF2020.10} }

@inproceedings{BBBFS-gandalf20, address = {Brussels, Belgium}, month = sep, volume = {326}, series = {Electronic Proceedings in Theoretical Computer Science}, editor = {Bresolin, Davide and Raskin, Jean-Fran\c{c}ois}, acronym = {{GandALF}'20}, booktitle = {{P}roceedings of the 11th {I}nternational {S}ymposium on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification ({GandALF}'20)}, author = {B{\'e}atrice B{\'e}rard and Benedikt Bollig and Patricia Bouyer and Matthias F{\"u}gger and Nathalie Sznajder}, title = {Synthesis in Presence of Dynamic Links}, pages = {33?49}, year = {2020}, doi = {10.4204/EPTCS.326.3}, pdf = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?GANDALF2020.3.pdf}, url = {http://eptcs.web.cse.unsw.edu.au/paper.cgi?GANDALF2020.3} }

@inproceedings{DFG-mfcs20, address = {Prague, Czech Republic}, month = aug, volume = {170}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Javier Esparza and Dan Kr{\'a}l}, acronym = {{MFCS}'20}, booktitle = {{P}roceedings of the 43rd {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'20)}, author = {Dou{\'e}neau-Tabot, Ga{\"e}tan and Filiot, Emmanuel and Gastin, Paul}, title = {Register transducers are marble transducers}, pages = {29:1--29:14}, year = 2020, doi = {https://doi.org/10.4230/LIPIcs.MFCS.2020.29}, pdf = {https://drops.dagstuhl.de/opus/volltexte/2020/12697/pdf/LIPIcs-MFCS-2020-29.pdf}, url = {https://drops.dagstuhl.de/opus/volltexte/2020/12697/} }

@inproceedings{BLORV-concur20, address = {Vienna, Austria}, month = sep, volume = {171}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Igor Konnov and Laura Kovacs}, acronym = {{CONCUR}'20}, booktitle = {{P}roceedings of the 31st {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'20)}, author = {Bouyer, Patricia and Le Roux, St{\'e}phane and Oualhadj, Youssouf and Randour, Mickael and Vandenhove, Pierre}, title = {Games Where You Can Play Optimally with Arena-Independent Finite Memory}, pages = {24:1--24:22}, year = 2020, doi = {10.4230/LIPIcs.CONCUR.2020.24}, url = {https://drops.dagstuhl.de/opus/volltexte/2020/12836} }

@inproceedings{AGSW-concur20, address = {Vienna, Austria}, month = sep, volume = {171}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Igor Konnov and Laura Kovacs}, acronym = {{CONCUR}'20}, booktitle = {{P}roceedings of the 31st {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'20)}, author = {Bharat Adsul and Paul Gastin and Saptarshi Sarkar and Pascal Weil}, title = {Wreath/cascade products and related decomposition results for the concurrent setting of {M}azurkiewicz traces}, pages = {19:1--19:17}, year = 2020, doi = {10.4230/LIPIcs.CONCUR.2020.19}, url = {https://drops.dagstuhl.de/opus/volltexte/2020/12831} }

@mastersthesis{m2-Doueneau, author = {Ga{\"e}tan Dou{\'e}neau-Tabot}, title = {{Register Models for Pebble Transducers and Applications to Optimization}}, school = {{M}aster {P}arisien de {R}echerche en {I}nformatique, Paris, France}, type = {Rapport de {M}aster}, year = {2019}, month = sep }

@phdthesis{jaziri-phd2019, author = {Samy Jaziri}, title = {{Automata on Timed Structures}}, school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France}, type = {Th{\`e}se de doctorat}, year = 2019, month = sep, url = {https://tel.archives-ouvertes.fr/tel-02384274}, pdf = {https://tel.archives-ouvertes.fr/tel-02384274/document} }

@phdthesis{saoud-phd2019, author = {Adnane Saoud}, title = {{Compositional and Efficient Controller Synthesis for Cyber-Physical Systems}}, school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France}, type = {Th{\`e}se de doctorat}, year = 2019, month = oct, url = {https://tel.archives-ouvertes.fr/tel-02317723}, pdf = {https://tel.archives-ouvertes.fr/tel-02317723/document} }

@phdthesis{gonzalez-phd2019, author = {Gonz{\'a}lez, Mauricio}, title = {{Stochastic Games on Graphs with Applications to Smart-Grids Optimization}}, school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France}, type = {Th{\`e}se de doctorat}, year = 2019, month = nov, url = {http://www.theses.fr/2019SACLN064}, pdf = {http://www.lsv.fr/~gonzalez/phd/Thesis_Gonzalez_V2_2.pdf} }

@article{LRP-dga20, publisher = {Springer}, journal = {Dynamic Games and Applications}, author = {Le Roux, St{\'e}phane and Pauly, Arno}, title = {A Semi-Potential for Finite and Infinite Games in Extensive Form}, volume = {10}, number = {1}, pages = {120-144}, year = 2020, doi = {10.1007/s13235-019-00301-7}, url = {https://doi.org/10.1007/s13235-019-00301-7} }

@inproceedings{AVLRM-sac20, address = {Brno, Czech Republic}, month = mar, publisher = {ACM Press}, editor = {Chih{-}Cheng Hung and Tom{\'{a}}s Cern{\'{y}} and Dongwan Shin and Alessio Bechini}, acronym = {{SAC}'20}, booktitle = {{P}roceedings of the 35th {ACM/SIGAPP} {S}ymposium on {A}pplied {C}omputing ({SAC}'20)}, author = {Nikolaos Alexopoulos and Emmanouil Vasilomanolakis and St{\'e}phane {Le Roux} and Steven Rowe and Max M{\"u}hlh{\"a}user}, title = {{TRIDEnT}: Towards a Decentralized Threat Indicator Marketplace}, pages = {332-341}, year = {2020}, doi = {10.1145/3341105.3374020}, url = {https://doi.org/10.1145/3341105.3374020} }

@inproceedings{ZSGF-ecc19, address = {Naples, Italy}, month = jun, publisher = {{IEEE} Press}, acronym = {{ECC}'19}, booktitle = {{P}roceedings of the 18th {E}uropean {C}ontrol {C}onference ({ECC}'19)}, author = {Daniele Zonetti and Adnane Saoud and Antoine Girard and Laurent Fribourg}, title = {A symbolic approach to voltage stability and power sharing in time-varying{DC} microgrids}, pages = {903-909}, year = {2019}, doi = {10.23919/ECC.2019.8796095}, url = {https://doi.org/10.23919/ECC.2019.8796095} }

@inproceedings{CF-cyphy19, address = {New York City, NY, USA}, month = oct, editor = {Roger D. Chamberlain and Martin Grimheden and Walid Taha}, volume = {11971}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, noeditor = {}, acronym = {{CyPhy/WESE}'19}, booktitle = {9th International Workshop on Cyber Physical Systems ({CyPhy}'19) and 15th International Workshop on Model-Based Design ({WESE}'19), Revised Selected Papers}, author = {Adrien {Le Co{\"{e}}nt} and Laurent Fribourg}, title = {Guaranteed Optimal Reachability Control of Reaction-Diffusion Equations Using One-Sided Lipschitz Constants and Model Reduction}, pages = {181-202}, year = {2019}, doi = {10.1007/978-3-030-41131-2_9}, url = {https://doi.org/10.1007/978-3-030-41131-2_9} }

@inproceedings{DFKN-dsd19, address = {Kallithea, Greece}, month = aug, publisher = {{IEEE} Press}, noeditor = {}, acronym = {{DSD}'19}, booktitle = {{P}roceedings of the 22nd {E}uromicro {C}onference on {D}igital {S}ystem {D}esign ({DSD}'19)}, author = {Jean{-}Luc Danger and Laurent Fribourg and Ulrich K{\"u}hne and Maha Naceur}, title = {LAOCO{\"O}N: {A} Run-Time Monitoring and Verification Approach for Hardware Trojan Detection}, pages = {269-276}, year = {2019}, doi = {10.1109/DSD.2019.00047}, url = {https://doi.org/10.1109/DSD.2019.00047} }

@inproceedings{CF-cdc19, address = {Nice, France}, month = dec, publisher = {{IEEE} Control System Society}, noeditor = {}, acronym = {{CDC}'19}, booktitle = {{P}roceedings of the 58th {IEEE} {C}onference on {D}ecision and {C}ontrol ({CDC}'19)}, author = {Adrien {Le Co{\"e}nt} and Laurent Fribourg}, title = {Guaranteed Control of Sampled Switched Systems using Semi-Lagrangian Schemes and One-Sided Lipschitz Constants}, pages = {599-604}, year = {2019}, doi = {10.1109/CDC40024.2019.9029376}, pdf = {https://arxiv.org/pdf/1903.05882.pdf}, url = {https://doi.org/10.1109/CDC40024.2019.9029376} }

@inproceedings{ACFJL-acsd19, address = {Aachen, Germany}, month = jun, publisher = {{IEEE} Computer Society Press}, editor = {J{\"o}rg Keller and Wojciech Penczek}, acronym = {{ACSD}'19}, booktitle = {{P}roceedings of the 19th {I}nternational {C}onference on {A}pplication of {C}oncurrency to {S}ystem {D}esign ({ACSD}'19)}, author = {{\'E}tienne Andr{\'e} and Emmanuel Coquard and Laurent Fribourg and Jawher Jerray and David Lesens}, title = {Parametric Schedulability Analysis of a Launcher Flight Control System Under Reactivity Constraints}, pages = {13-22}, year = {2019}, doi = {10.1109/ACSD.2019.00006}, url = {https://doi.org/10.1109/ACSD.2019.00006} }

@proceedings{CG-fsttcs2019, address = {Bombay, India}, month = dec, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Arkadev Chattopadhyay and Paul Gastin}, acronym = {{FSTTCS}'19}, booktitle = {{P}roceedings of the 39th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'19)}, title = {{P}roceedings of the 39th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'19)}, author = {Arkadev Chattopadhyay and Paul Gastin}, year = {2019}, url = {http://www.dagstuhl.de/dagpub/978-3-95977-131-3} }

@inproceedings{B-atva19, address = {Taipei, Taiwan}, month = oct, volume = {11781}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Yu{-}Fang Chen and Chih{-}Hong Cheng and Javier Esparza}, acronym = {{ATVA}'19}, booktitle = {{P}roceedings of the 17th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'19)}, author = {Patricia Bouyer}, title = {{A Note on Game Theory and Verification (Invited Talk)}}, pages = {3-22}, doi = {10.1007/978-3-030-31784-3_1}, year = 2019 }

@inproceedings{B-time19, address = {M{\'{a}}laga, Spain}, month = oct, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Johann Gamper and Sophie Pinchinat and Guido Sciavicco}, acronym = {{TIME}'19}, booktitle = {{P}roceedings of the 26th {I}nternational {S}ymposium on {T}emporal {R}epresentation and {R}easoning ({TIME}'19)}, author = {Patricia Bouyer}, title = {{On the Computation of Nash Equilibria in Games on Graphs (Invited Talk)}}, pages = {3:1-3:3}, doi = {10.4230/LIPIcs.TIME.2019.3}, year = 2019 }

@article{LRP-ic20, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Le Roux, St{\'e}phane and Pauly, Arno}, title = {Equilibria in multi-player multi-outcome infinite sequential games}, volume = {276}, year = 2021, doi = {https://doi.org/10.1016/j.ic.2020.104557}, url = {https://www.sciencedirect.com/science/article/pii/S0890540120300456?via%3Dihub} }

@article{BGHLR-ic20, publisher = {Elsevier Science Publishers}, journal = {Information and Computation}, author = {Brihaye, Thomas and Geeraerts, Gilles and Hallet, Marion and Le Roux, St{\'e}phane}, title = {On the termination of dynamics in sequential games}, volume = {272}, year = 2020, doi = {10.1016/j.ic.2019.104505} }

@inproceedings{AGKR-tacas2020, address = {Dublin, Ireland}, month = apr, volume = {12078}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Armin Biere and David Parker}, acronym = {{TACAS}'20}, booktitle = {{P}roceedings of the 26th {I}nternational {C}onference on {T}ools and {A}lgorithms for {C}onstruction and {A}nalysis of {S}ystems ({TACAS}'20)}, author = {Akshay, S. and Gastin, Paul and Krishna, Shankara Narayanan and Roychoudhary, Sparsa}, title = {Revisiting Underapproximate Reachability for Multipushdown Systems}, pages = {387--404}, doi = {10.1007/978-3-030-45190-5_21}, year = 2020, pdf = {https://arxiv.org/pdf/2002.05950.pdf}, url = {https://link.springer.com/chapter/10.1007/978-3-030-45190-5_21}, longurl = {https://arxiv.org/abs/2002.05950} }

@inproceedings{BBLS-fossacs2020, address = {Dublin, Ireland}, month = apr, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Barbara K{\"o}nig and Jean Goubault-Larrecq}, acronym = {{FoSSaCS}'20}, booktitle = {{P}roceedings of the 23rd {I}nternational {C}onference on {F}oundations of {S}oftware {S}cience and {C}omputation {S}tructures ({FoSSaCS}'20)}, author = {B{\'e}atrice B{\'e}rard and Benedikt Bollig and Mathieu Lehaut and Nathalie Sznajder}, title = {Parameterized Synthesis for Fragments of First-Order Logic over Data Words}, pages = {97--118}, doi = {10.1007/978-3-030-45231-5_6}, year = 2020 }

@inproceedings{BD-stacs2020, address = {Montpellier, France}, month = mar, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Bl{\"a}ser, Markus and Paul, Christophe}, acronym = {{STACS}'20}, booktitle = {{P}roceedings of the 37th {A}nnual {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'20)}, author = {Berwanger, Dietmar and Doyen, Laurent}, title = {Observation and Distinction. Representing Information in Infinite Games}, pages = {48:1--48:17}, doi = {10.4230/LIPIcs.STACS.2020.48}, year = 2020 }

*This file was generated by
bibtex2html 1.98.*