ТЕОРЕТИЧЕСКИЕ ВОПРОСЫ ПРОГРАММИРОВАНИЯ
УДК 681.3.06
ОБ УНИФИКАЦИИ ПОВЕДЕНЧЕСКИХ ЭКВИВАЛЕНТНОСТЕЙ ВРЕМЕННЫХ СИСТЕМ ПЕРЕХОДОВ*
© 2010 г. И. Б. Вирбицкайте, Н. С. Грибовская
Институт систем информатики им. А.П. Ершова СО РАН 630090 Новосибирск, пр. Ак. Лаврентьева, 6 Новосибирский государственный университет 630090 Новосибирск, ул. Пирогова, 2 E-mail: virb@iis.nsk.su, moskalyova@iis.nsk.su Поступила в редакцию 21.07.2008 г.
Временные системы переходов являются одной из самых популярных параллельных моделей с реальным временем. В работе определяются и исследуются различные поведенческие эквивалентности временных систем переходов. В частности, строятся категории данной модели и изучаются их свойства, а также на основе метода открытых морфизмов дается абстрактная характеризация рассматриваемых эквивалентностей. Такой подход позволяет разработать мета-теорию, предназначенную для унифицированного определения и исследования временных поведенческих эквивалентностей в спектре семантик "линейное время - ветвистое время".
1. ВВЕДЕНИЕ
Поведенческие эквивалентности обычно используются при спецификации и верификации систем с целью сравнения их поведения, а также упрощения их структуры. В теории параллельных систем и процессов известно большое разнообразие поведенческих эквивалентностей, взаимосвязи между которыми хорошо изучены в литературе (см., например, [1]). Можно выделить два критерия классификации семантик, относительно которых определяются и исследуются модели и эквивалентности параллельных недетерминированных систем. Первый критерий -степень точности, с которой учитываются точки недетерминированного выбора альтернативных действий системы. На основе этого критерия был сформирован так называемый спектр семантик "линейное время - ветвистое время" (linear time - branching time spectrum). Типичным представителем семантики линейного времени является трассовая эквивалентность [2]. При трассовом подходе сравниваются поведения
* Данная работа частично финансируется DFG-РФФИ (грант 436 RUS 113/1002/01, грант 09-01-91334).
систем, представленные в виде множеств последовательностей действий, выполняемых системами, - т.е. в виде языков систем. Такой подход полностью игнорирует информацию о недетерминированном выборе. Представителем противоположного края спектра - семантики ветвистого времени - является бисимуляционная эквивалентность [3, 4], строго учитывающая точки выбора дальнейших альтернативных выполнений системы. Две системы считаются бисимуля-ционно эквивалентными, если внешний наблюдатель не может обнаружить различий в поведении систем с учетом точек недетерминированного выбора. Между крайними представителями спектра находится понятие тестовой эквивалентности [5]. При тестовом подходе поведение систем исследуется на основе набора тестов: две системы считаются тестово эквивалентными, если они проходят один и тот же набор тестов. На основе второго критерия классификации семантик был построен так называемый спектр "интерливинг - частичный порядок". Семантики различаются по степени, с которой учитывается отношение причинной зависимости между действиями системы, представленное частичным порядком, причем отсутствие частичного
19
2*
порядка между действиями системы означает, что эти действия параллельны. В интерливин-говой семантике выполнение системы моделируется последовательностью выполняемых действий, не отражающей явно их причинную зависимость. Было сделано много попыток выйти за пределы интерливингового подхода, чтобы позволить внешнему наблюдателю с помощью эк-вивалентностей различать системы, учитывая параллелизм, используемый в их вычислениях. Как результат, в литературе появилось множество эквивалентностей, основанных на моделировании причинной зависимости с помощью частичных порядков (см. также [6]). Кульминацией таких разработок стала сохраняющая историю бисимуляция, впервые предложенная для сетей Петри [7], а затем адаптированная для структур событий [6].
В середине 90-х годов прошлого столетия с целью классификации и унификации большого разнообразия известных поведенческих эквива-лентностей параллельных систем было предложено на основе метода открытых морфизмов абстрактное понятие бисимуляции, позволяющее единообразно определять различные эквивалентности для широкого класса моделей. Сначала строится категория моделей вычислений, затем выбирается подкатегория "наблюдений", относительно которой вводится понятие открытого морфизма; две модели считаются абстрактно бисимуляционно эквивалентными, если существует специальная конструкция открытых мор-физмов. Первыми, кто показал применимость такой схемы для унификации поведенческих эк-вивалентностей, были Винскель, Нильсен и Джо-яль [8]. Оказалось, что абстрактная эквивалентность, определенная на категориях интерливин-говых моделей систем переходов, согласуется с интерливинговой бисимуляцией, тогда как эквивалентность на категориях моделей с явным представлением параллелизма действий системы - структур событий и систем переходов с независимостью - требует некоторого более сильного варианта сохраняющей историю бисимуля-ции. В работе [9] по предложенной схеме была выполнена унификация и других эквивалентнос-тей - трассовой, тестовой, слабой бисимуляцион-ной, и т.д. Кроме того, в статьях [10, 11] была дана теоретико-категорная характеризация поведенческой бисимуляционной эквивалентности на моделях высших размерностей.
Известно, что анализ поведения параллельных систем реального времени - сложная задача, решение которой невозможно без привлечения формальных методов и средств. С этой целью за последнее десятилетие были разработаны различные модели, учитывающие временные характеристики функционирования систем, - временные автоматы [12], временные системы переходов [13], временные алгебры процессов [14, 15], временные сети Петри [16, 17], временные структуры событий [18, 19] и т.д. Понятие времени также было введено и в поведенческие эквивалентности. Разрешимость временной бисимуляции для автоматных моделей с непрерывным временем была показана с использованием техники регионов [20, 21] и техники зон [22]. Полная аксиоматизация временной бисимуляции для класса регулярных временных CCS-процессов была разработана в [23]. В статье [20] изучаются временные и безвременные трассовые и бисимуля-ционные эквивалентности и их конгруэнтность относительно меняющегося количества временных счетчиков, введенных в модель временных систем переходов. В контексте формальных моделей систем, для которых не известны точные временные характеристики их функционирования, в работе [24] были определены специальные функции, характеризующие степень близости (точности совпадения поведения) моделируемых систем и обобщающие понятия временной симуляции и временной бисимуляции. Временная бисимуляция с ветвлением (timed branching bisimulation) на моделях временных систем переходов, которая действительно является отношением эквивалентности, была введена в работе [25]. Операционная и денотационная харак-теризации временных тестовых предпорядков в рамках модели систем переходов разработаны в статье [26]. Разрешимость тестовой эквивалентности для временных систем переходов показана в [27]. Тестовый подход был расширен на модели с семантикой частичного порядка - временные сети Петри [28] и временные структуры событий [29]. Иерархия взаимосвязей временных эквивалентностей в семантиках "интерливинг - частичный порядок" и "линейное время -ветвистое время" в контексте структур событий с непрерывным временем построена в статье [30]. Особо отметим, что метод унифициро-
ванной характеризации, предложенный в [8], был распространен и на временные поведенческие эквивалентности. С помощью механизма открытых морфизмов было дано абстрактное определение бисимуляции для временных систем переходов [31] и временных автоматов высших размерностей [32]. Теоретико-категорное доказательство того факта, что временная задержанная биси-муляция (timed delay bisimulation) действительно является отношением эквивалентности на моделях временных систем переходов, было представлено в работе [33]. В статье [19] были получены теоретико-категорные бисимуляции, которые, как было установлено, совпадают с временными расширениями эквивалентностей с частичным порядком из спектра "линейное время -ветвистое время" в контексте временных структур событий.
Данная работа является развитием подхода, предложенного в статье [31]. В дополнение к бисимуляционной эквивалентности определяются и исследуются трассовая и тестовая эквивалентности временных систем переходов. В частности, строятся категории данной модели и изучаются их свойства, а также на основе метода открытых морфизмов дается абстрактная харак-теризация рассматриваемых эквивалентностей. Такой подход позволяет, во-первых, убедиться в том, что введенные эквивалентностные понятия действительно являются отношениями эквивалентности временных систем переходов; во-вторых, унифицированно определять различные эквивалентности и переносить понятие бисиму-ляции из одной семантики в другую; в-третьих, применять некоторые общие результаты теории категорий (например, характеристические логики и игры, существование канонических моделей) для конкретных временных эквивалентнос-тей.
Оставшаяся часть статьи организована следующим образом. В разделе 2 вводятся основные понятия и обозначения, связанные со структурой и поведением временных систем переходов. В разделе 3 дается краткий обзор результатов статьи [31] по теоретико-категорной характери-зации временной бисимуляции. В двух последующих разделах определяются и исследуются временная трассовая и временная тестовая эквивалентности. В частности, вводятся две категории
временных систем переходов, выделяются подкатегории "наблюдений", позволяющие определить соответствующие понятия открытых мор-физмов, и приводятся теоретико-категорные ха-рактеризации временной трассовой и временной тестовой эквивалентностей в терминах открытых морфизмов. Заключение находится в разделе 6. В приложении напоминаются некоторые понятия теории категорий, используемые в работе.
2. ВРЕ
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.