An Equivalence Relation on Extended Finite State Machines

The extended finite state machine (EFSM) is an extension of the finite state machine, which creates input and output parameters, context variables, operations and predicates. It is applied widely in the fields of software engineering since there are many tools that support software development activities based on the EFSM models. However, the theoretical foundation of EFSM is not yet well-developed. This paper is a preliminary investigation of EFSM model. Firstly, this paper defines an equivalence relation on a class of EFSMs, namely restricted EFSMs. Secondly, the partial order relation and synchronous product on restricted EFSMs are approached. Finally, an algorithm is derived to decide the equivalence relation. The results of this paper are promising to be applied in software fields.