Model Checking Knowledge and Time

摘要: Model checking as an approach to the automatic verification of finite state systems has focussed predominantly on system specifications expressed in temporal logic. In distributed community, logics knowledge (epistemic logics) have been advocated for expressing desirable properties protocols and systems. A range combining epistemic components developed this purpose. However, model problem received (comparatively) little attention. paper, we address ourselves problem. Following a brief survey relevant issues literature, introduce logic (Halpern Vardi's CKLn). We then develop CKLn that combines ideas from interpreted semantics with local propositions by Engelhardt et al. With our approach, provide means reduce linear checking. After introducing exploring underpinning present case study (the bit transmission problem) which spin was used establish implemented promela.