bdi logics, i.e., logics with belief, desire and intention attitudes, are one of the most widely studied formal languages for modelling rational agents. In this paper, 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. We recall that in this semantics bdi relations vary over time according to a branching-time structure. We study the related model-checking question for finite-state structures, and in particular, we focus on models that are described as tuples of Kripke structures (one for each world) and where the bdi relations are captured by finite-state relations. Note that for formulas that do not contain bdi modalities this corresponds to standard Ctl∗ model-checking that is known to be Pspace-complete. We show that by adding the bdi modalities the computational complexity of model-checking remains Pspace-complete. The problem is still Pspace-hard even if we disallow the nesting of temporal operators in the path formulas, i.e., we restrict to the temporal modalities of Ctl. Finally, we give a fixed-point formulation of our algorithm for Ctlbdi that implements it on the top of existing symbolic fixed-point solvers.

On the model-checking of branching-time temporal logic with BDI modalities

Parlato G.
2020-01-01

Abstract

bdi logics, i.e., logics with belief, desire and intention attitudes, are one of the most widely studied formal languages for modelling rational agents. In this paper, 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. We recall that in this semantics bdi relations vary over time according to a branching-time structure. We study the related model-checking question for finite-state structures, and in particular, we focus on models that are described as tuples of Kripke structures (one for each world) and where the bdi relations are captured by finite-state relations. Note that for formulas that do not contain bdi modalities this corresponds to standard Ctl∗ model-checking that is known to be Pspace-complete. We show that by adding the bdi modalities the computational complexity of model-checking remains Pspace-complete. The problem is still Pspace-hard even if we disallow the nesting of temporal operators in the path formulas, i.e., we restrict to the temporal modalities of Ctl. Finally, we give a fixed-point formulation of our algorithm for Ctlbdi that implements it on the top of existing symbolic fixed-point solvers.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11695/96117
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? ND
social impact