Langley Formal Methods Program • César Muñoz • Grizzly

Grizzly

Grizzly is a prototype client-server interface to PVS that solves global optimization problems such as finding min/max values of polynomials, formally verifying polynomial inequalities, solving satisfiability of polynomial inequalities, and computing under/over-approximations of regions defined by conjunction/disjunction/implication of polynomial inequalities.

It is important to remark that Grizzly should not be compared against numerical tools for solving global optimization problems. The server side of Grizzly is running an algorithm through the PVS ground evaluator. That algorithm is written in PVS, uses PVS built-in infinite precision rational arithmetic, and has been verified to be correct in PVS.

Grizzly is pre-installed in the Bernstein library, which is part of the NASA PVS Library. The tool consists of two programs, which have to run in parallel: the server Bernstein/grizzly-server.sh, and the client Bernstein/Grizzly/grizzly.pl.

Server

The Grizzly server is implemented in the Prototype Verification System (PVS). To run the sever, go the directory Bernstein directory of the NASA PVS Libraries and execute:

./grizzly-server.sh

This command will run PVS in server mode. It will take a few seconds to start and in the mean time it displays a lot of information. You can ignore all of that. You know that the server is running because it prints the message:

Grizzly ID: 8267560. Log: grizzly-8267560.log. Type: insecure.

Grizzly is hibernating...

The command grizzly-server.sh accepts the following options:

Usage: grizzly-server [-port port] [-maxclients n] [-secure]

By default, the server starts at port 2327 (BEAR in a telephone keypad). The server option -maxclients sets the maximum number of clients attended by the server. By default, the server attends up to 5 clients. The server starts in mode "insecure", which means that special commands to the server such as die, close, etc, can be sent from any client. To start the server in "secure" mode, use the option -secure. A secure server attends these special commands only when the client also sent the server ID. Beware, -secure provides a very simple security mechanism, it doesn't guarantee that the server is secure from external attacks.

Client

The Grizzly client is written in PERL and it is called grizzly.pl. This script found in the directory Bernstein/Grizzly of the NASA PVS Libraries. No installation is required to run the script, other than a PERL interpreter in the client machine.

Assuming that a Grizzly server is running in the machine server and that the client has network access to the server, the client can be executed on a given file as follows:

./grizzly.pl -server server file

If the server is listening into a user-specified port, the client has to specify the same port using the form server:port. Note that the option -server is not required when the client and the server are running in the same computer. Furthermore, if a file is not specified, the client runs an interactive read-and-eval loop. To see available command line options to grizzly.pl, try:

./grizzly.pl -help

To see all the commands available inside the interactive environment, try:

grizzly> help;

Examples

Mini-tutorial

Assuming that the NASA PVS libraries is installed in the directory nasalib:

Execute the Grizzly server from directory nasalib/Bernstein:
```
  $ cd nasalib/Bernstein
  $ ./grizzly-server
```
Run Grizzly client interactively from any directory (assuming that nasalib/Bernstein/Grizzly is in the PATH).
```
  $ grizzly.pl
```

Declare variables x and y in the intervals [-5,5] and [0,1], respectively.

grizzly> var x in [-5,5];
Variable x in [-5,5]. 

grizzly> var y in [0,1];
Variable y in [0,1].

Define a polynomial P.

grizzly> poly P = 4*x^2 - (21/10)*x^4 + (1/3)*x^6 + x*y - 4*y^2 + 4*y^4;
Polynomial P = 4*x^2 - (21/10)*x^4 + (1/3)*x^6 + x*y - 4*y^2 + 4*y^4.

Check whether or not P >= -1.5 for all values in the variable ranges.

grizzly> check all P >= -1.5;
Let
  P(x,y) = 4*x^2 - (21/10)*x^4 + (1/3)*x^6 + x*y - 4*y^2 + 4*y^4. 
The polynomial inequality 
  P(x,y) >= -1.5,
holds for all 
  x in [-5,5],
  y in [0,1].

Check whether or not P <= -1 for some values in the variable ranges.

grizzly> check some P <= -1;
Let 
  P(x,y) = 4*x^2 - (21/10)*x^4 + (1/3)*x^6 + x*y - 4*y^2 + 4*y^4. 
The polynomial inequality 
  P(x,y) <= -1,
holds for some 
  x in [-5,5],
  y in [0,1],
e.g., P(x,y) <= -1, when x = -5/32, y = 3/4.

Set the precision and compute the minimum and maximum of P, within that precision.

grizzly> set precision = 0.0001;
Precision is set to 0.0001. 

grizzly> minmax P;
Let 
  x in [-5,5],
  y in [0,1],
  P(x,y) = 4*x^2 - (21/10)*x^4 + (1/3)*x^6 + x*y - 4*y^2 + 4*y^4. 
Then 
  min{P(x,y)} in [-1.03166930078632,-1.03159281870053],
  P(x,y) = -1.03159281870053, when x = -45/512, y = 91/128,
  max{P(x,y)} = 4000.83333333333,
  P(x,y) = 4000.83333333333, when x = 5, y = 1. 
--
Min/max values may be inaccurate due to decimal format. Set format to 
rational for precise values. 
--
Depth: 18. 
Number of splits: 35.

Define polynomial Q = P^2 - y^2 and a region R, where P>=0 and Q<= 1.

grizzly> poly Q = P^2 - y^2;
Polynomial Q = P^2 - y^2. 

grizzly> region R = P >= 0 and Q <= 1;
Region R = P >= 0 and Q <= 1.

Set the precision to 0.1 and pave region R with boxes that are inside and outside the region R. The minimum size of the boxes is one tenth of the original variable ranges.

grizzly> set precision = 0.1;
Precision is set to 0.1. 

grizzly> boxes R;
Let 
  x in [-5,5],
  y in [0,1],
  P(x,y) = 4*x^2 - (21/10)*x^4 + (1/3)*x^6 + x*y - 4*y^2 + 4*y^4,
  Q(x,y) = P^2 - y^2. 
Boxes for P >= 0 and Q <= 1:
  Inside : 14. Relative volume: 0.037109375. 
  Outside: 55. Relative volume: 0.7890625. 
  Unknown: 61. Relative volume: 0.173828125. 
--
Relative volumes may be inaccurate due to decimal format. Set format to 
rational for precise values. 
--
Boxes are found in R.m (MATLAB format).

The tag

identifies links that are outside the NASA domain

+ Contact NASA

Grizzly

Server

Client

Examples

Mini-tutorial