A Brief Experimental Comparison of the STC and LGG Analysis Algorithms in SpaceEx

The STC algorithm is a recent enhancement of the LGG algorithm that produces fewer convex sets for a given accuracy and computes more precise images of discrete transitions. Based on the LGG scenario, the reachable states over time (so-called flowpipes) are bounded with piecewise linear approximations of the support function over time. The approximation can be made arbitrarily precise using just two parameters: the number of template directions and an error bound that is evaluated in each of those directions. The image of discrete transitions is computed on polyhedral overapproximations that are projections from space-time onto the state space. The complexity (number of constraints) and number of polyhedra is adjusted automatically so the given error bound is met. This makes the clustering heuristics (commonly used with the LGG scenario) unnecessary in most cases and gives more predictable results than the hit-or-miss success rate of previous heuristics. This document presents some experiments that compare the performance of STC and LGG algorithms from a purely practical perspective.