-
DFAMiner: Mining minimal separating DFAs from labelled samples
Authors:
Daniele Dell'Erba,
Yong Li,
Sven Schewe
Abstract:
We propose DFAMiner, a passive learning tool for learning minimal separating deterministic finite automata (DFA) from a set of labelled samples. Separating automata are an interesting class of automata that occurs generally in regular model checking and has raised interest in foundational questions of parity game solving. We first propose a simple and linear-time algorithm that incrementally const…
▽ More
We propose DFAMiner, a passive learning tool for learning minimal separating deterministic finite automata (DFA) from a set of labelled samples. Separating automata are an interesting class of automata that occurs generally in regular model checking and has raised interest in foundational questions of parity game solving. We first propose a simple and linear-time algorithm that incrementally constructs a three-valued DFA (3DFA) from a set of labelled samples given in the usual lexicographical order. This 3DFA has accepting and rejecting states as well as don't-care states, so that it can exactly recognise the labelled examples. We then apply our tool to mining a minimal separating DFA for the labelled samples by minimising the constructed automata via a reduction to solving SAT problems. Empirical evaluation shows that our tool outperforms current state-of-the-art tools significantly on standard benchmarks for learning minimal separating DFAs from samples. Progress in the efficient construction of separating DFAs can also lead to finding the lower bound of parity game solving, where we show that DFAMiner can create optimal separating automata for simple languages with up to 7 colours. Future improvements might offer inroads to better data structures.
△ Less
Submitted 29 May, 2024;
originally announced May 2024.
-
An Objective Improvement Approach to Solving Discounted Payoff Games
Authors:
Daniele Dell'Erba,
Arthur Dumas,
Sven Schewe
Abstract:
While discounted payoff games and classic games that reduce to them, like parity and mean-payoff games, are symmetric, their solutions are not. We have taken a fresh view on the properties that optimal solutions need to have, and devised a novel way to converge to them, which is entirely symmetric. We achieve this by building a constraint system that uses every edge to define an inequation, and up…
▽ More
While discounted payoff games and classic games that reduce to them, like parity and mean-payoff games, are symmetric, their solutions are not. We have taken a fresh view on the properties that optimal solutions need to have, and devised a novel way to converge to them, which is entirely symmetric. We achieve this by building a constraint system that uses every edge to define an inequation, and update the objective function by taking a single outgoing edge for each vertex into account. These edges loosely represent strategies of both players, where the objective function intuitively asks to make the inequation to these edges sharp, leading to an `error' or 0. For co-optimal strategies, and only for them, this can be achieved, and while we have not found them, we step-wise improve the error by improving the solution for a given objective function or by improving the objective function for a given solution. This also challenges the gospel that methods for solving payoff games are either based on strategy improvement or on value iteration.
△ Less
Submitted 4 April, 2024;
originally announced April 2024.
-
Errata to: "Faster Deterministic Exponential Time Algorithm for Energy Games and Mean Payoff Games"
Authors:
Peter Austin,
Daniele Dell'Erba
Abstract:
An improved exponential time algorithm for Energy Games and Mean Payoff Games has been recently proposed in ICALP 19. The new algorithm prevents some of the repetitive operations performed by the classic value iteration algorithm of Brim et al., leading to an approach with time complexity $O(\min(mnW,mn2^{n/2}\log W))$. Unfortunately, the pseudo-code of the algorithm includes inaccuracies that vio…
▽ More
An improved exponential time algorithm for Energy Games and Mean Payoff Games has been recently proposed in ICALP 19. The new algorithm prevents some of the repetitive operations performed by the classic value iteration algorithm of Brim et al., leading to an approach with time complexity $O(\min(mnW,mn2^{n/2}\log W))$. Unfortunately, the pseudo-code of the algorithm includes inaccuracies that violate two Lemmata used in the correctness and complexity proofs. In this technical report, we describe the problems, propose a fixed version of the algorithm, and correct the proofs for the Lemmata.
△ Less
Submitted 6 October, 2023;
originally announced October 2023.
-
An Objective Improvement Approach to Solving Discounted Payoff Games
Authors:
Daniele Dell'Erba,
Arthur Dumas,
Sven Schewe
Abstract:
While discounted payoff games and classic games that reduce to them, like parity and mean-payoff games, are symmetric, their solutions are not. We have taken a fresh view on the constraints that optimal solutions need to satisfy, and devised a novel way to converge to them, which is entirely symmetric. It also challenges the gospel that methods for solving payoff games are either based on strategy…
▽ More
While discounted payoff games and classic games that reduce to them, like parity and mean-payoff games, are symmetric, their solutions are not. We have taken a fresh view on the constraints that optimal solutions need to satisfy, and devised a novel way to converge to them, which is entirely symmetric. It also challenges the gospel that methods for solving payoff games are either based on strategy improvement or on value iteration.
△ Less
Submitted 2 October, 2023;
originally announced October 2023.
-
Smaller Progress Measures and Separating Automata for Parity Games
Authors:
Daniele Dell'Erba,
Sven Schewe
Abstract:
Calude et al. have recently shown that parity games can be solved in quasi-polynomial time, a landmark result that has led to a number of approaches with quasi-polynomial complexity. Jurdinski and Lasic have further improved the precise complexity of parity games, especially when the number of priorities is low (logarithmic in the number of positions). Both of these algorithms belong to a class of…
▽ More
Calude et al. have recently shown that parity games can be solved in quasi-polynomial time, a landmark result that has led to a number of approaches with quasi-polynomial complexity. Jurdinski and Lasic have further improved the precise complexity of parity games, especially when the number of priorities is low (logarithmic in the number of positions). Both of these algorithms belong to a class of game solving techniques now often called separating automata: deterministic automata that can be used as witness automata to decide the winner in parity games up to a given number of states and colours. We suggest a number of adjustments to the approach of Calude et al. that lead to smaller statespaces. These include and improve over those earlier introduced by Fearnley et al.
We identify two of them that, together, lead to a statespace of exactly the same size Jurdzinski and Lasic's concise progress measures, which currently hold the crown as smallest statespace. The remaining improvements, hence, lead to a further reduction in the size of the statespace, making our approach the most succinct progress measures available for parity games.
△ Less
Submitted 2 May, 2022;
originally announced May 2022.
-
Priority Promotion with Parysian Flair
Authors:
Massimo Benerecetti,
Daniele Dell'Erba,
Fabio Mogavero,
Sven Schewe,
Dominik Wojtczak
Abstract:
We develop an algorithm that combines the advantages of priority promotion - one of the leading approaches to solving large parity games in practice - with the quasi-polynomial time guarantees offered by Parys' algorithm. Hybridising these algorithms sounds both natural and difficult, as they both generalise the classic recursive algorithm in different ways that appear to be irreconcilable: while…
▽ More
We develop an algorithm that combines the advantages of priority promotion - one of the leading approaches to solving large parity games in practice - with the quasi-polynomial time guarantees offered by Parys' algorithm. Hybridising these algorithms sounds both natural and difficult, as they both generalise the classic recursive algorithm in different ways that appear to be irreconcilable: while the promotion transcends the call structure, the guarantees change on each level. We show that an interface that respects both is not only effective, but also efficient.
△ Less
Submitted 31 August, 2021; v1 submitted 16 April, 2021;
originally announced May 2021.
-
From Quasi-Dominions to Progress Measures
Authors:
Massimo Benerecetti,
Daniele Dell'Erba,
Marco Faella,
Fabio Mogavero
Abstract:
We revisit the approaches to the solution of parity games based on progress measures and show how the notion of quasi dominions can be integrated with those approaches. The idea is that, while progress measure based techniques typically focus on one of the two players, little information is gathered on the other player during the solution process. Adding quasi dominions provides additional informa…
▽ More
We revisit the approaches to the solution of parity games based on progress measures and show how the notion of quasi dominions can be integrated with those approaches. The idea is that, while progress measure based techniques typically focus on one of the two players, little information is gathered on the other player during the solution process. Adding quasi dominions provides additional information on this player that can be leveraged to greatly accelerate convergence to a progress measure. To accommodate quasi dominions, however, non trivial refinements of the approach are necessary. In particular, we need to introduce a novel notion of measure and a new method to prove correctness of the resulting solution technique.
△ Less
Submitted 9 November, 2021; v1 submitted 10 August, 2020;
originally announced August 2020.
-
Solving Mean-Payoff Games via Quasi Dominions
Authors:
Massimo Benerecetti,
Daniele Dell'Erba,
Fabio Mogavero
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 perform…
▽ More
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.
△ Less
Submitted 14 July, 2019;
originally announced July 2019.
-
Robust Exponential Worst Cases for Divide-et-Impera Algorithms for Parity Games
Authors:
Massimo Benerecetti,
Daniele Dell'Erba,
Fabio Mogavero
Abstract:
The McNaughton-Zielonka divide et impera algorithm is the simplest and most flexible approach available in the literature for determining the winner in a parity game. Despite its theoretical worst-case complexity and the negative reputation as a poorly effective algorithm in practice, it has been shown to rank among the best techniques for the solution of such games. Also, it proved to be resistan…
▽ More
The McNaughton-Zielonka divide et impera algorithm is the simplest and most flexible approach available in the literature for determining the winner in a parity game. Despite its theoretical worst-case complexity and the negative reputation as a poorly effective algorithm in practice, it has been shown to rank among the best techniques for the solution of such games. Also, it proved to be resistant to a lower bound attack, even more than the strategy improvements approaches, and only recently a family of games on which the algorithm requires exponential time has been provided by Friedmann. An easy analysis of this family shows that a simple memoization technique can help the algorithm solve the family in polynomial time. The same result can also be achieved by exploiting an approach based on the dominion-decomposition techniques proposed in the literature. These observations raise the question whether a suitable combination of dynamic programming and game-decomposition techniques can improve on the exponential worst case of the original algorithm. In this paper we answer this question negatively, by providing a robustly exponential worst case, showing that no intertwining of the above mentioned techniques can help mitigating the exponential nature of the divide et impera approaches.
△ Less
Submitted 7 September, 2017;
originally announced September 2017.
-
A Delayed Promotion Policy for Parity Games
Authors:
Massimo Benerecetti,
Daniele Dell'Erba,
Fabio Mogavero
Abstract:
Parity games are two-player infinite-duration games on graphs that play a crucial role in various fields of theoretical computer science. Finding efficient algorithms to solve these games in practice is widely acknowledged as a core problem in formal verification, as it leads to efficient solutions of the model-checking and satisfiability problems of expressive temporal logics, e.g., the modal muC…
▽ More
Parity games are two-player infinite-duration games on graphs that play a crucial role in various fields of theoretical computer science. Finding efficient algorithms to solve these games in practice is widely acknowledged as a core problem in formal verification, as it leads to efficient solutions of the model-checking and satisfiability problems of expressive temporal logics, e.g., the modal muCalculus. Their solution can be reduced to the problem of identifying sets of positions of the game, called dominions, in each of which a player can force a win by remaining in the set forever. Recently, a novel technique to compute dominions, called priority promotion, has been proposed, which is based on the notions of quasi dominion, a relaxed form of dominion, and dominion space. The underlying framework is general enough to accommodate different instantiations of the solution procedure, whose correctness is ensured by the nature of the space itself. In this paper we propose a new such instantiation, called delayed promotion, that tries to reduce the possible exponential behaviours exhibited by the original method in the worst case. The resulting procedure not only often outperforms the original priority promotion approach, but so far no exponential worst case is known.
△ Less
Submitted 13 September, 2016;
originally announced September 2016.
