Template-based Analyses and Min-policy Iteration
This chapter considers other configurations aside from the direct synthesis of invariants as bound templates. A first case arises when the methods shown in the previous chapter only synthesizes the template but not the bound. A second appears when one wants to analyze a system with multiple templates. This chapter looks at bounds on each variable and considers the templates 𝑝(𝑥) = 𝑥²𝑖 for each variable 𝑥𝑖 in state characterization 𝑥 ∈ Σ. The chapter thus proposes a policy iteration algorithm, based on sum-of-squares (SOS) optimization, to refine such template bounds. In practice, the chapter uses it by combining a Lyapunov-based template obtained using one of the previous methods with additional templates encoding bounds on some variables or property specific templates.