TWO LOCAL STRATEGY ITERATION SCHEMES FOR PARITY GAME SOLVING

2012 ◽  
Vol 23 (03) ◽  
pp. 669-685 ◽  
Author(s):  
OLIVER FRIEDMANN ◽  
MARTIN LANGE
Keyword(s):  
Model Checking ◽  
Winning Strategy ◽  
Fractional Part ◽  
Program Synthesis ◽  
Global Strategy ◽  
Local Algorithm ◽  
The Core ◽  
Local Strategy ◽  
Parity Games ◽  
Satisfiability Checking

The problem of solving a parity game is at the core of many problems in model checking, satisfiability checking and program synthesis. Some of the best algorithms for solving parity game are strategy iteration algorithms. These are global in nature since they require the entire parity game to be present at the beginning. This is a distinct disadvantage because in many applications one only needs to know which winning region a particular node belongs to, and a witnessing winning strategy may cover only a fractional part of the entire game graph. We present two local strategy iteration algorithms which explore the game graph on-the-fly whilst performing the improvement steps. We also compare them empirically with existing global strategy iteration algorithms and the currently only other local algorithm for solving parity games. It turns out that local strategy iteration can outperform these others significantly.

scholarly journals Quasipolynomial Computation of Nested Fixpoints

2021 ◽  
pp. 38-56
Author(s):  
Daniel Hausmann ◽  
Lutz Schröder
Keyword(s):  
Model Checking ◽  
Relational Semantics ◽  
Suitable Function ◽  
Finite Lattices ◽  
Time Parity ◽  
Exponential Bounds ◽  
Straightforward Computation ◽  
Parity Games ◽  
Satisfiability Checking ◽  
Universal Graphs

AbstractIt is well-known that the winning region of a parity game with n nodes and k priorities can be computed as a k-nested fixpoint of a suitable function; straightforward computation of this nested fixpoint requires $$\mathcal {O}(n^{\frac{k}{2}})$$ O ( n k 2 ) iterations of the function. Calude et al.’s recent quasipolynomial-time parity game solving algorithm essentially shows how to compute the same fixpoint in only quasipolynomially many iterations by reducing parity games to quasipolynomially sized safety games. Universal graphs have been used to modularize this transformation of parity games to equivalent safety games that are obtained by combining the original game with a universal graph. We show that this approach naturally generalizes to the computation of solutions of systems of any fixpoint equations over finite lattices; hence, the solution of fixpoint equation systems can be computed by quasipolynomially many iterations of the equations. We present applications to modal fixpoint logics and games beyond relational semantics. For instance, the model checking problems for the energy $$\mu $$ μ -calculus, finite latticed $$\mu $$ μ -calculi, and the graded and the (two-valued) probabilistic $$\mu $$ μ -calculus – with numbers coded in binary – can be solved via nested fixpoints of functions that differ substantially from the function for parity games but still can be computed in quasipolynomial time; our result hence implies that model checking for these $$\mu $$ μ -calculi is in $$\textsc {QP}$$ QP . Moreover, we improve the exponent in known exponential bounds on satisfiability checking.

scholarly journals Higher-order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties

2021 ◽  
Vol 22 (2) ◽  
pp. 1-37
Author(s):  
Christopher H. Broadbent ◽  
Arnaud Carayol ◽  
C.-H. Luke Ong ◽  
Olivier Serre
Keyword(s):  
Model Checking ◽  
Free Variable ◽  
Higher Order ◽  
Second Order ◽  
Effective Solution ◽  
Parity Games ◽  
Transition Graphs ◽  
Second Order Logic ◽  
Pushdown Automata ◽  
Monadic Second Order Logic

This article studies the logical properties of a very general class of infinite ranked trees, namely, those generated by higher-order recursion schemes. We consider, for both monadic second-order logic and modal -calculus, three main problems: model-checking, logical reflection (a.k.a. global model-checking, that asks for a finite description of the set of elements for which a formula holds), and selection (that asks, if exists, for some finite description of a set of elements for which an MSO formula with a second-order free variable holds). For each of these problems, we provide an effective solution. This is obtained, thanks to a known connection between higher-order recursion schemes and collapsible pushdown automata and on previous work regarding parity games played on transition graphs of collapsible pushdown automata.

scholarly journals The strategy of demagoguery in Donald Trump’s thankful speech

2019 ◽  
Keyword(s):  
Political Discourse ◽  
Expressive Language ◽  
Global Strategy ◽  
Specific Strategy ◽  
The People ◽  
Political Views ◽  
National Convention ◽  
Local Strategy ◽  
The Masses ◽  
Linguistic Means

The article is focused on identifying local and speech strategies (tactics) that are subjected to the global strategy of demagoguery in American political discourse. The article concerns analysis of the definitions and synonyms of the term demagoguery. Such analysis confirmed the appropriateness of considering demagoguery as a specific strategy of political discourse. The results of the research ascertain that the term demagoguery is perceived differently in Ukrainian and English linguistic cultures. Ukrainians perceive demagoguery as a tool for deceiving and manipulation, while Englishmen think of it as of a method of leading a political game and broadening the voter base. The recipients of demagoguery in Ukrainian linguistic culture are uneducated groups of people, while in English linguistic culture the recipient is the people as a whole. Demagoguery as a specific strategy of political discourse is mainly used to influence the electorate through appealing to the feelings, instincts, and prejudices and through forming required political views and preferences. The analysis of the American sociologists’ works enabled us to identify the main features of demagoguery. They are the following: the focus on broadening the audience, using propaganda for manipulating the masses and entertaining character. Analysis of empirical evidence, Donald Trump's thankful speech, which was given at the Republican national convention in 2016, allows us to single out local strategies of demagoguery. The local strategies of demagoguery, which are typical for American political discourse, are the following: populism, manipulation, subjectivation, fascination, and information simplification. Moreover, the article identifies and describes speech tactics that are typical for each local strategy. Among them, there are tactics of empty promises, lies, accusing, ridicule, using slogans, vulgarization, intimidation, and a tactic of finding a scapegoat. The research also concerns analysis of the linguistic means used for the realization of every local strategy and speech tactic. The most frequently used linguistic means are usage of expressive language with positive and negative meaning, repetition, anthroponomy, and subjectivation.

scholarly journals Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems

2020 ◽  
pp. 307-324 ◽  
Author(s):  
Thomas Neele ◽  
Tim A. C. Willemse ◽  
Wieger Wesselink
Keyword(s):  
Fixed Point ◽  
Model Checking ◽  
Partial Order ◽  
Order Reduction ◽  
Partial Order Reduction ◽  
State Space Explosion ◽  
Boolean Equation ◽  
Parity Games ◽  
High Level ◽  
Established Technique

Abstract Partial-order reduction (POR) is a well-established technique to combat the problem of state-space explosion. We propose POR techniques that are sound for parity games, a well-established formalism for solving a variety of decision problems. As a consequence, we obtain the first POR method that is sound for model checking for the full modal $$\mu $$-calculus. Our technique is applied to, and implemented for the fixed point logic called parameterised Boolean equation systems, which provides a high-level representation of parity games. Experiments indicate that substantial reductions can be achieved.

Materializing Strategy in Mundane Tools: the Key to Coupling Global Strategy and Local Strategy Practice?

2015 ◽  
Vol 27 (1) ◽  
pp. 38-57 ◽  
Author(s):  
Nicolas Arnaud ◽  
Colleen E. Mills ◽  
Céline Legrand ◽  
Eric Maton
Keyword(s):  
Global Strategy ◽  
Local Strategy

scholarly journals TARNISHING THE IMAGE OF A POLITICAL OPPONENT AS A COMMUNICATIVE STRATEGY OF DONALD TRUMP’S TWITTING

2020 ◽  
pp. 84-90
Author(s):  
Meleshchenko O.O.
Keyword(s):  
Global Strategy ◽  
Negative Evaluation ◽  
Internet Service ◽  
Normative Evaluation ◽  
Local Strategy ◽  
Rhetorical Features ◽  
Communicative Strategy ◽  
Strategy I ◽  
Rational Reasoning ◽  
The Ideal

Purpose. At present when modern political leaders use the Internet service Twitter for strategic purposes, analysis of tarnishing the image of a political opponent as a communicative strategy becomes especially important. The aim of this article is to reveal cognitive (motivational and intentional), stylistic and rhetorical features of the communicative strategy of tarnishing the image of a political opponent in Donald Trump’s twitting.Methods. This research is based on the inferential, definitional, and stylistic-rhetorical analyses.Results. The study analyzes the concepts of image, communicative strategy, and rhetorical technique. It makes a case for the negative evaluation as the key characteristic of the communicative strategy of tarnishing the image of a political opponent. The analysis of the strategic organization of Trump’s Twitter-based Internet discourse has determined the strategy of tarnishing the image of a political opponent as a local one. This local strategy is subordinate to the global strategy of Trump’s twitting that aims to exert communicative influence in order to seize and retain political power. Within this local strategy, I further specify the sub-strategies of disqualification, discrediting, and discrimination, which are differentiated according to the type of the evaluation they rest on. The disqualification sub-strategy is based on the negative teleological evaluation of a political opponent, which highlights the incompatibility of his/her business, professional, and intellectual features with the image of the ideal politician. The discrediting sub-strategy is rooted in the negative ethical evaluation of a political opponent as being incompatible with the image of the ideal politician according to his/her moral/ethical features. The discrimination sub-strategy is based on the negative normative evaluation of a political opponent as belonging to a negatively assessed socio-political category, which indicates that he/she does not qualify for the ideal politician. These sub-strategies are implemented by the rhetorical techniques of influencing the addressee, which are differentiated according to the influence on different spheres of the human psyche they impact on: argumentation (the sphere of rational reasoning), declaration, and emotive contagion (emotions and feelings), and instruction (volition).Conclusions. The analysis of cognitive (motivational and intentional) characteristics of the communicative strategy of tarnishing the image of a political opponent allows to define it as a local one in the strategic organization of Trump’s twitting. This local strategy is realized through the sub-strategies of disqualification, discrediting, and discrimination, which are further implemented by rhetorical techniques of influencing the addressee. The analysis of the disqualification sub-strategy showed that Trump uses several rhetorical techniques simultaneously within one tweet, exerting communicative influence on different spheres of the addressee’s psyche.Key words: communicative influence, image of a politician, negative evaluation, rhetorical technique, strategic organization of discourse, Twitter. Мета. В умовах стратегічного використання інтернет-сервісу «Твітер» сучасними політичними лідерами вивчення руй-нування іміджу політичного опонента як комунікативної стратегії політичного твітінгу набуває особливого значення. Метою статті є встановлення когнітивних (мотиваційно-інтенціональних) та стилістично-риторичних характеристик комунікативної стратегії руйнування іміджу політичного опонента у твітінгу Дональда Трампа.Методи. В основу методики дослідження було покладено інференційний аналіз, який доповнюється дефініційним і сти-лістично-риторичним аналізами.Результати. У межах проведеного дослідження проаналізовано поняття іміджу, комунікативної стратегії, риторичної тех-ніки, обґрунтовано негативну оцінку як ключовий параметр стратегії руйнування іміджу політичного опонента. Аналіз стра-тегічної організації інтернет-дискурсу Д. Трампа на базі твітеру дозволив визначити стратегію руйнування іміджу політичного опонента як локальну стратегію, що підкорюється глобальній стратегії усього твітінгу Д. Трампа – спричиненню комуніка-тивного впливу з метою захоплення й утримання політичної влади. У межах локальної стратегії руйнування іміджу політич-ного опонента виокремлено субстратегії дискваліфікації, дискредитації й дискримінації. Критерієм їх розмежування виступає тип оцінки. В основі субстратегії дискваліфікації лежить негативна телеологічна оцінка політичного опонента, об’єктом якої є його ділові, професійні та інтелектуальні якості. Вони свідчать про невідповідність політичного опонента еталону політика за телеологічними чинниками. Субстратегія дискредитації ґрунтується на негативній етичній оцінці політичного опонента, об’єктом якої є його поведінка, яка свідчить про невідповідність еталону політика за морально-етичними чинникам. Основою субстратегії дискримінації є демонстрація негативної нормативної оцінки політичного опонента, об’єктом якої є його прина-лежність до негативно оцінюваної соціально-політичної категорії, що свідчить про його невідповідність еталону політика за нормативними чинниками. Інструментом реалізації цих субстратегій виступають риторичні техніки впливу на адресата, роз-межовані за критерієм впливу на різні сфери психіки: доведення (раціональне мислення), декларування й емотивне зараження (сфера емоцій і відчуттів), спонукання (волевиявлення).Висновки. Проведений аналіз когнітивних (мотиваційно-інтенціональних) характеристик комунікативної стратегії руйну-вання іміджу політичного опонента дозволяє визначити її як локальну стратегію у стратегічній організації твітінгу Д. Трампа. Ця локальна стратегія втілюється субстратегіями дискваліфікації, дискредитації й дискримінації, які реалізуються риторични-ми техніками впливу на адресата. Аналіз субстратегії дискваліфікації показав, що Д. Трамп використовує одночасно декілька риторичних технік у межах одного твіту, справляючи комунікативний вплив на різні сфери психіки адресата.Ключові слова: імідж політика, комунікативний вплив, негативна оцінка, риторична техніка, стратегічна організація дис-курсу, твітер.

scholarly journals Family-Based SPL Model Checking Using Parity Games with Variability

2020 ◽  
pp. 245-265
Author(s):  
Maurice H. ter Beek ◽  
Sjef van Loo ◽  
Erik P. de Vink ◽  
Tim A. C. Willemse
Keyword(s):  
Model Checking ◽  
Parity Games ◽  
Family Based

Using Only Elastic Stiffness in Nonlinear and Postbuckling Analysis of Structures

2019 ◽  
Vol 19 (10) ◽  
pp. 1950112 ◽  
Author(s):  
Y. B. Yang ◽  
Anquan Chen ◽  
Yuanyuan Yan ◽  
Zhilu Wang
Keyword(s):  
Elastic Stiffness ◽  
Global Strategy ◽  
Shell Structures ◽  
Stiffness Parameter ◽  
Structural Geometry ◽  
Path Tracing ◽  
Geometric Stiffness ◽  
Wide Range ◽  
Local Strategy ◽  
Number Of Iterations

This paper presents a new attempt for geometric nonlinear and postbuckling analysis of structures using only elastic stiffness. This can be achieved not without reasons. Aside from a correct updating of the structural geometry in the incremental sense, there are two concerns for iterations: (i) The local strategy is that the element forces recovered in each iteration should not violate the rigid body rule, in order not to induce any fictitious forces. (ii) The global strategy is that the path-tracing scheme should be able to deal with multi critical points, such as limit and snap-back points. Both strategies will be explained via the mechanism of iterations, which seems not new, but can shed some new lights. The results obtained using only the elastic stiffness will be compared with the normal case including the geometric stiffness, with the level of approximation assessed by the general stiffness parameter (GSP). Through the study of a number of trusses, beams and shell structures, it is confirmed that the elastic stiffness alone can be used to solve the nonlinear and postbuckling responses of a wide range of structures, with only an increase in the number of iterations. This paper represents a limit application of the elastic stiffness to nonlinear structural analysis.

scholarly journals Local Computation of Simultaneous Fixed-Points

2003 ◽  
Vol 21 (420) ◽  
Author(s):  
Henrik Reif Andersen
Keyword(s):  
Model Checking ◽  
Fixed Points ◽  
Ad Hoc ◽  
General Algorithm ◽  
General Mechanism ◽  
Local Algorithm ◽  
Worst Case ◽  
Local Algorithms ◽  
Logarithmic Factor ◽  
Strictness Analysis

<!--DAIMI Standard Header Begin--> <p>We present a very simple, yet general algorithm for computing simultaneous, minimum fixed-points of monotonic functions, or turning the newpoint slightly, an algorithm for computing minimum solutions to a system of monotonic equations. The algorithm is local (demand-driven, lazy, ... ), i.e. it will try to determine the value of a single component in the simultaneous fixed-point by investigating only certain necessary parts of the description of the monotonic function, or in terms of the equational presentation, it will determine the value of a single variable by investigating only a part of the equational system.</p><p>In the worst-case this involves inspecting the complete system, and the algorithm will be a logarithmic factor worse than a global algorithm (computing the values of all variables simultaneously). But despite its simplicity the local algorithm has some advantages which promise much better performance on typical cases. The algorithm should be seen as a schema that for any particular application needs to be refined to achieve better efficiency, but the general mechanism remains the same. As such it seems to achieve performance comparable to, and for some examples improving upon, carefully designed <em>ad hoc</em> algorithms, still maintaining the benefits of being local.</p><p>We illustrate this point by tailoring the general algorithm to concrete examples in such (apparently) diverse areas as type inference, model checking, and strictness analysis. Especially in connection with the last example, strictness analysis, and more generally abstract interpretation, it is illustrated how the local algorithm provides a very minimal approach when determining the fixed-points, reminiscent of, but improving upon, what is known as Pending Analysis. In the case of model checking a specialised version of the algorithm has already improved on earlier known local algorithms.</p>

Sign in / Sign up

Export Citation Format

Share Document