A block is an extended finite state machine

Every mechanism is one block with a fixed set of fields mined from the spec: a trigger that activates it, a guard that says when it is meaningful, an action, an objective, a configuration of toggles and parameters, typed dependencies to other blocks, and its own internal state machine. The guard does the work. Backoff is meaningful only if a failure signal exists, so removing all feedback turns it into dead code.

Four dependency types separate a legal protocol from a broken one

Strong edges are co-required, ACK and retransmission travel together. Conditional edges gate validity, backoff is valid only if a feedback signal exists. Weak edges are optional and toggleable, RTS/CTS improves carrier sense but can be switched off, and most of the design space lives on them. Independent blocks share no state and compose freely.

A protocol is a graph of blocks, and each decision has a home layer

CSMA/CA equals ALOHA plus a strong carrier-sense block plus an optional weak RTS/CTS block. Protocols differ by which blocks are present and how the edges wire them, not by being written from scratch.

Where each decision sits is fixed by layer: when to transmit at the MAC, the route at the network layer, the sending rate at transport, connection state and handover at the control plane. Wi-Fi owns PHY and MAC only; 5G owns the full access-stratum stack; NTN is that stack under long delay and Doppler; the transport protocols own transport.

A generate-evaluate-refine loop whose verifier is sound

Synthesis runs as generate, evaluate, refine, the pattern the recent AI-for-systems work established. Its documented failure is reward hacking when the verifier is incomplete. teNET replaces the gameable benchmark with a sound certificate, so the loop cannot reward-hack into a protocol that can collapse.

Two certificate families, one objective rule

Wi-Fi for depth, 5G for novelty, NTN for the frontier

Built on her doctoral thesis, and a year at Skylark Wireless

teNET grows directly out of two things. The first is her doctoral thesis, Learning-Driven Frameworks for Self-Driving Protocols in Next-Generation Networks, which introduced the idea of treating protocol mechanisms as learnable, composable building blocks rather than a hand-tuned monolith. The second is a year as a full-time research intern at Skylark Wireless LLC, working on on-device resource allocation and MU-MIMO scheduling in massive MIMO; the IEEE WCNC 2024 paper below is the on-device result of that work. teNET adds the three pieces the thesis line was missing: a generative model as the proposer, a sound certificate as the gate, and generalization beyond Wi-Fi MAC to the 5G and NTN stacks. The thesis is the foundation; this program is what it grew into.

teNET, running

The same pipeline on three technologies. Each run mines blocks from the spec, proposes a composition, gets vetoed by the certificate, refines against the reason it failed, and only then reaches the simulator. Numbers are illustrative until the benchmark lands.

$ tenet synth --spec 802.11ax --objective pf --density 50
mining blocks ............ 7 blocks: DCF, BEB, RTS/CTS, HARQ, OFDMA, TWT, MLO
dependency graph ......... 4 strong, 3 conditional, 5 weak edges
proposer  candidate #1 ... CW=[16,1024], HARQ on, TWT off
certificate (R0) ......... R0 = 1.37  >= 1   REJECTED
   reason: contention window too small at density 50
proposer  candidate #2 ... CW=[64,4096], HARQ on, TWT thinning  (refined)
certificate (R0) ......... R0 = 0.41  < 1    ADMITTED
simulator (ns-3 ax) ...... goodput 612 Mbps, p99 8.3 ms, Jain 0.94
deploy: distributed, per-station DCF _

$ tenet synth --spec 3gpp-rach --objective access-delay --ues 2000
mining blocks ............ RACH preamble, backoff, power ramping, msg3
dependency graph ......... 3 strong, 2 conditional, 2 weak edges
proposer  candidate #1 ... backoff 20 ms, 64 preambles
certificate (R0) ......... R0 = 1.12  >= 1   REJECTED
   reason: preamble collisions diverge at 2000 UEs
proposer  candidate #2 ... backoff 80 ms, ramp +2 dB  (refined)
certificate (R0) ......... R0 = 0.73  < 1    ADMITTED
simulator (5G-LENA) ...... access p99 142 ms, collisions 3.1%
deploy: centralized, gNB scheduler _

$ tenet synth --spec ts-38.331 --objective continuity --constellation leo
mining blocks ............ A3 event, TTT, hysteresis, RLF timers
dependency graph ......... 2 strong, 3 conditional, 1 weak edge
proposer  candidate #1 ... A3 offset 2 dB, TTT 40 ms
certificate (correctness) ping-pong loop REACHABLE   REJECTED
   reason: A3 offset too low, oscillation under Doppler
proposer  candidate #2 ... A3 offset 4 dB, TTT 160 ms  (refined)
certificate (correctness) no RLF, no ping-pong       ADMITTED
simulator (Hypatia, LEO) . handover failures 0, drops 0
deploy: predictive, UE plus gNB _

# install
pip install tenet-synth
# synthesize a certified Wi-Fi MAC at density 50
tenet synth --spec 802.11ax --objective pf --density 50
# validate the admitted design in a standard simulator
tenet validate --sim ns3 --design out/best.json

Selected publications

The self-driving wireless line below is what teNET grows from; the other groups show the wider program. First author throughout unless noted; some entries are under submission.

Self-driving wireless and protocols

Agentic AI systems

Direct-to-cell LEO satellite

Datacenter and web systems

An open, measurement-heavy framework

The simulator is built on SimPy, process-based discrete-event, with each block a process and the channel a shared resource. It is designed to be opened up: swap blocks, toggle configurations, plug in different objectives and reward functions, and instrument every event. Validation runs against ns-3 for Wi-Fi and Hypatia or StarryNet for LEO. The point is a shared block-level testbed for protocol synthesis, which the field does not have today.

The block model is formal and is the source of truth. The dependency graph and the block state machines are defined explicitly so the certificate can check a composition and the protocol stays readable. A graph neural network, if used at all, only accelerates the search; it never decides correctness.

Two papers, two projects

The work is told in two complementary projects. One names the problem and the abstraction; the other builds and measures it end to end.

Together they are the vision and its first proof point. The roadmap continues with 5G handover, where the correctness certificate against ping-pong and radio link failure is the novel core, then NTN, where both certificate families are stressed under long delay and constant handover, alongside an open framework and benchmark released for the community.

Structural precedent for the writing is TCP ex Machina: Computer-Generated Congestion Control (SIGCOMM 2013). The addition a generative search needs, which a fixed-action search did not, is the certificate.

Contact

If you work on protocol design, formal methods for networks, or agentic systems, and want to contribute a mining workstream, a certificate, or a case study, get in touch. The framework and benchmark will be released openly.

Email h.pasandi@berkeley.edu · code and benchmark on GitHub at release.