Model Checking and Artificial Intelligence
6th International Workshop, MoChArt 2010, Atlanta, GA, USA, July 11, 2010, Revised Selected and Invited Papers
Published on 21. April 2011
XI, 131 pages
978-3-642-20674-0 (ISBN)
Description
This book presents revised versions of selected papers from the 6th Workshop on Model Checking and Artificial Intelligence, MoChArt 2010, held in Atlanta, GA, USA in July 2010, as well as papers contributed subsequent to the workshop.
The 7 papers presented were carefully reviewed and selected for inclusion in this book. In addition, the book also contains an extended abstract of the invited talk held at the workshop.
The topics covered by these papers are general search algorithms, application of AI techniques to automated program verification, multiagent systems and epistemic logic, abstraction, epistemic model checking, and theory of model checking.
More details
Other editions
Additional editions
Ron van der Meyden | Jan-Georg Smaus
Model Checking and Artificial Intelligence
6th International Workshop, MoChArt 2010, Atlanta, GA, USA, July 11, 2010, Revised Selected and Invited Papers
Book
05/2011
1st Edition
Springer
€53.49
Shipment within 7-9 days
Content
- 6572
- Preface
- Organization
- Table of Contents
- Planning with Incomplete Information
- Introduction
- Classical Planning
- Incomplete Information
- Sensing and Finite-State Controllers
- Summary
- References
- External Memory Breadth-First Search with Delayed Duplicate Detection on the GPU
- Introduction
- External-Memory Breadth-First Search
- GPU Programming
- External Memory Breadth-First Search on the GPU
- Checking Enabledness on the GPU
- Generating the Successors on the GPU
- Delayed Duplicate Detection on the GPU
- Experiments
- Conclusion and Discussion
- References
- Program Model Checking via Action Planning
- Introduction
- Action Planning
- Program Model Checking
- Model Checking via Planning
- Parsing
- Generation of the Dependency Graph
- Translation into PDDL
- Fluents
- Propositions
- Expressions
- Assignments
- Program Counter
- Control Flow
- Conditional Branches
- Model Checking Statements
- Complex Statements
- Methods
- Data Abstraction
- Results
- Conclusion and Discussion
- References
- Automatic Data-Abstraction in Model Checking Multi-Agent Systems
- Introduction
- Interpreted Systems, ACTLK and Abstraction
- Implementation and Data Abstraction Theorem
- Experimental Results
- Conclusions
- References
- Automated Verification of Resource Requirements in Multi-Agent Systems Using Abstraction
- Introduction
- Communicating Reasoners
- Verification Framework
- Automated Verification Tool
- Maude Implementation
- Experimental Evaluation
- Scalability
- A More Complex Example
- Related Work
- Conclusion
- References
- The Blow-Up in Translating LTL to Deterministic Automata
- Introduction
- Preliminaries
- Linear Temporal Logic
- Automata over Infinite Words
- From LTL to DBW
- The Known Lower Bound: From O(n2) to 22n
- Improvement # 1: From O(n logn) to 22n with a Fixed Alphabet
- Improvement #2: from O(n) to 22n with a Linear Alphabet
- Discussion
- References
- Improved Bounded Model Checking for a Fair Branching-Time Temporal Epistemic Logic
- Introduction
- Preliminaries
- Model Checking Input Format
- Previous Bounded Model Checking Algorithms for ACTLKn
- Encoding of Penczeck et al
- Improved Encoding for ECTL by Zbrzezny
- Improved encoding for ACTLKn
- Motivation
- Encoding
- Experimental Results
- Related Work
- Conclusion and Future Work
- References
- Symbolic Model Checking the Knowledge in Herbivore Protocol
- Introduction
- A Brief Review of Knowledge and Time in Multi-agent Systems
- MCTK: A Symbolic Model Checker for Temporal Logic of Knowledge ECKLn
- The Herbivore Protocol
- The Environment in MCTK
- The Agent's Module in MCTK
- The Specifications in MCTK
- The Round Protocol in MCK
- Experimental Results
- Conclusions
- References
- Author Index
