Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2609.37728

Formal Reasoning about Performance Models

Moussa Labbadi·Rupak Majumdar·V. R. Sathiyanarayana·Sadegh Soudjani
View original source ↗Read source document ↗Export metadata ↓

Abstract

Discrete-event simulation is a standard technique for modelling and analysing the performance of computer systems, networks, and services. Although simulation tools are widely used, reasoning about the correctness and performance guarantees of the models they implement remains largely ad hoc: simulation outputs are interpreted statistically, but there is no logical foundation for deductive reasoning about their behaviour. We present a core imperative calculus that captures the essential constructs common to discrete-event simulators: asynchronous execution, continuous and discrete sampling from distributions, and time-based event scheduling through a global event queue. On top of this calculus, we develop a proof system for reasoning about almost-sure reachability and expected reaching time properties. Our main result is a sound and complete proof rule for these properties. Our framework generalizes deductive reasoning for discrete-time probabilistic programs to the setting of performance models, in which continuous time and continuous probability distributions are central. We have implemented the proof rules in a tool embedded in Lean. We demonstrate the applicability of our proof rule by deriving proofs of almost-sure reachability and expected reaching time for a number of case studies, including client-server examples that go beyond analytic solutions from queueing theory as well as convergence behaviours in network routing protocols. Establishing the soundness and completeness of our proof rules requires significantly more complex arguments than in the discrete-time setting. This is due to the fundamentally discontinuous nature of the operational semantics and the measure-theoretic challenges of continuous time and probability distributions.

Explore related subjects

cs.LOcs.PFcs.PL

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Moussa Labbadi, Rupak Majumdar, V. R. Sathiyanarayana, Sadegh Soudjani. 2026-09-29. Formal Reasoning about Performance Models. https://arxiv.org/abs/2609.37728

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

KEEP EXPLORING

Related papers

arXiv2026

New Proofs of Weak Normalization for Propositional Logic

We present new proofs of weak normalization for intuitionistic and classical propositional logics (with the full set of operators -- falsum, implication, conjunction and disjunction). These proofs work with cuts rather than cut segments, and they provide explicit ``local'' rules for determining whether to contract a whole proof or reduce one of its subproofs, and in the latter case, which subproof to reduce. Interestingly, much of the complication in the case of intuitionistic logic is due to the disjunction elimination rule, while our version of the same rule for classical logic has falsum as conclusion always, and so is much easier to handle. All the complication in the case of classical logic shifts to cuts involving the reductio ad absurdum rule. We also discuss a formalization of the entire proof in Lean, and present a deterministic algorithm for weak normalization.

cs.LO↗
arXiv2026

Flip-packability: uniform characterisations of tame graph classes

A class of graphs is monadically dependent if one cannot encode all graphs in coloured graphs from the class using a fixed first-order formula, and monadically stable if one cannot even encode arbitrarily long linear orders. Bonnet et al. (ICALP 2025) characterised monadic dependence by flip-separability: for every vertex weighting, boundedly many flips - complementations of the adjacency relation within a vertex subset - make every ball of radius $r$ carry at most an $\varepsilon$-fraction of the weight, so that every set carrying an $\varepsilon$-fraction has two elements pulled apart. We introduce flip-packability: boundedly many graphs, each obtained from the input by boundedly many flips and all determined by the weighting before any set is presented, such that every set carrying an $\varepsilon$-fraction of the weight has $m$ elements pairwise far apart in one of them. The number of flips producing each graph depends on the radius alone; only the number of graphs depends on $\varepsilon$ and $m$. We prove that a class of graphs is flip-packable if and only if it is monadically stable, and $2$-flip-packable, that is, flip-packable with $m=2$, if and only if it is monadically dependent. The passage from two scattered elements to $m$ is thus exactly what separates the two notions. For monadically stable classes we show that the flipped graphs can be computed from the weighting in cubic time. Varying the three parameters of the definition - the sparsifying operation, the radius, and the number $m$ of elements scattered - produces eight known characterisations of sparse and dense graph classes from the same template. In each case $m$ separates a depth-like notion from its width-like relaxation: treedepth from treewidth, shrubdepth from cliquewidth, and monadic stability from monadic dependence.

cs.LO↗
arXiv2026

A Rank-Preserving Gaifman Normal Form for First-Order Logic on Weighted Structures

We prove a rank-preserving version of Gaifman's Theorem. Compared to earlier rank-preserving locality theorems (in particular, [Grohe, Kreutzer, Siebertz, JACM 2017]), our theorem is much simpler and yields formulas in exactly the same normal form as Gaifman's original theorem. Furthermore, it holds not only for first-order logic, but also for first-order logic with modulo-counting quantifiers and, more generally, for the first-order logic on weighted structures ngFOW+ that is introduced in this article. As an application of our theorem, we give a simplified proof of the algorithmic meta-theorem of [Grohe, Kreutzer, Siebertz, JACM 2017] stating that first-order properties of nowhere dense structures can be decided in almost-linear time. Our locality theorem for the weight logic ngFOW+ can be seen as an essential step toward such a meta-theorem for this logic.

cs.LO↗