liblts_weak_bisim.h File Reference

This file defines an algorithm for weak bisimulation, by calculating the transitive tau closure and apply strong bisimulation afterwards. In order to apply this algorithm it is advisable to first apply a branching bisimulation reduction. More...

Go to the source code of this file.

Namespaces
namespace	mcrl2
	A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
namespace	mcrl2::lts
	The main LTS namespace.
namespace	mcrl2::lts::detail
	A base class for the lts_dot labelled transition system.

Functions
template<class LTS_TYPE >
void	mcrl2::lts::detail::weak_bisimulation_reduce (LTS_TYPE &l, const bool preserve_divergences=false)
	Reduce LTS l with respect to (divergence-preserving) weak bisimulation.
template<class LTS_TYPE >
bool	mcrl2::lts::detail::destructive_weak_bisimulation_compare (LTS_TYPE &l1, LTS_TYPE &l2, const bool preserve_divergences=false)
	Checks whether the initial states of two LTSs are weakly bisimilar.
template<class LTS_TYPE >
bool	mcrl2::lts::detail::weak_bisimulation_compare (const LTS_TYPE &l1, const LTS_TYPE &l2, const bool preserve_divergences=false)
	Checks whether the initial states of two LTSs are weakly bisimilar.

Detailed Description

This file defines an algorithm for weak bisimulation, by calculating the transitive tau closure and apply strong bisimulation afterwards. In order to apply this algorithm it is advisable to first apply a branching bisimulation reduction.

Definition in file liblts_weak_bisim.h.