Specification and Verification of Multi-agent Systems (eBook)

Mehdi Dastani, Koen V. Hindriks, John-Jules Meyer (Herausgeber)

eBook Download: PDF

2010
405 Seiten
Springer US (Verlag)
978-1-4419-6984-2 (ISBN)

Infos

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.

Inhalt

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

Produkt-Details

• Erscheint lt. Verlag: 20.7.2010
• Zusatzinfo: XVII, 405 p.
• Verlagsort: New York
• Sprache: englisch
• Themenwelt: Mathematik / Informatik ► Informatik ► Software Entwicklung
• Themenwelt: Informatik ► Theorie / Studium ► Künstliche Intelligenz / Robotik
• Themenwelt: Mathematik / Informatik ► Mathematik
• Themenwelt: Technik
• Schlagworte: Agents • Complexity • currentjm • logics • Model Checking • Modeling • multi-agent system • Multi-agent Systems • proving • specification and verification • theorem proving • verification
• ISBN-10: 1-4419-6984-5 / 1441969845
• ISBN-13: 978-1-4419-6984-2 / 9781441969842