Games For Behavioral Equivalences

In this thesis,we first give a summary of algebra,logic and game,which are three ways of describing abstract models.And we mainly introduce the Ehrenfeucht-Fra(i|¨)ss(?) game and its variants.Then we will revisit some important behavioral equivalences(or process equivalences) and their logic characterizations,also including the linear/branching time hierarchy which was proposed by Rob J.Van Glabbeek.The core part of this thesis is the game hierarchy. We give the definitions of the game template and some game rules such that different games can be defined by the different combinations of them.Furthermore,each equivalence in the linear/branching time hierarchy can be characterized by a game defined in such a way. We will organize these games by their strictnesses,and propose a game hierarchy,each game in it is a characterization of a behavioral equivalence.The hierarchy which is proposed in a game theoretical way is more finer than the linear/branching time hierarchy.This work has been published in APLAS 2008 which is an international conference.In the last part of this thesis,we will characterize behavioral equivalences by combinatorial games.We firstly define two basic games and four combination operations.The games which are defined by game template can also be defined by the combinations of several basic games.Therefore,combinatorial games can also be used to characterize behavioral equivalences.The combinatorial games are much finer than game template in characterizing behavioral equivalences,and are much closer to the design of equivalence checking algorithms.