Search

We consider the controller synthesis problem for stochastic, continuous-state, nonlinear systems against ω-regular specifications. We synthesize a symbolic controller that ensures almost sure (qualitative) satisfaction of the specification. The problem reduces, after some automata-theoretic constructions, to computing the almost sure winning region—the largest set of states from which a parity condition can be satisfied with probability 1 (on a possibly hybrid state space). While characterizing the exact almost sure winning region is still open for the considered system class, we propose an algorithm for obtaining a tight under-approximation of this set. The heart of our approach is a technique to symbolically compute this under-approximation via a finite-state abstraction as a 21/2-player parity game. Our abstraction procedure uses only the support of the probabilistic evolution; it does not use precise numerical transition probabilities. We have implemented our approach and evaluated it on the nonlinear model of the perturbed Dubins vehicle.

International audience; The resource-bounded alternating-time temporal logic RB±ATL combines strategic reasoning with reasoning about resources. Its model-checking problem is known to be 2EXPTIME-complete (the same as its proper extension RB±ATL$^⁎$) and fragments have been identified to lower the complexity.In this work, we consider the variant RB±ATL+ that allows for Boolean combinations of path formulae starting with single temporal operators, but restricted to a single resource, providing an interesting trade-off between temporal expressivity and resource analysis. We show that the model-checking problem for RB±ATL+ restricted to a single agent and a single resource is $\Delta_{2}^{P}$-complete, hence the same as for the standard branching-time temporal logic CTL+. In this case reasoning about resources comes at no extra computational cost. When a fixed finite set of linear-time temporal operators is considered, the model-checking problem drops to PTIME, which includes the special case of RB±ATL restricted to a single agent and a single resource. Furthermore, we show that, with an arbitrary number of agents and a fixed number of resources, the model-checking problem for RB±ATL+ can be solved in EXPTIME using a sophisticated Turing reduction to the parity game problem for alternating vector addition systems with states (AVASS).

We consider quantitative notions of parity automaton and parity game aimed at modelling resource-aware behaviour, and study (memory-full) strategies for exhibiting accepting runs that require a minimum amount of initial resources, respectively for winning a game with minimum initial resources. We also show how such strategies can be simplified to consist of only two types of moves: the former aimed at increasing resources, the latter aimed at satisfying the acceptance condition., Comment: In Proceedings GandALF 2019, arXiv:1909.05979

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 games. We then show that this algorithm is in fact identical to two earlier published fixpoint algorithms for parity games and thus that these earlier algorithms are the same. Furthermore, we modify our algorithm to only partially recompute deeper fixpoints after updating a higher set and show that this modification enables a simple method to obtain winning strategies. We show that the resulting algorithm is simple to implement and offers good performance on practical parity games. We empirically demonstrate this using games derived from model-checking, equivalence checking and reactive synthesis and show that our fixpoint algorithm is the fastest solution for model-checking games., In Proceedings GandALF 2019, arXiv:1909.05979

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 superpolynomial lower bounds for existing algorithms to improve the understanding of parity games. We present a parameterized parity game called the Two Counters game, which provides an exponential lower bound for a wide range of attractor-based parity game solving algorithms. We are the first to provide an exponential lower bound to priority promotion with the delayed promotion policy, and the first to provide such a lower bound to tangle learning., Comment: In Proceedings GandALF 2019, arXiv:1909.05979

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 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 \emph{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 QP. Moreover, we improve the exponent in known exponential bounds on satisfiability checking., Comment: extended version of conference paper

We propose a symbolic self-triggered controller synthesis procedure for non-deterministic continuous-time nonlinear systems without stability assumptions. The goal is to compute a controller that satisfies two objectives. The first objective is represented as a specification in a fragment of LTL, which we call 2-LTL. The second one is an energy objective, in the sense that control inputs are issued only when necessary, which saves energy. To this end, we first quantise the state and input spaces, and then translate the controller synthesis problem to the computation of a winning strategy in a mean-payoff parity game. We illustrate the feasibility of our method on the example of a navigating nonholonomic robot., 16th International Conference on Control, Automation, Robotics and Vision (ICARCV 2020)

Parity games are two player games with omega-winning conditions, played on finite graphs. Such games play an important role in verification, satisfiability and synthesis. It is therefore important to identify algorithms that can efficiently deal with large games that arise from such applications. In this paper, we describe our experiments with BDD-based implementations of four parity game solving algorithms, viz. Zielonka's recursive algorithm, the more recent Priority Promotion algorithm, the Fixpoint-Iteration algorithm and the automata based APT algorithm. We compare their performance on several types of random games and on a number of cases taken from the Keiren benchmark set., Comment: In Proceedings GandALF 2018, arXiv:1809.02416

Cost-parity games are a fundamental tool in system design for the analysis of reactive and distributed systems that recently have received a lot of attention from the formal methods research community. They allow to reason about the time delay on the requests granted by systems, with a bounded consumption of resources, in their executions. In this paper, we contribute to research on cost-parity games by combining them with hierarchical systems, a successful method for the succinct representation of models. We show that determining the winner of a Hierarchical Cost-parity Game is Pspace -complete, thus matching the complexity of the proper special case of Hierarchical Parity Games. This shows that reasoning about temporal delay can be addressed at a free cost in terms of complexity.

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 exponential 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 solving such games. Also, it proved to be resistant to a lower bound attack, even more than the strategy improvements approaches, but finally Friedmann provided a family of games on which the algorithm requires exponential time. 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 possible intertwining of the above mentioned techniques can help mitigating the exponential nature of the divide et impera approaches. The resulting worst case is even more robust than that, since it serves as a lower bound for progress measures based algorithms as well, such as Small Progress Measure and its quasi-polynomial variant recently proposed by Jurdzinski and Lazic.

Parity games play an important role for LTL synthesis as evidenced by recent breakthroughs on LTL synthesis, which rely in part on parity game solving. Yet state space explosion remains a major issue if we want to scale to larger systems or specifications. In order to combat this problem, we need to investigate symbolic methods such as BDDs, which have been successful in the past to tackle exponentially large systems. It is therefore essential to have symbolic parity game solving algorithms, operating using BDDs, that are fast and that can produce the winning strategies used to synthesize the controller in LTL synthesis. Current symbolic parity game solving algorithms do not yield winning strategies. We now propose two symbolic algorithms that yield winning strategies, based on two recently proposed fixpoint algorithms. We implement the algorithms and empirically evaluate them using benchmarks obtained from SYNTCOMP 2020. Our conclusion is that the algorithms are competitive with or faster than an earlier symbolic implementation of Zielonka's recursive algorithm, while also providing the winning strategies., Comment: In Proceedings GandALF 2020, arXiv:2009.09360

Parity games are infinite two-player games played on node-weighted directed graphs. Formal verification problems such as verifying and synthesizing automata, bounded model checking of LTL, CTL*, propositional µ-calculus, ...reduce to problems over parity games. The core problem of parity game solving is deciding the winner of some (or all) nodes in a parity game. In this paper, we improve several parity game solvers by using a justification graph. Experimental evaluation shows our algorithms improve upon the state-of-the-art. ispartof: pages:449-470 ispartof: Proceedings of VMCAI 2020 vol:11990 pages:449-470 ispartof: 21st International Conference on Verification, Model Checking, and Abstract Interpretation location:New Orleans date:19 Jan - 21 Jan 2020 status: Published online

Family-based SPL model checking concerns the simultaneous verification of multiple product models, aiming to improve on enumerative product-based verification, by capitalising on the common features and behaviour of products in a software product line (SPL), typically modelled as a featured transition system (FTS). We propose efficient family-based SPL model checking of modal \(\mu \)-calculus formulae on FTSs based on variability parity games, which extend parity games with conditional edges labelled with feature configurations, by reducing the SPL model checking problem for the modal \(\mu \)-calculus on FTSs to the variability parity game solving problem, based on an encoding of FTSs as variability parity games. We validate our contribution by experiments on SPL benchmark models, which demonstrate that a novel family-based algorithm to collectively solve variability parity games, using symbolic representations of the configuration sets, outperforms the product-based method of solving the standard parity games obtained by projection with classical algorithms.

We discuss expansions of \(\mathsf {CTL}\) with connectives able to express Streett fairness objectives for single paths. We focus on \(\mathsf {(E)SFCTL}\): (Extended) Streett-Fair \(\mathsf {CTL}\) inspired by a seminal paper of Emerson and Lei. Unlike several other fair extensions of \(\mathsf {CTL}\), our entire formalism (not just a subclass of formulas in some canonical form) allows a succinct embedding into the \(\mu \)-calculus, while being able to express concisely all relevant types of path-based fairness objectives. We implement our syntax in the well-known symbolic model checker NuSMV, consequently also implementing \(\mathsf {CTL}\) model checking with “compassion” objectives. Since the \(\mu \)-calculus embedding requires only alternation depth two, the resulting specifications correspond to parity games with two priorities. This allows a comparison of the performance of our NuSMV\(^{\mathsf {sf}}\) with existing parity game solvers (both explicit and symbolic). The advantages of the symbolic approach seem to extend to fair model checking.

This paper presents an abstraction-refinement based framework for optimal controller synthesis of discrete-time systems with respect to $\omega$-regular objectives. It first abstracts the discrete-time “concrete” system into a finite weighted transition system using a finite partition of the state-space. Then, a two-player mean payoff parity game is solved on the product of the abstract system and the Buchi automaton corresponding to the $\omega$-regular objective, to obtain an optimal “abstract” controller that satisfies the $\omega$-regular objective. The abstract controller is guaranteed to be implementable in the concrete discrete-time system, with a sub-optimal cost. The abstraction is refined with finer partitions to reduce the suboptimality. In contrast to existing formal controller synthesis algorithms based on abstractions, this technique provides an upper bound on the trajectory cost when implementing the suboptimal controller. A robot surveillance scenario is presented to illustrate the feasibility of the approach.

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 lattices, a quite general class of lattices widely used in semantics. For powerset lattices the fixpoint game is intimately connected with classical parity games for $\mu$-calculus model-checking, whose solution can exploit as a key tool Jurdzi\'nski's small progress measures. We show how the notion of progress measure can be naturally generalised to fixpoint games over continuous lattices and we prove the existence of small progress measures. Our results lead to a constructive formulation of progress measures as (least) fixpoints. We refine this characterisation by introducing the notion of selection that allows one to constrain the plays in the parity game, enabling an effective (and possibly efficient) solution of the game, and thus of the associated verification problem. We also propose a logic for specifying the moves of the existential player that can be used to systematically derive simplified equations for efficiently computing progress measures. We discuss potential applications to the model-checking of latticed $\mu$-calculi and to the solution of fixpoint equations systems over the reals.

We propose “semantic labelling” as a novel ingredient for solving games in the context of LTL synthesis. It exploits recent advances in the automata-based approach, yielding more information for each state of the generated parity game than the game graph can capture. We utilize this extra information to improve standard approaches as follows. (i) Compared to strategy improvement (SI) with random initial strategy, a more informed initialization often yields a winning strategy directly without any computation. (ii) This initialization makes SI also yield smaller solutions. (iii) While Q-learning on the game graph turns out not too efficient, Q-learning with the semantic information becomes competitive to SI. Since already the simplest heuristics achieve significant improvements the experimental results demonstrate the utility of semantic labelling. This extra information opens the door to more advanced learning approaches both for initialization and improvement of strategies.

In a mean-payoff parity game, one of the two players aims both to achieve a qualitative parity objective and to minimize a quantitative long-term average of payoffs (aka. mean payoff). The game is zero-sum and hence the aim of the other player is to either foil the parity objective or to maximize the mean payoff. Our main technical result is a pseudo-quasi-polynomial algorithm for solving mean-payoff parity games. All algorithms for the problem that have been developed for over a decade have a pseudo-polynomial and an exponential factors in their running times; in the running time of our algorithm the latter is replaced with a quasi-polynomial one. By the results of Chatterjee and Doyen (2012) and of Schewe, Weinert, and Zimmermann (2018), our main technical result implies that there are pseudo-quasi-polynomial algorithms for solving parity energy games and for solving parity games with weights. Our main conceptual contributions are the definitions of strategy decompositions for both players, and a notion of progress measures for mean-payoff parity games that generalizes both parity and energy progress measures. The former provides normal forms for and succinct representations of winning strategies, and the latter enables the application to mean-payoff parity games of the order-theoretic machinery that underpins a recent quasi-polynomial algorithm for solving parity games.

Small Progress Measures is one of the classical parity game solving algorithms. For games with n vertices, m edges and d different priorities, the original algorithm computes the winning regions and a winning strategy for one of the players in O(dm.(n/floor(d/2))^floor(d/2)) time. Computing a winning strategy for the other player requires a re-run of the algorithm on that player's winning region, thus increasing the runtime complexity to O(dm.(n/ceil(d/2))^ceil(d/2)) for computing the winning regions and winning strategies for both players. We modify the algorithm so that it derives the winning strategy for both players in one pass. This reduces the upper bound on strategy derivation for SPM to O(dm.(n/floor(d/2))^floor(d/2)). At the basis of our modification is a novel operational interpretation of the least progress measure that we provide., Comment: In Proceedings GandALF 2015, arXiv:1509.06858