Voir la source de Automate à pile visible

En [[informatique théorique]], et notamment en [[théorie des automates]] et des [[Langage formel|langages formels]], un '''automate à pile visible''' (en anglais {{Citation étrangère|visibly pushdown automaton|langue=en}}) est un [[automate à pile]] reconnaissant des mots sur un alphabet partitionné. Ils reconnaissent les '''langages à pile visible''' (en anglais {{Citation étrangère|visibly pushdown languages|langue=en}}). Cette famille de langages est intermédiaire entre les  [[Langage rationnel|langages rationnels]] et les [[Langage algébrique déterministe|langages algébriques déterministes]]. 

Un '''mot imbriqué''' (en anglais {{Citation étrangère|nested word|langue=en}}), notion proposée par [[Rajeev Alur]] et Parthasarathy Madhusudan, est un objet doté d'une double structure : d'un côté, c'est une [[chaîne de caractères]], comme dans l’usage traditionnel de la modélisation de structures [[Ordre total|totalement ordonnées]], d'un autre côté, c'est un modèle de structure hiérarchique, comme les [[Arbre enraciné|arbres enracinés]] ou les systèmes de parenthèses emboîtées. Les [[automate]]s  acceptant des ensembles de mots imbriqués sont les '''automates de mots imbriqués''' (en anglais {{Citation étrangère|langue=en|nested word automata}}). Ce sont des automates généralisant les [[automate fini non déterministe|automates finis]] de mots. Le codage par système de parenthèses de mots imbriqués redonne la classe des langages à pile visible. 

Depuis l'introduction de cette terminologie par Alur et Madhusudan en 2004<ref name="AlurMadhu2004">{{harvsp|Alur|Madhusudan|2004}}</ref>, suivie d'un développement autour de ces notions en 2009<ref name="AlurMadhu2009">{{harvsp|Alur|Madhusudan|2009}}</ref>, ces concepts ont déclenché un nombre important de recherches sur et autour de ces objets et de leurs applications<ref>[https://scholar.google.com/scholar?as_q=&as_oq=%22nested+words%22+%22visibly+pushdown%22 Recherche de Google Scholar] pour ''{{Langue|en|nested words}}'' ou ''{{Langue|en|visibly pushdown}}''.</ref>.

== Description et motivation ==

=== Description informelle ===
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<ref>{{harvsp|id=AlurPenn|texte= Rajeev Alur, ''Nested words aka Visibly Pushdown Languages''|p=}}.</ref>. Des exemples de données avec cette double structure hiérarchique et linéaire incluent les exécutions de [[Programmation structurée|programmes structurés]], des [[Linguistique informatique|données linguistiques annotées]] et des documents [[Hypertext Markup Language|HTML]] ou [[Extensible Markup Language|XML]]. Un mot imbriqué se compose d'une séquence de positions linéairement ordonnées, augmentée d'arcs d'imbrication reliant des [[Appel de procédure|appels]] à des retours (ou des [[Langage de balisage|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 [[Automate fini non déterministe|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 [[Langage algébrique déterministe|langages algébriques déterministes]] particuliers qui se classent entre les langages équilibrés et les langages de Floyd, engendrés par des [[Grammaire d'opérateurs|grammaires à précédence d'opérateurs]].

=== Applications ===
Les langages rationnels de mots imbriqués s'emploient avantageusement dans la [[Vérification de modèles|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 [[postcondition]]s) 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'[[Arbre enraciné|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 d'arbre|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 [[Analyse de données textuelles|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 [[Mot (mathématiques)|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 [[Algorithme de fouille de flots de données|de fouille]] de flots de données, comme ils servent dans les logiciels pour XML.

=== Note historique ===

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<ref>{{harvsp|Mehlhorn|1980}}.</ref> ; il a démontré qu’un langage défini par un tel automate peut être reconnu en temps polynomial, et  avec un espace <math>O(\log^2n/\log\log n)</math>. Cette borne a été améliorée par von Braunmühl et Verbeek<ref>{{harvsp|von Braunmühl|Verbeek|1985}}.</ref> qui ont donné, pour la reconnaissance, une complexité <math>O(\log n)</math> en espace et <math>O(n^2\log n)</math> 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<ref>{{harvsp|Dymond|1988}}.</ref> a montré que cette famille de langages est contenue dans la classe de complexité [[NC (complexité)|NC]]<sup>1</sup>.

== Mot imbriqué ==

=== Relation de couplage ===
Une ''relation de couplage'' (en anglais {{Citation étrangère|langue=en|matching relation}}) de longueur <math>\ell\ge 0</math>, aussi appelé une ''correspondance'', est une [[relation binaire]], partie du produit <math>\{-\infty, 1,2,\ldots,\ell-1,\ell\}\times\{1,2,\ldots,\ell-1,\ell,\infty\}</math>, notée traditionnellement <math>\rightsquigarrow</math>. Les couples de cette relation sont appelées ''flèches''. La relation vérifie les conditions suivantes :
# si <math>i\rightsquigarrow j</math> alors <math>i<j</math> : toutes les flèches sont vers la droite ;
# si <math>i_1\rightsquigarrow j</math> et <math>i_2\rightsquigarrow j</math> et <math>j<\infty</math>, alors <math>i_1=i_2</math> : deux flèches n'aboutissent pas à la même position ;
# si <math>i\rightsquigarrow j_1</math> et <math>i\rightsquigarrow j_2</math> et <math>i>-\infty</math>, alors <math>j_1=j_2</math> : deux flèches ne commencent pas à la même position ;
# si <math>i_1\rightsquigarrow j_1</math> et <math>i_2\rightsquigarrow j_2</math>, alors on n'a pas <math>i_1<i_2<j_1<j_2</math> : deux flèches ne se croisent pas.
Enfin, le couple <math>(-\infty,\infty)</math> n'est pas une flèche.
Si <math>i\rightsquigarrow j</math>, alors  
* <math>i</math> est une ''position d'appel''  (en anglais {{Citation|call position}}) et 
* <math>j</math> est une ''position de retour'' (en anglais {{Citation étrangère|langue=en|return position}}) ;
* si <math>i=-\infty</math>, alors <math>j</math> est un ''retour pendant'', 
* si <math>j=\infty</math>, alors <math>i</math> est un ''appel pendant'' (en anglais {{Citation étrangère|langue=en|pending call}}) 
* une position qui est ni d'appel ni de retour est une ''position interne'' (en anglais {{Citation étrangère|langue=en|internal position}}.
Un couple <math>(i,j)</math> dont aucun des deux indices n'est pendant est ''bien parenthésé'' (en anglais {{Citation étrangère|well matched|langue=en}}).
=== Mot imbriqué ===
Un ''mot imbriqué'' de longueur <math>\ell</math>  sur un [[alphabet]]  <math>\Sigma</math> est une couple <math>(w,\rightsquigarrow)</math>, où <math>w</math> est un mot de longueur <math>\ell</math> sur <math>\Sigma</math> , dans le sens usuel du terme, et où <math>\rightsquigarrow</math> est une  relation de couplage de longueur <math>\ell</math>.

=== Exemples ===
1. La relation <math>\rightsquigarrow = \{(-\infty,1),(2,\infty),(3,4),(5,7),(8,\infty)\}</math> définit les positions d'appel <math>-\infty</math>, 2,3,5, 8,  et les positions de retour <math>\infty</math>, 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 <math>3^n</math> relations de couplage de longueur <math>n</math><ref>{{harvsp|Alur|Madhusudan|2009|loc=Proposition 2.2}}.</ref>

== Codage de mots imbriqués par des mots ordinaires ==
=== Alphabet structuré ===
Les mots imbriqués sur un alphabet <math>\Sigma</math> peuvent être codés comme mots ordinaires sur un alphabet augmenté, appelé ''alphabet structuré'' noté <math> \hat{\Sigma}</math> ; chaque symbole <math>a</math> de <math>\Sigma</math> 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 <math>\Sigma</math> est composé de symboles <math>\langle a</math> (pour <math>a</math> en position d'appel), <math>a\rangle</math> (pour a <math>a</math> 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.

=== Exemple ===
Pour le mot 
: <math> w=abaabccca</math> 
et la relation de couplage
:<math>\rightsquigarrow = \{(-\infty,1),(2,\infty),(3,4),(5,7),(8,\infty)\}</math>
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
:<math>a\rangle\langle b\langle aa\rangle\langle  bcc\rangle ca</math>

== Automates ==
Les automates de mots imbriques<ref>Terminologie utilisée par exemple dans Grégoire Laurence, ''Normalisation et Apprentissage de Transductions d’Arbres en Mots''. Thèse de l'Université des Sciences et Technologie de Lille - Lille I, 2014.</ref> sont des automates qui opèrent, presque comme des automates finis usuels, sur les mots imbriqués, alors que les automates à pile visible sont des automates à pile qui opèrent sur le codage des mots sur l'alphabet structuré.

=== Automate de mots imbriqués ===
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é <math>(w,\rightsquigarrow)</math>, 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 <math>Q</math> d'états dits ''linéaires''
* un état initial (linéaire) <math>q_0\in Q</math>
* un ensemble d'états terminaux (linéaires) <math>Q_f\subseteq Q</math>
* un ensemble fini <math>P</math> d'états dits ''hiérarchiques''
* un état initial (hiérarchique) <math>p_0\in P</math>
* un ensemble d'états terminaux (hiérarchiques) <math>P_f\subseteq P</math>
et trois fonctions de transition, une pour chaque type de symbole
* une fonction de transitions d'appels <math>\delta_c:Q\times \Sigma\to Q\times P</math>
* une fonction de transitions internes <math>\delta_i:Q\times \Sigma\to Q</math>
* une fonction de transitions de retours <math>\delta_r:Q\times P \times \Sigma\to Q</math>
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 {{Citation étrangère|langue=en|run}}) sur un mot imbriqué <math>a_1a_2\cdots a_n</math> est une suite <math>q_0,q_1,\ldots,q_n</math> d'états linéaires et une suite d'états hiérarchiques <math>p_i\in P</math>, un pour chaque position d'appel et correspondants aux flèches du couplage, telles que
* si <math>i</math> est une position d'appel, <math>\delta_c(q_{i-1},a_i)=(q_i,p_i)</math> ;
* si <math>i</math> est une position interne, <math>\delta_i(q_{i-1},a_i)=q_i</math> ;
* si <math>i</math> est une position de retour et <math>j</math> est le prédécesseur d'appel de <math>i</math>, alors <math>\delta_r(q_{i-1},p_j,a_i)=q_i</math>, et si <math>i</math> est un retour pendant, alors <math>\delta_r(q_{i-1},p_0,a_i)=q_i</math>.
L'automate accepte le mot imbriqué si le dernier état est un état final : <math>q_n\in Q_f</math>.

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

=== Automate à pile visible ===

Un '''automate à pile visible déterministe''' est un [[Automate à pile#Automate à pile déterministe|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<ref name="AlurMadhu2009"/>, un automate à pile visible déterministe <math>M=(Q, \hat{\Sigma}, \Gamma, \delta, q_0, F)</math> comporte :
*<math>Q </math> un [[ensemble fini]] d'états ;
*<math>q_0\in\, Q </math> est l’état initial, et
*<math>F \subseteq Q</math> est l'ensemble des états d'acceptation ;
*<math>\hat{\Sigma}</math> un alphabet structuré, partitionné en trois ensembles <math>\Sigma_c</math>, <math>\Sigma_r</math>, et <math>\Sigma_i</math>. L'alphabet <math>\Sigma_c</math> contient les ''symboles d'appel'', <math>\Sigma_r</math> les ''symboles de retour'', et enfin <math>\Sigma_i</math> les ''symboles internes'' ;
*<math>\Gamma</math> est un ensemble fini, l{{'}}''alphabet de pile'', avec un symbole particulier <math>\bot\in\Gamma</math> de fond de pile ;
*<math>\delta = \delta_c \cup \delta_r \cup \delta_i</math> est la  ''fonction de transition'', elle-même partitionnée en trois parties correspondant aux transitions d'appel, internes et de retour, à savoir :
**<math>\delta_c : Q \times \Sigma_c \to Q \times \Gamma\setminus\{\bot\}</math>, la ''fonction de transition d'appel'' : le fond de pile ne peut être empilé à nouveau ;
**<math>\delta_r : Q \times \Sigma_r \times \Gamma \to Q </math>, la ''fonction de transition de retour ;''
**<math>\delta_i : Q \times \Sigma_i \to Q</math>, 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 <math>a</math>, il peut empiler un symbole seulement si c'est une lettre d'appel de <math>\Sigma_c</math>, dépiler seulement si c'est une lettre de <math>\Sigma_r</math>, enfin si  <math>a\in\Sigma_i</math> 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 

:<math>L=\{a^nba^n \mid n\in\N \}</math> 

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 [[Automate fini non déterministe|automates finis]] ; ceci les distingue des automates à pile usuels. Toutefois, la procédure de déterminisation, partant d'un automate non déterministe à <math>s</math> états, peut conduire à un automate  déterministe ayant jusqu'à <math>2^{s^2}</math> états<ref name="AlurMadhu2004"/>.

== Problèmes de décisions et complexité ==
Soit <math>|A|</math> la taille d'une description d'un automate <math>A</math>. On peut teste l'acceptation d'un mot de longueur ''n'' par l'automate en temps <math>O(|A|^3n)</math>. En particulier, on peut tester si le langage est vide en temps <math>O(|A|^3)</math>. Pour deux automates non déterministes <math>A</math> et <math>B</math>, décider si l’ensemble des mots acceptés par <math>A</math> est un sous-ensemble des mots acceptés par <math>B</math> est [[EXPTIME]]-complet. Il est aussi   EXPTIME-complet de savoir s'il existe un mot qui n'est pas accepté<ref name="AlurMadhu2009" />.

:{|| class="wikitable"  style="font-size:95%;border:0px;text-align:left;line-height:150%;"
|+  Complexité de problèmes de décision pour les automates
|-
!  
! vide
! universalité<br/>équivalence
! inclusion
|-
! scope="row"|automates finis déterministes
|Nlogspace ||Nlogspace||Nlogspace
|-
! scope="row"|automates finis non déterministes 
|Nlogspace ||Pspace||Pspace
|-
! scope="row"|automates à pile
|Ptime||indécidable||indécidable
|-
! scope="row"|automates à pile déterministes 
|Ptime||décidable||indécidable
|-
! scope="row"|automates de mots imbriqués déterministes
|Ptime||Ptime||Ptime
|-
! scope="row"|automates de mots imbriqués non déterministes
|Ptime||Exptime||Exptime
|}

== Langages ==
Les automates à pile visible déterministes peuvent être vus comme des [[Automate à pile#Automate à pile déterministe|automates à pile déterministes]] particuliers ; ainsi, la famille des langages à pile visible sur un alphabet <math>\,\hat{\Sigma}</math> donné est un sous-ensemble de la famille des langages algébriques déterministes sur  <math>\,\hat{\Sigma}</math>. En particulier, la fonction qui efface la relation de couplage des mots imbriqués transforme des langages de mots imbriqués en langages algébriques. 

=== Propriétés de fermeture ===
La famille des langages à pile visible sur un même alphabet structuré est fermée pour les opérations suivantes<ref name="AlurMadhu2004" /> :

*union
*intersection
*complément, 
*[[étoile de Kleene]]
*[[concaténation]]
* image miroir
* préfixe, suffixe, facteur.
La famille est donc une  [[Algèbre de Boole (structure)|algèbre de Boole]] et de plus une [[Famille abstraite de langages | 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<ref>{{harvsp|Hopcroft|Ullman|1979|loc=Section 10.5}}.</ref> 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<ref name="OkhotinSalomaa2019">{{harvsp|Okhotin|Salomaa|2019}}.</ref>.

=== Complexité des opérations ===
Alur et Madhusudan<ref name="AlurMadhu2004" />  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 à <math>n</math> états par un automate déterministe équivalent peut demander, dans le pire des cas, <math>2^{\Theta(n^2)}</math> états. Un article d’Alexander Okhotin et Kai Salomaa<ref name="OkhotinSalomaa2017">{{harvsp|OkhotinSalomaa2017}}.</ref> 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 <math>n</math> états peuvent être construit avec <math>2^{O(n\log n)}</math> états, assez proche d’une borne inférieure donnée antérieurement par Piao et Salomaa<ref>{{harvsp|PiaoSalomaa2009}}.</ref> et qui est <math>2^{\Omega(n \log n)}</math>. Quant à la concaténation, une construction de Okhotin et Salomaa pour concaténer deux automates, l'un à <math>n</math> et l'autre à <math>m</math> états donne un automate de <math>m2^{O(n \log n)}</math> états, et une borne inférieure en  <math>m2^{\Omega(n \log n)}</math>.

La table  suivante est extraite de l'article d'Okhotin et Salomaa<ref name="OkhotinSalomaa2017" />. Elle contient les bornes connues en 2017 pour la complexité des opérations pour les [[Automate fini déterministe|automates finis déterministes]] (DFA), [[Automate fini inambigu|inambigus]] (UFA), [[Automate fini non déterministe|non déterministes]](NFA), à pile visible déterministes (IDPFA) et non déterministes (NIDPDA)<ref>IDPDA est utilisé comme abréviation pour « input-driven pda ».</ref> :

:{|| class="wikitable"  style="font-size:95%;border:0px;text-align:center;line-height:150%;"
|+  Complexité des opérations de fermeture
|-
!
! DFA
! UFA
! NFA
!IDPDA
!NIDPDA
|-
! scope="row"|union || <math>mn</math> || <math>mn+m+n\le\cdot\le m+O(n2^{0.79m})</math> || <math> m+n+1</math> || <math>\Theta(mn)</math> || <math>m+n+O(1)</math>
|-
! scope="row"|intersection || <math>mn</math> || <math>mn</math> || <math>mn</math> || <math>\Theta(mn)</math> ||<math>\Theta(mn)</math>
|-
! scope="row"|complément|| <math>n</math> || <math>n^{2-o(1)} \le\cdot\le  O(2^{0.79n})</math>|| <math>2^n</math>|| <math>n</math>||<math>2^{\Theta(n^2)}</math>
|-

! scope="row"| produit || <math>m2^n-2^{n-1}</math> ||  <math>3/42^{m+n}-1</math> || <math>m+n</math> ||  <math>m 2^{\Theta(n\log n)}</math>  || <math>m+n+O(1)</math>
|-
! scope="row"| carré||<math> n2^n-2^{n-1}</math> || ? || <math>2n</math> ||  <math>2^{\Theta(n\log n)}</math>  || <math>n+O(1)</math>
|-
! scope="row"| étoile ||  <math>3/4\cdot  2^n</math> ||  <math>(n-1)^2\le\cdot\le 3/4\cdot 2^n</math> || <math>n+1</math> ||  <math>2^{\Theta(n\log n)}</math>  || <math>n+O(1)</math>
|-
! scope="row"| miroir||  <math>2^n</math> || <math>n</math> || <math>n+1</math> ||  <math>2^{\Theta(n\log n)}</math>  || <math>n+O(1)</math>
|}

=== Relation avec d'autres classes de langages ===
Alur et Madhusudan<ref name="AlurMadhu2004" /> montrent que les langages à pile visible sont plus généraux que les langages à parenthèses (en anglais  {{Citation étrangère|langue=en|parenthesis languages}}) décrits en 1967 par McNaughton<ref>{{harvsp|McNaughton|1967}}</ref>, puis étendus<ref name="AlurMadhu2009" />. En 2012, Crespi Reghizzi et Mandrioli<ref name="CR">{{harvsp|Crespi Reghizzi|Mandrioli|2012}}</ref> montrent que les langages à pile visible sont strictement contenus dans la classe des langages décrits par [[grammaire d'opérateurs|grammaire à précédence d'opérateurs]], introduits par Floyd en 1963<ref>{{harvsp|Floyd|1963}}</ref> et qui ont les mêmes propriétés de clôture<ref>Voir aussi {{harvsp|Lonati|Mandrioli|Panella|Pradella|2015}}</ref>. Voici une table, tirée des articles d'Alur et Madhusudan<ref name="AlurMadhu2009" /> et de Crespi Reghizzi et Mandrioli<ref name="CR" />, qui situe les langages à pile visible et leurs propriétés de clôture dans la [[hiérarchie de Chomsky]].

:{|| class="wikitable"  style="font-size:95%;border:0px;text-align:left;line-height:150%;"
|+  Propriétés de fermeture
|-
! Langages 
! union
! intersection
! complément
! produit<br/>étoile
! préfixe<br/>suffixe
! miroir
|-
! scope="row"|rationnels 
|oui||oui||oui||oui||oui||oui
|-
! scope="row"|équilibrés 
|oui||oui||non||oui||non||oui
|-
! scope="row"|à pile visible  
|oui||oui||oui||oui||oui||oui
|-
! scope="row"|Floyd 
|oui||oui||oui||oui||oui||oui
|-
! scope="row"|déterministes 
|non||non||oui||non||oui||non
|-
! scope="row"|algébriques 
|oui||non||non||oui||oui||oui
|}

== Autres modèles de description ==

=== Grammaires à pile visible ===
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'')<ref>{{Harvsp|Alur|Madhusudan|2009|p=|loc=section 5.2. Grammar-based Characterization}}</ref>. Ces grammaires sont définies comme une restriction des [[Grammaire non contextuelle|grammaires algébriques]]. Une grammaire à pile visible est  4-[[N-uplet|uplet]]

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

Les variables de <math>V^0</math> 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  <math>V^1</math>  contiennent des appels ou des retours pendants. 

Dans une règle <math>X\to aY</math>, si <math>a</math> 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 <math>X</math> doit être dans <math>V^1</math>. 

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

On peut montrer<ref>{{harvsp|Alur|Madhusudan|2009|loc=Théorème 5.3}}.</ref> qu’un langage de mots imbriqués est engendrée par une grammaire à pile visible et réciproquement.

=== Circuits booléens uniformes ===
Le problème de décider si un mot de longueur <math>\ell</math> 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 <math>\Omicron(\log\ell)</math><ref name="AlurMadhu2009" />.

=== Description logique ===
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 ↝<ref name="AlurMadhu2009" /> : les formules sont

:<math>\begin{align}\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{align}
</math>

où <math>a\in\Sigma</math>, <math>x,y</math> sont des variables du premier ordre et <math>X</math> du second ordre.

== Extension : transducteur à pile visible ==

Les '''transducteurs à pile visible''', dont la théorie est détaillée par Filiot, Raskin, Reynier, Servais et Talbot<ref name="FiliotRaskin2018">{{harvsp|Filiot|Raskin|Reynier|Servais|Talbot|2018}}.</ref>, permettent notamment de modéliser des transformations de mots imbriqués en mots. Ils ont de bonnes propriétés algorithmiques, comme la décidabilité de l'équivalence des fonctions réalisées, et sont fermés par ''look-ahead'' « régulier ».

Les transducteurs à pile visible étendent les automates à pile visible avec des sorties. Ils lisent des mots imbriqués, et produisent des mots de sortie qui ne sont pas nécessairement imbriqués. Comme pour les automates à pile visible, le comportement de la pile est synchronisé avec les types de symboles d'entrée : lors de la lecture d'un symbole d'appel, exactement un symbole de pile est ajouté au sommet de la pile ; lors de la lecture d'un symbole de retour, exactement un symbole de pile est supprimé au sommet de la pile ; et la pile n'est pas modifiée lors de la lecture des symboles internes. Durant leurs transitions, les transducteurs  peuvent ajouter des mots sur leur bande de sortie ; leur concaténation définit le mot de sortie résultant. Par conséquent, transducteurs à pile visible définissent des transformations des mots imbriqués en mots et peuvent être vus comme une sous-classe de transducteurs à pile.

Les transducteurs à pile visible jouissent de propriétés de clôture similaires à celles des [[Transducteur fini|transducteurs finis]] : ils sont clos par union, mais ni par intersection ni par complément. À la différence des transducteurs usuels, les transducteurs à pile visible ne sont pas fermés par composition, sauf pour des cas particuliers. 

Une des propriétés importantes à vérifier est l'équivalence, c'est-à-dire la propriété que deux transducteurs donnés définissent la même relation. L'équivalence est indécidable pour les transducteurs finis usuels ; elle est en revanche décidable pour des transducteurs à images bornées, c'est-à-dire tels que l'image de tout mot a au plus ''k'' éléments, pour un entier ''k'' fixe. Pour des transducteurs à pile visible à images bornées, la même propriété est encore ouverte ; pour des transducteurs à pile visible fonctionnels en revanche, la propriété est décidable, et le problème de décision est [[EXPTIME]]-complet.
== Notes ==
<references/>

== Références bibliographiques ==
*{{chapitre|libellé = Alur Madhusudan 2004
 | doi = 10.1145/1007352.1007390  | isbn = 1581138520
 | nom1 = Alur | prénom1 = Rajeev | nom2 = Madhusudan| prénom2 = Parthasarathy
 | titre = Visibly pushdown languages 
 | titre ouvrage = Proceedings of the thirty-sixth annual ACM symposium on Theory of computing  - STOC '04 
 | passage = 202–211
 | année = 2004 | url = http://www.cis.upenn.edu/~alur/Stoc04.pdf}}
*{{article|langue=en|libellé = Alur Madhusudan 2009
 | doi = 10.1145/1516512.1516518
 | nom1 = Alur | prénom1 = Rajeev 
 | nom2 = Madhusudan | prénom2 = Parthasarathy
 | titre = Adding nesting structure to words 
 | journal = Journal of the ACM | volume = 56 | numéro = 3 | pages = 1–43 
 | année = 2009 
 | url = http://www.cis.upenn.edu/~alur/Jacm09.pdf}}
*{{article|langue=en|libellé = Floyd 1963
| nom = Floyd | prénom = Robert W.  | lien auteur = Robert W. Floyd 
| titre = Syntactic Analysis and Operator Precedence | journal = Journal of the ACM 
| volume = 10 | numéro = 3 | pages = 316–333 | date=juillet 1963 
| doi = 10.1145/321172.321179}}
*{{article|langue=en|libellé = McNaughton 1967
 | nom1 = McNaughton | prénom1 = R. 
 | titre = Parenthesis Grammars | journal = Journal of the ACM | volume = 14 | numéro = 3 
 | pages = 490 | année = 1967 | doi = 10.1145/321406.321411}}
*{{article|langue=en|libellé = Alur et al. 2008
 | doi = 10.2168/LMCS-4(4:11)2008 
 | nom1 = Alur | prénom1 = R. | nom2 = Arenas | prénom2 = M. | nom3 = Barcelo | prénom3 = P. 
 | nom4 = Etessami | prénom4 = K. | nom5 = Immerman | prénom5 = N. | nom6 = Libkin | prénom6 = L. 
 <!--| editor1-last = Grädel--> <!--| editor1-first = Erich--> 
 | titre = First-Order and Temporal Logics for Nested Words 
 | journal = Logical Methods in Computer Science | volume = 4 | numéro = 4 | année = 2008 
 | arxiv = 0811.0537}}
*{{article|langue=en|libellé = Crespi Reghizzi, Mandrioli 2012
 |nom=Crespi Reghizzi|prénom=Stefano|nom2=Mandrioli|prénom2=Dino
 |titre=Operator precedence and the visibly pushdown property
 |journal=Journal of Computer and System Sciences
 |année=2012|volume=78|numéro=6|pages=1837–1867
 |doi=10.1016/j.jcss.2011.12.006
 |url=http://home.deib.polimi.it/crespi/OperPrecAndVPpropWithApp.pdf}}.
*{{article|langue=en|libellé = Lonati, Mandrioli, Panella, Pradella 2015
 |nom=Lonati|prénom=Violetta |nom2=Mandrioli|prénom2=Dino |nom3=Panella|prénom3=Federica |nom4=Pradella|prénom4=Matteo
 |titre=Operator Precedence Languages: Their Automata-Theoretic and Logic Characterization
 |journal=SIAM Journal on Computing|année=2015|volume=44|numéro=4
 |doi=10.1137/140978818}}.
*{{article|langue=en|libellé = Braunmühl, Verbeek 1985
 |nom1=von Braunmühl|prénom1=Burchard|nom2=Verbeek|prénom2=Rutger
 |titre=Input Driven Languages are Recognized in log n Space
 |volume=102|année=1985
 |numéro = C|pages=1–19
 |journal = North-Holland Mathematics Studies
 |issn=0304-0208
 |doi=10.1016/S0304-0208(08)73072-X}}.
*{{article|langue=en|libellé = Dymond 1988
 |nom1=Dymond|prénom1=Patrick W.
 |titre=Input-driven languages are in log n depth
 |journal=Information Processing Letters
 |volume=26|numéro=5|année=1988|pages=247–250
 |issn=0020-0190|doi=10.1016/0020-0190(88)90148-2}}.
*{{chapitre|libellé = Mehlhorn 1980
 |nom1=Mehlhorn|prénom1=Kurt
 |titre=Pebbling mountain ranges and its application to DCFL-recognition
 |titre ouvrage = Automata, Languages and Programming. ICALP 1980.
 |auteurs ouvrage =  J. Bakker et J. van Leeuwen (éditeurs)
 |éditeur = Springer
 |collection = Lecture Notes in Computer Science, vol 85
 |année=1980|passage=422–435|issn=0302-9743|doi=10.1007/3-540-10003-2_89}}.
*{{article|langue=en|libellé = Piao, Salomaa 2009
 |nom1=Piao|prénom1=Xiaoxue|nom2=Salomaa|prénom2=Kai
 |titre=Operational state complexity of nested word automata
 |journal=Theoretical Computer Science
 |volume=410|numéro=35|année=2009|pages=3290–3302
 |issn=0304-3975|doi=10.1016/j.tcs.2009.05.002}}.
*{{article|langue=en| libellé = Okhotin Salomaa 2017
 |nom1=Okhotin|prénom1=Alexander|nom2=Salomaa|prénom2=Kai
 |titre=State complexity of operations on input-driven pushdown automata
 |journal=Journal of Computer and System Sciences
 |volume=86|année=2017|pages=207–228
 |issn=0022-0000|doi=10.1016/j.jcss.2017.02.001}}.
*{{article| libellé = Okhotin Salomaa 2019
 |nom1=Okhotin|prénom1=Alexander |nom2=Salomaa|prénom2=Kai
 |titre=Further closure properties of input-driven pushdown automata
 |journal=Theoretical Computer Science
 |volume=798|année=2019|pages=65–77
 |issn=0304-3975|doi=10.1016/j.tcs.2019.04.006}}
* {{article|libellé = Filiot, Raskin, Reynier, Servais 2018
 |nom1=Filiot|prénom1=Emmanuel|nom2=Raskin|prénom2=Jean-François|nom3=Reynier|prénom3=Pierre-Alain|nom4=Servais|prénom4=Frédéric|nom5=Talbot|prénom5=Jean-Marc
 |titre=Visibly pushdown transducers
 |journal=[[Journal of Computer and System Sciences]]|volume=97
 |année=2018|pages=147-181|doi=10.1016/j.jcss.2018.05.002}}.
* {{article|libellé = Caralp, Reynier, Talbot 2015
 | auteur1=Mathieu Caralp| auteur2= Pierre-Alain Reynier| auteur3 = Jean-Marc Talbot
 |titre=Trimming visibly pushdown automata
 |journal=[[Theoretical Computer Science]]
 |volume=578|année=2015|pages=13–29
 |doi=10.1016/j.tcs.2015.01.018}}.
* {{article|libellé = Sakharov 2020
 |nom1=Sakharov|prénom1=Alexander
 |titre=Annotated regular expressions and input-driven languages
 |journal=[[Information Processing Letters]]
 |volume=159-160|année=2020
 |numéro article=105958
 |doi=10.1016/j.ipl.2020.105958}}.



* {{Ouvrage|langue=en|prénom1=John E.|nom1=Hopcroft|prénom2=Jeffrey D.|nom2=Ullman|titre=Introduction to Automata Theory, Languages, and Computation|éditeur=Addison-Wesley|année=1979|pages totales=418|isbn=978-0-201-02988-8|isbn10=0-201-02988-X}}.

== Articles liés ==
*[[Vérification de modèles]]

== Liens externes ==
*{{Lien web
 |url=http://www.cis.upenn.edu/~alur/nw.html
 |titre= Nested words aka Visibly Pushdown Languages
 |auteur= Rajeev Alur
 |id=AlurPenn}}.
* [http://qwiki.stanford.edu/index.php/Complexity_Zoo:V#vpl Classe VPL] sur le [[Scott Aaronson|Complexity Zoo]]
* {{Lien web
  | url=https://swt.informatik.uni-freiburg.de/teaching/SS2012/AutomataTheory/Resources/Slides/nestedwordautomata-seminarslides-christianschilling.pdf
  | titre=Nested Word Automata |série= Automata Theory
  |auteur=Christian Schilling 
  |site= swt.informatik.uni-freiburg.de
  |éditeur= Université de Fribourg, Sommersemester  2012
  |consulté le=25 février 2017
  |id=Schilling2012}}.

{{Palette|Automates finis et langages réguliers|Informatique théorique}}
{{Portail|informatique théorique}}

[[Catégorie:Langage formel]]
[[Catégorie:Théorie des automates]]