Constitutes the 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.

A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and Synthesis.- Verifying Space and Time Requirements for Resource-Bounded Agents.- Automated Creation of Pattern Database Search Heuristics.- Using Predicate Abstraction to Generate Heuristic Functions in UPPAAL.- Real-Time Model Checking on Secondary Storage.- Checking Liveness Properties of Concurrent Systems by Reinforcement Learning.- Bounded Model Checking Real-Time Multi-agent Systems with Clock Differences: Theory and Implementation.- Symbolic Model Checking of Logics with Actions.- A Framework for Model Checking Institutions.- SAT-Based Verification of Security Protocols Via Translation to Networks of Automata.- Distributed Extended Beam Search for Quantitative Model Checking.

GPSR Compliance The European Union's (EU) General Product Safety Regulation (GPSR) is a set of rules that requires consumer products to be safe and our obligations to ensure this. If you have any concerns about our products you can contact us on ProductSafety@springernature.com. In case Publisher is established outside the EU, the EU authorized representative is: Springer Nature Customer Service Center GmbH Europaplatz 3 69115 Heidelberg, Germany ProductSafety@springernature.com