Un comportement distribué peut être décrit avec un multi-ensemble partiellement ordonné (pomset). Bien que compacts et très intuitifs, ces modèles sont difficiles à vérifier. La principale technique utilisée dans cette thèse est de ramener les problèmes de décision de la logique MSO sur les pomsets à des problèmes de décision sur les mots. Les problèmes considérés sont la satisfiabilité et la vérification. Le problème de la vérification pour une formule donnée et un pomset consiste à décider si une interprétation est vraie, et le problème de satisfiabilité consiste à décider si un pomset répondant à la formule existe. Le problème de satisfiabilité de MSO sur pomsets est indécidable. Une procédure de semi-décision peut apporter des solutions pour de nombreux cas, en dépit du fait qu'elle peut ne pas terminer. Nous proposons un nouveau modèle, que l'on appelle ⌈-Pomset, pouvant rendre l'exploration des pomsets possible. Par conséquent, si une formule est satisfiable alors notre approche mènera éventuellement à la détection d'une solution. De plus, en utilisant les ⌈-Pomsets comme modèles pour systèmes concurrents, le model-checking de formules ordre partiel sur systèmes concurrents est décidable. Certaines expérimentations ont été faites en utilisant l'outil MONA. Nous avons comparé aussi la puissance expressive de certains modèles classiques de la concurrence comme les traces de Mazurkiewicz avec les ⌈-Pomsets. / Multiset of partially ordered events (pomset) can describe distributed behavior. Although very intuitive and compact, these models are difficult to verify. The main technique used in this thesis is to bring back decision problems for MSO over pomsets to problems for MSO over words. The problems considered are satisfiability and verification. The verification problem for a formula and a given pomset consists in deciding whether such an interpretation exists, and the satisfiability problem consists in deciding whether a pomset satisfying the formula exists. The satisfiability problem of MSO over pomsets is undecidable. A semi-decision procedures can provide solutions for many cases despite the fact that they may not terminate. We propose a new model, so called ⌈-Pomset, making the exploration of pomsets space possible. Consequently, if a formula is satisfiable then our approach will eventually lead to the detection of a solution. Moreover, using ⌈-Pomsets as models for concurrent systems, the model checking of partial order formulas on concurrent systems is decidable. Some experiments have been made using MONA. We compare also the expressive power of some classical model of concurrency such as Mazurkiewicz traces with our ⌈-Pomsets.
| Identifer | oai:union.ndltd.org:theses.fr/2014ORLE2068 |
| Date | 17 December 2014 |
| Creators | Sakho, Mouhamadou Tafsir |
| Contributors | Orléans, Université polytechnique de l'Ouest Africain (Dakar, Sénégal), Couvreur, Jean-Michel, Seydi, Hamet |
| Source Sets | Dépôt national des thèses électroniques françaises |
| Language | French |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation, Text |
Page generated in 0.0015 seconds