English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

We present several new algorithms as well as new lower and upper bounds for optimizing functions underlying infinite games pertinent to computer-aided verification. Infinite two-person adversary full information games are a well established framework for modeling interaction between a system and its environment. A correct system can be naturally interpreted as a player possessing a winning strategy against any strategy of the malicious environment. Respec- tively, a verification process can be considered as a proof that a system does possess such a strategy. If the system loses, then a winning strategy for the environment encompasses possible system im- provements. During the last decades a substantial progress has been achieved both on fitting diverse approaches to computer-aided verification into the game-theoretic paradigm and, simultaneously, on developing efficient algorithms for solving games, i.e., determining the winner and its strategy (12,8, 15,19,28,5). A naturally appealing approach to solving games (18,10,28) consists in taking an initial strategy of the system and gradually 'improving' it, since a non-optimal strategy is outperformed by some counterstrategy of the environment. This allows for improving either the strategy, or the system, or both. In this paper we address the complexity of such an approach in an abstract model based on pseudo-Boolean functions possessing essential properties of games. Game theory suggests, for numerous types of games, a nice characterization of the optimal solu- tions for behaviors of rational players, the so-called Nash equilibria. The 'only' remaining problem left widely open is: 'What is the exact computational complexity of finding Nash equilibria (optimal strategies) in two-person games with finitely many strategies? Could such games be solved in polyno- mial time?' This is a fundamental problem, the solution to which determines whether or not, and to what extent game theory will be applicable to solving and optimizing real large-scale games emerg- ing from practical verification of complex reactive systems. The problem is known to belong to the complexity class NP∩coNP (therefore, most probably not NP-complete, luckily!) but is not known to be polynomial time solvable. The best currently known algorithms are exponential (sometimes subexponential). Clearly, superpolynomial algorithms will not allow for practical solutions of the real-life verification games, no matter how fast the progress in hardware continues. Consequently, this problem is one of the most practical and (together with the NP versus P) most fundamental problems in the foundations of computing, complexity theory, and automata theory (24). In this paper we address the efficiency of iterative improvement algorithms for solving games in the following abstract setting. Consider a game where one of the players has n binary choices, e.g., selects whether to move left or right1 in n places, and every combination of choices is given a

Complexity of Model Checking by Iterative Improvement: The Pseudo-Boolean Framework