Skip to main content

Research Repository

Advanced Search

Verifying time and communication costs of rule-based reasoners

Alechina, Natasha; Logan, Brian; Nga, Nguyen Hoang; Rakib, Abdur


Natasha Alechina

Brian Logan

Nguyen Hoang Nga

Profile Image

Rakib Abdur
Senior Lecturer in Mobile Security


Doron A. Peled

Michael J. Wooldridge


We present a framework for the automated verification of time and communication requirements in systems of distributed rule-based reasoning agents which allows us to determine how many rule-firing cycles are required to solve the problem, how many messages must be exchanged, and the trade-offs between the time and communication resources. We extend CTL* with belief and communication modalities to express bounds on the number of messages the agents can exchange. The resulting logic, , can be used to express both bounds on time and on communication. We provide an axiomatisation of the logic and prove that it is sound and complete. Using a synthetic but realistic example system of rule-based reasoning agents which allows the size of the problem and the distribution of knowledge among the reasoners to be varied, we show the Mocha model checker [1] can be used to encode and verify properties of systems of distributed rule-based agents. We describe the encoding and report results of model checking experiments which show that even simple systems have rich patterns of trade-offs between time and communication bounds. © 2009 Springer Berlin Heidelberg.


Alechina, N., Logan, B., Nga, N. H., & Rakib, A. (2009). Verifying time and communication costs of rule-based reasoners. Lecture Notes in Artificial Intelligence, 5348 LNAI, 1-14.

Journal Article Type Conference Paper
Publication Date Apr 6, 2009
Journal Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Print ISSN 0302-9743
Electronic ISSN 1611-3349
Publisher Springer Verlag
Peer Reviewed Peer Reviewed
Volume 5348 LNAI
Pages 1-14
Keywords rule-based reasoning, distributed reasoning, model checking
Public URL
Publisher URL
Related Public URLs