The extraction function extracts a list of tau (silent) transtions from the mapped state space (aut file) based on a list of observable actions. The output list can be used in mCRL2 tool for reducing the transtion system based on difference equivalence relationships.

A mappped state space of a Timed Rebeca model (state dransition diagram): mapped state space (aut file)

A list of observable actions: observable actions

Output (i.e., tau transtions): heating_[20_true_false_]

The diagram of the messages passing between actors defined in a Timed Rebeca model of a room temperature control system.

First, the state space of the Timed Rebeca is mapped using cast function. The mappped state space of the Timed Rebeca model (state dransition diagram): mapped state space (aut file)

(The state space includes 76 states and 103 transtions.)

(the maped state space (aut file) contains 103 states and 129 transtions.)

Second, the extraction function uses the maped state space (aut file) and a list of observable actions to generate tau transitions. A list of observable actions: observable actions

Output: tau transitions

(This list shows tau transitions for reducing the casted_LTS based on equivalence relationships.)

The output list above shows tau transitions. The reduced model is generated based on tau transitions and tau_star equivalence relationship (i.e., weak trace equivalence) in mCRL2 tool.

The reduced state space (aut file): abstracted_LTS_diagram. (It contains 49 states and 71 transtions.)

The diagram of the messages passing between actors defined in a Timed Rebeca model of a secure water treatment system.

First, the state space of the Timed Rebeca is mapped using cast function. The mappped state space of the Timed Rebeca model (state dransition diagram): mapped state space (aut file)

(The state space of the Timed Rebeca model includes 688 states and 1825 transtions)

(The mapped state space (aut file) contains 760 states and 1896 transtions)

Second, the extraction function uses the maped state space (aut file) and a list of observable actions to generate tau transitions.

A list of observable actions: observable actions

Output: tau transitions

(This list shows tau transitions for reducing the casted_LTS based on equivalence relationships.)

The output list above shows tau transitions. The reduced model is generated based on tau transitions and tau_star equivalence relationship (i.e., weak trace equivalence) in mCRL2 tool.

The reduced state space (aut file): abstracted_LTS_diagram. (It contains 62 states and 90 transtions.)