Adresse mail : dima
at univ-paris12 dot fr La logique temporelle de la connaissance (voir le cours ici) permet, entre autres, d'exprimer des propriétés de fuite d'information, d'authentification ou d'anonymat. Il existe un certain nombre d'outils de model-checking, mais ils sont développés sur la base d'un codage particulier des opérateurs de connaissance, ou sur la base d'une sémantique restreinte.
Le travail demandé serait d'implémenter un tel outil de model-checking, et de le comparer avec des outils tels que LYS, MCMAS, MCK. Le point de départ est les articles [1] et [3] ci-dessous.
Possibilité de rémunération du stage sur projet ANR SPREADS.
Références :
[1] C.
Dima : Revisiting satisfiability and model-checking for CTLK with
synchrony and perfect recall, Proceedings of CLIMA 2008, disponible
sur la page web personnelle.
[2]
R. Fagin, J. Halpern, Y. Moses, M. Vardi : Reasoning
about knowledge, MIT Press (disponible à la bibliothèque
du LACL).
[3] Model
Checking Knowledge and Time in Systems with Perfect Recall, R.
van der Meyden and N. Shilov, Proc. Conf. on Foundations of Software
Technology and Theoretical Computer Science, Madras, Dec 1999.
Springer LNCS No. 1738, pp. 432-445.