cfl_bisimulation.h File Reference

Bisimulation relations. More...

#include "cfl_definitions.h"
#include "cfl_generator.h"
#include <vector>
#include <map>

Go to the source code of this file.

Namespaces
	faudes
	libFAUDES resides within the namespace faudes.

Functions
FAUDES_API void	faudes::ComputeBisimulation (const Generator &rGenOrig, std::map< Idx, Idx > &rMapStateToPartition)
	Computation of the coarsest bisimulation relation for a specified generator. More...
FAUDES_API void	faudes::ComputeBisimulation (const Generator &rGenOrig, std::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-plugin and moved in revised form to corefaudes by Version 2.26

Definition in file cfl_bisimulation.h.