O(m log n)-time branching bisimulation algorithm. More...

Classes
class	mcrl2::lts::detail::bisim_dnj::iterator_or_counter< Iterator >
	union: either iterator or counter (for initialisation) More...

class	mcrl2::lts::detail::bisim_dnj::state_info_entry
	stores information about a single state More...

union	mcrl2::lts::detail::bisim_dnj::state_info_entry::bl_t
	block where the state belongs More...

class	mcrl2::lts::detail::bisim_dnj::permutation_entry
	entry in the permutation array More...

class	mcrl2::lts::detail::bisim_dnj::block_t
	stores information about a block More...

class	mcrl2::lts::detail::bisim_dnj::part_state_t
	refinable partition data structure More...

class	mcrl2::lts::detail::bisim_dnj::succ_entry
	information about a transition sorted per source state More...

class	mcrl2::lts::detail::bisim_dnj::block_bunch_entry
	information about a transition grouped per (source block, bunch) pair More...

class	mcrl2::lts::detail::bisim_dnj::pred_entry
	information about a transition sorted per target state More...

class	mcrl2::lts::detail::bisim_dnj::action_block_entry
	information about a transition sorted per (action, target block) pair More...

class	mcrl2::lts::detail::bisim_dnj::bunch_t
	bunch of transitions More...

union	mcrl2::lts::detail::bisim_dnj::bunch_t::next_nontrivial_and_label_t
	pointer to next non-trivial bunch (in the single-linked list) or label More...

class	mcrl2::lts::detail::bisim_dnj::block_bunch_slice_t
	Information about a set of transitions with the same source block, in the same bunch. More...

class	mcrl2::lts::detail::bisim_dnj::part_trans_t

class	mcrl2::lts::detail::bisim_partitioner_dnj< LTS_TYPE >
	implements the main algorithm for the branching bisimulation quotient More...

Namespaces
namespace	mcrl2

namespace	mcrl2::lts
	The main LTS namespace.

namespace	mcrl2::lts::detail
	A base class for the lts_dot labelled transition system.

namespace	mcrl2::lts::detail::bisim_dnj

Macros
#define	PRINT_SG_PL(counter, sg_string, pl_string)

#define	PRINT_INT_PERCENTAGE(num, denom) (((num) * 200 + (denom)) / (denom) / 2)

Typedefs
using	mcrl2::lts::detail::bisim_dnj::permutation_t = fixed_vector< permutation_entry >

using	mcrl2::lts::detail::bisim_dnj::block_bunch_slice_iter_t = simple_list< block_bunch_slice_t >::iterator

using	mcrl2::lts::detail::bisim_dnj::block_bunch_slice_const_iter_t = simple_list< block_bunch_slice_t >::const_iterator

using	mcrl2::lts::detail::bisim_dnj::block_bunch_slice_iter_or_null_t = iterator_or_null_t< block_bunch_slice_t >

Enumerations
enum class	mcrl2::lts::detail::bisim_dnj::new_block_mode_t { mcrl2::lts::detail::bisim_dnj::new_block_mode_t::new_block_is_U , mcrl2::lts::detail::bisim_dnj::new_block_mode_t::new_block_is_R }

Functions
template<class LTS_TYPE >
static void	mcrl2::lts::detail::bisim_dnj::finalise_U_is_smaller (const block_t const block_U, const block_t const block_R, const bisim_partitioner_dnj< LTS_TYPE > &partitioner)
	moves temporary work counters to normal ones if the U-block is smaller

template<class LTS_TYPE >
static void	mcrl2::lts::detail::bisim_dnj::finalise_R_is_smaller (const block_t const block_U, const block_t const block_R, const bisim_partitioner_dnj< LTS_TYPE > &partitioner)
	moves temporary work counters to normal ones if the R-block is smaller

template<class LTS_TYPE >
void	mcrl2::lts::detail::bisimulation_reduce_dnj (LTS_TYPE &l, bool const branching=false, bool const preserve_divergence=false)
	Reduce transition system l with respect to strong or (divergence-preserving) branching bisimulation.

template<class LTS_TYPE >
bool	mcrl2::lts::detail::destructive_bisimulation_compare_dnj (LTS_TYPE &l1, LTS_TYPE &l2, bool const branching=false, bool const preserve_divergence=false, bool const generate_counter_examples=false, const std::string &="", bool=false)
	Checks whether the two initial states of two LTSs are strong or (divergence-preserving) branching bisimilar.

template<class LTS_TYPE >
bool	mcrl2::lts::detail::bisimulation_compare_dnj (const LTS_TYPE &l1, const LTS_TYPE &l2, bool const branching=false, bool const preserve_divergence=false)
	Checks whether the two initial states of two LTSs are strong or (divergence-preserving) branching bisimilar.

Variables
struct {

}	mcrl2::lts::detail::bisim_dnj::action_label_greater

Detailed Description

O(m log n)-time branching bisimulation algorithm.

This file implements an efficient partition refinement algorithm for labelled transition systems inspired by Groote / Jansen / Keiren / Wijs (2017) and Valmari (2009) to calculate the branching bisimulation classes of a labelled transition system. Different from the 2017 article, it does not translate the LTS to a Kripke structure, but works on the LTS directly. In this way the memory use can be reduced. The algorithm is described in the conference publication

David N. Jansen, Jan Friso Groote, Jeroen J.A. Keiren, Anton Wijs: An O(m log n) algorithm for branching bisimilarity on labelled transition systems. In: Armin Biere, David Parker (Eds.): Tools and Algorithms for the Construction and Analysis of Systems: TACAS. (LNCS 12070). Springer: Cham,

pp 3-20. https://doi.org/10.1007/978-3-030-45237-7_1

Partition refinement means that the algorithm maintains a partition of the state space of the LTS into "blocks". A block contains all states in one or several branching bisimulation equivalence classes. Blocks are being refined until every block contains exactly one branching bisimulation equivalence class.

The algorithm divides the non-inert transitions into action_block-slices. An action_block-slice contains all transitions with a given action label into one block. One or more action_block-slices are joined into a bunch. Bunches register which blocks have already been stabilised:

‍Invariant: The blocks are stable under the bunches, i. e. if a block has a transition in a bunch, then every bottom state in this block has a transition in this bunch.

However, if a bunch is non-trivial (i. e., it contains more than one action_block-slice), its slices may split some blocks into finer parts: not all states may have a transition in the same action_block-slice. So, a refinement step consists of moving one small action_block-slice from a non-trivial bunch to a new bunch and then splitting blocks to restore the Invariant. Splitting is always done by finding a small subblock and moving the states in that subblock to a new block. Note that we always handle a small part of some larger unit; that ensures that each state and transition is only touched O(log n) times.

After splitting blocks, some inert transitions may have become non-inert. These transitions mostly need to be inserted into their own bunch. Also, some states may have lost all their inert transitions and become new bottom states. These states need to be handled as well to re-establish the Invariant.

Overall, we spend time as follows:

Every transition is moved to a new bunch at most log₂(2 * n²) = 2*log₂(n) + 1 times. Every move leads to O(1) work.
Every state is moved to a new block at most log₂(n) times. Every move leads to work proportional to the number of its incoming and outgoing transitions.
Every state becomes a new bottom state at most once. When this happens, this leads to work proportional to the number of its outgoing transitions. When summing this up over all states and transitions, we get that the algorithm spends time in O(m log n), where m is the number of transitions and n ist the number of states.

Author: David N. Jansen, Institute of Software, Chinese Academy of Sciences, Beijing, PR China

Definition in file liblts_bisim_dnj.h.

Macro Definition Documentation

◆ PRINT_INT_PERCENTAGE

#define PRINT_INT_PERCENTAGE	(	num,
		denom
	)	(((num) * 200 + (denom)) / (denom) / 2)

◆ PRINT_SG_PL

#define PRINT_SG_PL	(	counter,
		sg_string,
		pl_string
	)

Value:

(counter) \

<< (1 == (counter) ? (sg_string) : (pl_string))

Classes

Namespaces

Macros

Typedefs

Enumerations

Functions

Variables

Detailed Description

Macro Definition Documentation

◆ PRINT_INT_PERCENTAGE

◆ PRINT_SG_PL