We study the complexity of temporal logics over concurrent systems that can be described by Mazurkiewicz traces. We develop a general method to prove that the uniform satisfiability problem of local temporal logics is in PSPACE. We also demonstrate that this method applies to all known local temporal logics.

We review the characterization of communicating finite-state machines whose behaviors have universally or existentially bounded channels. These results rely on the theory of Mazurkiewicz traces. We investigate the question whether channel bound conditions are decidable for a given communicating finite-state machine.

Mazurkiewicz traces were introduced by A. Mazurkiewicz in 1977 as a language representation of partial orders to model "true concurrency". The theory of Mazurkiewicz traces has been utilised to tackle not only various aspects of concurrency theory but also problems from other areas, including combinatorics, graph theory, algebra, and logic. However, neither Mazurkiewicz traces nor partial orders can model the "not later than" relationship. In 1995, comtraces (combined traces) were introduced by Janicki and Koutny as a formal language counterpart to finite stratified order structures. They show that each comtrace uniquely determines a finite stratified order structure, yet their work contains very little theory of comtraces. This thesis aims at enriching the tools and techniques for studying the theory of comtraces. Our first contribution is to introduce the notions of absorbing monoids, generalised comtrace monoids, partially commutative absorbing monoids, and absorbing monoids with compound generators, all of which are the generalisations of Mazurkiewicz trace and comtrace monoids. We also define and study the canonical representations of these monoids. Our second contribution is to define the notions of non-serialisable steps and utilise them to study the construction which Janicki and Koutny use to build stratified order structures from comtraces. Moreover, we show that any finite stratified order structure can be represented by a comtrace. Our third contribution is to study the relationship between generalised comtraces and generalised stratified order structures. We prove that each generalised comtrace uniquely determines a finite generalised stratified order structure. / Thesis / Master of Computer Science (MCS)

Cette thèse se place dans le cadre de la vérification automatique des systèmes distribués. Elle aborde le problème de la spécification pour de tels systèmes, qui consiste à définir un formalisme logique pour décrire des propriétés des comportements de systèmes. On en attend qu'il soit facile d'exprimer les propriétés courantes (accessibilité, sûreté, exclusion mutuelle, vivacité, etc.). On souhaite par ailleurs que la vérification de ces propriétés soient aisée. Il s'agit donc de trouver un compromis entre pouvoir d'expression et simplicité d'utilisation.<br /><br />On s'intéresse ensuite à la modélisation des systèmes concurrents, en recherchant à nouveau un compromis entre réalisme des modèles et facilité de vérification. Les modèles étudiés dans ce travail sont les automates asynchrones, qui modélisent des processus concurrents communiquant par mémoire partagée.<br /><br />La thèse s'intéresse enfin au problème de la synthèse de contrôleur. Étant donné un système spécifié de façon incomplète, donc non-déterministe, en interaction avec un environnement, il s'agit de calculer de manière automatique comment restreindre son comportement afin qu'il vérifie une spécification donnée (quelles que soient les actions de l'environnement). Ce problème se formule en<br />termes de jeux. Dans le cas distribué, les jeux ont naturellement plusieurs joueurs. Dans ce cadre, la plupart des résultats sont négatifs : il est indécidable de savoir si on peut ou non contrôler un tel système. Cette thèse prouve que certaines propriétés de l'architecture de communication garantissent décidabilité pour toute spécification régulière.

When system runs are modeled with interval orders, interval order structures are useful tools to model abstract concurrent histories, i.e. sets of equivalent system runs. For the general cases, Mazurkiewicz traces allow a representation of the entire partial order by a single sequence with independency relations, and Comtraces allow a representation of stratified order structures by single step sequences with appropriate simultaneity and serializability relations. Unfortunately, both of them are unable to clearly describe the abstract interval order semantics of inhibitor nets. The goal of the thesis is to provide a monoid based model called Interval Traces that would allow a single sequence of beginnings and endings to represent the entire stratified order structures as well as all equivalent interval order observations. And the thesis will also show how interval order structures can be modelled by interval traces and how interval traces can be used to describe interval order semantics. / Thesis / Doctor of Philosophy (PhD)