@article { , title = {Model checking ontology-driven reasoning agents using strategy and abstraction}, abstract = {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.}, doi = {10.1002/cpe.5205}, eissn = {1532-0634}, issn = {1532-0626}, issue = {2}, journal = {Concurrency and Computation: Practice and Experience}, note = {Comments and Suggestions : 12 month embargo and "This is the peer reviewed version of the following article: [FULL CITE], which has been published in final form at [Link to final article using the DOI]. This article may be used for non-commercial purposes in accordance with Wiley Terms and Conditions for Self-Archiving.}, publicationstatus = {Published}, publisher = {Wiley}, url = {https://uwe-repository.worktribe.com/output/853824}, volume = {33}, keyword = {Computer Science Research Centre, semantic web, ontology, rule-based reasoning, multi-agent systems, Maude, rewriting logic, model checking}, year = {2021}, author = {Rakib, Abdur and Faruqui, Rokan Uddin} }