Flowchart Programs, Regular Expressions, and Decidability of Polynomial Growth-Rate

TL;DR

This paper introduces a new method for analyzing flowchart programs to decide if their computed values and runtime are polynomially bounded, extending previous results to more general, Turing-incomplete flowcharts with arbitrary control flow.

Contribution

We propose a class of loop-annotated flowcharts and a novel polynomial-time analysis technique inspired by automata-to-regular expression translation, enabling decidability of polynomial growth for this class.

Findings

Decidable polynomial bounds for flowchart programs with arbitrary control flow.

A polynomial-time analysis technique inspired by automata and regular expressions.

Extension of decidability results to more general flowchart classes.

Abstract

We present a new method for inferring complexity properties for a class of programs in the form of flowcharts annotated with loop information. Specifically, our method can (soundly and completely) decide if computed values are polynomially bounded as a function of the input; and similarly for the running time. Such complexity properties are undecidable for a Turing-complete programming language, and a common work-around in program analysis is to settle for sound but incomplete solutions. In contrast, we consider a class of programs that is Turing-incomplete, but strong enough to include several challenges for this kind of analysis. For a related language that has well-structured syntax, similar to Meyer and Ritchie's LOOP programs, the problem has been previously proved to be decidable. The analysis relied on the compositionality of programs, hence the challenge in obtaining similar results for flowchart programs with arbitrary control-flow graphs. Our answer to the challenge is twofold: first, we propose a class of loop-annotated flowcharts, which is more general than the class of flowcharts that directly represent structured programs; secondly, we present a technique to reuse the ideas from the work on tructured programs and apply them to such flowcharts. The technique is inspired by the classic translation of non-deterministic automata to regular expressions, but we obviate the exponential cost of constructing such an expression, obtaining a polynomial-time analysis. These ideas may well be applicable to other analysis problems.