mcrl2/pbes/bisimulation.h

Include file:

#include "mcrl2/pbes/bisimulation.h"

Bisimulation algorithms.

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.

Parameters:

  • model A linear process specification

  • spec A linear process specification

Returns: A pbes that expresses branching bisimulation between the 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.

Parameters:

  • model A linear process specification

  • spec A linear process specification

Returns: A pbes that expresses branching simulation equivalence between the 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.

Parameters:

  • model A linear process specification

  • spec A linear process specification

Returns: A pbes that expresses strong bisimulation between the 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.

Parameters:

  • model A linear process specification

  • spec A linear process specification

Returns: A pbes that expresses weak bisimulation between the two specifications.