arXiv subjects

Calvin Chau

Publications and source records attributed to Calvin Chau.

5 recordsLinked to original sources

arXiv2026

Towards Actionable Strategy Certificates in Stochastic Parity Games

We propose a new approach for synthesizing large sets of winning strategies in stochastic parity games (2.5-player games) with quantitative objectives. Instead of computing a single, fully specified winning strategy, we introduce Actionable Strategy Certificates (ASCerts) as a local and permissive representation of a large class of system player winning strategies. To this end, we extend known certificates for stochastic invariants to the setting of games. Our certificates prove that synthesized strategies remain within a safe region of the game with probability at least $\lambda \in [0,1]$. As such, the certificates enhance the trustworthiness of synthesized strategies. The crux of our approach is to reinterpret and leverage the certificates as concise, local, and permissive representation of (possibly infinitely many) strategies. By carefully combining our certificates for stochastic invariants with strategy templates for almost-sure winning, we obtain a novel local representation of quantitatively winning strategies in stochastic parity games. This enables efficient synthesis, adaptation, and runtime strategy extraction, making ASCerts well suited for logical control in uncertain and adversarial environments. We provide a proof-of-concept implementation and demonstrate the potential of applying ASCerts in runtime adaptation on a case study.

cs.GT↗

arXiv2026

Concurrent Permissive Strategy Templates

Two-player games on finite graphs provide a rigorous foundation for modeling the strategic interaction between reactive systems and their environment. While concurrent game semantics naturally capture the synchronous interactions characteristic of many cyber-physical systems (CPS), their adoption in CPS design remains limited. Building on the concept of permissive strategy templates (PeSTels) for turn-based games, we introduce concurrent (permissive) strategy templates (ConSTels) -- a novel representation for sets of randomized winning strategies in concurrent games with Safety, B\"uchi, and Co-B\"uchi objectives. ConSTels compactly encode infinite families of strategies, thereby supporting both offline and online adaptation. Offline, we exploit compositionality to enable incremental synthesis: combining ConSTels for simpler objectives into non-conflicting templates for more complex combined objectives. Online, we demonstrate how ConSTels facilitate runtime adaptation, adjusting action probabilities in response to observed opponent behavior to optimize performance while preserving correctness. We implemented ConSTel synthesis and adaptation in a prototype tool and experimentally show its potential.

cs.GT↗

arXiv2025

Certificates and Witnesses for Multi-objective {\omega}-regular Queries in Markov Decision Processes

Multi-objective probabilistic model checking is a powerful technique for verifying stochastic systems against multiple (potentially conflicting) properties. To enhance the trustworthiness and explainability of model checking tools, we present independently checkable certificates and witnesses for multi-objective {\omega}-regular queries in Markov decision processes. For the certification, we extend and improve existing certificates for the decomposition of maximal end components and reachability properties. We then derive mixed-integer linear programs (MILPs) for finding minimal witnessing subsystems. For the special case of Markov chains and LTL properties, we use unambiguous B\"uchi automata to find witnesses, resulting in an algorithm that requires single-exponential space. Existing approaches based on deterministic automata require doubly-exponential space in the worst case. Finally, we consider the practical computation of our certificates and witnesses and provide an implementation of the developed techniques, along with an experimental evaluation, demonstrating the efficacy of our techniques.

cs.LO↗

arXiv2024

Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes

Certifying verification algorithms not only return whether a given property holds or not, but also provide an accompanying independently checkable certificate and a corresponding witness. The certificate can be used to easily validate the correctness of the result and the witness provides useful diagnostic information, e.g. for debugging purposes. Thus, certificates and witnesses substantially increase the trustworthiness and understandability of the verification process. In this work, we consider certificates and witnesses for multi-objective reachability-invariant and mean-payoff queries in Markov decision processes, that is conjunctions or disjunctions either of reachability and invariant or mean-payoff predicates, both universally and existentially quantified. Thereby, we generalize previous works on certificates and witnesses for single reachability and invariant constraints. To this end, we turn known linear programming techniques into certifying algorithms and show that witnesses in the form of schedulers and subsystems can be obtained. As a proof-of-concept, we report on implementations of certifying verification algorithms and experimental results.

cs.LO↗

arXiv2023

Syntactic vs Semantic Linear Abstraction and Refinement of Neural Networks

Abstraction is a key verification technique to improve scalability. However, its use for neural networks is so far extremely limited. Previous approaches for abstracting classification networks replace several neurons with one of them that is similar enough. We can classify the similarity as defined either syntactically (using quantities on the connections between neurons) or semantically (on the activation values of neurons for various inputs). Unfortunately, the previous approaches only achieve moderate reductions, when implemented at all. In this work, we provide a more flexible framework where a neuron can be replaced with a linear combination of other neurons, improving the reduction. We apply this approach both on syntactic and semantic abstractions, and implement and evaluate them experimentally. Further, we introduce a refinement method for our abstractions, allowing for finding a better balance between reduction and precision.

cs.LO↗