Specification and Verification of Multi-agent Systems

Foreword

Contents

List of Contributors

1 Using Theorem Proving to Verify Properties of Agent Programs

1.1 Introduction

1.2 An Agent Programming Language

1.2.1 SimpleAPL

1.2.2 SimpleAPL syntax

1.3 Operational Semantics

1.3.1 Non-interleaved execution

1.3.2 Interleaved execution

1.4 Logic

1.4.1 Preliminary

1.4.2 Language

1.4.3 Semantics

1.4.4 Axiomatisation

1.5 Verification

1.5.1 Expressing the non-interleaved strategy

1.5.2 Expressing the interleaved strategy

1.6 Example of using theorem proving to verify properties of an agent program

1.7 Related Work

1.8 Conclusion

1.9 Appendix: Encodings of properties in MSPASS

1.9.1 MSPASS encoding of the example

1.9.2 MSPASS encoding of a lemma for the proof of the blind commitment property of the vacuum cleaner agent

1.9.3 pdl-tableau encoding of the blind committment property

2 The Refinement of Multi-Agent Systems

2.1 Introduction

2.1.1 Related Works

2.2 From Specification to Implementation Agent Languages

2.2.1 Preliminaries

2.2.2 Formalising Mental States and Basic Actions

2.2.3 BUnity Agents

2.2.4 Why BUnity Agents Need Justice

2.2.5 BUpL Agents

2.2.6 Why BUpL Agents Need Compassion

2.2.7 Appraising Goals

2.3 The Refinement of Individual Agents

2.4 Towards Multi-Agent Systems

2.4.1 Action-based Choreographies

2.4.2 A Finer Notion of Refinement

2.5 Timing Extensions of MAS

2.5.1 Adding Time to BUnity

2.5.2 Adding Time to BUpL

2.5.3 A Short Note on Timed Refinement

2.6 Conclusion

3 Model Checking Agent Communication

3.1 Introduction

3.2 Brief Overview of Model Checking Multi-Agent Systems

3.2.1 Extending and Adapting Existing Model Checkers

3.2.2 Developing New Algorithms and Tools

3.3 Tableau-based Model Checking Dialogue Games

3.4 ACTL* Logic

3.4.1 Syntax

3.4.2 Semantics

3.4.3 Tableau Rules

3.5 Dialogue Game Protocols as Transition Systems

3.6 Verification of Dialogue Game Protocols

3.6.1 Alternating Büchi Tableau Automata (ABTA) for ACTL*

3.6.2 Translating ACTL* into ABTA (Step 1)

3.6.3 Run of an ABTA on a Transition System (Step 2)

3.6.4 Model Checking Algorithm (Step 3)

3.7 Case Studies

3.7.1 Verifying PNAWS

3.7.2 Verifying NetBill

3.8 Discussion and Future Work

4 Directions for Agent Model Checking

4.1 Introduction

4.1.1 Agents and Rational Agents

4.1.2 Logical Agent Descriptions

4.1.3 Formal Verification and Model Checking

4.1.4 Program Verification

4.1.5 Agent Programming Languages

4.2 Our Approach

4.2.1 AIL: Mapping Agent Languages to a Common Basis

4.2.2 AJPF: Specialising the AIL and JPF to work together

4.2.3 Current Status

4.3 Obstacles

4.3.1 Performance

4.3.2 Target Agent Languages

4.3.3 Using Agent Model Checking

4.3.4 Applicability

4.4 Directions

4.4.1 Applicability: Autonomous and Autonomic Systems

4.4.2 Efficiency: Potential for use of MJI

4.4.3 Efficiency: Potential for use of Program Slicing/Abstraction

4.4.4 Generality: Target Languages

4.4.5 Engineering: Agent Development Approach

4.4.6 Extension: Verification of Groups and Organisations

4.4.7 Applicability: Verifying Human-Agent Teamwork

4.4.8 Efficiency/Extension: Alternative Model Checkers

4.5 Concluding Remarks

5 Model Checking Logics of Strategic Ability: Complexity

5.1 Introduction

5.2 The Logics: Syntax and Semantics

5.2.1 Linear- and Branching-Time Logics

5.2.2 Strategic Abilities under Perfect Information

5.2.3 Strategic Abilities under Imperfect Information

5.2.4 Other Subsets of LATL*

5.2.5 Summary, Notation, and Related Work

5.3 Standard Model Checking Complexity Results

5.3.1 Model Checking Temporal Logics

5.3.2 Model Checking ATL and CL: Perfect Information

5.3.3 Model Checking ATL and CL: Imperfect Information

5.3.4 Model Checking ATL* and ATL+

5.4 Complexity for Implicit Models: States and Agents

5.4.1 Model Checking ATL and CL in Terms of States and Agents

5.4.2 CTL and CTL+ Revisited

5.4.3 ATL* and ATL+

5.5 Higher-Order Representations of Models

5.6 Summary

6 Correctness of Multi-Agent Programs: A Hybrid Approach

6.1 introduction

6.2 An agent-oriented Programming Language APL

6.2.1 Syntax of APL

6.2.2 Semantics of APL

6.3 CTLapl: A Specification Language for Agent Programs

6.3.1 CTLapl Syntax

6.3.2 CTLapl Semantics

6.4 Properties

6.4.1 Proving the Properties

6.5 Debugging Multi-Agent Programs

6.5.1 Debugging Modes

6.5.2 Specification Language for Debugging: Syntax

6.5.3 Specification Language for Debugging: Semantics

6.6 Multi-Agent Debugging Tools

6.6.1 Breakpoint

6.6.2 Watch

6.6.3 Logging

6.6.4 Message-list

6.6.5 Causal tree

6.6.6 Sequence diagram

6.6.7 Visualization

6.7 Conclusion and Future Work

7 The Norm Implementation Problem in Normative Multi-Agent Systems

7.1 Introduction

7.2 Normative multi-agent systems

7.2.1 Normative systems in computer science

7.2.2 Specification and verification of normative multi-agent systems

7.2.3 Assumptions of norm implementation

7.3 Formal framework and running example

7.3.1 Norms and logic

7.3.2 Norm implementation and games

7.3.3 Running example: ruling the Blocks World

7.3.4 Talking about norms and extensive games in the Blocks World

7.3.5 Two important caveats

7.4 Making violations impossible

7.4.1 Regimentation

7.4.2 Retarded preconditions

7.5 Perfect enforcement

7.6 Enforcers

7.6.1 Regimenting enforcement norms

7.6.2 Enforcing enforcement norms

7.6.3 Who controls the enforcers?

7.7 Implementation via norm change

7.8 Related work

7.9 Conclusions

8 A Verification Logic for Goal Agents

8.1 Introduction

8.2 Related work

8.3 The Agent Programming Language Goal

8.3.1 Goal Agent Programs

8.3.2 Knowledge Representation Language

8.3.3 Mental States

8.3.4 Actions and Action Selection

8.4 Verifying Goal Agent Programs

8.4.1 Verification Logic

8.4.2 Logical Characterization of Agent Programs

8.5 Conclusion

Appendix

9 Using the Maude Term Rewriting Language for Agent Development with Formal Foundations

9.1 Introduction

9.2 The BUpL Language

9.2.1 Syntax

9.2.2 Semantics

9.3 Prototyping

9.3.1 Introduction to Maude

9.3.2 Implementing BUpL: Syntax

9.3.3 Example BUpL Program

9.3.4 Implementing BUpL: Semantics

9.3.5 Executing an Agent Program

9.4 Model-Checking

9.4.1 Connecting BUpL Agents and Model-Checker

9.4.2 Examples

9.4.3 Fairness

9.5 Testing

9.5.1 Searching

9.5.2 Formalizing Test Cases

9.5.3 Introduction to Maude Strategies

9.5.4 Using Maude Strategies for Implementing Test Cases

9.6 Conclusion

10 The Cognitive Agents Specification Language and Verification Environment

10.1 Introduction

10.2 PVS

10.3 Action Theory

10.4 Knowledge

10.5 Goals

10.6 Agent Behaviour

10.7 A Meeting Scheduler Example

10.8 Verification

10.9 Example Proof

10.10 Conclusion

11 A Temporal Trace Language for Formal Modelling and Analysis of Agent Systems

11.1 Introduction

11.2 Syntax of TTL

11.3 Semantics of TTL

11.4 Multi-level Modelling of Multi-Agent Systems in TTL

11.4.1 Aggregation by agent clustering

11.4.2 Organisation structures

11.5 Relation to Other Languages

11.6 Normal Forms and Transformation Procedures

11.6.1 Past Implies Future Normal Form

11.6.2 Executable Normal Form

11.6.3 Abstraction of executable specifications

11.7 Verification of Specifications of Multi-Agent Systems in TTL

11.7.1 Verification of interlevel relations in TTL specifications by model checking

11.7.2 Verification of Traces in TTL

11.8 Conclusions

12 Assurance of Agent Systems: What Role Should Formal Verification Play?

12.1 Introduction

12.2 Existing Work

12.3 Case Study: A Waste Disposal Robot

12.4 Correctness Proof

12.5 Issues

12.5.1 Problems with Specifications

12.5.2 Problems with Proofs

12.6 Assumptions in the Waste Disposal Robot Case Study Revisited

12.7 A New Approach to Assurance of Agent Systems

12.7.1 An Engineering Approach to Risk Management

12.7.2 ``Send considered harmful?''

12.8 Combining Testing and Proving

12.8.1 Applying the Proposed Approach to the Case Study

12.8.2 Addressing Efficiency

12.9 Conclusions

References