cfl_bisimulation.cpp File Reference

Bisimulation relations. More...

#include <cfl_bisimulation.h>
#include <string>
#include <sstream>
#include <stack>

Go to the source code of this file.

Classes
struct	faudes::Pnode
class	faudes::Bisimulation
struct	faudes::Bisimulation::State

Namespaces
	faudes
	libFAUDES resides within the namespace faudes.

Functions
void	faudes::ComputeBisimulation (const Generator &rGenOrig, map< Idx, Idx > &rMapStateToPartition)
	Computation of the coarsest bisimulation relation for a specified generator. More...
void	faudes::ComputeBisimulation (const Generator &rGenOrig, map< Idx, Idx > &rMapStateToPartition, Generator &rGenPart)
	Computation of the coarsest bisimulation relation for a specified generator. More...
void	faudes::ComputeBisimulation (const Generator &rGenOrig, std::list< StateSet > &rPartitions)
	Computation of the coarsest bisimulation relation for a specified generator. More...

Detailed Description

Bisimulation relations.

Functions to compute bisimulation relations on dynamic systems (represented by non-deterministic finite automata).

The relevant algorithms are described in J.-C. Fernandez, "An implementation of an efficient algorithm for bisimulation equivalence", Science of Computer Programming, vol. 13, pp. 219-236, 1990.

This code was originally part of the observer plug-in (op_bisimulation.* and op_partition.*). It moved in revised form to corefaudes as of libFAUDES 2.26.

Definition in file cfl_bisimulation.cpp.