Although CheckMate is useful as a fully automatic tool for verifying hybrid systems, in practice it is sometimes difficult to make sure that a CheckMate model can be successfully verified. The reason ranges from highly involved issues such as the computational complexity to extremely trivial use of variable names. For example, if a SCSB block name has space in it, sometimes the explore code failed due to the fact that CheckMate is trying to a variable in the workspace with the same name. Since the developement of CheckMate is essentially inactive, we have described in this page a few useful (and very basic) functionalities of CheckMate, which can help the user to debug or use CheckMate as a toolbox instead of using it as a fully automatic verification tool.
The CheckMate code consists of five parts
where s is called a state formula (which specifies the property of a state) and p is called a path formula (which specifies the property of a path of execution of the finite state mathine. The meaning of the quantifiers stands for:
Finite Transition System
In CheckMate, the finite transition system is modeled in the global variable GLOBAL_TRANSITION. The variable is a cell array, each element correspond to the out-going transition of that state. The element is a vector consisting of the destination states of the out-going transitions. For example, consider the transition system shown in the following figure.
>> global GLOBAL_TRANSITION; >> GLOBAL_TRANSITION = {[2 3], 3, 2};
Region
Next we define a region object in CheckMate. A region object represents a subset of a finite set of states. The following command construct a set of all states of a three-state set.>> a = region(3, 'true');Variable a consists of all three states 1, 2, 3, which is the universe for the 3-state transition system.
>> b = region(3, 'false');Variable b consists of no states, which is the empty set.
>> c = region(3, [1 2]);Variable c consists of states 1,2 out of a three-state set. A region object can be viewed either as a subset or equivalently as a boolean expression. Region object supports basic set operations, such as intersection (and), union (or), and compliment (not).
Model Checking
In CheckMate, it is necessary to first construct the atomic propositions of the formula to verify. Each atomic proposition in the ACTL formula must be put in the global variable GLOBAL_AP. ". Besides the user-defined atomic propositions, it has to contain two trivial atomic propositions, "true" for all states in the system and "false" for an empty set. The following code construct the global atomic proposition for a three-state system, f consists of state 2 and 3, and proposition g consists of state 2 only.>> global GLOBAL_AP >> GLOBAL_AP.true = region(3, 'true'); >> GLOBAL_AP.false = region(3, 'false'); >> GLOBAL_AP.f = region(3, [2 3]); >> GLOBAL_AP.g = region(3, 2);As a preprocess step, it is necessary to construct the reverse transition system. This is used in the model checking algorithm together with the original transition system. In CheckMate, the reverse transition system is stored in the global variable GLOBAL_REV_TRANSITION. The following command construct the reverse transition system.
>> global GLOBAL_REV_TRANSITION >> GLOBAL_REV_TRANSITION = revtran(GLOBAL_TRANSITION);The model checking routine assumes that
>> a = model_check('AX AG f')
The return argument a is a region object consists of the states where the forumula is true. The command model_check first parse the ACTL formula and then evaluate the ACTL formula by traversing the parse tree of the specification and evaluate each node in a bottom-up manner. A detailed reference of the implementation can be found in [2].
[1] M. R. A. Huth and M. D. Ryan, "Logic In Computer Science: Modeling and reasoning about systems", Cambridge University Press, 2001.
[2] E. M. Clarke Jr, O. Grumberg and D. A. Peled, "Model Checking", The MIT Press, 2001.
Polylib: a library for polyhedra computation
CheckMate uses closed convex polyhedra, i.e., polytopes, to represent sets in the continuous states. A polytope can either be represented as the intersection of a number of closed halfspaces or as the convex hull of a finite set of points. Note that an intersection of a finite set of closed halfspaces may not be a polytope, since it may be unbounded. On the other hand, the convex hull of a finite number of points may not be a full-dimensional polytope. For example, the convex hull may be a line segment if all the points happen to be on the line segment. To avoid confusion and facilitate the computation, three classes are implemented in CheckMate:
Conversion
Each object can be converted to other object using the constructor.
Linearcon and polyhedron are both used to represent polytopes. The conversion is just converting from one representation to the other representation of the set. One limitation is that when a linearcon is used to represent open polytope, the result can be unexpected: Either error or wrong result can be found.
Vertices objects are essentially different from linearcon or polyhedron. When constructing a linearcon or polyhedron object from a vertices object, a convex over-approximation of the set of point is computed. Depending on the underlying algorithm, CheckMate may compute either a convex hull or a rectangular hull of the set of point.
The following example illustrates the differences between the convex hull and oriented rectangular hull. Suppose we have three points (0,0), (0,1) and (1,0), the convex hull is the red triangle shown in the following figure and the rectangular hull is the blue box. To generate the plot, use the following command in MATLAB. For an extensive discussion of rectangular hull, see [1]. The convex hull algorithm of CheckMate relies on the qhull built-in functions in MATLAB.
NOTE The global variable GLOBAL_APPROX_PARAM is used in polylib, which should first be set to use the library.
GLOBAL_APPROX_PARAM = parameters(0); global GLOBAL_APPROX_PARAM a = vertices([0 0; 0 1; 1 0]') a1 = polyhedron(a) GLOBAL_APPROX_PARAM.hull_flag = 'convexhull'; a2 = polyhedron(a); plot(a1); plot(a2, 'r');
Computation with linearcon
Although all three classes are implemented for set operations, only linearcon is the workhorse for set computation. For continuous set in n-D space, CheckMate only support sets in n-D or (n-1)-D polytopes. Polytopes with dimension less than n-1 is either considered as empty or over-approximated by an n-d polytope. Polyhedron and vertices are normally first converted to linearcon objects and then converted back after the set computations. The most commonly used computations on sets are
[1] B. H. Krogh and O. Stursberg, On efficient representation and computation of reachable sets for hybrid systems, in Hybrid Systems: Computation and Control (HSCC'03), Lecture Notes in Computer Science (LNCS), Springer.
[2] Qhull website: http://www.qhull.org
[3] CDD website: http://www.ifor.math.ethz.ch/~fukuda/cdd_home/cdd.html
Reachability analysis of CheckMate
The reachability analysis of CheckMate involves the computation of continuous successor of a given location of a PIHA. Given a polyhedral invariant (note it can be unbounded), the continuous dynamics given in the format of Matlab ODE suite, and an initial set given as a bounded, full-dimensional polytope. CheckMate computes what can be informally called consinuous successor, i.e., the intersection of the flow-pipe (from 0 to a given t_max) with the facets of the invariant.
Limitation of CheckMate
Note that in the above description, the continuous successor is merely an over-approximation of the continuous part of actual reach set. Consider the situation illustrated in the following figure, the continuous successor computed from CheckMate is illustrated as the bold line segment. The invariant I is the shaded area in the figure. Consider one of the trajectory in the flow, the state first reaches the boundary of the invariant, where the hybrid system leaves the location. The trajectory after that does not exist because the dynamics depends on the new location. Therefore the parts illustrated by the red curve does not belong to the reach set. One may argue that this can be done by intersecting the reach set in each small time step, or even taking the vector field into consideration. In CheckMate, this intersection is not implemented to avoid the complexity of set computation (intersection of polytopes). The actual reach set should only contain the lower half of the line segment (below the dashed trajectory). But CheckMate computes the whole line segment as an over-approximation.
The reachability analysis algorithms have the form
xxx_map( sys, X0, I, T, T_max )
where sys gives the system dynamics, X0 is the initial state polytope, I is the polyhedral invariant set, T is the step size and T_max is the maximum analysis time. Depending on the dynamics of the location, CheckMate implments three different procedures to compute the continuous successors
The main difference between these algorithms are the input parameters for the functions and the underlying algorithms. The input/output format for these functions are quite similar. The global variable GLOBAL_APPROX_PARAM has to be set to use these functions.
Affine dynamics
In affine dynamics, the system ODE is given as
f(x) = A* x + b
. The procedure fs_lin_map takes A and b as input arguments. A sample code to use fs_lin_map is shown as the following
%DEMO2 A 2-D reach set demo script global GLOBAL_APPROX_PARAM GLOBAL_APPROX_PARAM = parameters(1); GLOBAL_APPROX_PARAM.T = 1e-2; % time step % Construct the invariant for x_1 < 1 INV = linearcon([],[],[1 0],[1]); A = [-1 1; 0 -1]; b = [1 2]'; X0 = linearcon([],[],[eye(2); -eye(2)],1e-2*[1;1;1;1]); % Compute continuous successor for the system [MAPPING,null_event,time_limit] = fs_lin_map(A,b,X0,INV)
Nonlinear dynamics
In nonlinear dynamics, the system ODE is given as general nonlinear function f(x). The procedure fs_nonlin_map takes the function handle to f(x) as one of the input arguments. Where function f(x) must be implemented in the format of MATLAB ODE suite. A sample code to use fs_nonlin_map is shown as the following
%DEMO2 A 2-D reach set demo script global GLOBAL_APPROX_PARAM GLOBAL_APPROX_PARAM = parameters(1); GLOBAL_APPROX_PARAM.T = 1e-2; % time step % Construct the invariant for x_1 < 1 INV = linearcon([],[],[1 0],[1]); X0 = linearcon([],[],[eye(2); -eye(2)],1e-1*[1;1;1;1]); % Compute continuous successor for the system mapping = fs_nonlin_map(@dblclk,[],X0,INV,linearcon,0.1,2)
Clock dynamics
In clock dynamics, the system ODE is given as constant rates. The procedure clk_map takes the rates of the state variables as one of the input arguments. CheckMate assumes t_max is infinity for clock dynamics. And no step size is used. A sample code to use clk_map is shown as the following
%DEMO2 A 2-D reach set demo script global GLOBAL_APPROX_PARAM GLOBAL_APPROX_PARAM = parameters(1); GLOBAL_APPROX_PARAM.T = 1e-2; % time step % Construct the invariant for x_1 < 1 INV = linearcon([],[],[1 0],[1]); X0 = linearcon([],[],[eye(2); -eye(2)],1e-1*[1;1;1;1]); v = [1;2]; % Compute continuous successor for the system mapping = clk_map(X0,v,INV);