Research On Concurrent Weighted ?-Calculus

With the area of fomal methods,various kinds of automata,systmes of process calculus and logical languages are the most common mathematical tools for modeling and analysis.Timed automata,weighted automata and weighted timed automata are used to model and analyze the systems of quantitative information;Process calculus is available for the modular designing of concurrent systmes,while process algebras cannot express basic boolean operations;Spatial logic,separation logic and probabilistic logic are not good enough to describe the quantitative properties.In order to address these problems,concurrent weighted logic CWL is proposed by Kim.G.Larsen.CWL is a multimodal logic in which the the state modality and the transition modality can describe the quantitative information of a system because of the number information.In addition,the composition modality in CWL supports the modular reasoning and specification.However,the fix point is not involved in CWL,and that is important for describing the properties of computational system of infinite behavior(for example,safety\liveness).This paper intends to study CWL further.Main contributions include:1.Adding the fix point to CWL(not contain the daul form of the composition modality)and researching a segment of CWL with fix point so that concurrent weighted ?-calculus(? CWL)formed.The corresponding alternating tree automata is given aimed at ?CWL.The basic properties of the automata is researched and two basic conclusions is proved:the nonemptiness of the automata is decidable in exponential time;the automata can accept a finite model if its acceptable language is not empty.2.A transformation between ?CWL and ?CWL oriented alternating tree automata is realized.Firstly,a ?CWL oriented automata A(?)based on the structure of the formula ? is advocated,and it is proved that the acceptable languages of A(?)are really the models of ? so that the satisfiable problem of ?CWL is reducted to the nonemptiness of the automata.Also,each ?CWL oriented alternating tree automata A can be converted into a ?CWL fomula ?A and the acceptable languages of A are really the models of ?A.3.Based on above conclusions,the basic properties of ?CWL is researched.And the decidability of satisfiability and small model property of ?CWL are proved to be true.By introducing the bisimulation quantifier on label weighted transition system and combining with the ?CWL oriented alternating tree automata,the uniform interpolation theorem on ?CWL is proved to be true.