minim

Minimization of Timed Automata
with respect to
Time-Abstracting Bisimulation


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:

minim also generates refinement statistics in stdout.
 

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:

NOTICE:
When using options -i, -P,  or -p you create some dummy states and transitions. Do not forget to update the corresponding fields #states and #trans at the head of the .tg file.
 

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:


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