Verifying time and communication costs of rule-based reasoners

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

Abstract

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.

• Presentation Conference Type: Conference Paper (published)
• Publication Date: Apr 6, 2009
• Deposit Date: Jun 16, 2017
• Journal: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
• Print ISSN: 0302-9743
• Publisher: Springer Verlag
• Peer Reviewed: Peer Reviewed
• Volume: 5348 LNAI
• Pages: 1-14
• DOI: https://doi.org/10.1007/978-3-642-00431-5_1
• Keywords: rule-based reasoning, distributed reasoning, model checking
• Public URL: https://uwe-repository.worktribe.com/output/1010688
• Publisher URL: http://dx.doi.org/10.1007/978-3-642-00431-5_1
• Related Public URLs: https://link.springer.com/chapter/10.1007%2F978-3-642-00431-5_1
• Contract Date: Jun 16, 2017