CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

MCK: Model Checking the Logic of Knowledge

Peter Gammie (Institutionen för datavetenskap) ; Ron van der Meyden
Lecture Notes in Computer Science (0302-9743). Vol. 3114 (2004), p. 479-483.
[Artikel, refereegranskad vetenskaplig]

The specification formalism employed in model checking is usually some flavour of temporal or process algebraic language that expresses properties of the behavioural aspects of a system. Knowledge [5] is a modality that is orthogonal to the behavioural dimension, capturing properties of information flow. Logics of knowledge have been shown to be a useful framework for the analysis of distributed algorithms and security protocols, and model checking of these logics was first mooted by Halpern and Vardi [6]. Since that time theoretical aspects of model checking the logic of knowledge and its combinations with temporal logic have been studied [8–10]. The system MCK introduced in this paper implements parts of this theory.

Nyckelord: Logic of Knowledge, Model Checking

Proceedings paper in: 16th International Conference on Computer Aided Verification (CAV 2004), Boston, MA. JUL 13-17, 2004

Denna post skapades 2006-08-25. Senast ändrad 2013-06-19.
CPL Pubid: 2107


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för datavetenskap (2002-2004)


Information Technology

Chalmers infrastruktur