ABSTRACT. Zero-knowledge (ZK) protocols are well-known cryptographic primitives that allow one party to prove to another party a statement without revealing anything beyond the statement.  A ZK protocol consists of two parties: a "prover" and a "verifier".  In our work, the prover holds a secret formula and its proof of validity and needs to convince the verifier about the correctness of the proof. The verifier validates the prover's claims, by checking every step of the proof. To be able to do that without revealing any details about the formula, we use so-called commitment schemes. Commitment schemes are a fundamental part of zero-knowledge protocols as they allow a prover to commit to a value while keeping it hidden, ensuring the value cannot be altered later. A polynomial commitment scheme can be used to commit polynomials and prove the properties of the polynomials.  Our work encodes proofs as polynomials and transforms this way checking the proofs steps into checking relations between polynomials. By doing these, we are able to verify the proof without revealing the formulae (and the proof itself).

In this talk, we focus on proofs for formulas produced in the verification process and we explain how to encode them as polynomials. Initially, we developed a protocol for validating the unsatisfiability of Boolean formulas in privacy-preserving settings. We use the resolution calculus to produce a proof of unsatisfiability: we encoded each clause appearing in the proof as a polynomial and we reduced checking the correctness of the resolution rule to checking the divisibility of two polynomials. 

A natural extension of this technique is to consider more expressive logics, such as those supported by SMT (Satisfiability Modulo Theories) solvers. To this end, we extended our initial work and developed a virtual machine for validating general unsatisfiability proofs. This virtual machine can support the majority of popular theories when proving program safety while being complete and sound. To demonstrate this, we use theories of equality and linear integer arithmetic as examples. These theories require non-trivial checking procedures and we proposed optimized arithmetizations based on multiset interpretation and polynomial encodings.

Finally, we will conclude the talk by outlining how this approach benefits and empowers the verification process: we can now obtain privacy while preserving correctness.

This talk is based on the following papers:

[1] Ning Luo, Timos Antonopoulos, William Harris, Ruzica Piskac, Eran Tromer, Xiao Wang: Proving UNSAT in Zero Knowledge, CCS 2022

[2] Daniel Luick, John C. Kolesar, Timos Antonopoulos, William R. Harris, James Parker, Ruzica Piskac, Eran Tromer, Xiao Wang, Ning Luo: ZKSMT: A VM for Proving SMT Theorems in Zero Knowledge. USENIX ‘24 Security.

ABSTRACT. We report on a specific reachability problem which asks to find one-dimensional functions along the faces of a collection of cubes in three-dimensional Euclidean real space that respect certain local monotonicity criteria and certain global connectivity properties. The motivation for this problem is drawn from efforts to provide the background technology that is necessary to digitalise simple experiments in natural sciences' school classes. In particular, we aim to provide methods of logical reasoning which determine the correctness of statements about the way that variables influence each other in such experiments. Here we focus on situations in which two variables influence a third one: for example temperature and pressure influence the volume of a gas. Solving the aforementioned problem about the existence of a web of one-dimensional functions in three-dimensional space turns out to be the key to completeness and to an algorithmic approach in a calculus for reasoning about such situations.

ABSTRACT. Graph games lie at the algorithmic core of many automated design problems in computer science. These are games usually played between two players on a given graph, where the players keep moving a token along the edges according to pre-determined rules (turn-based, concurrent, etc.), and the winner is decided based on the infinite path (aka play) traversed by the token from a given initial position. In bidding games, the players initially get some monetary budgets which they need to use to bid for the privilege of moving the token at each step. Each round of bidding affects the players' available budgets, which is the only form of update that the budgets experience. We introduce bidding games with charging where the players can additionally improve their budgets during the game by collecting vertex-dependent monetary rewards, aka the "charges." Unlike traditional bidding games (where all charges are zero), bidding games with charging allow non-trivial recurrent behaviors. For example, a reachability objective may require multiple detours to vertices with high charges to earn additional budget. We show that, nonetheless, the central property of traditional bidding games generalizes to bidding games with charging: For each vertex there exists a threshold ratio, which is the necessary and sufficient fraction of the total budget for winning the game from that vertex. While the thresholds of traditional bidding games correspond to unique fixed points of linear systems of equations, in games with charging, these fixed points are no longer unique. This significantly complicates the proof of existence and the algorithmic computation of thresholds for infinite-duration objectives. We also provide the lower complexity bounds for computing thresholds for Rabin and Streett objectives, which are the first known lower bounds in any form of bidding games (with or without charging), and we solve the following repair problem for safety and reachability games that have unsatisfiable objectives: Can we distribute a given amount of charge to the players in a way such that the objective can be satisfied?

To appear in CONCUR 2024.

ABSTRACT. A classic solution technique for Markov decision processes (MDP) and stochastic games (SG) is value iteration (VI). Due to its good practical performance, this approximative approach is typically preferred over exact techniques, even though no practical bounds on the imprecision of the result could be given until recently: Over the past decade, different works derived stopping criteria, indicating when the precision reaches the desired level, for various settings, however each specialized to a specific objective and often with ad-hoc solutions. We provide a unified theoretical solution to this problem by isolating objective-specific subroutines as well as identify objective-independent concepts. These structural concepts, while surprisingly simple, form the very essence of the unified solution: We simply need to ask "Should I stay or should I go?".

Moreover, we also implement and extend this theoretical foundation in version 2.0 of the Partial Exploration Tool (PET2), adding support for stochastic games. Thereby, PET2 is the first tool implementing a sound and efficient approach for solving stochastic games with reachability/safety and mean payoff objectives. We complement this approach by developing and implementing a partial-exploration based variant for all three objectives. Our experimental evaluation shows that PET2 offers the most efficient partial-exploration based algorithm and is the most viable tool on SGs, even outperforming unsound tools.

The theory was presented at LICS 2023 and the tool at CAV 2024 (tool paper, distinguished paper award). The presentation is intended to be given by both authors and aims to cover both theory and practice.

ABSTRACT. This paper considers the problem of finding strategies that satisfy a mixture of sure and threshold objectives in Markov decision processes. We focus on a single omega-regular objective expressed as parity that must be surely met while satisfying n reachability objectives towards sink states with some probability thresholds too. We consider three variants of the problem: (a) strict and (b) non-strict thresholds on all reachability objectives, and (c) maximizing the thresholds with respect to a lexicographic order. We show that (a) and (c) can be reduced to solving parity games, and (b) can be solved in EXPTIME. Strategy complexities as well as algorithms are provided for all cases.

ABSTRACT. Turn-based discounted-sum games are two-player zero-sum games played on finite directed graphs. The vertices of the graph are partitioned between player 1 and player 2. Plays are infinite walks on the graph where the next vertex is decided by a player that owns the current vertex. Each edge is assigned an integer weight and the payoff of a play is the discounted-sum of the weights of the play. The goal of player 1 is to maximize the discounted-sum payoff against the adversarial player 2. These games lie in NP and coNP and are among the rare combinatorial problems that belong to this complexity class and the existence of a polynomial-time algorithm is a major open question. Since breaking the general exponential barrier has been a challenging problem, faster parameterized algorithms have been considered. If the discount factor is expressed in unary, then discounted-sum games can be solved in polynomial time. However, if the discount factor is arbitrary (or expressed in binary), but the weights are in unary, none of the existing approaches yield a sub-exponential bound. Our main result is a new analysis technique for a classical algorithm (namely, the strategy iteration algorithm) that presents a new runtime bound which is $n^{O ( W^{1/4} \sqrt{n} )}$, for game graphs with $n$ vertices and maximum absolute weight of at most $W$. In particular, our result yields a deterministic sub-exponential bound for games with weights that are constant or represented in unary.

ABSTRACT. We consider two-player, turn-based weighted timed games played on timed automata equipped with (positive and negative) integer weights, in which one player seeks to reach a goal location whilst minimising the cumulative weight of the underlying path. Although the value problem for such games (is the value of the game below a given threshold?) is known to be undecidable, the question of whether one can approximate this value has remained a longstanding open problem. In this paper, we resolve this question by showing that approximating arbitrarily closely the value of a given weighted timed game is computationally unsolvable.

ABSTRACT. Achieving consensus in collective systems is essential for coordinated behaviour, yet the presence of strongly opinionated minorities can disrupt opinion dynamics. In this paper, we investigate the robustness of consensus-reaching among stubborn individuals and contrarians, and we explore the effects of their interplay on consensus dynamics. We propose a methodology using formal technique of statistical model checking to quantify robustness under perturbations of the amount of disruptive individuals in the group. Unlike existing works that focus on robustness of a single group of disruptive individuals, our approach allows to investigate the robustness landscape for combinations of different disruptive agents. To this end, our approach can be used to guide the design and control of swarm robotics systems with a focus on resilience to disruptive agents.

ABSTRACT. In this extended abstract, we summarize our recent work on the efficient synthesis of sequential decision-making agents that optimize statistical properties such as maximum and average response times. In the setting of sequential decision-making, the environment is modeled as a random process that generates inputs. The agent responds to each input, aiming to maximize rewards and minimize costs within a specified time horizon. The corresponding synthesis problem is known to be PSPACE-hard in general. We consider the special case where the input distribution, reward, and cost depend on input-output statistics specified by counter automata. For such problems, we introduce the notion of statistical abstraction, which clusters statistically indistinguishable input- output sequences into equivalence classes. Using statistical abstractions, we present the first PTIME synthesis algorithms for such problems.

ABSTRACT. We present a method for constructing discrete abstractions for discrete-time, continuous-state systems. Related approaches construct a discrete bisimulation, which leaves little room for non-determinism in the outputs and quickly leads to highly complex models since all concrete behavior is covered. Our approach is to relax these requirements and build a satisficing solution: a discrete abstraction that is deterministic, robust, and as complete as possible under the given parameters. This allows us to balance granularity and computational feasibility. We leverage linearization and linear feedback control to extend the approach from globally contractive systems to systems with contractive cycles. The resulting abstraction directly induces a supervisor policy. The approach is illustrated with numerical experiments and has potential applications in various domains where system safety and reversibility are essential.

ABSTRACT. The quest for accurate modeling and simulation of dynamical systems is the Holy Grail of computational physics and numerical engineering. In deep learning, the two main approaches proposed in the literature include time series prediction and ODE modelling. Methods are based on learning (possibly locally) optimal parameters that minimize the cost associated with some suitable reachability problem. However, these two approaches fail to model specific complex dynamical systems. The presented work considers the case of modelling and predicting the behaviour of beams in particle accelerators. The difficulty lies in the associated dynamics’ highly versatile and possibly discontinuous behaviours. Extending the scope of dynamical system modelling to meet the particle accelerator modelling challenge, we present a new approach called Implicit Neural ODE (INode). INode approaches the modelling of discontinuous behaviour through integral operators; these operators are used to pre-process the data and define a classical regression problem. Finally, the global model of the dynamical system is formulated as the solution of an ODE, which contains the solution of the regression problem. INode thus enables the learning of a data-driven ODE while removing the computationally heavy ODE resolution from the training loop. The formal analysis of the approach establishes its consistency and con- vergence properties under moderate assumptions.

ABSTRACT. Polynomial, geometric, binomial, and factorial sequences all satisfy first-order recurrence relations and lie within the class of rational-valued hypergeometric sequences. The Threshold Problem for hypergeometric sequences is as follows: given such a sequence (u_n)_n and a rational constant t, decide whether u_n ≥ t for each n. We shall discuss challenging aspects of the Threshold Problem in this setting and how recent work establishes (un)conditional decidability results for subclasses of hypergeometric sequences---those with quadratic parameters alluded to in the title.

ABSTRACT. Many challenges of fully automated verification of recursive programs are rooted in the hardness of generating appropriate invariants (relations among variables that hold throughout program execution). This work focuses on algebraic invariants of simple linear loops (branch-free loop programs with a single linear update). Whilst this model is elementary, even the most natural verification problems (such as termination and reachability) are arguably difficult in this setting, see Ouaknine and Worrell, https://doi.org/10.1145/2766189.2766191. As a crucial step to understanding possible relations among variables of a simple linear loop, we present a polynomial-space algorithm to compute a representation of the strongest algebraic invariant of a given loop. This set comprises all invariant polynomial equalities. We further discuss the complexity of verifying whether a given algebraic relation, that is, a collection of polynomial equalities in loop variables, is a loop invariant. Finally, we turn to synthesising simple linear loops from desired relations. Specifically, we ask whether there exists a simple linear loop that possesses a given algebraic invariant. Notably, this problem is as hard as Hilbert's Tenth Problem and thus undecidable over the integers, while decidability is open over the rationals. To this end, we explore the complexity landscape for bit-bounded loop synthesis, where the bound on the number of bits used to describe the loop is an input parameter. We show that this problem admits a polynomial-space algorithm.

The material in this presentation is based on the work undertaken in https://arxiv.org/abs/2407.09154.