Efficient decision procedure for Belief modality

This paper defines decision algorithm for subclass of BKD45DKDIKD logic which is based on known algorithm for temporal BKD45DKDIKD logic [2]. BDI logics are widely used in agent based systems. Such usage of BDI logic can be found in [1]. The original decision algorithm uses loop-check technique for...

Full description

Saved in:
Bibliographic Details
Main Author: Adomas Birštunas
Format: Article
Language:English
Published: Vilnius University Press 2005-12-01
Series:Lietuvos Matematikos Rinkinys
Subjects:
Online Access:https://www.journals.vu.lt/LMR/article/view/26673
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper defines decision algorithm for subclass of BKD45DKDIKD logic which is based on known algorithm for temporal BKD45DKDIKD logic [2]. BDI logics are widely used in agent based systems. Such usage of BDI logic can be found in [1]. The original decision algorithm uses loop-check technique for BEL and temporal operators. Applied loop-check technique is not optimized and therefore loop-check takes most of the time used in decision algorithm. Some examples of efficient loop-check applications for logic KT, S4 and some subclasses of intuitionistic logic can be found in [4]. Another efficient loop-check can be found in work [3]. We concentrate on our attitude on loop-check optimization for BEL operator. This paper defines decision algorithm modification, which uses efficient loop-check for BEL operator, but do not effect performance of other parts of algorithm. We define optimization only for BEL operator and therefore we omit temporal operators in this paper.
ISSN:0132-2818
2335-898X