The amc package

Model Check using over(under)-approximation of the transition relation.

By Woohyuk Lee

The package implements the approximate_model_check command. The command is designed as a wrapper around the model_check command. The command contains dual algorithms. Predefined abstraction of the transition relation is performed in a controlled way to ensure that the result is reliable. By default, the command makes its effort to prove whether the given ACTL formula is positive. User must set an environment variable "amc_prove_false" when he/she wishes to prove whether the given ACTL formula is negative. When the formula is proven FALSE, then the error trace is returned as in the model_check command. Currently, one predefined approximation method, namely a "block-tearing" method, is implemented. The package manipulate the internal data structure of FSM to obtain over(under)-approximation of a given system. The algorithm begin with coarse approximation in which the degree of initial approximation is set by the user. Initial degree of approximation can be set by using "amc_sizeof_group" environment. When the initial attempt using the coarse approximation fails, the algorithm automatically combine subsystems(take synchronous product) to obtain refined approximations. The procedure is repeated until the approximation is good enough so that the result is reliable.

Last updated on 20050519 00h50