Verifying time and communication costs of rule-based reasoners

N. Alechina, B. Logan, N.H. Nga, A. Rakib

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review

8 Citations (Scopus)


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, LCRB, 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.
Original languageEnglish
Title of host publicationModel Checking and Artificial Intelligence
EditorsDoron A. Peled, Michael J. Wooldridge
Number of pages14
ISBN (Electronic)978-3-642-00431-5
ISBN (Print)978-3-642-00430-8
Publication statusPublished - 2009
Externally publishedYes
EventModel Checking and Artificial Intelligence, 5th International Workshop, - Patras, Greece
Duration: 21 Jul 200821 Jul 2008

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceModel Checking and Artificial Intelligence, 5th International Workshop,
Abbreviated titleMoChArt 2008


  • Multiagent System
  • Communication Cost
  • Communication Modality
  • Computation Tree Logic
  • Verify Time


Dive into the research topics of 'Verifying time and communication costs of rule-based reasoners'. Together they form a unique fingerprint.

Cite this