Nous rappelons d’abord le concept d’algèbre de Kleene avec domaine (AKD). Puis,
nous expliquons comment utiliser les opérateurs des AKD pour définir un ordre partiel
appelé raffinement démoniaque ainsi que d’autres opérateurs démoniaques (plusieurs de
ces définitions proviennent de la littérature). Nous cherchons à comprendre comment se
comportent les AKD munies des opérateurs démoniaques quand on exclut les opérateurs
angéliques usuels. C’est ainsi que les propriétés de ces opérateurs démoniaques nous
servent de base pour axiomatiser une algèbre que nous appelons Algèbre démoniaque
avec domaine et opérateur t-conditionnel (ADD-[opérateur t-conditionnel]). Les lois des ADD-[opérateur t-conditionnel] qui ne concernent
pas l’opérateur de domaine correspondent à celles présentées dans l’article Laws
of programming par Hoare et al. publié dans la revue Communications of the ACM en
1987.
Ensuite, nous étudions les liens entre les ADD-[opérateur t-conditionnel] et les AKD munies des opérateurs
démoniaques. La question est de savoir si ces structures sont isomorphes. Nous
démontrons que ce n’est pas le cas en général et nous caractérisons celles qui le sont.
En effet, nous montrons qu’une AKD peut être transformée en une ADD-[opérateur t-conditionnel] qui peut
être transformée à son tour en l’AKD de départ. Puis, nous présentons les conditions
nécessaires et suffisantes pour qu’une ADD-[opérateur t-conditionnel] puisse être transformée en une AKD qui
peut être transformée à nouveau en l’ADD-[opérateur t-conditionnel] de départ.
Les conditions nécessaires et suffisantes mentionnées précédemment font intervenir
un nouveau concept, celui de décomposition. Dans un contexte démoniaque, il est
difficile de distinguer des transitions qui, à partir d’un même état, mènent à des
états différents. Le concept de décomposition permet d’y arriver simplement. Nous
présentons sa définition ainsi que plusieurs de ses propriétés. / We first recall the concept of Kleene algebra with domain (KAD). Then we explain
how to use the operators of KAD to define a demonic refinement ordering and demonic
operators (many of these definitions come from the literature). We want to know how
do KADs with the demonic operators but without the usual angelic ones behave. Then,
taking the properties of the KAD-based demonic operators as a guideline, we axiomatise
an algebra that we call Demonic algebra with domain and t-conditional (DAD-[opérateur t-conditionnel]). The
laws of DAD-[opérateur t-conditionnel] not concerning the domain operator agree with those given in the 1987
Communications of the ACM paper Laws of programming by Hoare et al.
Then, we investigate the relationship between DAD-[opérateur t-conditionnel] and KAD-based demonic
algebras. The question is whether every DAD-[opérateur t-conditionnel] is isomorphic to a KAD-based demonic
algebra. We show that it is not the case in general. However, we characterise those
that are. Indeed, we demonstrate that a KAD can be transformed into a DAD-[opérateur t-conditionnel]
which can be transformed back into the initial KAD. We also establish necessary and
sufficient conditions for which a DAD-[opérateur t-conditionnel] can be transformed into a KAD which can be
transformed back into the initial DAD-[opérateur t-conditionnel].
Finally, we define the concept of decomposition. This notion is involved in the
necessary and sufficient conditions previously mentioned. In a demonic context, it is
difficult to distinguish between transitions that, from a given state, go to different
states. The concept of decomposition enables to do it easily. We present its definition
together with some of its properties.
| Identifer | oai:union.ndltd.org:LACETR/oai:collectionscanada.gc.ca:QQLA.2009/25981 |
| Date | 01 1900 |
| Creators | De Carufel, Jean-Lou |
| Contributors | Desharnais, Jules |
| Publisher | Université Laval |
| Source Sets | Library and Archives Canada ETDs Repository / Centre d'archives des thèses électroniques de Bibliothèque et Archives Canada |
| Language | English |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation |
| Format | text/html, application/pdf |
| Rights | © Jean-Lou De Carufel, 2009 |
Page generated in 0.0224 seconds