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 reasons range from highly involved issues such as the computational complexity to extremely trivial uses of variable names. For example, if a SCSB block name has space in it, sometimes the explore code fails due to the fact that CheckMate is trying to use a variable in the workspace with the same name. This violates the MATLAB rule for naming variables in the workspacem, which results in a MATLAB error. Since the developement of CheckMate is essentially inactive, we describe 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. In other words, to use CheckMate without building a CheckMate GUI model in Simulink.
The CheckMate code consists of five parts
Global variables are used widely in the code of CheckMate. This is mostly due to the fact that CheckMate was implemented initialliy in MATLAB 5.3, where handle class is still not available. CheckMate uses global variables for two purposes: first, as a global switch for algorithm settings, e.g., to switch between convex hull approximation and oriented rectangular hull approximation; second, to save memory consumption without using references.
The global variables in CheckMate was added as the functionalities grows, and sometimes the parameter settings are confusing. However, for most of the core functionalities the code base is relatively stable and only a few global variables are needed. The following table lists the global variable needed by the libraries described in this document.
Library | Global variable(s) |
ACTL | GLOBAL_TRANSITION, GLOBAL_AP, GLOBAL_REV_TRANSITION |
Polylib | GLOBAL_APPROX_PARAM |
Reachability | GLOBAL_APPROX_PARAM |
The way to set these variables are described in more detail in the later sections.
Computational-Tree Logic (CTL) is a temporal logic for formally specifying and verifying dynamic properties of finite state machines. A CTL formula has the following formwhere 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 quantifiers are defined as follows:
Finite Transition System
In CheckMate, the finite transition system is modeled in the global variable GLOBAL_TRANSITION. The variable is a cell array in which each element corresponds to an out-going transition of a state. The cell 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. For any property of the system, it is represented in CheckMate as the set of states that satisfy the property. The following command constructs 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 property. The region object supports basic set operations, such as intersection (and), union (or), and compliment (not). Regions for atomic properties must be constructed first. And then each ACTL formula is evaluated using the known APs by traversing the parse tree of the formula.
Model Checking
In CheckMate, it is necessary to first construct the atomic propositions of the formula of interests. 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 constructs the global atomic proposition for a three-state system: proposition f is true in states 2 and 3, and proposition g is true in 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. Because the model-checking algorithm needs to visit the finite transition system both in forward direction and in backward direction. This reverse transition system is used in the model checking algorithm together with the original transition system. In CheckMate, the reverse transition system must be stored in the global variable GLOBAL_REV_TRANSITION. The following command constructs the reverse transition system for a given 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 containing the states where the forumula is true. The command model_check first parses the ACTL formula and then evaluates the ACTL formula by traversing the parse tree of the specification, evaluating each node in a bottom-up manner. A detailed reference for 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 to represent sets of continuous states. CheckMate uses bounded closed convex polyhedra, i.e., polytopes, to represent the reachable set in the continuous state space. Conceptually a polytope can be represented either 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 the set 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.
Conversion
Each object for representing polytopes can be converted to another object using the constructor function.
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 polyhedra, the result can be unexpected: Either an error or wrong result can be found. Because of the assumptions of CheckMate.
Vertices objects are different from linearcon or polyhedron, because it is actually a finite set of points. When constructing a linearcon or polyhedron object from a vertices object, a convex over-approximation of the set of points is computed. Depending on the underlying algorithm specified by the flag "hull_flag" of the gobal variable GLOBAL_APPROX_PARAM, 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 MATLAB commands. (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');
Converting a set to a vertices object will result in the set of vertices of the polytope. This is done by enumerating all the extremal points (vertices) of the polytope. CheckMate uses an implementation of CDD ([3]) to enumerate all the vertices. The interior points of the polytope are not stored in the polytope. Hence conversion from vertices to polytheron and then back to vertices will result in a different set of points than the original set. This operation is used extensively in CheckMate to reduce the complexity resulting from the growing number of vertices in the computation.
>> GLOBAL_APPROX_PARAM.hull_flag = 'convexhull'; >> a = vertices([0 0; 0 1; 1 0; 0.5 0.5]') a: v1 = [0.000000 0.000000 ]^T v2 = [0.000000 1.000000 ]^T v3 = [1.000000 0.000000 ]^T v4 = [0.500000 0.500000 ]^T >> b = vertices(polyhedron(a)) b: v1 = [0.000000 0.000000 ]^T v2 = [0.000000 1.000000 ]^T v3 = [1.000000 0.000000 ]^T
Computation with linearcon objects
Although all three classes are implemented for set operations, linearcon is the workhorse for set computation. For continuous sets in n-D space, CheckMate supports only sets in n-D or (n-1)-D polytopes. And the linear constraint must be given explicitly in the constructor. Implicit linear constraints are silently "bloated", i.e., relaxed for a small amount, so that the resulting polytope is full-dimensional. 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 operationss on linearcon objects 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 in CheckMate involves the computation of continuous successors of a given location of a polyhedral invariant hybrid automaton (PIHA). Given a polyhedral invariant (which can be unbounded), the continuous dynamics given in the form to use with the MATLAB ODE suite, and an initial set given as a 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.
A 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 invariant I is the shaded area in the figure. And X0 is the set of initial states. The continuous successor computed from CheckMate is illustrated as the bold line segment. Normally the reach set is the set of states can be reached without leaving the invariant. Consider one of the trajectories in the flow: the state first reaches the boundary of the invariant, where the hybrid automaton leaves the location. The trajectory after that (the red curve) does not exist because the continuous dynamics is governed by the new location. Therefore the parts illustrated by the red curve do not belong to the actual reach set. One may argue that this can be done by intersecting the reach set with the invariant and excluding the sets that has left the location, or taking the vector field into the computation. In CheckMate, these computations are not implemented to avoid the complexity of set computation (intersection of polytopes). In this example, 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 to use with the MATLAB ODE suite. An example of such file:
Content of the nonlinear dynamics m-file:
% dblclk.m function dydt = dblclk(t,y, varargin) dydt = [1;2];
Sample code to use fs_nonlin_map:
%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 time derivative of each state is given as constants, hence the name clock. 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. Sample code to use clk_map:
%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]; %ratio of the clocks % Compute continuous successor for the system mapping = clk_map(X0,v,INV);