Dastani / Hindriks / Meyer Specification and Verification of Multi-agent Systems

1. Auflage 2010
ISBN: 978-1-4419-6984-2
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, 405 Seiten

Specification and Verification of Multi-agent Systems presents a coherent treatment of the area of formal specification and verification of agent-based systems with a special focus on verification of multi-agent programs. This edited volume includes contributions from international leading researchers in the area, addressing logical formalisms and techniques, such as model checking, theorem proving, and axiomatisations for (semi) automatic verification of agent-based systems. Chapters include: • Using Theorem Proving to Verify Properties of Agent Programs • The Refinement of Multi-Agent Systems • Model Checking Agent Communication • Directions for Agent Model Checking • Model Checking Logics of Strategic Ability: Complexity • Correctness of Mult-Agent Programs: A Hybrid Approach • The Norm Implementation Problem in Normative Multi-Agent Systems • A Verification Logic for GOAL Agents • Using the Maude Term Rewriting Language for Agent Development with Formal Foundations • The Cognitive Agents Specification Language and Verification Environment • A Temporal Trace Language for Formal Modelling and Analysis of Agent Systemns • Assurance of Agent Systems: What Role Should Formal Verification Play? Specification and Verification of Multi-agent Systems is a comprehensive guide that makes a useful tool for researchers, practitioners and students, and serves as a reference work summarizing the state of the art in an accessible manner.

Autoren/Hrsg.

Dastani, Mehdi

Hindriks, Koen V.

Meyer, John-Jules

Inhaltsverzeichnis

1;Foreword;5
2;Contents;7
3;List of Contributors;15
4;1 Using Theorem Proving to Verify Properties of Agent Programs;18
4.1;1.1 Introduction;19
4.2;1.2 An Agent Programming Language;20
4.2.1;1.2.1 SimpleAPL;20
4.2.2;1.2.2 SimpleAPL syntax;23
4.3;1.3 Operational Semantics;23
4.3.1;1.3.1 Non-interleaved execution;25
4.3.2;1.3.2 Interleaved execution;26
4.4;1.4 Logic;28
4.4.1;1.4.1 Preliminary;28
4.4.2;1.4.2 Language;28
4.4.3;1.4.3 Semantics;29
4.4.4;1.4.4 Axiomatisation;30
4.5;1.5 Verification;33
4.5.1;1.5.1 Expressing the non-interleaved strategy;34
4.5.2;1.5.2 Expressing the interleaved strategy;36
4.6;1.6 Example of using theorem proving to verify properties of an agent program;41
4.7;1.7 Related Work;43
4.8;1.8 Conclusion;44
4.9;1.9 Appendix: Encodings of properties in MSPASS;45
4.9.1;1.9.1 MSPASS encoding of the example;45
4.9.2;1.9.2 MSPASS encoding of a lemma for the proof of the blind commitment property of the vacuum cleaner agent;47
4.9.3;1.9.3 pdl-tableau encoding of the blind committment property;49
5;2 The Refinement of Multi-Agent Systems;51
5.1;2.1 Introduction;52
5.1.1;2.1.1 Related Works;54
5.2;2.2 From Specification to Implementation Agent Languages;55
5.2.1;2.2.1 Preliminaries;55
5.2.2;2.2.2 Formalising Mental States and Basic Actions;55
5.2.3;2.2.3 BUnity Agents;57
5.2.4;2.2.4 Why BUnity Agents Need Justice;59
5.2.5;2.2.5 BUpL Agents;60
5.2.6;2.2.6 Why BUpL Agents Need Compassion;62
5.2.7;2.2.7 Appraising Goals;63
5.3;2.3 The Refinement of Individual Agents;64
5.4;2.4 Towards Multi-Agent Systems;68
5.4.1;2.4.1 Action-based Choreographies;69
5.4.2;2.4.2 A Finer Notion of Refinement;70
5.5;2.5 Timing Extensions of MAS;74
5.5.1;2.5.1 Adding Time to BUnity;75
5.5.2;2.5.2 Adding Time to BUpL;77
5.5.3;2.5.3 A Short Note on Timed Refinement;78
5.6;2.6 Conclusion;80
6;3 Model Checking Agent Communication;82
6.1;3.1 Introduction;83
6.2;3.2 Brief Overview of Model Checking Multi-Agent Systems;85
6.2.1;3.2.1 Extending and Adapting Existing Model Checkers;85
6.2.2;3.2.2 Developing New Algorithms and Tools;87
6.3;3.3 Tableau-based Model Checking Dialogue Games;89
6.4;3.4 ACTL* Logic;89
6.4.1;3.4.1 Syntax;89
6.4.2;3.4.2 Semantics;91
6.4.3;3.4.3 Tableau Rules;93
6.5;3.5 Dialogue Game Protocols as Transition Systems;95
6.6;3.6 Verification of Dialogue Game Protocols;97
6.6.1;3.6.1 Alternating Büchi Tableau Automata (ABTA) for ACTL*;97
6.6.2;3.6.2 Translating ACTL* into ABTA (Step 1);98
6.6.3;3.6.3 Run of an ABTA on a Transition System (Step 2);99
6.6.4;3.6.4 Model Checking Algorithm (Step 3);105
6.7;3.7 Case Studies;108
6.7.1;3.7.1 Verifying PNAWS;108
6.7.2;3.7.2 Verifying NetBill;114
6.8;3.8 Discussion and Future Work;116
7;4 Directions for Agent Model Checking;118
7.1;4.1 Introduction;119
7.1.1;4.1.1 Agents and Rational Agents;119
7.1.2;4.1.2 Logical Agent Descriptions;120
7.1.3;4.1.3 Formal Verification and Model Checking;121
7.1.4;4.1.4 Program Verification;123
7.1.5;4.1.5 Agent Programming Languages;123
7.2;4.2 Our Approach;124
7.2.1;4.2.1 AIL: Mapping Agent Languages to a Common Basis;126
7.2.2;4.2.2 AJPF: Specialising the AIL and JPF to work together;127
7.2.3;4.2.3 Current Status;129
7.3;4.3 Obstacles;129
7.3.1;4.3.1 Performance;129
7.3.2;4.3.2 Target Agent Languages;130
7.3.3;4.3.3 Using Agent Model Checking;131
7.3.4;4.3.4 Applicability;131
7.4;4.4 Directions;131
7.4.1;4.4.1 Applicability: Autonomous and Autonomic Systems;132
7.4.2;4.4.2 Efficiency: Potential for use of MJI;132
7.4.3;4.4.3 Efficiency: Potential for use of Program Slicing/Abstraction;133
7.4.4;4.4.4 Generality: Target Languages;134
7.4.5;4.4.5 Engineering: Agent Development Approach;134
7.4.6;4.4.6 Extension: Verification of Groups and Organisations;135
7.4.7;4.4.7 Applicability: Verifying Human-Agent Teamwork;136
7.4.8;4.4.8 Efficiency/Extension: Alternative Model Checkers;137
7.5;4.5 Concluding Remarks;137
8;5 Model Checking Logics of Strategic Ability: Complexity;139
8.1;5.1 Introduction;140
8.2;5.2 The Logics: Syntax and Semantics;141
8.2.1;5.2.1 Linear- and Branching-Time Logics;142
8.2.2;5.2.2 Strategic Abilities under Perfect Information;145
8.2.3;5.2.3 Strategic Abilities under Imperfect Information;149
8.2.4;5.2.4 Other Subsets of LATL*;152
8.2.5;5.2.5 Summary, Notation, and Related Work;153
8.3;5.3 Standard Model Checking Complexity Results;153
8.3.1;5.3.1 Model Checking Temporal Logics;154
8.3.2;5.3.2 Model Checking ATL and CL: Perfect Information;156
8.3.3;5.3.3 Model Checking ATL and CL: Imperfect Information;158
8.3.4;5.3.4 Model Checking ATL* and ATL+;160
8.4;5.4 Complexity for Implicit Models: States and Agents;163
8.4.1;5.4.1 Model Checking ATL and CL in Terms of States and Agents;165
8.4.2;5.4.2 CTL and CTL+ Revisited;167
8.4.3;5.4.3 ATL* and ATL+;168
8.5;5.5 Higher-Order Representations of Models;169
8.6;5.6 Summary;172
9;6 Correctness of Multi-Agent Programs: A Hybrid Approach;174
9.1;6.1 introduction;175
9.2;6.2 An agent-oriented Programming Language APL;177
9.2.1;6.2.1 Syntax of APL;178
9.2.2;6.2.2 Semantics of APL;179
9.3;6.3 CTLapl: A Specification Language for Agent Programs;183
9.3.1;6.3.1 CTLapl Syntax;184
9.3.2;6.3.2 CTLapl Semantics;185
9.4;6.4 Properties;188
9.4.1;6.4.1 Proving the Properties;188
9.5;6.5 Debugging Multi-Agent Programs;192
9.5.1;6.5.1 Debugging Modes;193
9.5.2;6.5.2 Specification Language for Debugging: Syntax;194
9.5.3;6.5.3 Specification Language for Debugging: Semantics;196
9.6;6.6 Multi-Agent Debugging Tools;197
9.6.1;6.6.1 Breakpoint;200
9.6.2;6.6.2 Watch;201
9.6.3;6.6.3 Logging;201
9.6.4;6.6.4 Message-list;202
9.6.5;6.6.5 Causal tree;203
9.6.6;6.6.6 Sequence diagram;203
9.6.7;6.6.7 Visualization;204
9.7;6.7 Conclusion and Future Work;205
10;7 The Norm Implementation Problem in Normative Multi-Agent Systems;208
10.1;7.1 Introduction;209
10.2;7.2 Normative multi-agent systems;212
10.2.1;7.2.1 Normative systems in computer science;212
10.2.2;7.2.2 Specification and verification of normative multi-agent systems;216
10.2.3;7.2.3 Assumptions of norm implementation;218
10.3;7.3 Formal framework and running example;219
10.3.1;7.3.1 Norms and logic;219
10.3.2;7.3.2 Norm implementation and games;220
10.3.3;7.3.3 Running example: ruling the Blocks World;221
10.3.4;7.3.4 Talking about norms and extensive games in the Blocks World;222
10.3.5;7.3.5 Two important caveats;224
10.4;7.4 Making violations impossible;225
10.4.1;7.4.1 Regimentation;225
10.4.2;7.4.2 Retarded preconditions;226
10.5;7.5 Perfect enforcement;229
10.6;7.6 Enforcers;230
10.6.1;7.6.1 Regimenting enforcement norms;232
10.6.2;7.6.2 Enforcing enforcement norms;233
10.6.3;7.6.3 Who controls the enforcers?;234
10.7;7.7 Implementation via norm change;234
10.8;7.8 Related work;235
10.9;7.9 Conclusions;237
11;8 A Verification Logic for Goal Agents;238
11.1;8.1 Introduction;239
11.2;8.2 Related work;240
11.3;8.3 The Agent Programming Language Goal;241
11.3.1;8.3.1 Goal Agent Programs;241
11.3.2;8.3.2 Knowledge Representation Language;242
11.3.3;8.3.3 Mental States;245
11.3.4;8.3.4 Actions and Action Selection;250
11.4;8.4 Verifying Goal Agent Programs;255
11.4.1;8.4.1 Verification Logic;255
11.4.2;8.4.2 Logical Characterization of Agent Programs;256
11.5;8.5 Conclusion;263
11.6;Appendix;265
12;9 Using the Maude Term Rewriting Language for Agent Development with Formal Foundations;268
12.1;9.1 Introduction;269
12.2;9.2 The BUpL Language;270
12.2.1;9.2.1 Syntax;270
12.2.2;9.2.2 Semantics;272
12.3;9.3 Prototyping;274
12.3.1;9.3.1 Introduction to Maude;274
12.3.2;9.3.2 Implementing BUpL: Syntax;276
12.3.3;9.3.3 Example BUpL Program;279
12.3.4;9.3.4 Implementing BUpL: Semantics;280
12.3.5;9.3.5 Executing an Agent Program;283
12.4;9.4 Model-Checking;284
12.4.1;9.4.1 Connecting BUpL Agents and Model-Checker;285
12.4.2;9.4.2 Examples;287
12.4.3;9.4.3 Fairness;290
12.5;9.5 Testing;291
12.5.1;9.5.1 Searching;292
12.5.2;9.5.2 Formalizing Test Cases;293
12.5.3;9.5.3 Introduction to Maude Strategies;295
12.5.4;9.5.4 Using Maude Strategies for Implementing Test Cases;297
12.6;9.6 Conclusion;299
13;10 The Cognitive Agents Specification Language and Verification Environment;301
13.1;10.1 Introduction;302
13.2;10.2 PVS;302
13.3;10.3 Action Theory;303
13.4;10.4 Knowledge;306
13.5;10.5 Goals;311
13.6;10.6 Agent Behaviour;317
13.7;10.7 A Meeting Scheduler Example;321
13.8;10.8 Verification;323
13.9;10.9 Example Proof;325
13.10;10.10 Conclusion;327
14;11 A Temporal Trace Language for Formal Modelling and Analysis of Agent Systems;328
14.1;11.1 Introduction;329
14.2;11.2 Syntax of TTL;331
14.3;11.3 Semantics of TTL;334
14.4;11.4 Multi-level Modelling of Multi-Agent Systems in TTL;336
14.4.1;11.4.1 Aggregation by agent clustering;336
14.4.2;11.4.2 Organisation structures;340
14.5;11.5 Relation to Other Languages;343
14.6;11.6 Normal Forms and Transformation Procedures;345
14.6.1;11.6.1 Past Implies Future Normal Form;346
14.6.2;11.6.2 Executable Normal Form;349
14.6.3;11.6.3 Abstraction of executable specifications;353
14.7;11.7 Verification of Specifications of Multi-Agent Systems in TTL;356
14.7.1;11.7.1 Verification of interlevel relations in TTL specifications by model checking;356
14.7.2;11.7.2 Verification of Traces in TTL;359
14.8;11.8 Conclusions;361
15;12 Assurance of Agent Systems: What Role Should Formal Verification Play?;364
15.1;12.1 Introduction;365
15.2;12.2 Existing Work;366
15.3;12.3 Case Study: A Waste Disposal Robot;368
15.4;12.4 Correctness Proof;371
15.5;12.5 Issues;372
15.5.1;12.5.1 Problems with Specifications;373
15.5.2;12.5.2 Problems with Proofs;375
15.6;12.6 Assumptions in the Waste Disposal Robot Case Study Revisited;377
15.7;12.7 A New Approach to Assurance of Agent Systems;380
15.7.1;12.7.1 An Engineering Approach to Risk Management;381
15.7.2;12.7.2 ``Send considered harmful?'' ;383
15.8;12.8 Combining Testing and Proving;384
15.8.1;12.8.1 Applying the Proposed Approach to the Case Study;387
15.8.2;12.8.2 Addressing Efficiency;389
15.9;12.9 Conclusions;392
16;References;395