UPDATE:

From this page, you can get information on the tool minim and download the tool as a stand-alone executable.

minim is also available as part of the latest release of Kronos (command-line option -ta).

DESCRIPTION:

minim generates the quotient graph (or minimal model) of a timed automaton (TA), with respect to the (strong) time-abstracting bisimulation. This bisimulation ignores exact time delays, that is, two states are equivalent iff they can perform the same discrete and time transitions (in time transitions the exact time delay is irrelevant), leading to equivalent states.

minim starts by building an initial partition of each control state of the TA into a number of time zones, simple convex polyhedra recording the possible values of clocks. It then keeps refining these zones until they become stable, that is, until all states belonging to the same zone are time-abstracting equivalent. The vertices of the minimal graph are zones, and its transitions are either discrete (labeled as in the TA) or time (labeled by a symbolic label t).

minim takes as input a TA in KRONOS format (file .kro), and generates output in various formats, among which:

• an analytical report (options -F, -O) where vertices are completely displayed as zones. Transitions are also displayed in detail;
• a Caesar/Aldebaran-compatible format (options -l, -L) where vertices are simply numerotated, and transitions are labeled pairs of vertices. Time transitions are labeled i (Aldebaran's silent action);
• a TA format (option -k or -K) where guards are all true.

DISTRIBUTION:

minim is publicly available for non-military purposes. The disctribution contains an executable for Sun5 or Linux machines, man pages, and some examples. Notice that the input has to be pre-processed by KRONOS first, so you might want to get also KRONOS.
 

OPTIONS:

-X: Perform refining upon all zones, whether or not accessible. By default, minim refines only accessible zones, i.e., zones with at least one reachable state.

-I: Consider, for each control state, an initial partition included in its invariant. By default, minim starts with an initial partition containing also the zones violating the invariant. The latter are "pseudo" zones serving merely for the refinement of "real" zones. (Under this option, zone complementation is generally necessary. However, performance does not seem to be affected. In fact, this option sometimes performs better than the default.) (Not to be confused with option -i.)

-A: Refine a zone with respect to all outgoing unstable discrete transitions. By default, the zone is refined with respect to only one such transition (the first that yields a successful refinement) and the algorithm goes on to find another zone to refine.

-T: Give priority to refinement with respect to time transitions. By default, minim refines with respect to discrete transitions first.

-i: Use the last control location of the TA as a dummy location, in order to specify an initial zone: the initial zone is taken to be the constraint of the first transition of the location. By default, the initial zone is the one with all clocks equal to zero. (Not to be confused with option -I.)

-p: Use the last (or one before last, if -i is present) control location of the TA as a dummy location, in order to:

Refine the zones of the initial partition with respect to a set of constraints (the constraints of the transitions of the location).

and/or

Specify a set of atomic propositions of the control locations of the TA, which are to appear as labels of self loops of the minimal graph. This set is the set of atomic propositions of the location.

-P: As -p, where in the case of (a), a self-loop is added in each vertex of the minimal graph, for each constraint that it satisfies. This loop is labeled as the corresponding transition of the TA.

-O: Dump analytical output to stdout.

-F: Dump analytical output in file .min

-l: Dump output in Caesar/Aldebaran format in file .aut

-L: As before, but also add a self loop to vertex i of the minimal graph, labeled state_i. (This is useful to characterize vertex i, as the unique vertex where the mu-calculus formula <"state_i">TRUE holds.)

-k: Dump output in standard KRONOS TA format in file .Mtg (Time transitions appear labeled as "EPSILON".)

-K: Dump output in new KRONOS TA format in file .Mtg (Time transitions appear in a special field called time-succ.)

-r: (Valid with option -k or -K). Print reset clocks (by default not printed).

-D: Set debugging on.
 

AUTHORS:
Stavros Tripakis has implemented the minimization algorithm. Thanks to Conrado Daws and Sergio Yovine for providing the KRONOS library of zone structures and operations. Authors' address:

VERIMAG
Centre Equation,
2, avenue de Vignate
38610 Gieres, FRANCE
tel: +(33) 4 76 63 48 48
fax: +(33) 4 76 63 48 50
e-mail: Stavros.Tripakis@imag.fr
 

FILES:

• file.min: Analytical output.
• file.aut: Output in Caesar/Aldebaran format.
• file.min.tg: Output in KRONOS TA format.
• file.[tg,kro,reg,lab,prop]: Input TA files (generated by KRONOS).

SEE ALSO:
S. Tripakis and S. Yovine. Analysis of timed systems based on time-abstracting bisimulations. In Proc. 8th Conf. on Computer-Aided Verification, CAV'96. Pg.232-243, Lecture Notes in Computer Science 1102.
 
S. Tripakis and S. Yovine. Analysis of Timed Systems using Time-abstracting Bisimulations. Formal Methods in System Design, 18(1):25--68, January 2001. Kluwer Academic Publishers.
 

BUGS:
Hope there aren't any. However, option -A hasn't been used for quite some time, so it isn't polished. Moreover, the way input is passed for options -iPp is really a hack, and should be improved. For any kind of strange behavior, please report it to Stavros.Tripakis@imag.fr.

Back to home page of Stavros Tripakis