mcrl2/pbes/bisimulation.h

Include file:

#include "mcrl2/pbes/bisimulation.h"

Bisimulation algorithms.

Classes

• mcrl2::pbes_system::bisimulation_algorithm
• mcrl2::pbes_system::branching_bisimulation_algorithm
• mcrl2::pbes_system::branching_simulation_equivalence_algorithm
• mcrl2::pbes_system::strong_bisimulation_algorithm
• mcrl2::pbes_system::weak_bisimulation_algorithm

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.