Verification of Multi-agent Systems with Timeouts for Migration and Communication

被引：2
作者：
Aman, Bogdan [1 ,2 ]
Ciobanu, Gabriel [1 ,2 ]
机构：
[1] Alexandru Ioan Cuza Univ, Fac Comp Sci, Iasi, Romania
[2] Romanian Acad, Inst Comp Sci, Iasi, Romania
来源：
THEORETICAL ASPECTS OF COMPUTING - ICTAC 2019 | 2019年 / 11884卷
关键词：
ALGEBRA;
D O I：
10.1007/978-3-030-32505-3_9
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
A prototyping high-level language is used to describe multiagent systems using timeouts for migration between explicit locations and local communication in a distributed system. We translate such a high-level specification into the real-time Maude rewriting language. We prove that this translation is correct, and provide an operational correspondence between the evolutions of the mobile agents with timeouts and their rewriting translations. These results allow to analyze the multiagent systems with timeouts for migration and communication by using the real-time Maude tools. A running example is used to illustrate the whole approach.
引用
收藏
页码：134 / 151
页数：18
相关论文
共 17 条
[1]   A THEORY OF TIMED AUTOMATA [J].
ALUR, R ;
DILL, DL .
THEORETICAL COMPUTER SCIENCE, 1994, 126 (02) :183-235
[2]  
Aman B, 2013, LECT NOTES COMPUT SC, V8137, P31, DOI 10.1007/978-3-642-40561-7_3
[3]  
Behrmann G, 2004, LECT NOTES COMPUT SC, V3185, P200
[4]  
Ciobanu Gabriel, 2011, FM 2011: Formal Methods. Proceedings 17th International Symposium on Formal Methods, P293, DOI 10.1007/978-3-642-21437-0_23
[5]   Timers for Distributed Systems [J].
Ciobanu, Gabriel ;
Prisacariu, Cristian .
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 164 (03) :81-99
[6]   Automatic Analysis of TiMo Systems in PAT [J].
Ciobanu, Gabriel ;
Zheng, Manchun .
2013 18TH INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS), 2013, :121-124
[7]   Flexible software architecture and language for mobile agents [J].
Ciobanu, Gabriel ;
Juravle, Calin .
CONCURRENCY AND COMPUTATION-PRACTICE & EXPERIENCE, 2012, 24 (06) :559-571
[8]   Timed Mobility in process algebra and Petri nets [J].
Ciobanu, Gabriel ;
Koutny, Maciej .
JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2011, 80 (07) :377-391
[9]   ORDER-SORTED ALGEBRA .1. EQUATIONAL DEDUCTION FOR MULTIPLE INHERITANCE, OVERLOADING, EXCEPTIONS AND PARTIAL OPERATIONS [J].
GOGUEN, JA ;
MESEGUER, J .
THEORETICAL COMPUTER SCIENCE, 1992, 105 (02) :217-273
[10]  
Hessel Anders, 2008, Formal Methods and Testing. An Outcome of the FORTEST Network. Revised Selected Papers, P77, DOI 10.1007/978-3-540-78917-8_3
12