4.1 Equivalences
The
tool can check simulation equivalence, and (weak) trace equivalence between LTSs. In the latest release an algorithm for checking ready simulation was implemented and integrated into the toolset [
23]. Regarding bisimulations, the tool can furthermore check strong, branching and weak bisimulation between LTSs. The latter two are sensitive to so-called
internal behaviour, represented by the action
\(\tau \).
Divergence-preserving variants of these bisimulations are supported, which take the ability to perform infinite sequences of internal behaviour into account. The above mentioned equivalences can also be used by the
tool.
Recently, the Groote/Jansen/Keiren/Wijs algorithm (GJKW) for branching bisimulation [
24], with complexity
\(O(m(\log | Act |+\log n))\), was implemented. When tested in practice, it frequently demonstrates performance improvements by a factor of 10, and occasionally by a factor of 100 over the previous algorithm by Groote and Vaandrager [
31].
The improved complexity is the result of combining the
process the smaller half principle [
35] with the key observations made by Groote and Vaandrager regarding internal transitions [
31]. GJKW uses partition refinement to identify all classes of equivalent states. Repeatedly, one class (or
block)
B is selected to be the so-called
splitter, and each block
\(B'\) is checked for the reachability of
B, where internal behaviour should be skipped over. In case
B is reachable from some states in
\(B'\) but not from others,
\(B'\) needs to be split into two subblocks, separating the states from which
B can and cannot be reached. Whenever a fixed-point is reached, the obtained partition defines the equivalence relation.
GJKW applies process the smaller half in two ways. First of all, it is ensured that each time a state s is part of a splitter B, the size of B, in terms of number of states, is at most half the size of the previous splitter in which s resided. To do this, blocks are partitioned in constellations. A block is selected as splitter iff its size is at most half the number of states in the constellation in which it resides. When a splitter is selected, it is moved into its own, new, constellation, and when a block is split, the resulting subblocks remain in the same constellation.
Second of all, it has to be ensured that splitting a block \(B'\) takes time proportional to the smallest resulting subblock. To achieve this, two state selection procedures are executed in lockstep, one identifying the states in \(B'\) that can reach the splitter, and one detecting the other states. Once one of these procedures has identified all its states, those states can be split off from \(B'\).
Reachability checking is performed efficiently by using the notion of
bottom state [
31], which is a state that has no outgoing internal transitions leading to a state in the same block. It suffices to check whether any bottom state in
\(B'\) can reach
B. Hence, it is crucial that for each block, the set of bottom states is maintained during execution of the algorithm.
GJKW is very complicated due to the amount of book keeping needed to achieve the complexity. Among others, a data structure by Valmari, called
refinable partition [
46] is used, together with three copies of all transitions, structured in different ways to allow fast retrieval in the various stages of the algorithm.
Besides checking for branching bisimulation, GJKW is used as a basis for checking strong bisimulation (in which case it corresponds to the Paige-Tarjan algorithm [
41]) and as a preprocessing step for checking weak bisimulation.
For the support of the analysis of probabilistic systems, a number of preliminary extensions have been made to the mCRL2 toolset. In particular, a new algorithm has been added to reduce PLTSs – containing both non-deterministic and probabilistic choice [
44] – modulo strong probabilistic bisimulation. This new Paige-Tarjan style algorithm, called GRV [
26] and implemented in the tool
ltspbisim
, improves upon the complexity of the best known algorithm so far by Baier
et al. [
2]. The GRV algorithm was inspired by work on lumping of Markov Chains by Valmari and Franceschinis [
47] to limit the number of times a probabilistic transition needs to be sorted. Under the assumption of a bounded fan-out for probabilistic states, the time complexity of GRV is
\(O( n_p \log n_a)\) with
\(n_p\) equal to the number of probabilistic transitions and
\(n_a\) being the number of non-deterministic states in a PLTS.
4.2 Refinement
In model checking there is typically a single model on which properties, defined in another language, are verified. An alternative approach that can be employed is refinement checking. Here, the correctness of the model is verified by establishing a refinement relation between an implementation LTS and a specification LTS. The chosen refinement relation must be strong enough to preserve the desired properties of the model, but also weak enough to allow many valid implementations.
For refinement relations the
ltscompare
tool can check the asymmetric variants of simulation, ready simulation and (weak) trace equivalence between LTSs. In the latest release, several algorithms have been added to check (weak) trace, (weak) failures and failures-divergences refinement relations based on the algorithms introduced in [
48]. We remark that weak failures refinement is known as stable failures refinement in the literature. Several improvements have been made to the reference algorithms and the resulting implementation has been successfully used in practice, as described in Sect.
7.1.
The newly introduced algorithms are based on the notion of antichains. These algorithms try to find a witness to show that no refinement relation exists. The antichain data structure keeps track of the explored part of the state space and assists in pruning other parts based on an ordering. If no refinement relation exists, the tool provides a counterexample trace to a violating state. To further speed up refinement checking, the tool applies divergence-preserving branching bisimulation reduction as a preprocessing step.