It plays a central role in intelligent agent systems to model agents’epistemic states and their changes.Asynchrony plays a key role in distributed systems,in which the messages transmitted may not be received instant...It plays a central role in intelligent agent systems to model agents’epistemic states and their changes.Asynchrony plays a key role in distributed systems,in which the messages transmitted may not be received instantly by the agents.To characterize asynchronous communications,Asynchronous Announcement Logic(AAL)has been presented,which focuses on the logic laws of the change of epistemic state after receiving information.However AAL does not involve the interactive behaviours between an agent and its environment.Epistemic interactions can change agents’epistemic states,while the latter will affect the former.Through enriching the well-known-calculus by adding the operators for passing basic facts and applying the well-known action model logic to describe agents’epistemic states,this paper presents the ecalculus to model epistemic interactions between agents with epistemic states.The e-calculus can be adopted to characterize synchronous and asynchronous communications between agents.To capture the asynchrony,a buffer pool is constructed to store the basic facts announced and each agent reads these facts from this buffer pool in some order.Based on the transmission of link names,the e-calculus is able to realize reading from this buffer pool in different orders.This paper gives two examples:one is to read in the order in which the announced basic facts are sent(First-in-first-out,FIFO),and the other is in an arbitrary order.展开更多
This paper introduces the modifications on actions of a topologyon names of actions and the simplest topology on agents induced by a topology onnames of actions and shows that the limit behaviour of some agents is com...This paper introduces the modifications on actions of a topologyon names of actions and the simplest topology on agents induced by a topology onnames of actions and shows that the limit behaviour of some agents is compatiblewith transitional semantics.展开更多
Formal models of communicating and concurrent systems are one of the most important topics in formal methods,and process calculus is one of the most successful formal models of communicating and concurrent systems.In ...Formal models of communicating and concurrent systems are one of the most important topics in formal methods,and process calculus is one of the most successful formal models of communicating and concurrent systems.In the previous works,the author systematically studied topology in process calculus,probabilistic process calculus and pi-calculus with noisy channels in order to describe approximate behaviors of communicating and concurrent systems as well as randomness and noise in them.This article is a brief survey of these works.展开更多
This paper focuses on the problem of seeking complete axiomatization for finite processes in the process calculus called symbolic probabilistic π-calculus introduced by Wu,Palamidessi and Lin.We provide inference sys...This paper focuses on the problem of seeking complete axiomatization for finite processes in the process calculus called symbolic probabilistic π-calculus introduced by Wu,Palamidessi and Lin.We provide inference systems for both strong and weak symbolic probabilistic bisimulations and also prove their soundness and completeness.This is the first work,to our knowledge,that provides complete axiomatization for symbolic probabilistic bisimulations in the presence of both nondeterministic and probabilistic choice.展开更多
Applying dynamic web services composition is one of the important schemas for solving service-oriented architecture （SOA）and service-oriented computing（SOC）.For implementing dynamic web services composition,the mu...Applying dynamic web services composition is one of the important schemas for solving service-oriented architecture （SOA）and service-oriented computing（SOC）.For implementing dynamic web services composition,the multi agent system （MAS）is applied to web services composition.First, the essentials of the MAS and web services composition are analyzed and their relationship is discussed.Secondly, an MAS-based architecture is designed for dynamic web services composition,and it is named as CSMWC.A Jade tool is used to implement the major components.The architecture can primarily implement syntactic level dynamic web services composition,and it gives a basis for semantic level dynamic web services composition.For specifying the correctness of the architecture,by using pi-calculus,the architecture of the MAS is formally described,and its dynamic properties and adaptability are reasoned.Finally,it demonstrates the idea proposed by the Pi4SOA tool.展开更多
Provable security has become a popular approach for analyzing the security of cryptographic protocols.However,writing and verifying proofs by hand are prone to errors.This paper advocates the automatic security proof ...Provable security has become a popular approach for analyzing the security of cryptographic protocols.However,writing and verifying proofs by hand are prone to errors.This paper advocates the automatic security proof framework with sequences of games.We make slight modifications to Blanchet's calculus to make it easy for parsing the initial game.The main contribution of this work is that it introduces algebraic properties with observational equivalences to automatic security proofs,and thus can deal with some practical cryptographic schemes with hard problems.We illustrate the use of algebraic properties in the framework by proving the semantic security of the ElGamal encryption scheme.展开更多
Correctness is a key attribute of software. Parameterized bisimulation provides a kind of abstract description to verify the correctness of software under environment. In real world situations, many softwares contain ...Correctness is a key attribute of software. Parameterized bisimulation provides a kind of abstract description to verify the correctness of software under environment. In real world situations, many softwares contain some probabilistic information. In this paper, we focus on the probabilistic construction of parameterized bisimulation. Firstly, we extend parameterized bisimulation to probabilistic parameterized bisimulation. Secondly, a quantitative model of approximate correctness of software is proposed. Finally, the subsititutivity laws of quantitative model with various combinators are proved.展开更多
In the study of process calculi, encoding between different calculi is an effective way to compare the expressive power of calculi and can shed light on the essence of where the difference lies. Thomsen and Sangiorgi ...In the study of process calculi, encoding between different calculi is an effective way to compare the expressive power of calculi and can shed light on the essence of where the difference lies. Thomsen and Sangiorgi have worked on the higher-order calculi （higher-order Calculus of Communicating Systems （CCS） and higher-order π-calculus, respectively） and the encoding from and to first-order π-calculus. However a fully abstract encoding of first-order π-calculus with higher-order CCS is not available up-today. This is what we intend to settle in this paper. We follow the encoding strategy, first proposed by Thomsen, of translating first-order π-calculus into Plain CHOCS. We show that the encoding strategy is fully abstract with respect to early bisimilarity （first-order π-calculus） and wired bisimilarity （Plain CHOCS） （which is a bisimulation defined on wired processes only sending and receiving wires）, that is the core of the encoding strategy. Moreover from the fact that the wired bisimilarity is contained by the well-established context bisimilarity, we secure the soundness of the encoding, with respect to early bisimilarity and context bisimilarity. We use index technique to get around all the technical details to reach these main results of this paper. Finally, we make some discussion on our work and suggest some future work.展开更多
Two-thirds simulation provides a kind of abstract description of an implementation with respect to a specification. In order to characterize the approximate two-thirds simulation, we propose the definition of a two- t...Two-thirds simulation provides a kind of abstract description of an implementation with respect to a specification. In order to characterize the approximate two-thirds simulation, we propose the definition of a two- thirds simulation index which expresses the degree to which a binary relation between processes is two-thirds simulation. 2-two-thirds simulation and its substitutivity laws are given in this paper. And, based on 2-two-thirds simulation, we present a measure model for describing the degree of approximation between processes. In particular, we give the modal logical characterization of 2-two-thirds simulation.展开更多
The X calculus is a model of concurrent and mobile systems. It emphasizes that communications are information exchanges. In the paper, two constructions are incorporated into the framework of the chi calculus, which a...The X calculus is a model of concurrent and mobile systems. It emphasizes that communications are information exchanges. In the paper, two constructions are incorporated into the framework of the chi calculus, which are asymmetric communication and mismatch condition widely used in applications. Since the barbed bisimilarity has proved its generality and gained its popularity as an effective approach to generating a reasonable observational equivalence, we study both the operational and algebraic properties of the barbed bisimilarity in this enriched calculus. The investigation supports an improved understanding of the bisimulation behaviors of the model. It also gives a general picture of how the two constructions affect the observational theory.展开更多
基金support of the Natural Science Foundation of Shandong Province(No.ZR2020MF144)Postgraduate Research and Practice Innovation Program of Jiangsu Province(No.KYCX17_0288).
文摘It plays a central role in intelligent agent systems to model agents’epistemic states and their changes.Asynchrony plays a key role in distributed systems,in which the messages transmitted may not be received instantly by the agents.To characterize asynchronous communications,Asynchronous Announcement Logic(AAL)has been presented,which focuses on the logic laws of the change of epistemic state after receiving information.However AAL does not involve the interactive behaviours between an agent and its environment.Epistemic interactions can change agents’epistemic states,while the latter will affect the former.Through enriching the well-known-calculus by adding the operators for passing basic facts and applying the well-known action model logic to describe agents’epistemic states,this paper presents the ecalculus to model epistemic interactions between agents with epistemic states.The e-calculus can be adopted to characterize synchronous and asynchronous communications between agents.To capture the asynchrony,a buffer pool is constructed to store the basic facts announced and each agent reads these facts from this buffer pool in some order.Based on the transmission of link names,the e-calculus is able to realize reading from this buffer pool in different orders.This paper gives two examples:one is to read in the order in which the announced basic facts are sent(First-in-first-out,FIFO),and the other is in an arbitrary order.
文摘This paper introduces the modifications on actions of a topologyon names of actions and the simplest topology on agents induced by a topology onnames of actions and shows that the limit behaviour of some agents is compatiblewith transitional semantics.
基金supported by the National Natural Science Foundation of China(Grant No.60621062).
文摘Formal models of communicating and concurrent systems are one of the most important topics in formal methods,and process calculus is one of the most successful formal models of communicating and concurrent systems.In the previous works,the author systematically studied topology in process calculus,probabilistic process calculus and pi-calculus with noisy channels in order to describe approximate behaviors of communicating and concurrent systems as well as randomness and noise in them.This article is a brief survey of these works.
基金the National Basic Research Program (973) of China (No.2003CB317005)the National Nature Science Foundation of China (Nos.60573002 and 60703033)
文摘This paper focuses on the problem of seeking complete axiomatization for finite processes in the process calculus called symbolic probabilistic π-calculus introduced by Wu,Palamidessi and Lin.We provide inference systems for both strong and weak symbolic probabilistic bisimulations and also prove their soundness and completeness.This is the first work,to our knowledge,that provides complete axiomatization for symbolic probabilistic bisimulations in the presence of both nondeterministic and probabilistic choice.
基金The National Natural Science Foundation of China(No.90612014)IBM China Research Lab Joint Project
文摘Applying dynamic web services composition is one of the important schemas for solving service-oriented architecture （SOA）and service-oriented computing（SOC）.For implementing dynamic web services composition,the multi agent system （MAS）is applied to web services composition.First, the essentials of the MAS and web services composition are analyzed and their relationship is discussed.Secondly, an MAS-based architecture is designed for dynamic web services composition,and it is named as CSMWC.A Jade tool is used to implement the major components.The architecture can primarily implement syntactic level dynamic web services composition,and it gives a basis for semantic level dynamic web services composition.For specifying the correctness of the architecture,by using pi-calculus,the architecture of the MAS is formally described,and its dynamic properties and adaptability are reasoned.Finally,it demonstrates the idea proposed by the Pi4SOA tool.
基金National High Technical Research and Development Program of China(863 program)under Grant No. 2007AA01Z471
文摘Provable security has become a popular approach for analyzing the security of cryptographic protocols.However,writing and verifying proofs by hand are prone to errors.This paper advocates the automatic security proof framework with sequences of games.We make slight modifications to Blanchet's calculus to make it easy for parsing the initial game.The main contribution of this work is that it introduces algebraic properties with observational equivalences to automatic security proofs,and thus can deal with some practical cryptographic schemes with hard problems.We illustrate the use of algebraic properties in the framework by proving the semantic security of the ElGamal encryption scheme.
基金Supported by the National Natural Science Foundation of China(61300048)the Anhui Provincial Natural Science Foundation(1308085QF117,1508085MA14)+2 种基金the Key Natural Science Foundation of Universities of Anhui Province(KJ2014A003,KJ2014A223)the Major Teaching Reform Project of Anhui Higher Education Revitalization Plan(2014ZDJY058)the Excellent Young Talents in Universities of Anhui Province
文摘Correctness is a key attribute of software. Parameterized bisimulation provides a kind of abstract description to verify the correctness of software under environment. In real world situations, many softwares contain some probabilistic information. In this paper, we focus on the probabilistic construction of parameterized bisimulation. Firstly, we extend parameterized bisimulation to probabilistic parameterized bisimulation. Secondly, a quantitative model of approximate correctness of software is proposed. Finally, the subsititutivity laws of quantitative model with various combinators are proved.
基金supported by the National Basic Research 973 Program of China under Grant No.2003CB317005the National Natural Science Foundation of China under Grant Nos.60473006 and 60573002the National Research Foundation for the Doctoral Program of Higher Education of China Research Fund under Grant No.20010248033.
文摘In the study of process calculi, encoding between different calculi is an effective way to compare the expressive power of calculi and can shed light on the essence of where the difference lies. Thomsen and Sangiorgi have worked on the higher-order calculi （higher-order Calculus of Communicating Systems （CCS） and higher-order π-calculus, respectively） and the encoding from and to first-order π-calculus. However a fully abstract encoding of first-order π-calculus with higher-order CCS is not available up-today. This is what we intend to settle in this paper. We follow the encoding strategy, first proposed by Thomsen, of translating first-order π-calculus into Plain CHOCS. We show that the encoding strategy is fully abstract with respect to early bisimilarity （first-order π-calculus） and wired bisimilarity （Plain CHOCS） （which is a bisimulation defined on wired processes only sending and receiving wires）, that is the core of the encoding strategy. Moreover from the fact that the wired bisimilarity is contained by the well-established context bisimilarity, we secure the soundness of the encoding, with respect to early bisimilarity and context bisimilarity. We use index technique to get around all the technical details to reach these main results of this paper. Finally, we make some discussion on our work and suggest some future work.
文摘Two-thirds simulation provides a kind of abstract description of an implementation with respect to a specification. In order to characterize the approximate two-thirds simulation, we propose the definition of a two- thirds simulation index which expresses the degree to which a binary relation between processes is two-thirds simulation. 2-two-thirds simulation and its substitutivity laws are given in this paper. And, based on 2-two-thirds simulation, we present a measure model for describing the degree of approximation between processes. In particular, we give the modal logical characterization of 2-two-thirds simulation.
基金Supported by the National Grand Fundamental Research 973 Program of China under Grant No.2003CB317005the National Natural Science Foundation of China under Grant No.60473006the National Research Foundation for the Doctoral Program of Education of China under Grant No.20010248033.
文摘The X calculus is a model of concurrent and mobile systems. It emphasizes that communications are information exchanges. In the paper, two constructions are incorporated into the framework of the chi calculus, which are asymmetric communication and mismatch condition widely used in applications. Since the barbed bisimilarity has proved its generality and gained its popularity as an effective approach to generating a reasonable observational equivalence, we study both the operational and algebraic properties of the barbed bisimilarity in this enriched calculus. The investigation supports an improved understanding of the bisimulation behaviors of the model. It also gives a general picture of how the two constructions affect the observational theory.
