BDI agents are among the most widely studied models of rational agents. In this architecture, systems are seen as rational agents with certain mental attitudes such as belief, desire, and intention. In this paper, we consider the model-checking problem for CTL_BDI, the branching-time logic CTL augmented with the BDI modalities, over finite-state structures, and in particular, a proof-ofconcept tool that is based on a translation to a formula in a fixed-point logic. We give a description of this tool in some details and also discuss some preliminary evaluations.
A Fixed-point Model-checker for BDI Logics over Finite-state Worlds
Salvatore La Torre;Gennaro Parlato
2020-01-01
Abstract
BDI agents are among the most widely studied models of rational agents. In this architecture, systems are seen as rational agents with certain mental attitudes such as belief, desire, and intention. In this paper, we consider the model-checking problem for CTL_BDI, the branching-time logic CTL augmented with the BDI modalities, over finite-state structures, and in particular, a proof-ofconcept tool that is based on a translation to a formula in a fixed-point logic. We give a description of this tool in some details and also discuss some preliminary evaluations.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.
