Second-Order Occupation Measures for Synthesizing Probabilistic Loop Transformers

Presenter: Bohan Ma

Author: Darion Haase et al.; Mingshuai Chen et al.

Abstract: We try to turn the higher-order fixed-point problem of synthesizing a probabilistic loop transformer into a first-order symbolic fixed-point problem over second-order generating functions.

URL:

• https://arxiv.org/abs/2601.13991
• https://arxiv.org/abs/2205.01449