Abstract FR:

Le systeme mec manipule les systemes de transitions representant des processus. Il execute le produit de synchronisation de arnold-nivat afin de construire les modeles des systemes de processus communicants. Il calcule des ensembles d'etats et des ensembles de transitions dans un systeme de transitions ce qui permet de verifier les proprietes de ce systeme. Il est egalement possible de l'utiliser dans le calcul des operateurs definis par l'utilisateur comme les plus petites solutions de systemes d'equations. L'utilisation d'algorithmes efficaces rend praticable l'evaluation de toutes les fonctions sur des systemes de transitions de grande taille