More about HKUST
Algorithmic Optimization and Verification for Decentralized and Probabilistic Systems
The Hong Kong University of Science and Technology
Department of Computer Science and Engineering
PhD Thesis Defence
Title: "Algorithmic Optimization and Verification for
Decentralized and Probabilistic Systems"
By
Mr. Sergei NOVOZHILOV
Abstract:
Modern computational systems have stepped beyond classical settings. They may
exhibit stochastic behavior, operate in distributed environments whose
participants are financially motivated toward certain outcomes, or be subject
to non-standard resource constraints. Some systems do not perform computation
themselves, yet pose challenging computational tasks in their analysis.
Examples of such systems range from probabilistic programs and recursive
programs modeled by recurrence systems, to blockchain protocols and dynamic
graphs of exchange rates.
For such domains, computability and complexity theory often gives negative or
incomplete answers, from undecidability to NP-hardness. Yet these worst case
barriers do not explain when quantitative analysis is possible for structured
instances arising in practice.
In this thesis, we develop tailored analysis methods for several such
domains. The common strategy is to identify problem-specific structure, for
instance the regular structure of infinite-state Markov chains induced by
probabilistic counter programs, the polynomial nature of recursive
constraints, and structural sparsity in transaction dependencies and graphs
of decentralized-exchange routes. As a consequence, we obtain tractability
results, decision procedures, and techniques capable of scaling to instances
seen in practice.
We first develop methods for two central problems in program analysis:
automated resource analysis for recursive programs and termination analysis
for probabilistic counter programs. For recursive programs, we obtain a
semi-completeness result for synthesizing tight polynomial upper bounds on
their runtime. For almost-sure termination of probabilistic counter programs,
we prove a sharp boundary between one-dimensional and higher-dimensional
systems: the problem is decidable for the former class, while it remains
undecidable for the latter.
We next extend this structure-aware perspective to revenue optimization when
constructing blockchain blocks by selecting and ordering transactions.
Dependencies among Cardano transactions and Ethereum gas costs that vary with
ordering lead to distinct optimization problems, which we solve using
tailored combinatorial algorithms and learning methods. In both cases, we
obtain algorithms that scale to real-world instances, with experimentally
observed annual revenue improvements of $0.4 million and $63 million,
respectively, based on retrospective experiments.
Finally, we study routing in decentralized exchanges, where liquidity is
fragmented and price updates are frequent, making shortest path computation
both economically important and algorithmically delicate. We exploit the
empirically low treewidth of exchange graphs to support efficient route
queries with formal guarantees, showing again how a carefully chosen
structural parameter can turn an intractable worst case problem into a
practical algorithmic tool.
Overall, the thesis demonstrates a phenomenon across domains in which
problems that are intractable in the worst case exhibit structural properties
not captured by classical theory. Accounting for these properties leads to
algorithms that are both practically efficient and theoretically grounded,
highlighting the limitations of worst case analysis as a sole predictor of
computational feasibility.
Date: Thursday, 3 September 2026
Time: 4:15pm - 6:15pm
Venue: TBC
Chairman: Prof. Weiping LI (MATH)
Committee Members: Dr. Dimitris PAPADOPOULOS (Supervisor)
Dr. Amir GOHARSHADY (Co-Supervisor, University of Oxford)
Dr. Lionel PARREAUX
Prof. Pedro SANDER
Dr. Maximilian Alexander NITZSCHNER (MATH)
Prof. William KNOTTENBELT (Imperial College London)