IMI/Publicaţii/CSJM/Ediţii/CSJM v.32, n.1 (94), 2024/

Formal Analysis of Medical Systems using Multi-Agent Systems with Information Sharing

Authors: Bogdan Aman, Gabriel Ciobanu
Keywords: multi-agent systems, rewriting engine Maude, strategies and model-checking, example of airway laser surgery.


Improving safety is a main objective for medical systems. To assist the modelling and formal analysis of medical systems, we define a language for multi-agent systems handling information, timed communication, and timed migration. We use a simplified airway laser surgery scenario to demonstrate our approach. An implementation in Maude is presented; we use the strategies allowed by Maude to guide the rules application in order to decrease substantially the number of possible executions and results in the highly nondeterministic and concurrent multi-agent systems. Finally, we present how the executable specifications can be verified with the model-checking tools in Maude to detect the behavioural problems or desired properties of the~agents.

Bogdan Aman
Institute of Computer Science, Romanian Academy, Iasi Branch
Str. Teodor Codrescu 2, 700481, Iaşi, Romania

Gabriel Ciobanu
Academia Europaea,



Adobe PDF document0.33 Mb