P. Gastin, Dan Teodosiu Resource Traces: A Domain for Processes Sharing Exclusive Resources La théorie des mots finis et infinis avec terminaison explicite est usuellement utilisée pour donner des sémantiques dénotationnelles à des algèbres de processus séquentiels. Dans cet article, on généralise cette théorie au cas de processus concurrents qui se synchronisent sur un ensemble fixe de ressources partagées. On part d'un alphabet d'actions, d'un ensemble de ressources et d'une application qui fait correspondre à chaque action le sous- ensemble non-vide des ressources qu'elle utilise. Deux actions sont déclarées indépendantes si elles ne partageny aucune ressource. La description d'un processus (trace à ressource) comprend deux parties: une trace de Mazurkiewicz pour décrire ce qui a déjà été observé et l'ensemble des resources réservées par le processus pour terminer son exécution. On peut alors définir une con­ caténation ``concurrente'' des processus de telle sorte que des actions du deuxième processus puissent être exécutée avant la fin du premier processus si ces actions n'utilisent pas les ressources reservées par le premier processus pour terminer son exécution. On définit ensuite un ordre d'approximation entre les processus et on ob­ tient un domaine de Scott cohéremment complet et premier algébrique. De plus, on définit une distance ultramétrique na­ turelle. La topologie induite par cette distance coïncide avec la topologie de Lawson associée à l'ordre d'approximation. Le do­ maine des traces à ressources est ainsi compact et la con­ caténation est en fait uniformément continue. L'un des principaux avantages de ce modèle est que la concaténation est continue par rapport à l'ordre d'approximation. Ceci en fait un bon candidat pour donner des sémantiques dénotationnelles, particulièrement lorsqu'on considère une spécification modulaire d'un ensemble de processus partageant des ressources exclusives. A titre d'exemple, les machines de type PRAM basées sur des registres partagés aussi bien que les algèbres de processus comme CSP où les synchronisations se font au travers de canaux devraient bénéficier de cette nouvelle approche. The theory of finite and infinite words with explicit termina­ tion is commonly used to give denotational semantics for algebras of sequential processes. In this paper we generalize this theory to the case of partially terminated concurrent processes synchro­ nizing on a fixed set of shared exclusive resources. We start with an alphabet of actions, a set of resources, and a resource map assigning to each action the non-empty subset of resources it uses. Actions that do not share common resources are declared independent. The specification we use for partially terminated processes (resource traces) is similar to failure se­ mantics. It consists of two components: an already observed part represented as an action-labeled event structure (Mazurkiewicz trace), and a guard set containing the resources granted to the process for its further development. A process concatenation is then defined such that independent actions can be dispatched con­ currently. Specification refinement leads to the definition of a natural approximation ordering between processes which generates a coherently complete prime algebraic Scott domain, where process concatenation is continuous in both arguments. Furthermore, we define a natural ultrametric on processes based on prefix infor­ mation. The induced topology is shown to be equivalent to the compact Lawson topology generated by the approximation ordering. Moreover, process concatenation is shown to be uniformly continu­ ous with respect to the defined ultrametric. We develop a mathe­ matical theory which perfectly extends the central properties of the domain of finite and infinte words with explicit termination and the domain of finite and infinite Mazurkiewicz traces. Its natural semantics is well suited to the design of modular denota­ tional semantics for algebras of processes sharing exclusive re­ sources such as programs using some set of shared registers (PRAM) or concurrent sequential processes synchronizing over exclusive communication channels (CSP). The theory of finite and infinite words with explicit termina­ tion is commonly used to give denotational semantics for algebras of sequential processes. In this paper we generalize this theory to the case of partially terminated concurrent processes synchro­ nizing on a fixed set of shared exclusive resources. We start with an alphabet of actions, a set of resources, and a resource map assigning to each action the non-empty subset of resources it uses. Actions that do not share common resources are declared independent. The specification we use for partially terminated processes (resource traces) is similar to failure se­ mantics. It consists of two components: an already observed part represented as an action-labeled event structure (Mazurkiewicz trace), and a guard set containing the resources granted to the process for its further development. A process concatenation is then defined such that independent actions can be dispatched con­ currently. Specification refinement leads to the definition of a natural approximation ordering between processes which generates a coherently complete prime algebraic Scott domain, where process concatenation is continuous in both arguments. Furthermore, we define a natural ultrametric on processes based on prefix infor­ mation. The induced topology is shown to be equivalent to the compact Lawson topology generated by the approximation ordering. Moreover, process concatenation is shown to be uniformly continu­ ous with respect to the defined ultrametric. We develop a mathematical theory which perfectly extends the central properties of the domain of finite and infinte words with explicit termination and the domain of finite and infinite Mazurkiewicz traces. Its natural semantics is well suited to the design of modular denotational semantics for algebras of process­ es sharing exclusive resources such as programs using some set of shared registers (PRAM) or concurrent sequential processes synchronizing over exclusive communication channels (CSP).