Runtime Complexity Analysis of Logically Constrained Rewriting

TL;DR

This paper presents a new method for analyzing the worst-case runtime complexity of logically constrained rewrite systems, combining existing techniques and novel modularization, with implementation in TCT for validation.

Contribution

It adapts and combines decomposition and bound approximation techniques for LCTRSs, introducing modularization for sublinear bounds, and implements the approach in TCT.

Findings

Effective analysis of LCTRS runtime complexity

Integration of decomposition and recurrence-based bounds

Successful implementation in TCT tool

Abstract

Logically constrained rewrite systems (LCTRSs) are a versatile and efficient rewriting formalism that can be used to model programs from various programming paradigms, as well as simplification systems in compilers and SMT solvers. In this paper, we investigate techniques to analyse the worst-case runtime complexity of LCTRSs. For that, we exploit synergies between previously developed decomposition techniques for standard term rewriting by Avanzini et al. in conjunction with alternating time and size bound approximations for integer programs by Brockschmidt et al. and adapt these techniques suitably to LCTRSs. Furthermore, we provide novel modularization techniques to exploit loop bounds from recurrence equations which yield sublinear bounds. We have implemented the method in TCT to test the viability of our method.