Patent Document ID: 8352222
Application ID: 12236071
Patent Flag: 1

Claim One:
1. A system for automatically determining reachable states of a hybrid system utilizing template polyhedra, constructed in part using linear template expressions, comprising: a processor to execute an expression generation module configured to generate a set of template polyhedra expressions from a system description; a policy iteration unit configured to employ policy iteration to produce an over-approximation of states reachable by the hybrid system from the expressions in the form of a relaxed invariant; wherein the hybrid system includes discrete and continuous systems that handle ordinary differential equations; obtaining over-approximation of reachable states over infinite time horizons and using the over-approximations of reachable states over infinite time horizons to prune the over-approximations of reachable states over finite time horizons; applying a linear programming solver at each step to derive the template polyhedral of over-approximations for finite as well as infinite horizons; and a flowpipe module configured to construct a flowpipe of template polyhedra based on the relaxed invariant obtained from policy iteration to refine the over-approximation of reachable states and thereby determine the reachable states of the hybrid system; wherein for each template (H i , c 0 ,i) of a given template (H, c), the flowpipe approximate seeks to bound the function H i x+c 0 ,i locally as an univariate polynomial of a chosen degree m, where the coefficients of the polynomial a j 0≦j≦m are a result of solving an optimization problem a j = max ⁢ H i ( j ) ⁡ ( x ) j ! ⁢ subj. ⁢ to. ⁢ x ∈ 〈 H , c 0 〉 .