Methods and systems for efficient analysis of hybrid systems using template polyhedra
View Patent ↗In accordance with aspects of the present principles, an over-approximation of reachable states of a hybrid system may be determined by utilizing template polyhedra. Policy iteration may be utilized to obtain an over-approximation of reachable states in the form of a relaxed invariant based upon template polyhedra expressions. The relaxed invariant may be used to construct a flowpipe to refine the over-approximation and thereby determine the reachable states of the hybrid system.
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
〉
.
2. The system of claim 1 , wherein the policy iteration unit is further configured to reinitialize policy iteration to obtain an improved approximation of reachable states by using a bound of the flowpipe and determining an improved relaxed invariant.
3. The system of claim 2 , wherein the flowpipe module is further configured to construct an inner flowpipe based on the improved relaxed invariant obtained from the reinitialized policy iteration to refine the improved approximation of reachable states.
4. The system of claim 1 , wherein the flowpipe module is further configured to advance an approximation for a time interval by applying a series expansion over template expressions to generate a flowpipe segment.
5. The system of claim 4 , wherein the flowpipe module is further configured to truncate the series expansion and is further configured to employ the relaxed invariant to bound a remainder term of the series expansion.
6. The system of claim 1 , further comprising:
a verification unit configured to verify whether the hybrid system meets safety specifications by comparing reachable states in the flowpipe to the safety specifications.
7. The system of claim 1 , further comprising:
a verification unit configured to employ the determined reachable states to compute likely paths leading to property violations of the hybrid system.
8. The system of claim 1 , further comprising:
a verification unit configured to employ the determined reachable states to instantiate parameters in the system description and thereby guarantee safe operation.
9. The system of claim 1 , further comprising:
a verification unit configured to employ the determined reachable states to generate finite state models of the hybrid system.
10. The system claim 1 , wherein each optimization is a linear programming problem used to construct the polynomial
p
(
Δ
)
=
∑
j
=
0
m
a
j
Δ
j
+
a
m
+
1
Δ
m
+
1
for a time step Δ≧0 chosen by the user such that for a given template H, c 0 the polyhedron formed by H i x≦ρ(Δ) is a bound function H i x+c 0 ,i at time t=Δ and furthermore the polyhedron formed by H i x≦max t∈[0,Δ] ρ(t) is a bound for the function H i x+c 0 ,i over the time interval t∈[0,Δ].