Sequent calculi with an efficient loop-check for BDI logics ; Sekvenciniai skaičiavimai BDI logikoms su efektyvia ciklų paieška

VILNIUSUNIVERSITY
AdomasBirštunas
SEQUENTCALCULIWITHANEFFICIENTLOOP-CHECKFOR
BDILOGICS
Doctoraldissertation
Physicalsciences,Informatics(09P)
Vilnius,2010Thisworkwasperformedin2004-2009atVilniusUniversity,Lithuania.
Researchsupervisor :
Assoc. Prof. Habil. Dr. Regimantas Pliuškevičius (Institute of Mathematics and
Informatics,phisicalscience,mathematics-01P)VILNIAUSUNIVERSITETAS
AdomasBirštunas
SEKVENCINIAISKAIČIAVIMAIBDILOGIKOMSSUEFEKTYVIA
CIKLŲPAIEŠKA
Daktarodisertacija
Fiziniaimokslai,Informatika(09P)
Vilnius,2010Disertacijarengta2004-2009metaisVilniausuniversitete.
Mokslinisvadovas :
doc. habil. dr. Regimantas Pliuškevičius (Matematikos ir informatikos institutas,
fiziniaimokslai,matematika-01P)Abstract
BDI logics are widely used for agent system description and implementation. Agents
are autonomous systems, those acts in some environment and aspire to achieve preas-
signed goals. Decision making mechanism is the main and the most complicated part
of agent systems implementation. Different logics are used as a basis for the decision
making. OneofsuchalogicsisBDI logic,whichexpressagentviaitsbeliefs,desires
andintentions. Inthisthesis,thereareresearchedsequentcalculiforBDI logics.
KnownsequentcalculiforBDI logics,likesequentcalculiforothermodallogics,
use loop-check technique to get decidability. Inefficient loop-check takes a major part
oftheresourcesusedforthederivation. Forsomemodallogics,thereareknownloop-
checkfreesequentcalculiorcalculiwithanefficientloop-check.
In this thesis, there is presented loop-check free sequent calculus forKD45 logic,
which is the main fragment of the BDI logics. Introduced not only elimi-
nates loop-check, but also simplifies sequent derivation. For the branching time logic
(another BDI logic fragment) there is presented sequent calculus with an efficient
loop-check.
Obtained results are adapted for creation sequent calculi for monoagent and multi-
agentBDI logics. Introduced calculi use only restricted loop-check. Moreover, loop-
check is totally eliminated for some types of the loops. These results enables to create
moreefficientagentsystems,thosearebasedontheBDI logics.
12Acknowledgements
Iwouldliketotaketheopportunitytothankthepeoplewhohavesupportedme. Iowe
my deepest gratitude to my supervisor Assoc. Prof. Regimantas Pliuškevičius, for his
valuablesupportthroughthework.
It is an honor for me to thank Assoc. Prof. Stanislovas Leonas Norgėla, who was
mysupervisorofthepreviousworks. Iamindebtedtomymanyofmycolleaguesfrom
theUniversitytosupportandencouragemethroughallmystudies. Iamgratefultothe
staff of the Logical section of the Institute of Mathematics and Informatics, for their
adviseandinterestingdiscussions.
Itisapleasuretothankmyparentsandmysister,fortheirloveandsupport. Iwould
like to show my special gratitude to my wife Vilma and my daughter Miglė, for their
patienceandlove.
34Contents
Abstract 1
Acknowledgements 3
Contents 5
ListofFigures 7
Introduction 8
1 AgentsandBDI logic 13
1.1 Agents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
1.2 BDIAgents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
2 SequentCalculusandLoop-check 19
2.1 Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
2.2 SequentCalculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
2.3 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2.4 Loop-checkandBacktracking . . . . . . . . . . . . . . . . . . . . . . 30
3 Loop-checkFreeSequentCalculusforKD45Logic 34
3.1 CalculiforKD45Logic . . . . . . . . . . . . . . . . . . . . . . . . . 34
3.2 Loop-checkFreeSequentCalculusforKD45Logic . . . . . . . . . . 36
3.3 ComplexityResultsforSequentCalculusKD45 . . . . . . . . . . . 47lcf
4 SequentCalculusWithanEfficientLoop-checkforBranchingTimeLogic 54
4.1 TemporalLogics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
4.2 Sequent Calculus With an Efficient Loop-check for Branching Time
Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
4.3 ComplexityResultsforSequentCalculusPTL . . . . . . . . . . . 76rlc
5 SequentCalculiWithanEfficientLoop-checkforBDI Logics 82
5.1 CalculiforBDI Logic . . . . . . . . . . . . . . . . . . . . . . . . . 82
55.2 SequentCalculusWithanEfficientLoop-checkforBDI Logic . . . . 85
5.3 MultiagentBDILogic . . . . . . . . . . . . . . . . . . . . . . . . . . 92
5.4 Sequent Calculus With an Efficient Loop-check for Multiagent BDI
Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
n5.5 ComplexityResultsforSequentCalculusBDI . . . . . . . . . . . . 104elc
6 Conclusion 106
Bibliography 108
A DecisionAlgorithmforKD45Logic 113
6