Speaker:

Toru Takisaka (University of Electronic Science and Technology of China)

Time:

• 16:20-17:20 (Time in Beijing)
• May 10, 2024 (Friday)

Venue:

518, Research Building 4

Abstract:

Lexicographic Ranking SuperMartingale (LexRSM) is a probabilistic extension of Lexicographic Ranking Function (LexRF), which is a widely accepted technique for verifying program termination. In this paper, we are the first to propose sound probabilistic extensions of LexRF with a weaker non-negativity condition, which is called single-component non-negativity. It is known that such an extension, if it exists, will be nontrivial due to the intricacies of the probabilistic circumstances.
As the basis of technical development, we first devise a novel notion of rescalability, which ensures that a LexRSM does not take negative values in a “harmful” way. This notion yields a sound probabilistic extension of single-component non-negative LexRF for general stochastic processes. Toward the application to automated verification, we then introduce another extension, called lazy LexRSM. Linear lazy LexRSM is sound for probabilistic programs with linear arithmetics, and its subclass is amenable to automated synthesis algorithms via linear programming. Experiments show an advantage of the algorithm over existing LexRSM synthesis algorithms.

This is a joint work with Libo Zhang, Changjiang Wang, and Jiamou Liu.