Expressivité des logiques d'espace
Institution:
École normale supérieure (Lyon ; 1987-2009)Disciplines:
Directors:
Abstract EN:
Spatial logics are a new formalism for specifying properties of concurrent systems in the line of modal logics (Hennessy - Milner). They may be seen also as an extension of classical logic better suited for giving an axiomatic semantics for imperative programs manipulating pointers in the line of Hoare-Floyd logic. This thesis present these several issues and compare the different approaches from the point of view of expressiveness. Several encoding, minimal fragments, and decidability results are presented.
Abstract FR:
Les logiques spatiales sont une nouvelle classe de formalismes dedies a la specification des systemes distribues dans la lignee des logiques modales (Hennessy-Milner). Elles peuvent aussi etre vues comme une extension de la logique classique mieux adaptee a la semantique axiomatique des langages imperatifs manipulant des pointeurs, dans la lignee de la logique de Hoare-Floyd. Cette these presente ces diverses logiques en les comparant du point de vue de leur expressivite. On etablit ainsi des encodages des logiques, des fragments minimaux, des unifications de logiques, et des resultats de decidabilite.