Ktz profiles in TINA 3.8.0

Motivations

Several classes of properties over state spaces of nets can be distinguished:

- State properties, about net markings;

- Transition (or Event) properties, about net transitions or steps;

- Properties mixing the previous two classes;

- Modal properties, involving in addition temporal logic or mu-calculus modalities;

- Reachability properties, a restricted class expressing invariance properties or their negation.

The properties in some of these classes could be checked on the fly while traversing the state space, without need to store it in a file. But storing it may still have some interest, especially if there are many properties to check, and for a deep analysis of counter examples. We assume in the sequel that the state space is stored in ktz format by tool sift (faster and using less space than tool tina).

Now, the ktz files produced by tools tina and sift record as much informations as available, regardless of any properties it will be used to check, hence it can be unnecessarilly rich and bulky. If, for instance, the sole properties of interest of a model are reachability properties on markings, then it is not necessary at all to store informations on transitions in the ktz file. Not storing them can reduce considerably the size of the file, and speed up its processing and the verification process. Ktz profiles are meant to address these particular issues.

Profiles

Ktz profiles make precise what informations are to be recorded in the ktz file. Ktz files are produced by the tina, sift and ktzio tools; the later two support profiles.

Six potentially useful profiles have been identified.

The first three record the reachability relation between markings and are suitable for checking modal formulas with tools muse (supporting a rich modal mu-calculus with state and transition properties) and selt (supporting State/Event LTL, a variamt of linear time temporal logic with both state and transition properties). They are:

- "kts" (for Kripke Transition System): It is the default profile, and that recording the maximum informations.

- "lts" (for Labelled Transition System): In this profile, state properties are forgotten, as in the formats supported by many tool for model checking process calculi (e.g. CADP ou the Concurrency Workbench).

- "ks" (for Kripke Structure): It is in some sense the dual of profile lts: it provides state properties but transition properties are forgotten. State transitions are recorded, but they all are silent (anonymous).

The last three record state properties but not the state reachability relation. They are suitable for model checking reachability properties via e.g. tool scan.

- "rsf" (Reachability Set + Firable transitions): For each reachable state, this profile stores its state properties and the net transitions it enables. In the ktz file, transitions and their properties are still present, but the targets of transitions are replaced by the current state. This allows to check absence of deadlocks, quasi liveness of transitions or firability of transitions under some state properties.

- "rsd" (Reachability Set + Deadlock): Like profile rsf except that state properties are forgotten. No more allows to check firability of transitions, but still allowing to check state properties and deadlocks.

- "rs" (Reachability Set): Only stores state properties; state transitions are totally omitted. This profile yields the smallest ktz files, but they are only marginally smaller than those produced by profile rsd.

Support by tools

Ktz files are produced by tools tina, sift and ktzio and consumed by tools ktzio, selt, muse and scan.

Tool tina always produces ktz files with the default kts profile, but it can produce ktz descriptions for unbounded or labelled nets that tool sift cannot.

Tool sift can produce ktz files in any profile: if some profile is made precise when genersating ktz output, by one of the options with the names of the above described profiles, then it produces a ktz file according to that profile.

Tool ktzio can transform various state space representations to/from ktz files, possibly with a profile specification when the input is a ktz file. Independantly of profiles, tool ktzio has a number of output options. Whenever there is a sequence of output options equivalent to a profile option, the profile option should be prefered as the profile option will be recorded into the ktz file, what may be a useful for the tools processing ktz files (selt, muse, scan) to check if the necessary features are provided by the ktz file (in particular the presence of the state reachability relation for selt and muse).

In terms of ktz file sizes, the benefits of profiles widely depends on the structure of the state space (number of state properties, transition properties and transitions). We observed on typical use cases ktz size ratios of profile kts over rs varying from 1.1 to 7 (if there are many transitions and transition properties), and of kts over lts between 1.25 and more than 100 (if there are few transitions and transition properties). Our benchmark incude some very large ktz files (up to 30Gb), some capturing very large state spaces (up to 750M states and 5G transaitions).