Huili Grace Xing

h-index74
2papers
22,018citations

2 Papers

2.5AIJun 29, 2022
An extension of process calculus for asynchronous communications between agents with epistemic states

Huili Xing

It plays a central role in intelligent agent systems to model agent's epistemic state and its change. 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. Through enriching the well-known pi-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 e-calculus 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 pools 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.

1.2LOAug 5, 2022
Covariant-Contravariant Refinement Modal $μ$-calculus

Huili Xing

The notion of covariant-contravariant refinement (CC-refinement, for short) is a generalization of the notions of bisimulation, simulation and refinement. This paper introduces CC-refinement modal $μ$-calculus (CCRML$^μ$) obtained from the modal $μ$-calculus system K$^μ$ by adding CC-refinement quantifiers, establishes an axiom system for CCRML$^μ$ and explores the important properties: soundness, completeness and decidability of this axiom system. The language of CCRML$^μ$ may be considered as a specification language for describing the properties of a system referring to reactive and generative actions. It may be used to formalize some interesting problems in the field of formal methods.