CNAM: salle 17.1.08 - comment y aller
Abstract: In concurrent systems, weak fairness (WF) intuitively states that no transition from a given set can stay enabled forever, i.e. it must eventually either fire or be disabled. In the occurrence net semantics for (safe) Petri nets known as "unfolding technique", one finds the weakly fair executions to be exactly the maximal configurations, or runs, of the system. Since weak fairness is a more-than-reasonable assumption in many real-life systems (who would bet his life on an enabled transition cluster to stay inert forever ?), it is interesting to see that WF allows to deduce logical dependencies hidden in the semantics; in particular, a binary relation "a reveals b" , expressing that any WF execution in which a occurs must also have an occurrence of b, can hold even without any direct causal chain linking a and b. The computation of this relation is effectively feasible, allowing e.g. to compact behavioral representations if WF can be assumed. Expanding to a more general, set-to-set reveals relation, we can address also "weak diagnosis"- where one asks whether a concurrent chronicle of observed events allows to determine that a non-observable fault will inevitably occur, sooner or later, on any maximal system run that is compatible with the observation - and the associated WF-diagnosability property.
Abstract: aReachability-cost games are two-player zero-sum games played on directed graphs with weights on edges, where two players take turns to choose transitions in order to optimize the total cost to reach a target set of vertices. More precisely, Player 1 wants to reach the target by minimizing its cost, whereas Player 2 wants to avoid the target, or, if not possible, maximize the cost of Player 1. When weights of edges are non-negative, polynomial algorithms are known in order to compute optimal values as well as optimal strategies for both players, see, e.g., an adaptation of Dijkstra’s shortest path algorithm by Khachiyan et al. Moreover, both players are known to have optimal memoryless strategies. The case where weights can be any integer is more complex, especially in the presence of negative cycles. Filiot, Gentilini and Raskin prove that deciding whether the value of such a game is positive can be done in $NP cap co-NP$, by using methods similar to the one used for mean-payoff games: this holds even though optimal strategies may require memory, contrary to the nonnegative case. Our contribution is threefold. First, we present a value iteration algorithm to compute the optimal values, as well as optimal strategies for both players when they exist. This iterative algorithm has a pseudo-polynomial complexity (i.e., polynomial if weights of edges are encoded in unary). We also show that Player 2 always has optimal memoryless strategies and that a memory of size pseudo-polynomial is sufficient (and sometimes necessary) for Player 1. Finally we introduce another value iteration algorithm to compute the optimal value of a total payoff game (without the reachability constraint), based on the previous algorithm.