Оригинал статьи представлен на cis.upenn.edu.

Що таке вкладені слова?

Вкладені слова — це модель представлення даних як з лінійним порядком, так і з ієрархічно вкладеним співпадінням елементів. Приклади даних з такою подвійною лінійно-ієрархічною структурою включають виконання структурованих програм, анотованих лінгвістичних даних і документів HTML/XML.  Вкладене слово складається з послідовності лінійно впорядкованих позицій, доповненої полями вкладеності, що з’єднують виклики з поверненням (або відкриті теги з закритими тегами). Поля не перетинаються, створюючи правильно вкладену ієрархічну структуру, і ми дозволяємо деяким сторонам перебувати в очікуванні. Ця структура вкладеності може бути унікально представлена послідовністю, яка визначає типи позицій (виклики, повернення і внутрішні елементи). Вкладені слова узагальнюють як слова, так і впорядковані схеми, і дозволяють виконувати операції над словом і схемою.

Автомати вкладених слів – кінцеві акцептори для вкладених слів, які визначають клас регулярних мов вкладених слів. Цей клас має всі привабливі теоретичні властивості, якими володіють класичні регулярні мови слів: детерміновані вкладені автомати слів так само виразні, як і їх недетерміновані аналоги; клас закритий в об’єднанні, перетином, доповненням, конкатенацією, Кліні (Kleene -*), префіксами і гомоморфізмами мови. Членство, пустота, включення мови та еквівалентність – все це  допустимо. Визначність в монадичній логіці другого порядку точно відповідає розпізнаваності кінцевого стану. Ці результати також узагальнюються на нескінченні вкладені слова.

Як вони співвідносяться з мовами слів вільними від контексту?

При подачі мови L вкладених слів над алфавітом, лінійне кодування вкладених слів дає мову L ‘ над позначеним алфавітом, що складається з символів, позначених типом позиції. Якщо L – звичайна мова вкладених слів, то L ‘ не містить контексту. Фактично, автомат з магазинною памяттю, включаючи L’, має спеціальну структуру: при читанні виклику автомат повинен натиснути один символ, при читанні символу повернення він повинен видалити один символ (якщо стек не порожній), а при читанні внутрішнього символу він може тільки оновити стан управління. Ми називаємо такі автомати називаються  автоматами з видимим відтінком  (visibly pushdown automata), а клас мови слів, які вони приймають видимий відтінок мов (visibly pushdown languages VPL). Оскільки наші автомати можуть визначатись, VPL відповідають підкласу детермінованих контекстно-вільних мов (DCFL). VPL узагальнюють парантезіс (paranthesis) мов, (мов взятих в дужки), і збалансованих мов, і вони мають кращі властивості закриття, ніж CFLs, DCFLs, або мови парантезіс.

Ми стверджуємо, що для алгоритмічної перевірки структурованих програм замість того, щоб розглядати програму як контекстно-вільну мову над словами, слід розглядати її як звичайну мову вкладених слів (або, що те ж саме, видимі відтінки мови), і це дозволило б перевіряти моделі багатьох властивостей (таких як перевірка стеку, попередні умови), які не виражаються в існуючих логіках специфікацій.

В цілому, автомати магазинної пам’яті служать двом різним цілям: виявленню ієрархічного відповідності та обробці / запиту відповідності. У додатках, де актуальна тільки друга мета (як в аналізі програм), можна замінити магазинні автомати на NWA та отримати багато переваг.

Як вони ставляться до впорядкованих схем?

Дані з подвійною лінійно-ієрархічною структурою традиційно моделюються за допомогою двійкових і, в більш загальному плані, з використанням впорядкованих нерейтингових схем і запитів з використанням деревовидних автоматів. В упорядкованих схемах вузли з одним і тим же батьківським елементом лінійно впорядковані, а класичні обходи дерева, такі як інфікс (або спершу глибші зліва направо), можуть використовуватися для визначення невидиміго порядку всіх вузлів. Виявляється, хеджування, де воно є послідовністю впорядкованих схем, є особливим класом вкладених слів, а саме, тих, які відповідають словами Dyck, а регулярні мови хеджування відповідають збалансованим мовам.

Для обробки документів вкладені слова мають багато переваг перед впорядкованими схемами. Подання на основі деревовидної структури невидимі припускає, що вхідні лінійні дані можуть бути проаналізовані в схемі, і, таким чином, не можна уявити і обробити дані, які можуть бути неправильно проаналізовані. Операції Word, такі як префікси, суфікси та конкатенації, хоча і природні для обробки документів, не мають аналогічних операцій для схем. По-друге, деревовидні автомати можуть природно виражати обмеження на послідовність міток уздовж ієрархічного шляху, а також уздовж однорівневих вузлів зліва направо, але їм важко захопити обмеження, які відносяться до глобального лінійного порядку. Наприклад, запит, з паттерном p1,… pk з’являється в документі в такому порядку, компілюється в детермінований автоматон слова (і, отже, детермінований NWA) лінійного розміру, але стандартний детермінований знизу вгору деревовидний автомат для цього запиту повинен мати експоненціальний розмір k. NWA можна розглядати як свого роду деревовидні автомати, так що як нижні, так і верхні деревовидні автомати є приватними випадками. Ці результати означають, що запит може бути більш лаконічно закодований в представленні вкладених слів з перевагами складності. вкладений автомат слова читає слово зліва направо, обробляючи поля вкладеності в міру їх надходження. Це відповідає SAX API для XML і, таким чином, має природне використання в потокових алгоритмах.

Посилання

Модель вкладених слів пройшла через кілька ітерацій: див. Мови зниження Видимості; Алур і Мадхусудан; STOC 2004; і Додавання структури вкладеності у слова; Алур і Мадхусудан,; DLT 2006. Ми рекомендуємо ознайомитися з цією уніфікованою повною версією (журнал ACM, 2009). Запрошена доповідь на CSR 2007 також є хорошою відправною точкою.

Інструменти

  • OpenNWA: бібліотека автоматів вкладених слів; Дріскол, Такур і Репс; CAV 2012.
  • Бібліотека кінцевих автоматів (Ultimate Automata Library); Хейзман, Нуц і Шилінг, 2017.

Додаткові проблеми прийняття рішень по VPA / NWA

  • Видимі магазинні ігри; Лодінг, Мадхусудан, і Серр; FSTTCS 2004.
  • Видимі магазинні автомати: від мовної еквівалентності до моделювання та бісимуляції; Сбра; CSL 2006.
  • Проблеми регулярності для видимі магазинних мов; Барані, Лодінг і Серре; STACS 2006.
  • Про проблему членства для видимі магазинних мов; Ла Торре, Napoli і Parente; ATVA 2006.
  • Символічні видимі магазинні автомати; D Antoni і Alur; CAV 2014.

Конґруенції та мінімізація

  • Конгруенції для видимі магазинних мов; Алур, Кумар, Мадхусудан і Вішванатан; ICALP 2005.
  • Мінімізація, навчання і тестування відповідності булевих програм; Кумар, Мадхусудан і Вішванатан; CONCUR 2006.
  • Мінімізують варіанти явних магазинних автоматів; Червет і Валукевич; MFCS 2007.
  • Мінімізація явних магазинних автоматів з використанням часткового Max-SAT; Хейзман, Шілінг і Тіщнер; TACAS 2017.

Тимчасова і фіксована логіка; виразність

  • Часова логіка вкладених викликів і повернень; Алур, Етессамі, Мадхусудан; TACAS 2004.
  • Регулярні мови вкладених слів: нерухомі точки, автомати і синхронізація; Arenas, Barcelo і Libkin; ICALP 2007.
  • Першопорядкові і темпоральні логіки для вкладених слів, Алур, Аренас, Барсело, Етессамі, — місіс Тіммерман, і Лібкін; LICS 2007.
  • Чергувальні автомати і тимчасове обчислення фіксованих точок для видимі магазинних мов; Bozzelli; CONCUR 2007.
  • Граматична репрезентація явних магазинних мов; баран і Барринджер; WoLLIC 2007.
  • Зважена логіка для вкладених слів і алгебраїчних формальних статечних рядів; Матіссен; ICALP 2008.
  • Помітно раціональні вирази; Боззеллі і Санчес; FSTTCS 2012.
  • Помітно лінійна тимчасова логіка; Боззеллі і Санчес; IJCAR 2014.

Специфікації для аналізу програми

  • Аспекти на основі VPA: краща підтримка AOP за протоколами; Нгуєн і Судхольт; SEFM 2006.
  • Інструментування C-програм з вкладеними словесними моніторами; Чаудхурі і Алур; SPIN 2007.
  • Синтезування моніторів для властивостей безпеки — це час з дзвінками і поверненнями; Росу, Чен, і Болл; RV 2008.
  • Тимчасові міркування для процедурних програм; Алур і Чаудхурі; VMCAI 2010.
  • Вкладені інтерполянти; Хайцманн, Хоеніке, і Поделскі; POPL 2010.
  • Перевірка сумісності виробника і споживача; Дрскол, Бартон, Репс; FSE 2011.
  • Безпечне програмування через видимі ігри магазинної безпеки; Харріс, Джа і Репс; CAV 2012.

Обробка XML і деревовидні автомати

  • Видимі магазинні ефекти виразів для обробки XML потоку; Пітчер; план-X 2005.
  • Видимі магазинні мови для потокової передачі XML; Кумар, Мадхусудан, і Вішванатан; WWW 2007.
  • З’єднання слова і схеми; Алур; стручки 2007.
  • Переписування явних магазинних мов для впровадження даних по XML; Томо і Венкатеш; CIKM 2008.
  • Потокова автоматна схема; Гаувін, Ніехрен, і Роос; Обробка інформаційних листів 2009.
  • Сама рання відповідь на запит для детермінованих вкладених автоматів слів; Гаувін, Ніехрен і Тісон; FCT 2009.
  • Автомати запитів для вкладених слів; Мадхусудан і Вішванатан; MFCS 2009.
  • Від регулярних виразів до вкладених слів: уніфікація мов і виконання запитів для реляційних і XML послідовностей; Мозафарі, Женг, Заніоло; VLDB 2010.
  • Високопродуктивна комплексна обробка подій по XML потоках; Мозафарі, Женг, Заніоло; SIGMOD 2012.
  • Стрімінгові фрагменти наступного XPath; Гаувін і Ніегрен; CIAA 2012.
  • Раннє виділення вузлів в XPath на XML-потоках; Дебарбо, Гаувін, Ніегрен, Себастьян, і Жергаві; 2012.

Перетворювачі

  • Видимі магазинні датчики для приблизної перевірки потокової передачі XML; Томо, Венкатеш і Йе; FoIKS 2008.
  • Видимі магазинні датчики; Раскін і Сервос; ICALP 2008.
  • Еквівалентність детермінованих вкладених слів словам перетворювачам; Ставорко, Лоренц, Лемей, Ніегрен; FCT 2009.
  • Властивості явних магазинних перетворювачів; Е. Філло, Ж.-Ф. Раскін, П.-А. Реньє, Ф. Серве і Ж.-М. Талбо; MFCS 2010.
  • XEvolve: Основи еволюції схеми XML; Ф. Пікалауса, Ф. Серве і Е. Жіманий ; SACSVT 2011.
  • Можливість стрімінгу вкладених слів трансдукції; Е. Філіот, О. Гаувін, П.-А. Реньє, Ф. Серве. FSTTCS 2011.
  • Потокове перетворювачі дерево; Р. Алур і Л. Д Ентоні; ICALP 2012.
  • Видимі магазинні датчики з поглядом-вперед. Е. Філіо і Ф. Серве. SOFSEM 2012.

Вкладені схеми

  • Обчислення фіксованих точок для локальних і глобальних програмних потоків; Алур, Чаудхурі і Мадхусудан; POPL 2006.
  • Мови вкладених схем; Алур, Чаудхурі і Мадхусудан; CAV 2006.
  • Видимі магазинні мови і переписування умов; Чабин і Реті; FroCos 2007.
  • Видимі деревовидні автомати з пам’яттю і обмеженнями; Комон-Лаун, Джакмар, Перрін; логічні методи в інформатиці 2008.

Слова з множинними вкладеннями

  • Примітка про вкладені слова; Бласс і Гуревич; Microsoft Research TR; 2006.
  • Надійний клас контекстно-залежних мов; Ла Торре, Мадхусудан і Парлато; LICS 2007.
  • 2-видимі магазинні автомати; Каротенуто, Мурано і Перон; DLT 2007.
  • Реалізація паралельних рекурсивних програм; Болліг, Гріндей і Габермель; FoSSaCS 2009.

Нові результати з використанням видимості викликів / повернень

  • Ідеалізований Алгол третього порядку з ітерацією дозвоів; Муравський І Валукевич; FoSSaCS 2005.
  • Синхронізація магазинних автоматів; Caucal; DLT 2006.
  • Пропозиціональна динамічна логіка з рекурсивними програмами; Лодінг і Серре; FoSSaCS 2006.
  • Високо-детерміновані магазинні автомати; Новотка і Срба; ПМП 2007.
  • Нескінченна автоматна характеристика подвійного експоненціального часу; Ла Торре, Мадхусадан і Парлато; CSL 2008.

Складна відкрита проблема (Тепер вирішена!)

Розглянемо наступне питання: дано дві регулярні мови L1 і L2 вкладених слів, існує регулярна мова R слів с позначками алфавіту, що перетину (R,L1), чи рівна вона L2? Це, як відомо, не дозволено, навіть для приватного випадку, коли L1 є безліччю всіх добре підібраних слів. Мотивація наступна: в загальному випадку, щоб перевірити, чи належить вхід L2, обробній машині потрібен стек. Але припустимо, що у нас вже є деякі додаткові знання про вході, що він належить множині L1 (наприклад, ми можемо знати, що вхід добре узгоджений), чи можуть ці знання бути використані для побудови DFA таким чином, що для входів в L1 A може вирішатися приналежність до L2. Ця проблема натхненна документом «перевірка потокових XML-документів» Сегуфіна і Віану, PODS 2002, який також представляє часткове рішення.

Нещодавно Ерік Копчинський довів невирішеність цієї проблеми: Див. Невидимі відтінки мови, LICS 2016.