Title: Liveness Verification and Synthesis: New Algorithms for Recursive Programs,
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.