Model Checking and Artificial Intelligence: 4th Workshop, MoChArt IV, Riva del Garda, Italy, August 29, 2006, Revised Selected and Invited Papers (Lecture Notes in Computer Science, 4428)

The refereed post-proceedings of the 4th Workshop on Model Checking and Artificial Intelligence are presented in this volume. Eight full workshop papers are presented along with three post-proceedings papers. Papers are organized into topical sections covering planning and model checking, heuristics for real-time model checking, verification of multi-agent systems, and logics for model checking and artificial intelligence. Title Page Preface Organization Table of Contents A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and Synthesis Introduction Symbolic Model Checking SafetyAnalysis Diagnosis and Diagnosability Planning Conclusions and Future Work References Verifying Space and Time Requirements for Resource-Bounded Agents Introduction Memory Bounds Formal Model Definite Reasoners Rule-Based Reasoners More General Reasoners Classical Reasoners Verifying Reasoning Capabilities Experiments Related Work Conclusions and Future Work References Automated Creation of Pattern Database Search Heuristics Introduction Pattern Databases in Planning Admissible Heuristics in Planning Explicit-State Planning Pattern Databases Symbolic Planning Pattern Databases Automated Pattern Selection Experiments Explicit-State Pattern Databases Symbolic Pattern Databases Conclusion References Using Predicate Abstraction to Generate Heuristic Functions in UPPAAL Introduction Predicate Abstraction Technicalities Predicate Abstraction Heuristics Predicate Abstraction Pattern Databases Network Splitting Syntax-Based Abstractions Abstraction Refinement Conclusion References Real-Time Model Checking on Secondary Storage Introduction Timed Automata External Breadth First Search External Search in Real-Time Systems Linearly Priced Timed Automata External Breadth First Branch-and-Boundin Priced Real-Time Systems Iterative Broadening External Breadth First Branch-and-Bound Correctness Experiments Conclusion References Checking Liveness Properties of Concurrent Systems by Reinforcement Learning Introduction Research Background Testing of Liveness Properties in Temporal Formulas Reinforcement Learning and the Q-Learning Algorithm Control in Runtime Monitoring Problem: Finding a Counterexample of Response Property Applying Q-Learning Other LTL Formulas Implementation Experiments Discussion References Bounded Model Checking Real-Time Multi-agent Systems with Clock Differences: Theory and Implementation Introduction Diagonal Real-Time Interpreted Systems TECTLK Bounded Model Checking for TECTLK Translation from TECTLK to $ECTLK_y$ $ECTLK_y$ Bounded Model Checking Translation to Boolean Formulae A Real-Time Alternating Bit Transmission Problem Conclusions References Symbolic Model Checking of Logics with Actions Introduction Background State-Based Logics Action-Based Logics Mixing States and Actions Mixed Transition Systems Action-Restricted CTL Model Checking of ARCTL Fairness From Mixed to State-Based Logic Post-Projection of Mixed Models Post-Projection of Action-Based Logics Action-Based Model-Checking in SMV Overview of SMV Post-Projection to SMV Action Logics in SMV Using ARCTL for Knowledge Logics From CTLK to ARTCL Experimental Results Related Work Conclusions and Perspectives References A Framework for Model Checking Institutions Introduction Modelling Institutions Institutional Models and Computational Models Domain-Dependent Properties Domain-Independent Properties The Verification Framework Discussion and Conclusions References SAT-Based Verification of Security Protocols Via Translation to Networks of Automata Introduction Syntax of Security Protocols Computational Structure Attacks Upon Protocols Networks of Communicating Automata Automata for Modelling Executions of the Participants Automata for Modelling the Knowledge of the Participants Experimental Results Conclusions and Perspectives References Distributed Extended Beam Search for Quantitative Model Checking Introduction Preliminaries Modelling Scheduling Problems Using $\mu$CRL Beam Search Extended Detailed Beam Search Sequential Detailed Beam Search Distributed Detailed Beam Search Other Beam Search Variants Experimental Results The Zebra Finch Problem Results Related Work Conclusions References Author Index This book constitutes the thoroughly refereed post-proceedings of the 4th Workshop on Model Checking and Artificial Intelligence, MoChArt IV, held in Riva Del Garda, Italy in August 2006, as a satellite event of ECAI0 2006, the 17th biannual European conference on Artificial Intelligence. The 8 revised full workshop papers and 3 revised post-proceedings papers presented have gone through two rounds of reviewing and improvement and were carefully selected for inclusion in the book. The workshop covers all ideas, research, experiments and tools that relate to both MC and AI fields. The papers are organized in topical sections on planning and model checking, heuristics for real-time model checking, verification of multi-agent systems, as well as logics for model checking and artificial intelligence