Modeling the consumption of limited resources, e.g., time or energy, plays a central role on the design of reactive systems such as embedded controllers. To this aim, quantitative objectives are defined on game arenas that can be easily modeled as weighted graphs. Instances of these games, calledenergy games, can be solved in${\mathcal {O}(\vert {E}\vert {\cdot }\vert {V}\vert {\cdot }W)}$where$W$is the maximum weight. Recent work has demonstrated that sequential implementations hardly solve practical instances due to their size and the number of interactions required to converge to a solution. Recent work has demonstrated that sequential implementations hardly solve practical instances. Furthermore, emerging approaches, that have investigated the parallelism of CPUs multi-core and GPU for solving theinitial credit problemfor energy games, still perform poorly due to the non-trivial characteristics of these graphs. In this article we first describe a revised version of the algorithm on multi-core CPU that obtains a faster convergence time on real-world graphs with up to 30x against the serial implementation by showing good scalability overall. Second, we provide a new GPU-based parallel implementation based on warp-level primitives that allows to reduce the time-to-solution on several instances with up to 3.6x of speed-up against traditional parallel vertex-based approaches. We also discuss a methodology to build synthetic energy games to validate the scalability of parallel algorithms on two totally different settings.

In this paper, we study the notion of adversarial Stackelberg value for two-player non-zero sum games played on bi-weighted graphs with the mean-payoff and the discounted sum functions. The adversarial Stackelberg value of Player 0 is the largest value that Player 0 can obtain when announcing her strategy to Player 1 which in turn responds with any of his best response. For the mean-payoff function, we show that the adversarial Stackelberg value is not always achievable but epsilon-optimal strategies exist. We show how to compute this value and prove that the associated threshold problem is in NP. For the discounted sum payoff function, we draw a link with the target discounted sum problem which explains why the problem is difficult to solve for this payoff function. We also provide solutions to related gap problems.

In this paper, we study the rational synthesis problem for turn-based multiplayer non zero-sum games played on finite graphs for omega-regular objectives. Rationality is formalized by the concept of Nash equilibrium (NE). Contrary to previous works, we consider here the more general and more practically relevant case where players are imperfectly informed. In sharp contrast with the perfect information case, NE are not guaranteed to exist in this more general setting. This motivates the study of the NE existence problem. We show that this problem is ExpTime-C for parity objectives in the two-player case (even if both players are imperfectly informed) and undecidable for more than 2 players. We then study the rational synthesis problem and show that the problem is also ExpTime-C for two imperfectly informed players and undecidable for more than 3 players. As the rational synthesis problem considers a system (Player 0) playing against a rational environment (composed of k players), we also consider the natural case where only Player 0 is imperfectly informed about the state of the environment (and the environment is considered as perfectly informed). In this case, we show that the ExpTime-C result holds when k is arbitrary but fixed. We also analyse the complexity when k is part of the input.

We study the computational complexity of the cooperative and non-cooperative rational synthesis problems, as introduced by Kupferman, Vardi and co-authors. We provide tight results for most of the classical omega-regular objectives, and show how to solve those problems optimally.

We consider the algorithmic problem of computing the maximal simulation preorder (and quotient) on acyclic labelled graphs. The acyclicity allows to exploit an inner structure on the set of nodes, that can be processed in stages according to a set-theoretic notion of rank. This idea, previously used for bisimulation computation, on the one hand improves on the performances of the ensuing procedure and, on the other hand, gives to the solution an orderly iterative flavour making the algorithmic idea more explicit. The computational complexity achieved is good as we obtain the best performing algorithm for simulation computation on acyclic graphs, in both time and space. © The Author, 2013. Published by Oxford University Press. All rights reserved.

Any weighted automaton (WA) defines a relation from finite words to values: given an input word, its set of values is obtained as the set of values computed by each accepting run on that word. A WA is k-valued if the relation it defines has degree at most k, i.e., every set of values associated with an input word has cardinality at most k. We investigate the class of quantitative languages defined by k-valued automata, for all parameters k. We consider several measures to associate values with runs: sum, discounted-sum, and more generally values in groups. We define a general procedure which decides, given a bound k and a WA over a group, whether this automaton is k-valued. We also show that any k-valued WA over a group, under some general conditions, can be decomposed as a union of k unambiguous WA. While inclusion and equivalence are undecidable problems for arbitrary sum-automata, we show, based on this decomposition, that they are decidable for k-valued sum-automata, and k-valued discounted sum-automata over inverted integer discount factors. We finally show that the quantitative Church problem is undecidable for k-valued sum-automata, even given as finite unions of deterministic sum-automata.

We deal with the problem of designing suitable languages for the modeling and the automatic verification of properties over analog circuits. To this purpose, we suitably enrich classical temporal logics with basic formul\ae allowing to model arbitrary functions relating analog variables. We show how to automatically check the resulting CTLf formulæ on analog circuits. In particular, we rely on interval arithmetic methods and we extend to the analog context a number of techniques for the abstraction and the verification of digital systems, based on three-valued temporal logics.