El. knyga: Model Checking and Artificial Intelligence: 5th International Workshop, MoChArt 2008, Patras, Greece, July 21, 2008, Revised Selected and Invited Papers

Model checking is a branch of software and hardware veri cation that involves developingalgorithmsfortheautomaticveri cationofsystems.Originatingfrom mathematical logic, “model checking” stands for the process of determining whether or not a formula of some logic is satis ed by a model for the logic. Initiated two and a half decades ago, with papers that have gained their authors the 2007 Turing award, this active research area has resulted in rich theory, and the developmentof a number ofwidely used model-checkingtools.Theseinclude Carnegie-Mellon’s SMV, Cadence-SMV, and Bell Laboratories’ SPIN. Some of the main activities in model checking involve development of expressive spec- cation formalisms, in particular, temporal logics, the modeling of systems, and ?nding e cient algorithms for automatically checking that a model of a system satis es its temporal speci cation. The success of model checking in the computer-aided veri cation com- nity has led to a growth of interest in the use of model checking in AI. One common interest between these two ?elds is veri cation of autonomous s- tems. Logics for autonomous systems can express properties that are not c- monly used for reactive systems, expressing properties related to the knowledge and belief of components (agents) of the system about other components. New model-checkingalgorithms,for suchspeci cation properties,are challengingand useful for various applications, including online auction mechanisms, which are embedded in various Internet services, and autonomous robots.