Author name cluster

Yaron Velner

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers

1 author row

I&C Journal 2017 Journal Article

Quantitative fair simulation games

Krishnendu Chatterjee
Thomas A. Henzinger
Jan Otop
Yaron Velner

Simulation is an attractive alternative to language inclusion for automata as it is an under-approximation of language inclusion, but usually has much lower complexity. Simulation has also been extended in two orthogonal directions, namely, (1) fair simulation, for simulation over specified set of infinite runs; and (2) quantitative simulation, for simulation between weighted automata. While fair trace inclusion is PSPACE-complete, fair simulation can be computed in polynomial time. For weighted automata, the (quantitative) language inclusion problem is undecidable in general, whereas the (quantitative) simulation reduces to quantitative games, which admit pseudo-polynomial time algorithms. In this work, we study (quantitative) simulation for weighted automata with Büchi acceptance conditions, i. e. , we generalize fair simulation from non-weighted automata to weighted automata. We show that imposing Büchi acceptance conditions on weighted automata changes many fundamental properties of the simulation games, yet they still admit pseudo-polynomial time algorithms.

Details DOI

I&C Journal 2015 Journal Article

The complexity of multi-mean-payoff and multi-energy games

Yaron Velner
Krishnendu Chatterjee
Laurent Doyen
Thomas A. Henzinger
Alexander Rabinovich
Jean-François Raskin

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 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 NP ∩ coNP, whereas mean-payoff-inf objectives are coNP-complete.

Details DOI

Highlights Conference 2014 Conference Abstract

Games on Graphs with Robust Multidimensional Mean-Payoff Objectives

Yaron Velner

Two-player games on graphs provide the mathematical foundation for the study of reactive systems. In the quantitative framework, an objective assigns a value to every play, and the goal of Player 1 is to minimize the value of the objective. In this framework, there are two relevant synthesis problems to consider: the quantitative analysis problem is to compute the minimal (or infimum) value that Player 1 can assure, and the boolean analysis problem asks whether Player 1 can assure that the value of the objective is at most ν (for a given threshold ν). Mean-payoff expression games are played on a multidimensional weighted graph. An atomic mean-payoff expression objective is the mean-payoff value (the long-run average weight) of a certain dimension, and the class of mean-payoff expressions is the closure of atomic mean-payoff expressions under the algebraic operations of max, min, numerical complement and sum. In this work, we study for the first time the strategy synthesis problems for games with robust quantitative objectives, namely, games with mean-payoff expression objectives. While in general, optimal strategies for these games require infinite-memory, in synthesis we are typically interested in the construction of a finite-state system. Hence, we consider games in which Player 1 is restricted to finite-memory strategies, and our main contribution is as follows. We prove that for mean-payoff expressions, the quantitative analysis problem is computable, and the boolean analysis problem is inter-reducible with Hilbert's tenth problem over rationals-a fundamental long-standing open problem in computer science and mathematics. We also show that when both players may play with infinite memory both problems become undecidable.

PDF Details

GandALF Workshop 2014 Workshop Paper

Visibly Pushdown Modular Games

Ilaria De Crescenzo
Salvatore La Torre
Yaron Velner

Games on recursive game graphs can be used to reason about the control flow of sequential programs with recursion. In games over recursive game graphs, the most natural notion of strategy is the modular strategy, i. e. , a strategy that is local to a module and is oblivious to previous module invocations, and thus does not depend on the context of invocation. In this work, we study for the first time modular strategies with respect to winning conditions that can be expressed by a pushdown automaton. We show that such games are undecidable in general, and become decidable for visibly pushdown automata specifications. Our solution relies on a reduction to modular games with finite-state automata winning conditions, which are known in the literature. We carefully characterize the computational complexity of the considered decision problem. In particular, we show that modular games with a universal Buchi or co Buchi visibly pushdown winning condition are EXPTIME-complete, and when the winning condition is given by a CARET or NWTL temporal logic formula the problem is 2EXPTIME-complete, and it remains 2EXPTIME-hard even for simple fragments of these logics. As a further contribution, we present a different solution for modular games with finite-state automata winning condition that runs faster than known solutions for large specifications and many exits.

PDF Details DOI