Automate à pile visible

Les mots imbriqués sont un modèle pour la représentation de données avec à la fois un ordre linéaire et un couplage hiérarchique des éléments[4]. Des exemples de données avec cette double structure hiérarchique et linéaire incluent les exécutions de programmes structurés, des données linguistiques annotées et des documents HTML ou XML. Un mot imbriqué se compose d'une séquence de positions linéairement ordonnées, augmentée d'arcs d'imbrication reliant des appels à des retours (ou des balises ouvrantes à des balises fermantes). Les arcs ne se croisent pas dans une structure hiérarchique correctement imbriquée, mais on autorise des arcs non couplés. Cette structure d'imbrication peut être représentée de manière unique par une séquence spécifiant les types de positions (appels, retours et internes). Les mots imbriqués généralisent à la fois les mots et les arbres ordonnés, et permettent les opérations sur les mots et sur les arbres.

Les automates de mots imbriqués sont des automates finis acceptant des mots imbriqués ; ils définissent la classe des langages rationnels (ou réguliers) des mots imbriqués.

Pour un langage L donné de mots imbriqués sur un alphabet, un codage linéaire des mots imbriqués donne un langage L' sur l'alphabet marqué composé de symboles marqués avec le type de la position. Si L est un langage rationnel de mots imbriqués, alors L' est un langage algébrique. En fait, il est accepté par un automate à pile particulier appelé automate à pile visible ; la classe des langages de mots qu'ils acceptent sont des langages à pile visible. Ce sont tous de langages algébriques déterministes particuliers qui se classent entre les langages équilibrés et les langages de Floyd, engendrés par des grammaires à précédence d'opérateurs.

Les langages rationnels de mots imbriqués s'emploient avantageusement dans la vérification algorithmique des programmes structurés, car au lieu de considérer un programme comme un langage algébrique de mots, le considérer comme un langage régulier de mots imbriqués (ou équivalent, comme un langage à pile visible), permet la vérification de nombreuses propriétés (telles que l'inspection de la pile, les pré et postconditions) qui ne sont pas exprimables dans les logiques de spécification existantes.

Les données qui possèdent un double structure, à la fois linéaire et hiérarchique, sont traditionnellement modélisées à l'aide d'arbres ordonnés, et elles sont interrogées à l'aide d'automates arborescents. Dans les arbres ordonnés, les nœuds de même parent sont ordonnés linéairement, et les parcours d'arbre classiques tels que le parcours infixe (ou le parcours en profondeur de gauche à droite) peuvent être utilisés pour définir un ordre implicite sur les nœuds.

Pour le traitement des documents, les mots imbriqués ont de nombreux avantages sur les arbres ordonnés. La représentation par arbre suppose implicitement que les données linéaires peuvent être analysés dans un arbre ; on ne peut donc pas traiter des données qui ne peuvent pas être représenter correctement. Des opérations sur les mots comme la prise des préfixes, des suffixes, et la concaténation, sont naturelles en traitement des documents et n'ont pas d'analogues dans les arbres. Pareillement, les automates d'arbre peuvent difficilement exprimer des contraintes qui font référence à l'ordre linéaire dans sa totalité. Par exemple, une requête demandant que des modèles apparaissent dans un ordre donné à l'intérieur d'un document se vérifie par un automate de mots ordinaires en temps linéaire, mais requiert un temps exponentiel dans un automate d'arbre ascendant. Cet exemple montre que certaines requêtes peuvent être codées de façon plus succincte dans un automate de mots imbriqués qui lit le mot de gauche à droite et traite les liens d'imbrication au fur et à mesure qu'ils apparaissent. Ceci correspond à des logiciels de fouille de flots de données, comme ils servent dans les logiciels pour XML.

Les automates à pile visible ont été introduits, avant Alur et Madhusudan, sous le nom de « input-driven pushdown automata » par Kurt Mehlhorn dans les années 1980[5] ; il a démontré qu’un langage défini par un tel automate peut être reconnu en temps polynomial, et avec un espace ${\displaystyle O(\log ^{2}n/\log \log n)}$. Cette borne a été améliorée par von Braunmühl et Verbeek[6] qui ont donné, pour la reconnaissance, une complexité ${\displaystyle O(\log n)}$ en espace et ${\displaystyle O(n^{2}\log n)}$ en temps. Ces auteurs ont fait une autre contribution importante en montrant que les variantes déterministe et non déterministe du modèle reconnaissent les mêmes langages. Ultérieurement, Dymond[7] a montré que cette famille de langages est contenue dans la classe de complexité NC¹.

Une relation de couplage (en anglais « matching relation ») de longueur ${\displaystyle \ell \geq 0}$, aussi appelé une correspondance, est une relation binaire, partie du produit ${\displaystyle \{-\infty ,1,2,\ldots ,\ell -1,\ell \}\times \{1,2,\ldots ,\ell -1,\ell ,\infty \}}$, notée traditionnellement ${\displaystyle \rightsquigarrow }$. Les couples de cette relation sont appelées flèches. La relation vérifie les conditions suivantes :

1. si ${\displaystyle i\rightsquigarrow j}$ alors ${\displaystyle i<j}$ : toutes les flèches sont vers la droite ;
2. si ${\displaystyle i_{1}\rightsquigarrow j}$ et ${\displaystyle i_{2}\rightsquigarrow j}$ et ${\displaystyle j<\infty }$, alors ${\displaystyle i_{1}=i_{2}}$ : deux flèches n'aboutissent pas à la même position ;
3. si ${\displaystyle i\rightsquigarrow j_{1}}$ et ${\displaystyle i\rightsquigarrow j_{2}}$ et ${\displaystyle i>-\infty }$, alors ${\displaystyle j_{1}=j_{2}}$ : deux flèches ne commencent pas à la même position ;
4. si ${\displaystyle i_{1}\rightsquigarrow j_{1}}$ et ${\displaystyle i_{2}\rightsquigarrow j_{2}}$, alors on n'a pas ${\displaystyle i_{1}<i_{2}<j_{1}<j_{2}}$ : deux flèches ne se croisent pas.

Enfin, le couple ${\displaystyle (-\infty ,\infty )}$ n'est pas une flèche. Si ${\displaystyle i\rightsquigarrow j}$, alors

• ${\displaystyle i}$ est une position d'appel (en anglais « call position ») et
• ${\displaystyle j}$ est une position de retour (en anglais « return position ») ;
• si ${\displaystyle i=-\infty }$, alors ${\displaystyle j}$ est un retour pendant,
• si ${\displaystyle j=\infty }$, alors ${\displaystyle i}$ est un appel pendant (en anglais « pending call »)
• une position qui est ni d'appel ni de retour est une position interne (en anglais « internal position ».

Un couple ${\displaystyle (i,j)}$ dont aucun des deux indices n'est pendant est bien parenthésé (en anglais « well matched »).

Un mot imbriqué de longueur ${\displaystyle \ell }$ sur un alphabet ${\displaystyle \Sigma }$ est une couple ${\displaystyle (w,\rightsquigarrow )}$, où ${\displaystyle w}$ est un mot de longueur ${\displaystyle \ell }$ sur ${\displaystyle \Sigma }$ , dans le sens usuel du terme, et où ${\displaystyle \rightsquigarrow }$ est une relation de couplage de longueur ${\displaystyle \ell }$.

1. La relation ${\displaystyle \rightsquigarrow =\{(-\infty ,1),(2,\infty ),(3,4),(5,7),(8,\infty )\}}$ définit les positions d'appel ${\displaystyle -\infty }$, 2,3,5, 8, et les positions de retour ${\displaystyle \infty }$, encore que les deux infinis peuvent ne pas être comptés dans les positions ; les positions 1, 2 et 8 sont pendantes, la position 6 est interne, les couples (3,4) et (5,7) sont bien parenthésés. Une façon de présenter la nature des positions est une suite de c (call), r (retour), et i (interne) selon le type rencontré ; ainsi, la relation ci-dessus se décrit par :

r c c r c i r c

2. La suite

r c r r c i c i

ne contient qu'un seul couple bien parenthésé, le couple (2,3) ; 1 et 4 sont de positions de retour pendantes, et 5 et 7 des positions d'appel pendantes.

3. Le mot

i c i c i i r r i

ne contient aucune position pendante.

La représentation des relations de couplage par des mots montre qu'il y a ${\displaystyle 3^{n}}$ relations de couplage de longueur ${\displaystyle n}$[8]

Les mots imbriqués sur un alphabet ${\displaystyle \Sigma }$ peuvent être codés comme mots ordinaires sur un alphabet augmenté, appelé alphabet structuré noté ${\displaystyle {\hat {\Sigma }}}$ ; chaque symbole ${\displaystyle a}$ de ${\displaystyle \Sigma }$ est présenté en trois exemplaires, le premier quand il figure, dans un mot imbriqué, en position d'appel, le deux quand il est en position de retour, le troisième enfin quand il figure en position interne. L'alphabet ${\displaystyle \Sigma }$ est composé de symboles ${\displaystyle \langle a}$ (pour ${\displaystyle a}$ en position d'appel), ${\displaystyle a\rangle }$ (pour a ${\displaystyle a}$ en position de retour) et de a lui-même quand il est en position interne. L'alphabet triple donc de taille. Cette écriture revient donc à superposer un mot ordinaire avec la séquence des i c r introduits plus haut.

Pour le mot

${\displaystyle w=abaabccca}$

et la relation de couplage

${\displaystyle \rightsquigarrow =\{(-\infty ,1),(2,\infty ),(3,4),(5,7),(8,\infty )\}}$

qui est aussi représentée par la séquence

r c c r c i r c i

le codage sur l'alphabet structuré est

${\displaystyle a\rangle \langle b\langle aa\rangle \langle bcc\rangle ca}$

Un automate de mots imbriqués a un nombre fini d'états, et opère presque comme un automate fini déterministe sur les mots usuels, où les lettres sont lues de gauche à droite et où l'état courant dépend de l'état précédent et de la lettre lue ; dans un automate de mots imbriqués, à la lecture d'une lettre d'un mot imbriqué ${\displaystyle (w,\rightsquigarrow )}$, le comportement varie en fonction de nature de la position de la lettre lue ; en plus des états ordinaires, l'automate possède des états hiérarchiques qui se propagent depuis une position d'appel et dont l'automate tient compte au moment de la position de retour correspondante. Un langage reconnu par un automate de mots imbriqués est un langage régulier ou rationnel de mots imbriqués.

De manière formelle, un automate de mots imbriqué comporte

• un ensemble fini ${\displaystyle Q}$ d'états dits linéaires
• un état initial (linéaire) ${\displaystyle q_{0}\in Q}$
• un ensemble d'états terminaux (linéaires) ${\displaystyle Q_{f}\subseteq Q}$
• un ensemble fini ${\displaystyle P}$ d'états dits hiérarchiques
• un état initial (hiérarchique) ${\displaystyle p_{0}\in P}$
• un ensemble d'états terminaux (hiérarchiques) ${\displaystyle P_{f}\subseteq P}$

et trois fonctions de transition, une pour chaque type de symbole

• une fonction de transitions d'appels ${\displaystyle \delta _{c}:Q\times \Sigma \to Q\times P}$
• une fonction de transitions internes ${\displaystyle \delta _{i}:Q\times \Sigma \to Q}$
• une fonction de transitions de retours ${\displaystyle \delta _{r}:Q\times P\times \Sigma \to Q}$

Un automate démarre dans l'état initial, et lit le mot imbriqué dans l'ordre linéaire des lettres. Quand il rencontre une lettre d'appel, l'automate propage un état hiérarchique le long de la flèche sortante. Cet état hiérarchique est récupéré lorsque l'automate lit la lettre de retour correspondante.

Formellement, un calcul (en anglais « run ») sur un mot imbriqué ${\displaystyle a_{1}a_{2}\cdots a_{n}}$ est une suite ${\displaystyle q_{0},q_{1},\ldots ,q_{n}}$ d'états linéaires et une suite d'états hiérarchiques ${\displaystyle p_{i}\in P}$, un pour chaque position d'appel et correspondants aux flèches du couplage, telles que

• si ${\displaystyle i}$ est une position d'appel, ${\displaystyle \delta _{c}(q_{i-1},a_{i})=(q_{i},p_{i})}$ ;
• si ${\displaystyle i}$ est une position interne, ${\displaystyle \delta _{i}(q_{i-1},a_{i})=q_{i}}$ ;
• si ${\displaystyle i}$ est une position de retour et ${\displaystyle j}$ est le prédécesseur d'appel de ${\displaystyle i}$, alors ${\displaystyle \delta _{r}(q_{i-1},p_{j},a_{i})=q_{i}}$, et si ${\displaystyle i}$ est un retour pendant, alors ${\displaystyle \delta _{r}(q_{i-1},p_{0},a_{i})=q_{i}}$.

L'automate accepte le mot imbriqué si le dernier état est un état final : ${\displaystyle q_{n}\in Q_{f}}$.

Les automates peuvent être aussi non déterministes, et avoir alors plusieurs états initiaux.

Un automate à pile visible déterministe est un automate à pile déterministe particulier, où l'alphabet des données est partitionné en trois parties, chacune déterminant la nature des opérations de pile.

Formellement[2], un automate à pile visible déterministe ${\displaystyle M=(Q,{\hat {\Sigma }},\Gamma ,\delta ,q_{0},F)}$ comporte :

• ${\displaystyle Q}$ un ensemble fini d'états ;
• ${\displaystyle q_{0}\in \,Q}$ est l’état initial, et
• ${\displaystyle F\subseteq Q}$ est l'ensemble des états d'acceptation ;
• ${\displaystyle {\hat {\Sigma }}}$ un alphabet structuré, partitionné en trois ensembles ${\displaystyle \Sigma _{c}}$, ${\displaystyle \Sigma _{r}}$, et ${\displaystyle \Sigma _{i}}$. L'alphabet ${\displaystyle \Sigma _{c}}$ contient les symboles d'appel, ${\displaystyle \Sigma _{r}}$ les symboles de retour, et enfin ${\displaystyle \Sigma _{i}}$ les symboles internes ;
• ${\displaystyle \Gamma }$ est un ensemble fini, l'alphabet de pile, avec un symbole particulier ${\displaystyle \bot \in \Gamma }$ de fond de pile ;
• ${\displaystyle \delta =\delta _{c}\cup \delta _{r}\cup \delta _{i}}$ est la fonction de transition, elle-même partitionnée en trois parties correspondant aux transitions d'appel, internes et de retour, à savoir :
  • ${\displaystyle \delta _{c}:Q\times \Sigma _{c}\to Q\times \Gamma \setminus \{\bot \}}$, la fonction de transition d'appel : le fond de pile ne peut être empilé à nouveau ;
  • ${\displaystyle \delta _{r}:Q\times \Sigma _{r}\times \Gamma \to Q}$, la fonction de transition de retour ;
  • ${\displaystyle \delta _{i}:Q\times \Sigma _{i}\to Q}$, la fonction de transition interne ;

La notion de calcul pour un automate à pile visible est une restriction et en même temps une variation de celle des automate à pile. La restriction porte sur le choix des opérations : quand un automate à pile visible lit une lettre ${\displaystyle a}$, il peut empiler un symbole seulement si c'est une lettre d'appel de ${\displaystyle \Sigma _{c}}$, dépiler seulement si c'est une lettre de ${\displaystyle \Sigma _{r}}$, enfin si ${\displaystyle a\in \Sigma _{i}}$ il ne peut pas modifier la pile. La modification porte sur la forme des opérations de pile : dans un automate à pile usuel, l'empilement éventuel est toujours précédé d'un dépilement, alors qu'ici, les deux opérations sont séparées. De plus, quand il y a empilement, on n'empile qu'un seul symbole sur la pile. Un calcul acceptant est un calcul qui se termine en un état d'acceptation.

Un automate à pile visible ne peut pas empiler et dépiler avec le même symbole d'entrée. Par conséquent, des langages comme

${\displaystyle L=\{a^{n}ba^{n}\mid n\in \mathbb {N} \}}$

ne sont pas acceptés par des automates à pile visible, alors qu'ils peuvent l'être par un automate à pile déterministe usuel.

Les automates à pile visible non déterministes peuvent être déterminisés, comme c'est le cas pour les automates finis ; ceci les distingue des automates à pile usuels. Toutefois, la procédure de déterminisation, partant d'un automate non déterministe à ${\displaystyle s}$ états, peut conduire à un automate déterministe ayant jusqu'à ${\displaystyle 2^{s^{2}}}$ états[1].

La famille des langages à pile visible sur un même alphabet structuré est fermée pour les opérations suivantes[1] :

• union
• intersection
• complément,
• étoile de Kleene
• concaténation
• image miroir
• préfixe, suffixe, facteur.

La famille est donc une algèbre de Boole et de plus une famille rationnellement fermée de langages. De plus l'ensemble des préfixes d'un langage à pile visible l'est encore, et par image miroir aussi l'ensemble des suffixes (les suffixes sont les retournés des préfixes de l'image miroir), et donc aussi l'ensemble des facteurs.

En ce qui concerne la complémentation, la construction usuelle pour les automates à pile déterministes[10] s'étend simplement aux automates à pile visible. Ceci n'est pas le cas pour l’intersection, puisque les langages algébriques déterministes ne sont pas fermés par intersection, et une construction spécifique doit être réalisée. Une preuve simple de la fermeture par complémentation est au moyen des automates de mots imbriqués : il suffit d'échanger les états terminaux et non terminaux.

D'autres propriétés de fermeture, comme l'insertion ou la suppression de facteurs dans un mot, ont été étudiées par Alexander Okhotin et Kai Salomaa[11].

Alur et Madhusudan[1] ont prouvé les diverses propriétés de clôture des langages rapportés plus haut, et évalué la complexité du test de savoir si le langage est vide. Ils ont aussi prouvé que la simulation d’un automate non déterministe à ${\displaystyle n}$ états par un automate déterministe équivalent peut demander, dans le pire des cas, ${\displaystyle 2^{\Theta (n^{2})}}$ états. Un article d’Alexander Okhotin et Kai Salomaa[12] donne des constructions efficaces pour la concaténation l’étoile de Kleene et l’image miroir (ou transposition). Ils montrent que l’étoile et le transposé d’un automate à pile visible avec ${\displaystyle n}$ états peuvent être construit avec ${\displaystyle 2^{O(n\log n)}}$ états, assez proche d’une borne inférieure donnée antérieurement par Piao et Salomaa[13] et qui est ${\displaystyle 2^{\Omega (n\log n)}}$. Quant à la concaténation, une construction de Okhotin et Salomaa pour concaténer deux automates, l'un à ${\displaystyle n}$ et l'autre à ${\displaystyle m}$ états donne un automate de ${\displaystyle m2^{O(n\log n)}}$ états, et une borne inférieure en ${\displaystyle m2^{\Omega (n\log n)}}$.

La table suivante est extraite de l'article d'Okhotin et Salomaa[12]. Elle contient les bornes connues en 2017 pour la complexité des opérations pour les automates finis déterministes (DFA), inambigus (UFA), non déterministes(NFA), à pile visible déterministes (IDPFA) et non déterministes (NIDPDA)[14] :

Complexité des opérations de fermeture

	DFA	UFA	NFA	IDPDA	NIDPDA
union	${\displaystyle mn}$	${\displaystyle mn+m+n\leq \cdot \leq m+O(n2^{0.79m})}$	${\displaystyle m+n+1}$	${\displaystyle \Theta (mn)}$	${\displaystyle m+n+O(1)}$
intersection	${\displaystyle mn}$	${\displaystyle mn}$	${\displaystyle mn}$	${\displaystyle \Theta (mn)}$	${\displaystyle \Theta (mn)}$
complément	${\displaystyle n}$	${\displaystyle n^{2-o(1)}\leq \cdot \leq O(2^{0.79n})}$	${\displaystyle 2^{n}}$	${\displaystyle n}$	${\displaystyle 2^{\Theta (n^{2})}}$
produit	${\displaystyle m2^{n}-2^{n-1}}$	${\displaystyle 3/42^{m+n}-1}$	${\displaystyle m+n}$	${\displaystyle m2^{\Theta (n\log n)}}$	${\displaystyle m+n+O(1)}$
carré	${\displaystyle n2^{n}-2^{n-1}}$	?	${\displaystyle 2n}$	${\displaystyle 2^{\Theta (n\log n)}}$	${\displaystyle n+O(1)}$
étoile	${\displaystyle 3/4\cdot 2^{n}}$	${\displaystyle (n-1)^{2}\leq \cdot \leq 3/4\cdot 2^{n}}$	${\displaystyle n+1}$	${\displaystyle 2^{\Theta (n\log n)}}$	${\displaystyle n+O(1)}$
miroir	${\displaystyle 2^{n}}$	${\displaystyle n}$	${\displaystyle n+1}$	${\displaystyle 2^{\Theta (n\log n)}}$	${\displaystyle n+O(1)}$

Alur et Madhusudan[1] montrent que les langages à pile visible sont plus généraux que les langages à parenthèses (en anglais « parenthesis languages ») décrits en 1967 par McNaughton[15], puis étendus[2]. En 2012, Crespi Reghizzi et Mandrioli[16] montrent que les langages à pile visible sont strictement contenus dans la classe des langages décrits par grammaire à précédence d'opérateurs, introduits par Floyd en 1963[17] et qui ont les mêmes propriétés de clôture[18]. Voici une table, tirée des articles d'Alur et Madhusudan[2] et de Crespi Reghizzi et Mandrioli[16], qui situe les langages à pile visible et leurs propriétés de clôture dans la hiérarchie de Chomsky.

Propriétés de fermeture

Langages	union	intersection	complément	produit étoile	préfixe suffixe	miroir
rationnels	oui	oui	oui	oui	oui	oui
équilibrés	oui	oui	non	oui	non	oui
à pile visible	oui	oui	oui	oui	oui	oui
Floyd	oui	oui	oui	oui	oui	oui
déterministes	non	non	oui	non	oui	non
algébriques	oui	non	non	oui	oui	oui

Les langages à pile visible sont exactement les langages que l'on peut engendrer avec une famille de grammaires appelées grammaires à pile visible (en anglais visibly pushdown grammars)[19]. Ces grammaires sont définies comme une restriction des grammaires algébriques. Une grammaire à pile visible est 4-uplet

${\displaystyle G=(V,\Sigma ,R,S)}$ où

• ${\displaystyle V=V^{0}\cup V^{1}}$, l'ensemble des variables est l'union disjointe de deux ensembles ${\displaystyle V^{0}}$ et ${\displaystyle V^{1}}$. Les langages engendrés par des variables de ${\displaystyle V^{0}}$ sont composés de mots sans éléments pendants, ceux engendrés par .
• ${\displaystyle \Sigma }$ est l'alphabet terminal, mais les règles comportent des lettres de l’alphabet structuré.
• ${\displaystyle R}$ est l'ensemble des règles ou productions de la grammaire. Les règles sont de trois sortes, avec ${\displaystyle X,Y\in V,Z\in V^{0}}$ :
  • ${\displaystyle X\to \varepsilon }$
  • ${\displaystyle X\to aY}$ avec ${\displaystyle a\in {\hat {\Sigma }}}$ et, si ${\displaystyle X\in V^{0}}$, alors ${\displaystyle a\in \Sigma }$ et ${\displaystyle Y\in V^{0}}$
  • ${\displaystyle X\to \langle aYb\rangle Z}$ avec ${\displaystyle a,b\in \Sigma ,\,Y\in V^{0}}$ et, si ${\displaystyle X\in V^{0}}$ alors ${\displaystyle Z\in V^{0}}$
• ${\displaystyle S\in V\,}$ est l'axiome.

Les variables de ${\displaystyle V^{0}}$ n'engendres que des langages de mots bien parenthésés, sans appel ou retour pendant, alors que les mots engendrés par des variables de ${\displaystyle V^{1}}$ contiennent des appels ou des retours pendants.

Dans une règle ${\displaystyle X\to aY}$, si ${\displaystyle a}$ est en position d'appel ou de retour, alors ou bien c’est un lettre qui n’est pas couplée ou sa lettre couplée n’est pas mémorisée, et par conséquent ${\displaystyle X}$ doit être dans ${\displaystyle V^{1}}$.

Dans une règle ${\displaystyle X\to \langle aYb\rangle Z}$, les positions correspondant aux symboles ${\displaystyle a}$ et ${\displaystyle b}$ forment un couple parenthésé, avec entre elles un mot bien parenthésé engendré par ${\displaystyle Y\in V^{0}}$, et si ${\displaystyle X}$ engendre des mots bien parenthésés, cette propriété se propage à ${\displaystyle Z}$.

On peut montrer[20] qu’un langage de mots imbriqués est engendrée par une grammaire à pile visible et réciproquement.

Le problème de décider si un mot de longueur ${\displaystyle \ell }$ est acceptée par un automate de mots imbriqués donné peut être résolu par une par un circuit booléen uniforme de profondeur ${\displaystyle \mathrm {O} (\log \ell )}$[2].

Les langages réguliers de mots imbriqués sont exactement les langages décrits par la logique monadique du second ordre avec les deux prédicats unaires call et return, la fonction successeur et la relation de couplage ↝[2] : les formules sont

${\displaystyle {\begin{aligned}\varphi$ :=&a(x)\mid X(x)\mid {\mathsf {call}}(x)\mid {\mathsf {ret}}(x)\mid x=y+1\mid x\rightsquigarrow y\\&\mid \varphi \lor \varphi \mid \varphi \land \varphi \mid \lnot \varphi \mid \exists x.\varphi \mid \forall x.\varphi \end{aligned}}}

où ${\displaystyle a\in \Sigma }$, ${\displaystyle x,y}$ sont des variables du premier ordre et ${\displaystyle X}$ du second ordre.