Skip to main content

Research Repository

Advanced Search

Model checking ontology-driven reasoning agents using strategy and abstraction

Rakib, Abdur; Faruqui, Rokan Uddin

Model checking ontology-driven reasoning agents using  strategy and abstraction Thumbnail


Profile Image

Rakib Abdur
Senior Lecturer in Mobile Security

Rokan Uddin Faruqui


We present a framework for the modelling, specification and verification of ontology-driven multi-agent rule-based systems (MASs). We assume that each agent executes in a separate process and that they communicate via message passing. The proposed approach makes use of abstract specifications to model the behaviour of some of the agents in the system, and exploits information about the reasoning strategy adopted by the agents. Abstract specifications are given as Linear Temporal Logic (LTL) formulas which describe the external behaviour of the agents, allowing their temporal behaviour to be compactly modelled. Both abstraction and strategy have been combined in an automated model checking encoding tool Tovrba for rule-based multi-agent systems which allows the system designer to specify information about agents' interaction, behaviour, and execution strategy at different levels of abstraction. The Tovrba tool generates an encoding of the system for the Maude LTL model checker, allowing properties of the system to be verified.


Rakib, A., & Faruqui, R. U. (2021). Model checking ontology-driven reasoning agents using strategy and abstraction. Concurrency and Computation: Practice and Experience, 33(2), Article e5205.

Journal Article Type Article
Acceptance Date Jan 16, 2019
Online Publication Date Apr 7, 2019
Publication Date Jan 25, 2021
Deposit Date Jan 25, 2019
Publicly Available Date Apr 8, 2020
Journal Concurrency and Computation: Practice and Experience
Print ISSN 1532-0626
Electronic ISSN 1532-0634
Publisher Wiley
Peer Reviewed Peer Reviewed
Volume 33
Issue 2
Article Number e5205
Keywords semantic web, ontology, rule-based reasoning, multi-agent systems, Maude, rewriting logic, model checking
Public URL
Publisher URL


You might also like

Downloadable Citations