Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2609.34878

Synthesizing Update Schedules with Game-Based Extension of Bounded Model Checking

Janis Kröger·Paul Kröger·Martin Fränzle
View original source ↗Read source document ↗Export metadata ↓

Abstract

Ensuring safe software updates in safety-critical systems without interrupting operation and without provisioning and activating cold spare hardware poses a fundamental challenge due to the conflict between system availability and update execution. In this paper, we present a bounded SMT encoding for synthesizing fixed global-time update schedules for timed-games with linear update automata and a fixed number of update transitions. We model the interaction between the system and the update as a two-player timed game. Our key contribution is the synthesis of global time points that define a fixed update schedule which guarantees safe and complete deployment of the update independently of the autonomous system behavior. To this end, we reduce the scheduling problem to a reachability and safety objective and encode it as a quantified SMT problem. We demonstrate it on an example system of a trajectory planner for autonomous driving, showing that the synthesized schedule ensures safe deployment under all admissible executions.

Explore related subjects

cs.GTcs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Janis Kröger, Paul Kröger, Martin Fränzle. 2026-09-28. Synthesizing Update Schedules with Game-Based Extension of Bounded Model Checking. https://doi.org/10.4204/eptcs.452.2

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

LLM Bidders Preserve the Mechanism-Level Orderings of Human Bidders

Training on vast amounts of human-generated data has motivated growing interest in using large language models (LLMs) to simulate human behavior. We ask which features of human behavior general-purpose models preserve when used out of the box in auctions, where multiple bidders interact under explicit rules and incentives. We evaluate five LLMs across seven laboratory settings against human benchmarks reconstructed from published experiments, with uncertainty bands for the private-value comparisons. Our main focus is on three large models without extended test-time reasoning: GPT-4o, Claude~3.5 Haiku, and Gemini~2.0 Flash. LLM and human deviations from theory differ in magnitude and often in direction: humans overbid in second-price auctions, whereas most models that deviate underbid. Surprisingly, without task-specific fine-tuning or calibration to human bids, the three non-reasoning large models robustly preserve key orderings of auction formats by deviation from theory. First-price auctions are harder than second-price, and ascending clocks reduce deviations relative to sealed bids wherever data are adequate. Kendall's $τ_b$ between the human and GPT-4o difficulty rankings is $0.60$ and positive in every joint bootstrap draw. The reasoning model bids almost at equilibrium in the observed private-value settings, leaving little variation in errors to compare; the small model's large errors yield an inverted ranking. All five models nevertheless reproduce the stronger first-price winner's curse. Clock framing improves bidding for two of the three non-reasoning large models, and GPT-4o recovers the ordering of last-minute bidding across closing rules in an eBay-style marketplace.

cs.GT↗
arXiv2026

Dynamic Transaction Scheduling and Pricing in the Ethereum Mempool

The Ethereum blockchain utilizes the EIP-1559 algorithm to manage transaction inclusion and block assembly. However, EIP-1559 and much of the existing literature study this problem from a static perspective, focusing on price evolution without modelling transaction dynamics within the mempool. Motivated by this limitation, we study a dynamic transaction scheduling problem in which transactions with heterogeneous sizes and per-unit values arrive over time and remain in the mempool until scheduled. To capture the stochastic mempool evolution, we formulate the problem as a Markov Decision Process (MDP) whose state represents the mempool configuration and whose actions correspond to block prices. We first provide a primal-dual interpretation of the static EIP-1559 mechanism, showing that block prices arise naturally as dual variables of a social-welfare maximization problem. Building on this perspective, we extend the framework to the dynamic setting and formulate an objective that maximizes long-run discounted reward while incorporating holding costs and overshoot penalties. We then employ a Natural Policy Gradient (NPG) algorithm to compute the optimal policy. Our results show that dynamic pricing stabilizes the mempool while maximizing long-run discounted reward. In particular, as the overshoot penalty increases, the average scheduled transaction volume converges to the target block capacity, and the resulting NPG updates closely resemble the EIP-1559 price update rule. Finally, we study two special cases of the MDP formulation: homogeneous transactions and uniform arrivals. In the homogeneous setting, where the protocol directly controls scheduled volume, we show that the optimal policy has a threshold structure. We then propose a bang-bang pricing mechanism for uniform arrivals and derive a lower bound on the block capacity needed to ensure system stability.

cs.GT↗
arXiv2026

Computational Complexity of Strong and Average Justified Representation

We study the approval-based multiwinner election problem where a set of $n$ voters cast approval-based ballots to a set of $m$ candidates, and we are to select a winner committee consisting of $k$ candidates. We consider two axioms: strong justified representation (SJR) and average justified representation (AJR). A winner committee satisfies SJR if the satisfaction for each voter in every $\ell$-cohesive group is at least $\ell$. AJR is a weaker axiom that requires the average satisfaction for each $\ell$-cohesive group to be at least $\ell$. It is well known that a winner committee satisfying AJR may not exist (and neither does SJR). In this paper, we study the computational complexity of the following decision problem: given an approval-based multiwinner election instance, decide if there exists a winner committee satisfying SJR/AJR. We prove that this problem is $Θ_2^p$-complete for SJR, and $Σ_2^p$-complete for AJR. As byproducts, we derive some results that are interesting in their own right. Firstly, we show that adding one more adaptive query to an NP oracle on top of polynomially many non-adaptive NP queries does not add more computational power, and the resulting complexity class is still $Θ_2^p$. Secondly, we construct a set system that can be useful in other applications, especially when doing reductions from typical satisfiability problems such as 3SAT.

cs.GT↗