An extension of process calculus for asynchronous communications between agents with epistemic states

doi:10.1007/s11704-023-3208-4

Front. Comput. Sci.

2025, Vol. 19

Issue (3) : 193401 https://doi.org/10.1007/s11704-023-3208-4

Theoretical Computer Science

An extension of process calculus for asynchronous communications between agents with epistemic states

Huili XING^1,²(

), Zhaohui ZHU¹, Jinjin ZHANG³(

)

¹. College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 211106, China
². Department of Medical Information, Binzhou Medical University, Yantai 264003, China
³. College of Information Science, Nanjing Audit University, Nanjing 211815, China

Download: PDF(2198 KB) HTML
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

Abstract

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 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 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.

Keywords process calculus epistemic interaction asynchronous communication

Corresponding Author(s): Huili XING,Jinjin ZHANG

About author: Li Liu and Yanqing Liu contributed equally to this work.

Issue Date: 24 April 2024

Cite this article:

Huili XING,Zhaohui ZHU,Jinjin ZHANG. An extension of process calculus for asynchronous communications between agents with epistemic states[J]. Front. Comput. Sci., 2025, 19(3): 193401.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-023-3208-4
https://academic.hep.com.cn/fcs/EN/Y2025/V19/I3/193401

$(OUT-name) a ¯ c . P ? a ¯ c p P$	$(TAU) τ . P ? τ p P$
$(IN-name) a (z) . P ? a c p P {c / z}$	$(SUM-L) P ? α p P ′ P + Q ? α p P ′$
$(PAR-L) P ? β p P ′ P ∣ Q ? β p P ′ ∣ Q (b n (β) ∩ f n (Q) = ∅)$
$(RES) P ? β p P ′ ν z P ? β p ν z P ′ (z ∉ n a (β))$	$(OPEN) P ? a ¯ z p P ′ ν z P ? a ¯ (z) p P ′ (z ≠ a)$
$(CLOSE-L) P ? a ¯ (z) p P ′ Q ? a z p Q ′ P ∣ Q ? τ p ν z (P ′ ∣ Q ′) (z ∉ f n (Q))$	$(REP-ACT) P ? β p P ′! P ? β p P ′ ∣! P$
$(COMM-L) P ? a ¯ c p P ′ Q ? p a c Q ′ P ∣ Q ? p τ P ′ ∣ Q ′$	$(REP-COMM) P ? p a ¯ c P ′ P ? a c p P ″! P ? τ p (P ′ ∣ P ″) ∣! P$
$(REP-CLOSE) P ? a ¯ (z) p P ′ P ? a z p P ″! P ? τ p (ν z (P ′ ∣ P ″)) ∣! P (z ∉ f n (P))$

Tab.1 The SOS rules for processes

Fig.1 The action model for trivial announcement

Fig.2 The action model for public

q (∈ A t o m)

-announcement

Fig.3 Applying action models on Kripke models through the operator

⊗

Fig.4 The action model for the agent

B

receiving the fact

q

Fig.5 The action model for passing the fact

q

from the agent

A

B

(OUT-fact) a ¯ q . P ? a ¯ q p P

(IN-fact) a (χ) . P ? a q p P {q / χ}

Tab.2 The SOS rules for processes added in the e-calculus

$(π)$	$P ? β p P ′ (M, s) ? [P] A ? β (M, s) ? [P ′] A (β ∈ A c t and β ≠ a ¯ q, a q)$	$(IN e) P ? a q p P ′ (M, s) ? [P] A → ? a q, A ? (M, s) ⊗ (M q, A, s) ? [P ′] A$
$(OUT e)$	$P ? a ¯ q p P ′ (M, s) ? [P] A → ? a ¯ q, A ? (M, s) ? [P ′] A (M, s ⊨ ? A q)$	$(PAR e -L) (M, s) ? G ? l (M ′, s ′) ? G ′ (M, s) ? G ∥ H ? l (M ′, s ′) ? G ′ ∥ H (b n (l) ∩ f n (H) = ∅)$
$(OPEN e)$	$(M, s) ? G ? a ¯ z (M, s) ? G ′ (M, s) ? ν z G ? a ¯ (z) (M, s) ? G ′ (z ≠ a)$	$(RES e) (M, s) ? G ? l (M ′, s ′) ? G ′ (M, s) ? ν z G ? l (M ′, s ′) ? ν z G ′ (z ∉ n a (l) whenever l ≠ ? a, q, A, B ?)$
$(CLOSE e -L)$	$(M, s) ? G ? a ¯ (z) (M, s) ? G ′ (M, s) ? H ? a z (M, s) ? H ′ (M, s) ? G ∥ H ? τ (M, s) ? ν z (G ′ ∥ H ′) (z ∉ f n (H))$
$(COMM e -fact-L)$	$(M, s) ? G → ? a ¯ q, A ? (M 1, s 1) ? G ′ (M, s) ? H → ? a q, B ? (M 2, s 2) ? H ′ (M, s) ? G ∥ H → ? a, q, A, B ? (M, s) ⊗ (M q, A, B, s) ? G ′ ∥ H ′$	$(COMM e -name-L) (M, s) ? G ? a ¯ c (M, s) ? G ′ (M, s) ? H ? a c (M, s) ? H ′ (M, s) ? G ∥ H ? τ (M, s) ? G ′ ∥ H ′$

Tab.3 The SOS rules for the e-calculus (SOS

e

)

1	M J, Pettinati R C Arkin . Push and pull: shepherding multi-agent robot teams in adversarial situations. In: Proceedings of 2019 IEEE International Conference on Advanced Robotics and Its Social Impacts (ARSO). 2019, 665−679
2	S, Seuken S Zilberstein . Formal models and algorithms for decentralized decision making under uncertainty. Autonomous Agents and Multi-Agent Systems, 2008, 17( 2): 190–250
3	K, Harikumar J, Senthilnath S Sundaram . Multi-UAV oxyrrhis marina-inspired search and dynamic formation control for forest firefighting. IEEE Transactions on Automation Science and Engineering, 2019, 16( 2): 863–873
4	S M, Azizi K Khorasani . A hierarchical architecture for cooperative actuator fault estimation and accommodation of formation flying satellites in deep space. IEEE Transactions on Aerospace and Electronic Systems, 2012, 48( 2): 1428–1450
5	J, Hu P, Bhowmick A Lanzon . Distributed adaptive time-varying group formation tracking for multiagent systems with multiple leaders on directed graphs. IEEE Transactions on Control of Network Systems, 2020, 7( 1): 140–150
6	Ditmarsch H van . Asynchronous announcements. 2017, arXiv preprint arXiv: 1705.03392v2
7	P, Balbiani Ditmarsch H, van S F González . Asynchronous announcements. ACM Transactions on Computational Logic, 2022, 23( 2): 10
8	S, Knight B, Maubert F Schwarzentruber . Reasoning about knowledge and messages in asynchronous multi-agent systems. Mathematical Structures in Computer Science, 2019, 29( Spec.1): 127–168
9	A, Baltag L S, Moss S Solecki . The logic of public announcements, common knowledge, and private suspicions. In: Proceedings of the 7th Conference on Theoretical Aspects of Rationality and Knowledge. 1998, 43−56
10	J Plaza . Logics of public communications. Synthese, 2007, 158( 2): 165–179
11	R, Fagin J Y, Halpern Y, Moses M Y Vardi . Reasoning About Knowledge. Cambridge: The MIT Press, 2003
12	Ditmarsch H, van der Hoek W, van B Kooi . Dynamic Epistemic Logic. Berlin: Springer, 2007, 337
13	Benthem J, van Eijck J, van B Kooi . Logics of communication and change. Information and Computation, 2006, 204( 11): 1620–1662
14	T, Ågotnes P, Balbiani Ditmarsch H, van P Seban . Group announcement logic. Journal of Applied Logic, 2010, 8( 1): 62–81
15	T, French J, Hales E Tay . A composable language for action models. In: Goré R, Kooi B, Kurucz A, eds. Advances in Modal Logic, Volume 10. CSLI Publications, 2014, 197−216
16	J Hales . Arbitrary action model logic and action model synthesis. In: Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science. 2013, 253−262
17	B, Renne J, Sack A Yap . Logics of temporal-epistemic actions. Synthese, 2016, 193( 3): 813–849
18	T, Engesser R, Mattmüller B, Nebel M Thielscher . Game description language and dynamic epistemic logic compared. Artificial Intelligence, 2021, 292: 103433
19	Ditmarsch H van . The logic of knowledge games: showing a card. In: Proceedings of the BNAIC 99. 1999, 35−42
20	Ditmarsch H P, van der Hoek W, van B P Kooi . Dynamic epistemic logic with assignment. In: Proceedings of the 4th International Joint Conference on Autonomous Agents and Multiagent Systems. 2005, 141−148
21	M F, Benevides I M S Lima . Dynamic Epistemic Logic with Assignments, Concurrency and Communication Actions. Porto Alegre: Sociedade Brasileira de Computação, 2020
22	Ditmarsch H, van T French . Simulation and information: quantifying over epistemic events. In: Proceedings of the 1st International Workshop on Knowledge Representation for Agents and Multi-Agent Systems. 2008, 51−65
23	Ditmarsch H, van T, French S Pinchinat . Future event logic-axioms and complexity. In: Beklemishev L, Goranko V, Shehtman V, eds. Advances in Modal Logic, Volume 8. Moscow: College Publications, 2010, 77−99
24	P, Balbiani A, Baltag Ditmarsch H, van A, Herzig T, Hoshi Lima T de . ‘knowable’ as ‘known after an announcement’. The Review of Symbolic Logic, 2008, 1( 3): 305–334
25	Milner R, Parrow J, Walker D. A calculus of mobile processes, parts I and II. Technical Report ECS-LFCS-89-85 and -86. Scotland: University of Edinburgh, 1989
26	R, Milner J, Parrow D Walker . A calculus of mobile processes, parts I and II. Information and Computation, 1992, 100(1): 1−77
27	Sangiorgi D, Walker D. The π-Calculus: A Theory of Mobile Processes. New York: Cambridge University Press, 2001
28	Plotkin G D. A structural approach to operational semantics. Report DAIMI FN-19. Computer Science Department, Aarhus University, 1981, 17−139
29	Bozzelli L, van Ditmarsch H, French T, Hales J, Pinchinat S. Refinement modal logic. Information and Computation, 2014, 239: 303-339
30	Knight S. The epistemic view of concurrency theory. In: Logic in Computer Science. Palaiseau: Ecole Polytechnique, 2013 1991, 333−352
31	Saraswat V A, Rinard M, Panangaden P. Semantic foundations of concurrent constraint programming. In: Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 1991, 333-352
32	D, Dubois H Prade . Belief revision: belief change and possibility theory. In: Gärdenfors P, ed. Belief Revision. Cambridge: Cambridge University Press, 1992
33	Y, Jin M Thielscher . Iterated belief revision, revised. Artificial Intelligence, 2007, 171( 1): 1–18
34	P, Blackburn Rijke M, de Y Venema . Modal Logic. Cambridge: Cambridge University Press, 2002
35	H, Xing Z, Zhu J Zhang . A calculus for epistemic interactions. 2022, arXiv preprint arXiv: 2206.14506v1

[1]	Ying JIANG, Shichao LIU, Thomas EHRHARD. A fully abstract semantics for value-passing CCS for trees[J]. Front. Comput. Sci., 2019, 13(4): 828-849.
[2]	Yanwen CHEN,Yixiang CHEN,Eric MADELAINE. Timed-pNets: a communication behavioural semantic model for distributed systems[J]. Front. Comput. Sci., 2015, 9(1): 87-110.

Viewed

Full text

Abstract

Cited

Shared

Discussed