We investigate refinements of the mean-payoff criterion in two-player zero-sum perfect-information stochastic games. A strategy is *Blackwell optimal* if it is optimal in the discounted game for all discount factors sufficiently close to $1$. The notion of *$d$-sensitive optimality* interpolates between mean-payoff optimality (corresponding to the case $d=-1$) and Blackwell optimality ($d=\infty$). The *Blackwell threshold* $\alpha_{\sf bw} \in [0,1[$ is the discount factor above which all optimal strategies in the discounted game are guaranteed to be Blackwell optimal. The *$d$-sensitive threshold* $\alpha_{\sf d} \in [0,1[$ is defined analogously. Bounding $\alpha_{\sf bw}$ and $\alpha_{\sf d}$ are fundamental problems in algorithmic game theory, since these thresholds control the complexity for computing Blackwell and $d$-sensitive optimal strategies, by reduction to discounted games which can be solved in $O\left((1-\alpha)^{-1}\right)$ iterations. We provide the first bounds on the $d$-sensitive threshold $\alpha_{\sf d}$ beyond the case $d=-1$, and we establish improved bounds for the Blackwell threshold $\alpha_{\sf bw}$. This is achieved by leveraging separation bounds on algebraic numbers, relying on Lagrange bounds and more advanced techniques based on Mahler measures and multiplicity theorems.

This paper revisits the Brewer-Nash security policy model inspired by ethical Chinese Wall policies. We draw attention to the fact that write access can be revoked in the Brewer-Nash model. The semantics of write access were underspecified originally, leading to multiple interpretations for which we provide a modern operational semantics. We go on to modernise the analysis of information flow in the Brewer-Nash model, by adopting a more precise definition adapted from Kessler. For our modernised reformulation, we provide full mechanised coverage for all theorems proposed by Brewer & Nash. Most theorems are established automatically using the tool {log} with the exception of a theorem regarding information flow, which combines a lemma in {log} with a theorem mechanised in Coq. Having covered all theorems originally posed by Brewer-Nash, achieving modern precision and mechanisation, we propose this work as a step towards a methodology for automated checking of more complex security policy models.

Abstract $\{log\}$ (‘setlog’) is a satisfiability solver for formulas of the theory of finite sets and finite set relation algebra (FS&RA). As such, it can be used as an automated theorem prover for this theory. $\{log\}$ is able to automatically prove a number of FS&RA theorems, but not all of them. Nevertheless, we have observed that many theorems that $\{log\}$ cannot automatically prove can be divided into a few subgoals automatically dischargeable by $\{log\}$. The purpose of this work is to present a prototype interactive theorem prover (ITP), called $\{log\}$-ITP, providing evidence that a proper integration of $\{log\}$ into world-class ITP’s can deliver a great deal of proof automation concerning FS&RA. An empirical evaluation based on 210 theorems from the TPTP and Coq’s SSReflect libraries shows a noticeable reduction in the size and complexity of the proofs with respect to Coq.

Faces play a central role in the combinatorial and computational aspects of polyhedra. In this paper, we present the first formalization of faces of polyhedra in the proof assistant Coq. This builds on the formalization of a library providing the basic constructions and operations over polyhedra, including projections, convex hulls and images under linear maps. Moreover, we design a special mechanism which automatically introduces an appropriate representation of a polyhedron or a face, depending on the context of the proof. We demonstrate the usability of this approach by establishing some of the most important combinatorial properties of faces, namely that they constitute a family of graded atomistic and coatomistic lattices closed under interval sublattices. We also prove a theorem due to Balinski on the $d$-connectedness of the adjacency graph of polytopes of dimension $d$.