bisimulation.h File Reference

Bisimulation algorithms. More...

Go to the source code of this file.

Classes
class	mcrl2::pbes_system::bisimulation_algorithm
	Base class for bisimulation algorithms. More...
class	mcrl2::pbes_system::branching_bisimulation_algorithm
	Algorithm class for branching bisimulation. More...
class	mcrl2::pbes_system::strong_bisimulation_algorithm
	Algorithm class for strong bisimulation. More...
class	mcrl2::pbes_system::weak_bisimulation_algorithm
	Algorithm class for weak bisimulation. More...
class	mcrl2::pbes_system::branching_simulation_equivalence_algorithm
	Algorithm class for branching simulation equivalence. More...

Namespaces
namespace	mcrl2
namespace	mcrl2::pbes_system
	The main namespace for the PBES library.

Functions
pbes	mcrl2::pbes_system::branching_bisimulation (const lps::specification &model, const lps::specification &spec)
	Returns a pbes that expresses branching bisimulation between two specifications.
pbes	mcrl2::pbes_system::strong_bisimulation (const lps::specification &model, const lps::specification &spec)
	Returns a pbes that expresses strong bisimulation between two specifications.
pbes	mcrl2::pbes_system::weak_bisimulation (const lps::specification &model, const lps::specification &spec)
	Returns a pbes that expresses weak bisimulation between two specifications.
pbes	mcrl2::pbes_system::branching_simulation_equivalence (const lps::specification &model, const lps::specification &spec)
	Returns a pbes that expresses branching simulation equivalence between two specifications.

Detailed Description

Bisimulation algorithms.

Definition in file bisimulation.h.