The Precongruence And Axiomatic System Of CC-simulation Under GSOS/ntyft/ntyxt Operators

Process calculus is a prototype specification language that characterizes the behavior of concurrent and interactive reaction systems,which describes the specification and implementation of reactive systems through process terms.Whether or not the specifications are met is characterized by behavioral equivalence or refinement relations.The classical simulation relationships are mainly for the characterization of refinement relationships between reactive systems,which only have passive behaviors.For systems with active behavior,the classical simulation relationships will no longer be applyed.To this end,the academic community promotes the concept Covariant-Contravariant simulation(CC-simulation),which is the extension of the bisimulation and simulation.It distinguishes the types of actions and describes the different requirements of active,passive and communication actions in refinement relationships between specifications and implementations.Since the(pre)congruence of the operators in the calculus system is the fundamental basis for the specification and the implementation of modular construction,analysis and reasoning,establishing the(pre)congruence of behavioral relations is one of the important research contents of process calculus.In addition,the characterization of the(in)equality of behavioral relations is a concentrated expression of the algebraic characteristics of process calculus,which lays an indispensable theoretical foundation for the mechanical theorem proving of equivalence(or refinement)relations between processes.The proof of(pre)congruence and the axiomatization of behavioral relationship depend on the structural operational semantics(SOS)rules of the operators in the calculus systems.In order to avoid duplication of these works,academia has carried out research on SOS meta-theory.It is hoped that based on the SOS rule formats of normalizing the operation semantics of process operators,the universal conclusion and the proof of(pre)congruence and the construction methods for the axiomatic construction will be given.This thesis will study the(pre)congruence and axiomatic systems of CC-simulation based on the widely used GSOS and ntyft/ntyxt rule formats.The main work is as follows:1.Based on the GSOS rule format,some sufficient conditions for the precongruence of CC-simulation are given and the CC-GSOS rule format is proposed,we illustrate the necessity of its constraints by examples.The precongruence of CC-simulation under CC-GSOS operators is proved.Furthermore,we study the precongruence of CC-simulatin relative operators in ntyft/ntyxt,a more general rule format,and propose the CC-ntyft/ntyxt rule format.The precongruence of CC-simulation under CC-ntyft/ntyxt operators is also given.2.Based on the above research and the work of Aceto et al,a general method for constructing the axiomatizatic systems of CC-simulation is proposed on the transition system specifications defined by CC-GSOS rules,and the soundness and ground completeness of the axiomatic systems are proved.3.The relationship between the two axiomatizations of bisimulation and CC-simulation under the CC-ntyft/ntyxt operators is studied.It is proved that for finite processes,by adding two axioms S_p~r andS_p~l,the new axiomatic system is sound and complete for CC-simulation,if the original one is sound and complete for bisimulation.