Logics with belief, desire and intention attitudes (BDI logics) are among the most widely studied formal languages for modelling rational agents. We consider the logic CTL∗bdi that augments the branching-time logic CTL∗ with the BDI modalities and adopt the possible-world semantics by Rao and Georgeff. In this paper, we introduce the model-checking problem of CTL∗bdi over finite-state models that are described by tuples of Kripke structures (one for each world) and where the BDI relations are captured by finite-state relations. We then solve the problem by giving an exponential time decision algorithm that is obtained by adapting the standard decision algorithm for CTL∗
Model checking BDI logics over finite-state worlds
Parlato G.
2020-01-01
Abstract
Logics with belief, desire and intention attitudes (BDI logics) are among the most widely studied formal languages for modelling rational agents. We consider the logic CTL∗bdi that augments the branching-time logic CTL∗ with the BDI modalities and adopt the possible-world semantics by Rao and Georgeff. In this paper, we introduce the model-checking problem of CTL∗bdi over finite-state models that are described by tuples of Kripke structures (one for each world) and where the BDI relations are captured by finite-state relations. We then solve the problem by giving an exponential time decision algorithm that is obtained by adapting the standard decision algorithm for CTL∗I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
