Feature-based SPL analysis and family-based model checking have seen rapid development. Many model checking problems can be reduced to two-player games on finite graphs. A prominent example is mu-calculus model checking, which is generally done by translating to parity games, but also many quantitative model-checking problems can be reduced to (quantitative) games.
In their FASE'20 paper, ter Beek et al.\ introduce parity games with variability in order to develop family-based mu-calculus model checking of featured transition systems. We generalize their model to general featured games and show how these may be analysed in a family-based manner.
We introduce featured reachability games, featured minimum reachability games, featured discounted games, featured energy games, and featured parity games. We show how to compute winners and values of such games in a family-based manner. We also show that all these featured games admit optimal featured strategies, which project to optimal strategies for any product. Further, we develop family-based algorithms, using late splitting, to compute winners, values, and optimal strategies for all the featured games we have introduced.
Variational systems allow effective building of many custom variants by using features (configuration options) to mark the variable functionality. In many of the applications, their quality assurance and formal verification are of paramount importance. Family-based model checking allows simultaneous verification of all variants of a variational system in a single run by exploiting the commonalities between the variants. Yet, its computational cost still greatly depends on the number of variants (often huge). In this work, we show how to achieve efficient family-based model checking of CTL* tem…
This paper revisits the well-established relationship between the modal mu calculus and parity games to show that it is even more robust than previously known. It addresses the question of whether the descriptive complexity of modal mu model-checking games, previously known to depend on the syntactic complexity of a formula, depends in fact on its semantic complexity. It shows that up to formulas of semantic co-Büchi complexity, the descriptive complexity of their model-checking games coincides exactly with their semantic complexity. Beyond co-Büchi, the descriptive complexity of the model-che…
We consider quantitative extensions of the alternating-time temporal logics ATL/ATLs called quantitative alternating-time temporal logics (QATL/QATLs) in which the value of a counter can be compared to constants using equality, inequality and modulo constraints. We interpret these logics in one-counter game models which are infinite duration games played on finite control graphs where each transition can increase or decrease the value of an unbounded counter. That is, the state-space of these games are, generally, infinite. We consider the model-checking problem of the logics QATL and QATLs on…
Algorithms for model checking and satisfiability of the modal $μ$-calculus start by converting formulas to alternating parity tree automata. Thus, model checking is reduced to checking acceptance by tree automata and satisfiability to checking their emptiness. The first reduces directly to the solution of parity games but the second is more complicated. We review the non-emptiness checking of alternating tree automata by a reduction to solving parity games of a certain structure, so-called emptiness games. Since the emptiness problem for alternating tree automata is EXPTIME-complete, the size …
Probabilistic model checking for stochastic games enables formal verification of systems that comprise competing or collaborating entities operating in a stochastic environment. Despite good progress in the area, existing approaches focus on zero-sum goals and cannot reason about scenarios where entities are endowed with different objectives. In this paper, we propose probabilistic model checking techniques for concurrent stochastic games based on Nash equilibria. We extend the temporal logic rPATL (probabilistic alternating-time temporal logic with rewards) to allow reasoning about players wi…
In this work, we present a logic based on first-order CTL, namely Game Analysis Logic (GAL), in order to reason about games. We relate models and solution concepts of Game Theory as models and formulas of GAL, respectively. Precisely, we express extensive games with perfect in- formation as models of GAL, and Nash equilibrium and subgame perfect equilibrium by means of formulas of GAL. From a practical point of view, we provide a GAL model checker in order to analyze games automatically. We use our model checker in at least two directions: to find solution con- cepts of Game Theory; and, to an…
A naive way to solve the model-checking problem of the mu-calculus uses fixpoint iteration. Traditionally however mu-calculus model-checking is solved by a reduction in linear time to a parity game, which is then solved using one of the many algorithms for parity games. We now consider a method of solving parity games by means of a naive fixpoint iteration. Several fixpoint algorithms for parity games have been proposed in the literature. In this work, we introduce an algorithm that relies on the notion of a distraction. The idea is that this offers a novel perspective for understanding parity…
We introduce differential games for FO logic of graphs, a variant of Ehrenfeucht-Fraïssé games in which the game is played on only one graph and the moves of both players restricted. We prove that, in a certain sense, these games are strong enough to capture essential information about graphs from graph classes which are interpretable in nowhere dense graph classes. This, together with the newly introduced notion of differential locality and the fact that the restriction of possible moves by the players makes it easy to decide the winner of the game in some cases, leads to a new approach to th…
We develop game-theoretic semantics (GTS) for the fragment ATL+ of the full Alternating-time Temporal Logic ATL*, essentially extending a recently introduced GTS for ATL. We first show that the new game-theoretic semantics is equivalent to the standard semantics of ATL+ (based on perfect recall strategies). We then provide an analysis, based on the new semantics, of the memory and time resources needed for model checking ATL+. Based on that, we establish that strategies that use only a very limited amount of memory suffice for ATL+. Furthermore, using the GTS we provide a new algorithm for mod…
We prove that the model checking ATL* on concurrent game structures with propositional control for atom-visibility (vCGS) is undecidable. To do so, we reduce this problem to model checking ATL* on iCGS.
Design and control of autonomous systems that operate in uncertain or adversarial environments can be facilitated by formal modelling and analysis. Probabilistic model checking is a technique to automatically verify, for a given temporal logic specification, that a system model satisfies the specification, as well as to synthesise an optimal strategy for its control. This method has recently been extended to multi-agent systems that exhibit competitive or cooperative behaviour modelled via stochastic games and synthesis of equilibria strategies. In this paper, we provide an overview of probabi…
Parity games play a central role in model checking and satisfiability checking. Solving parity games is computationally expensive, among others due to the size of the games, which, for model checking problems, can easily contain $10^9$ vertices or beyond. Equivalence relations can be used to reduce the size of a parity game, thereby potentially alleviating part of the computational burden. We reconsider (governed) bisimulation and (governed) stuttering bisimulation, and we give detailed proofs that these relations are equivalences, have unique quotients and they approximate the winning regions…
We introduce a new game-theoretic semantics (GTS) for the modal mu-calculus. Our so-called bounded GTS replaces parity games with alternative evaluation games where only finite paths arise; infinite paths are not needed even when the considered transition system is infinite. The novel games offer alternative approaches to various constructions in the framework of the mu-calculus. For example, they have already been successfully used as a basis for an approach leading to a natural formula size game for the logic. While our main focus is introducing the new GTS, we also consider some application…
We study the model-checking problem for a quantitative extension of the modal mu-calculus on a class of hybrid systems. Qualitative model checking has been proved decidable and implemented for several classes of systems, but this is not the case for quantitative questions that arise naturally in this context. Recently, quantitative formalisms that subsume classical temporal logics and allow the measurement of interesting quantitative phenomena were introduced. We show how a powerful quantitative logic, the quantitative mu-calculus, can be model checked with arbitrary precision on initialised l…
We introduce a new game-theoretic semantics (GTS) for the modal mu-calculus. Our so-called bounded GTS replaces parity games with alternative evaluation games where only finite paths arise; infinite paths are not needed even when the considered transition system is infinite. The novel games offer alternative approaches to various constructions in the framework of the mu-calculus. For example, they have already been successfully used as a basis for an approach leading to a natural formula size game for the logic. While our main focus is introducing the new GTS, we also consider some application…
Many analysis and verifications tasks, such as static program analyses and model-checking for temporal logics reduce to the solution of systems of equations over suitable lattices. Inspired by recent work on lattice-theoretic progress measures, we develop a game-theoretical approach to the solution of systems of monotone equations over lattices, where for each single equation either the least or greatest solution is taken. A simple parity game, referred to as fixpoint game, is defined that provides a correct and complete characterisation of the solution of equation systems over continuous latt…
It is known that the model checking problem for the modal mu-calculus reduces to the problem of solving a parity game and vice-versa. The latter is realised by the Walukiewicz formulas which are satisfied by a node in a parity game iff player 0 wins the game from this node. Thus, they define her winning region, and any model checking algorithm for the modal mu-calculus, suitably specialised to the Walukiewicz formulas, yields an algorithm for solving parity games. In this paper we study the effect of employing the most straight-forward mu-calculus model checking algorithm: fixpoint iteration. …
Model-checking the alternating-time temporal logics ATL and ATL* with incomplete information is undecidable for perfect recall semantics. However, when restricting to memoryless strategies the model-checking problem becomes decidable. In this paper we consider two other types of semantics based on finite-memory strategies. One where the memory size allowed is bounded and one where the memory size is unbounded (but must be finite). This is motivated by the high complexity of model-checking with perfect recall semantics and the severe limitations of memoryless strategies. We show that both types…
We present a new strategic logic NCHATL that allows for reasoning about norm compliance on concurrent game structures that satisfy anonymity. We represent such game structures compactly, avoiding models that have exponential size in the number of agents. Then we show that model checking can be done in polynomial time with respect to this compact representation, even for normative systems that are not anonymous. That is, as long as the underlying game structures are anonymous, model checking normative formulas is tractable even if norms can prescribe different sets of forbidden actions to diffe…
We study stochastic games with energy-parity objectives, which combine quantitative rewards with a qualitative $ω$-regular condition: The maximizer aims to avoid running out of energy while simultaneously satisfying a parity condition. We show that the corresponding almost-sure problem, i.e., checking whether there exists a maximizer strategy that achieves the energy-parity objective with probability $1$ when starting at a given energy level $k$, is decidable and in $NP \cap coNP$. The same holds for checking if such a $k$ exists and if a given $k$ is minimal.
Model checking linear-time properties expressed in first-order logic has non-elementary complexity, and thus various restricted logical languages are employed. In this paper we consider two such restricted specification logics, linear temporal logic (LTL) and two-variable first-order logic (FO2). LTL is more expressive but FO2 can be more succinct, and hence it is not clear which should be easier to verify. We take a comprehensive look at the issue, giving a comparison of verification problems for FO2, LTL, and various sublogics thereof across a wide range of models. In particular, we look at …
Alternating-time Temporal Logic (ATL*) is a central logic for multiagent systems. Its extension to the imperfect information setting (ATL*i ) is well known to have an undecidable model-checking problem when agents have perfect recall. Studies have thus mostly focused either on agents without memory, or on alternative semantics to retrieve decidability. In this work we establish new decidability results for agents with perfect recall: We first prove a meta-theorem that allows the transfer of decidability results for classes of multiplayer games with imperfect information, such as games with hie…
It 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}})$ 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 equiv…
Reykjavik University（雷克雅未克大学）；University of Salerno（萨勒诺大学）
Verification of multi-agents systems (MAS) has been recently studied taking into account the need of expressing resource bounds. Several logics for specifying properties of MAS have been presented in quite a variety of scenarios with bounded resources. In this paper, we study a different formalism, called Priced Resource-Bounded Alternating-time Temporal Logic (PRBATL), whose main novelty consists in moving the notion of resources from a syntactic level (part of the formula) to a semantic one (part of the model). This allows us to track the evolution of the resource availability along the comp…
$μ$-Calculus and automata on infinite trees are complementary ways of describing infinite tree languages. The correspondence between $μ$-Calculus and alternating tree automaton is used to solve the satisfiability and model checking problems by compiling the modal $μ$-Calculus formula into an alternating tree automata. Thus advocating an automaton model specially tailored for working with modal $μ$-Calculus. The advantage of the automaton model is its ability to deal with arbitrary branching in a much simpler way as compare to the one proposed by Janin and Walukiewicz. Both problems (i.e., mode…
A model checking computation checks whether a given logical sentence is true in a given finite structure. Provenance analysis abstracts from such a computation mathematical information on how the result depends on the atomic data that describe the structure. In database theory, provenance analysis by interpretations in commutative semirings has been rather succesful for positive query languages (such a unions of conjunctive queries, positive relational algebra, or datalog). However, it did not really offer an adequate treatment of negation or missing information. Here we propose a new approach…
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 improvement 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 a local strategy improvement algorit…
We define memory-efficient certificates for $μ$-calculus model checking problems based on the well-known correspondence of the $μ$-calculus model checking with winning certain parity games. Winning strategies can independently checked, in low polynomial time, by observing that there is no reachable strongly connected component in the graph of the parity game whose largest priority is odd. Winning strategies are computed by fixpoint iteration following the naive semantics of $μ$-calculus. We instrument the usual fixpoint iteration of $μ$-calculus model checking so that it produces evidence in t…
In the context of formal verification in general and model checking in particular, parity games serve as a mighty vehicle: many problems are encoded as parity games, which are then solved by the seminal algorithm by Jurdzinski. In this paper we identify the essence of this workflow to be the notion of progress measure, and formalize it in general, possibly infinitary, lattice-theoretic terms. Our view on progress measures is that they are to nested/alternating fixed points what invariants are to safety/greatest fixed points, and what ranking functions are to liveness/least fixed points. That i…
In open systems verification, to formally check for reliability, one needs an appropriate formalism to model the interaction between agents and express the correctness of the system no matter how the environment behaves. An important contribution in this context is given by modal logics for strategic ability, in the setting of multi-agent games, such as ATL, ATL\star, and the like. Recently, Chatterjee, Henzinger, and Piterman introduced Strategy Logic, which we denote here by CHP-SL, with the aim of getting a powerful framework for reasoning explicitly about strategies. CHP-SL is obtained by …
Parity games have important practical applications in formal verification and synthesis, especially to solve the model-checking problem of the modal mu-calculus. They are also interesting from the theory perspective, because they are widely believed to admit a polynomial solution, but so far no such algorithm is known. We propose a new algorithm to solve parity games based on learning tangles, which are strongly connected subgraphs for which one player has a strategy to win all cycles in the subgraph. We argue that tangles play a fundamental role in the prominent parity game solving algorithms…
We consider graph games of infinite duration with winning conditions in parameterized linear temporal logic, where the temporal operators are equipped with variables for time bounds. In model checking such specifications were introduced as "PLTL" by Alur et al. and (in a different version called "PROMPT-LTL") by Kupferman et al.. We present an algorithm to determine optimal variable valuations that allow a player to win a game. Furthermore, we show how to determine whether a player wins a game with respect to some, infinitely many, or all valuations. All our algorithms run in doubly-exponentia…
Parity games have important practical applications in formal verification and synthesis, especially to solve the model-checking problem of the modal mu-calculus. They are also interesting from the theory perspective, as they are widely believed to admit a polynomial solution, but so far no such algorithm is known. In recent years, a number of new algorithms and improvements to existing algorithms have been proposed. We implement a new and easy to extend tool Oink, which is a high-performance implementation of modern parity game algorithms. We further present a comprehensive empirical evaluatio…
The coalgebraic $μ$-calculus provides a generic semantic framework for fixpoint logics with branching types beyond the standard relational setup, e.g. probabilistic, weighted, or game-based. Previous work on the coalgebraic $μ$-calculus includes an exponential time upper bound on satisfiability checking, which however requires a well-behaved set of tableau rules for the next-step modalities. Such rules are not available in all cases of interest, in particular ones involving either integer weights as in the graded $μ$-calculus, or real-valued weights in combination with non-linear arithmetic. I…
Stochastic games are a convenient formalism for modelling systems that comprise rational agents competing or collaborating within uncertain environments. Probabilistic model checking techniques for this class of models allow us to formally specify quantitative specifications of either collective or individual behaviour and then automatically synthesise strategies for the agents under which these specifications are guaranteed to be satisfied. Although good progress has been made on algorithms and tool support, efficiency and scalability remain a challenge. In this paper, we investigate a symbol…
Parity games play an important role in model checking and synthesis. In their paper, Calude et al. have shown that these games can be solved in quasi-polynomial time. We show that their algorithm can be implemented efficiently: we use their data structure as a progress measure, allowing for a backward implementation instead of a complete unravelling of the game. To achieve this, a number of changes have to be made to their techniques, where the main one is to add power to the antagonistic player that allows for determining her rational move without changing the outcome of the game. We provide …
We consider parity games on infinite graphs where configurations are represented by control-states and integer vectors. This framework subsumes two classic game problems: parity games on vector addition systems with states (vass) and multidimensional energy parity games. We show that the multidimensional energy parity game problem is inter-reducible with a subclass of single-sided parity games on vass where just one player can modify the integer counters and the opponent can only change control-states. Our main result is that the minimal elements of the upward-closed winning set of these singl…
We show a new simple algorithm that solves the model-checking problem for recursion schemes: check whether the tree generated by a given higher-order recursion scheme is accepted by a given alternating parity automaton. The algorithm amounts to a procedure that transforms a recursion scheme of order $n$ to a recursion scheme of order $n-1$, preserving acceptance, and increasing the size only exponentially. After repeating the procedure $n$ times, we obtain a recursion scheme of order $0$, for which the problem boils down to solving a finite parity game. Since the size grows exponentially at ea…
Parity games are simple infinite games played on finite graphs with a winning condition that is expressive enough to capture nested least and greatest fixpoints. Through their tight relationship to the modal mu-calculus, they are used in practice for the model-checking and synthesis problems of the mu-calculus and related temporal logics like LTL and CTL. Solving parity games is a compelling complexity theoretic problem, as the problem lies in the intersection of UP and co-UP and is believed to admit a polynomial-time solution, motivating researchers to either find such a solution or to find s…
In this paper we introduce Epistemic Strategy Logic (ESL), an extension of Strategy Logic with modal operators for individual knowledge. This enhanced framework allows us to represent explicitly and to reason about the knowledge agents have of their own and other agents' strategies. We provide a semantics to ESL in terms of epistemic concurrent game models, and consider the corresponding model checking problem. We show that the complexity of model checking ESL is not worse than (non-epistemic) Strategy Logic
We give a direct polynomial-time reduction from parity games played over the configuration graphs of collapsible pushdown systems to safety games played over the same class of graphs. That a polynomial-time reduction would exist was known since both problems are complete for the same complexity class. Coming up with a direct reduction, however, has been an open problem. Our solution to the puzzle brings together a number of techniques for pushdown games and adds three new ones. This work contributes to a recent trend of liveness to safety reductions which allow the advanced state-of-the-art in…
The window mechanism was introduced by Chatterjee et al. to reinforce mean-payoff and total-payoff objectives with time bounds in two-player turn-based games on graphs. It has since proved useful in a variety of settings, including parity objectives in games and both mean-payoff and parity objectives in Markov decision processes. We study window parity objectives in timed automata and timed games: given a bound on the window size, a path satisfies such an objective if, in all states along the path, we see a sufficiently small window in which the smallest priority is even. We show that checking…
