Class BisimulationCheckerSupport<B extends Bigraph<? extends Signature<?>>,AST extends ReactionGraph<B>>

java.lang.Object
org.bigraphs.framework.simulation.equivalence.BisimulationCheckerSupport<B,AST>
Type Parameters:
B - the type of the state of <AST>
AST - the type of the transition system

public class BisimulationCheckerSupport<B extends Bigraph<? extends Signature<?>>,AST extends ReactionGraph<B>> extends Object
This implementation provides a basic extensible (template) method for computing bisimilarity of LTSs. The type of the transition system is those whose transition relations are reaction rules, and states are bigraphs.

This class contains the checkBisimulation_Bighuggies(ReactionGraph, ReactionGraph) method that implements the bisimulation check using a breadth-first search approach.

Depending on the complexity of the transition systems, this method needs to be adapted with more sophisticated logic.

Author:
Dominik Grzelak
See Also:
  • "https://github.com/bighuggies/bisimulation"
  • Constructor Details

    • BisimulationCheckerSupport

      public BisimulationCheckerSupport()
  • Method Details

    • checkBisimulation_Bighuggies

      public boolean checkBisimulation_Bighuggies(AST system1, AST system2)
      Bisimilarity checking using the KANELLAKIS_SMOLKA algorithm from the external "bighuggies:bisimulation" Java library.

      Input: Two states, one from each transition system. Output: Boolean value indicating whether the states are bisimilar.

      Parameters:
      system1 -
      system2 -
      Returns:
      true, if both systems are bisimilar; otherwise false