# Liveness Verification and Synthesis: New Algorithms for Recursive Programs

## TL;DR

This paper introduces new algorithms with optimal complexity for verifying and synthesizing liveness properties in recursive programs, extending existing finite-state methods to infinite and recursive settings.

## Contribution

It generalizes recent algorithms for finite programs to recursive and infinite contexts, achieving optimal time complexity for liveness verification and synthesis.

## Key findings

- Algorithms with optimal exponential time complexity
- Generalization of lasso-finding algorithms to recursive programs
- Extension of summary-based algorithms to infinite words

## Abstract

We consider the problems of liveness verification and liveness synthesis for recursive programs. The liveness verification problem (LVP) is to decide whether a given omega-context-free language is contained in a given omega-regular language. The liveness synthesis problem (LSP) is to compute a strategy so that a given omega-context-free game, when played along the strategy, is guaranteed to derive a word in a given omega-regular language. The problems are known to be EXPTIME-complete and EXPTIME-complete, respectively. Our contributions are new algorithms with optimal time complexity. For LVP, we generalize recent lasso-finding algorithms (also known as Ramsey-based algorithms) from finite to recursive programs. For LSP, we generalize a recent summary-based algorithm from finite to infinite words. Lasso finding and summaries have proven to be efficient in a number of implementations for the finite state and finite word setting.