scholarly journals Solving Mean-Payoff Games via Quasi Dominions

2020 ◽  
pp. 289-306
Author(s):  
Massimo Benerecetti ◽  
Daniele Dell’Erba ◽  
Fabio Mogavero
Keyword(s):  
Solution Algorithm ◽  
Problem Solution ◽  
Worst Case ◽  
Case Complexity ◽  
Worst Case Complexity ◽  
Mean Payoff Games ◽  
Parity Games ◽  
Mean Payoff ◽  
Novel Algorithm ◽  
Better Than

Abstract We propose a novel algorithm for the solution of mean-payoff games that merges together two seemingly unrelated concepts introduced in the context of parity games, small progress measures and quasi dominions. We show that the integration of the two notions can be highly beneficial and significantly speeds up convergence to the problem solution. Experiments show that the resulting algorithm performs orders of magnitude better than the asymptotically-best solution algorithm currently known, without sacrificing on the worst-case complexity.

scholarly journals LTLƒ Synthesis with Fairness and Stability Assumptions

2020 ◽  
Vol 34 (03) ◽  
pp. 3088-3095
Author(s):  
Shufang Zhu ◽  
Giuseppe De Giacomo ◽  
Geguang Pu ◽  
Moshe Y. Vardi
Keyword(s):  
Worst Case ◽  
Case Complexity ◽  
Worst Case Complexity ◽  
Ltl Synthesis ◽  
Finite Trace ◽  
Better Than ◽  
Rule Out

In synthesis, assumptions are constraints on the environment that rule out certain environment behaviors. A key observation here is that even if we consider systems with LTLƒ goals on finite traces, environment assumptions need to be expressed over infinite traces, since accomplishing the agent goals may require an unbounded number of environment action. To solve synthesis with respect to finite-trace LTLƒ goals under infinite-trace assumptions, we could reduce the problem to LTL synthesis. Unfortunately, while synthesis in LTLƒ and in LTL have the same worst-case complexity (both 2EXPTIME-complete), the algorithms available for LTL synthesis are much more difficult in practice than those for LTLƒ synthesis. In this work we show that in interesting cases we can avoid such a detour to LTL synthesis and keep the simplicity of LTLƒ synthesis. Specifically, we develop a BDD-based fixpoint-based technique for handling basic forms of fairness and of stability assumptions. We show, empirically, that this technique performs much better than standard LTL synthesis.

scholarly journals Two-Stage Technique for LTLf Synthesis Under LTL Assumptions

2020 ◽  
Author(s):  
Giuseppe De Giacomo ◽  
Antonio Di Stasio ◽  
Moshe Y. Vardi ◽  
Shufang Zhu
Keyword(s):  
Two Stage ◽  
Worst Case ◽  
Case Complexity ◽  
Worst Case Complexity ◽  
Ltl Synthesis ◽  
Better Than ◽  
Rule Out

In synthesis, assumption are constraints on the environments that rule out certain environment behaviors. A key observation is that even if we consider system with LTLf goals on finite traces, assumptions need to be expressed considering infinite traces, using LTL on infinite traces, since the decision to stop the trace is controlled by the agent. To solve synthesis of LTLf goals under LTL assumptions, we could reduce the problem to LTL synthesis. Unfortunately, while synthesis in LTLf and in LTL have the same worst-case complexity (both are 2EXPTIME-complete), the algorithms available for LTL synthesis are much harder in practice than those for LTLf synthesis. Recently, it has been shown that in basic forms of fairness and stability assumptions we can avoid such a detour to LTL and keep the simplicity of LTLf synthesis. In this paper, we generalize these results and show how to effectively handle any kind of LTL assumptions. Specifically, we devise a two-stage technique for solving LTLf under general LTL assumptions and show empirically that this technique performs much better than standard LTL synthesis.

scholarly journals Computing Maximal Lyndon Substrings of a String

2020 ◽  
Author(s):  
Frantisek Franek ◽  
Michael Liut
Keyword(s):  
Theoretical Analysis ◽  
Suffix Array ◽  
Input String ◽  
Sorting Algorithm ◽  
Worst Case ◽  
Average Case ◽  
Linear Algorithm ◽  
Case Complexity ◽  
Worst Case Complexity ◽  
Novel Algorithm

There are two reasons to have an efficient algorithm for identifying all maximal Lyndon substrings of a string: firstly, Bannai et al. introduced in 2015 a linear algorithm to compute all runs of a string that relies on knowing all maximal Lyndon substrings of the input string, and secondly, Franek et al. showed in 2017 a linear equivalence of sorting suffixes and sorting maximal Lyndon substrings of a string, inspired by a novel suffix sorting algorithm of Baier. In 2016, Franek et al. presented a brief overview of algorithms for computing the Lyndon array that encodes the knowledge of maximal Lyndon substrings of the input string. Among the presented were two well-known algorithms for computing the Lyndon array: a quadratic in-place algorithm based on iterated Duval's algorithm for Lyndon factorization, and a linear algorithmic scheme based on linear suffix sorting, computing inverse suffix array, and applying to it the Next Smaller Value algorithm. Duval's algorithm works for strings over any ordered alphabet, while for linear suffix sorting, a constant or an integer alphabet is required. The authors at that time were not aware of Baier's algorithm. In 2017, our research group proposed a novel algorithm for the Lyndon array. Though the proposed algorithm is linear in the average case and has O(n log(n)) worst-case complexity, it is interesting as it emulates the fast Fourier algorithm's recursive approach and introduces tau-reduction that might be of independent interest. In 2018, we presented a linear algorithm to compute the Lyndon array of a string inspired by Phase I of Baier's algorithm for suffix sorting. This paper presents theoretical analysis of these two algorithms and provides empirical comparisons of both their C++ implementations with respect to iterated Duval's algorithm.

scholarly journals Computing Maximal Lyndon Substrings of a String

Algorithms ◽  
2020 ◽  
Vol 13 (11) ◽  
pp. 294
Author(s):  
Frantisek Franek ◽  
Michael Liut
Keyword(s):  
Theoretical Analysis ◽  
Suffix Array ◽  
Input String ◽  
Sorting Algorithm ◽  
Worst Case ◽  
Average Case ◽  
Linear Algorithm ◽  
Case Complexity ◽  
Worst Case Complexity ◽  
Novel Algorithm

There are two reasons to have an efficient algorithm for identifying all right-maximal Lyndon substrings of a string: firstly, Bannai et al. introduced in 2015 a linear algorithm to compute all runs of a string that relies on knowing all right-maximal Lyndon substrings of the input string, and secondly, Franek et al. showed in 2017 a linear equivalence of sorting suffixes and sorting right-maximal Lyndon substrings of a string, inspired by a novel suffix sorting algorithm of Baier. In 2016, Franek et al. presented a brief overview of algorithms for computing the Lyndon array that encodes the knowledge of right-maximal Lyndon substrings of the input string. Among those presented were two well-known algorithms for computing the Lyndon array: a quadratic in-place algorithm based on the iterated Duval algorithm for Lyndon factorization and a linear algorithmic scheme based on linear suffix sorting, computing the inverse suffix array, and applying to it the next smaller value algorithm. Duval’s algorithm works for strings over any ordered alphabet, while for linear suffix sorting, a constant or an integer alphabet is required. The authors at that time were not aware of Baier’s algorithm. In 2017, our research group proposed a novel algorithm for the Lyndon array. Though the proposed algorithm is linear in the average case and has O(nlog(n)) worst-case complexity, it is interesting as it emulates the fast Fourier algorithm’s recursive approach and introduces τ-reduction, which might be of independent interest. In 2018, we presented a linear algorithm to compute the Lyndon array of a string inspired by Phase I of Baier’s algorithm for suffix sorting. This paper presents the theoretical analysis of these two algorithms and provides empirical comparisons of both of their C++ implementations with respect to the iterated Duval algorithm.

scholarly journals On the optimal order of worst case complexity of direct search

2015 ◽  
Vol 10 (4) ◽  
pp. 699-708 ◽  
Author(s):  
M. Dodangeh ◽  
L. N. Vicente ◽  
Z. Zhang
Keyword(s):  
Direct Search ◽  
Optimal Order ◽  
Worst Case ◽  
Case Complexity ◽  
Worst Case Complexity

USING STRATEGY IMPROVEMENT TO STAY ALIVE

2012 ◽  
Vol 23 (03) ◽  
pp. 585-608 ◽  
Author(s):  
LUBOŠ BRIM ◽  
JAKUB CHALOUPKA
Keyword(s):  
Experimental Study ◽  
Energy Level ◽  
Initial Energy ◽  
Minimum Amount ◽  
Usual Sense ◽  
Mean Payoff Games ◽  
Mean Payoff ◽  
Novel Algorithm

We design a novel algorithm for solving Mean-Payoff Games (MPGs). Besides solving an MPG in the usual sense, our algorithm computes more information about the game, information that is important with respect to applications. The weights of the edges of an MPG can be thought of as a gained/consumed energy – depending on the sign. For each vertex, our algorithm computes the minimum amount of initial energy that is sufficient for player Max to ensure that in a play starting from the vertex, the energy level never goes below zero. Our algorithm is not the first algorithm that computes the minimum sufficient initial energies, but according to our experimental study it is the fastest algorithm that computes them. The reason is that it utilizes the strategy improvement technique which is very efficient in practice.

Worst-case Complexity of Exact Algorithms forNP-hard Problems

2010 ◽  
pp. 203-240
Author(s):  
Federico Della Croce ◽  
Bruno Escoffier ◽  
Marcin Kamiski ◽  
Vangelis Th. Paschos
Keyword(s):  
Exact Algorithms ◽  
Worst Case ◽  
Case Complexity ◽  
Worst Case Complexity ◽  
Hard Problems
Sign in / Sign up

Export Citation Format

Share Document