Plusieurs connexions ont été trouvées entre les différents types d'automates et les logiques dans la littérature. D'abord, Buchi a montré que les automates de Kleene et la logique MSO interprétée sur les mots finis ont la même expressivité. Ceci implique la décidabilité de la logique MSO quand elle est interprétée sur les mots finis. Cette même logique a été prouvée décidable lorsqu'elle est interprétée sur des mots de longueurs dénombrables (Rabin).
Les automates de Kleene peuvent servir comme modèles pour les programmes séquentiels. En effet, on peut voir chaque lettre de l'alphabet de l'automate comme une instruction et donc assimiler mot et exécution de programme séquentiel. Cette assimilation ainsi que le théorème de Buchi sont utilisés notamment pour la vérification de programmes. Il existe plusieurs types d'automates modélisant les programmes concurrents. Parmi eux, on s'intéresse aux automates branchants proposés par K. Lodaya et P. Weil. C'est une généralisation des automates de Kleene avec deux nouveaux types de transitions : Fork et Join, permettant de modéliser le parallélisme. Les automates branchants ne reconnaissent plus que des mots, mais plutôt des ensembles partiellement ordonnés (posets) de lettres qui sont équivalents aux posets finis sans N.
Dans ce travail, on s'intéresse aux automates branchants introduits par N. Bedon et C. Rispal qui sont une généralisation des automates branchants de Lodaya et Weil et des automates d'ordres linéaires de Bruyère et Carton. Ces automates reconnaissent les langages de posets sans N dont les chaînes sont des ordres linéaires dénombrables et dispersés et les antichaines sont finies. On montre l'équivalence d'expressivité entre ces automates et une extension de MSO par la logique de Presburger nommée P-MSO. Les construction d'un formalisme à l'autre étant effective, on en déduit la décidabilité de P-MSO.