Model Checking and Artificial Intelligence

Name: Model Checking and Artificial Intelligence | 6th International Workshop, MoChArt 2010, Atlanta, GA, USA, July 11, 2010, Revised Selected and Invited Papers
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

6th International Workshop, MoChArt 2010, Atlanta, GA, USA, July 11, 2010, Revised Selected and Invited Papers

Ron van der Meyden Jan-Georg Smaus(Herausgeber*in)

Springer (Verlag)

Erschienen am 21. April 2011

XI, 131 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-20674-0 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

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

Systemvoraussetzungen

Als PDF speichern Als Link merken