автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Методы спецификации и верификации параллельных моделей с непрерывным временем

Введение

1 Метод верификации на основе темпоральной логики реального времени ТСТЬ

1.1 Определение временной сети.

1.2 ТСТЬ: синтаксис и семантика.

1.3 Алгоритм проверки на модели.

1.4 Повышение эффективности путем использования частичных порядков . ".

2 Метод параметрической верификации на основе параметрической темпоральной логики реального времени РТСТЬ

2.1 Определение параметрической временной сети

2.2 РТСТЬ: синтаксис и семантика.

2.3 Построение графа обобщенных состояний.

2.4 Алгоритм поведенческого анализа.

3 Метод верификации на основе параллельной темпоральной логики реального времени ТССТЪ

3.1 Построение древесной структуры состояний временной сети

3.2 ТССТЬ: синтаксис и семантика.

3.3 Верификационный алгоритм.

Актуальность проблемы. Параллельная обработка информации широко используется для увеличения производительности вычислительных систем. Особое место среди параллельных систем занимают системы реального времени, поведение которых в значительной степени зависит от количественных временных характеристик. Процесс проектирования систем такого типа — нетривиальная задача, требующая для своего решения фундаментальных исследований, основанных на различных формальных методах и средствах, которые варьируются в зависимости от класса моделируемых систем, степени детализации их структуры и поведения, а также от характера изучаемых проблем.

Для систем реального времени важны как модели времени, так и модели вычислений. Известны следующие дихотомии при задании временных характеристик: явное/неявное, линейное/ветвистое, ссылками на временные точки/интервалы, в непрерывной/дискретной временной области. Введение временных характеристик привело к появлению многих специализированных моделей вычислений с известными различиями: синхронные/асинхронные, с глобальным/локальным временем, интерливинговые/"истинно" параллельные, соотношением между действиями и временем (действия с нулевыми задержками).

Наиболее популярными среди формализмов систем реального времени являются как интерливинговые модели: временные автоматы [9], временные системы переходов [26], алгебры временных процессов [45], так и модели "истинного параллелизма": временные структуры событий [29], временные причинно-следственные структуры [7], временные и стохастические сети Петри [33, 14, 46, 43, 57]. При интерливинговом подходе параллелизм событий моделируемой системы линеаризуется, то есть моделируется последовательной реализацией параллельных событий в произвольном недетерминированном порядке. Достоинством такого подхода является его простота и математическая элегантность. Однако параллелизм вычислений сводится к некоторой форме недетерминизма. Альтернативный подход основывается на моделях с "истинным параллелизмом", в которых все события изначально предполагаются независимыми. Отношение причинной зависимости между событиями задается частичным порядком, а отношение параллелизма - отсутствием такого порядка. Данные модели являются более приемлемыми для изучения таких свойств параллельных систем, как отсутствие тупиков, "справедливость", максимальный параллелизм.

К достоинствам временных сетей Петри следует отнести удобное графическое представление, а также то, что благодаря семантике "истинного параллелизма" , данный формализм позволяет моделировать параллелизм системы естественным образом. Как правило, временные модели являются расширением традиционных моделей параллельных/распределенных систем за счет введения понятия времени. Так, временные сети Петри являются расширением сетей Петри [4], для которых существуют хорошо разработанные алгоритмы анализа поведенческих свойств [1].

Впервые временное расширение сетей Петри было предложено Рамхандани [43]. Существуют различные способы введения понятия времени в сеть Петри. Время может быть сопоставлено различным элементам сети Петри (местам, переходам, дугам, фишкам, шагам). При этом различают временные ограничения, которые сопоставляют некоторому элементу временной сети Петри фиксированную временную величину, и временные элементы счетчики, контролирующие локальное или глобальное время. Временная информация может быть представлена как одним числом (что соответствует дискретному представлению времени), так и интервалом (что соответствует непрерывному представлению времени). В модели может предполагаться принуждение к срабатыванию переходов, то есть невозможность превышения заданных временных границ. Отдельным вопросом является наличие автопараллелизма в модели, а также возможность наличия в месте фишек с разными временными параметрами. В таблице 1 приведена информация о некоторых существующих моделях временных сетей Петри.

Темпоральные логики являются удобным формализмом для спецификации и верификации свойств параллельных и распределенных систем. В данной проблематике сформировалось два подхода: аксиоматический и алгоритмический. При первом подходе разрабатывается система аксиом, с помощью которой может быть описана как сама система, так и ее свойства [17]. Для верификационных целей используется механический доказыватель теорем. Основу второго подхода составляют алгоритмы проверки на моделях (model checking), объединяющие в себе традиционные и логические методы анализа свойств параллельных/распределенных систем [19]. Основная цель исследований в этой области состоит в том, чтобы сформулировать ясную логическую основу для создания автоматических систем верификации, синтеза и оптимизации параллельных систем.

Среди языков темпоральной логики, используемых для анализа параллельных систем различают логики линейного времени (linear-time) и логики ветвящегося времени (branching-time). Если представлять поведение системы в виде множества возможных последовательностей реализаций ее событий, то теряется информация не только о параллелизме, но также и о конфликтных событиях (недетерминированном выборе), то есть пропадает информация о ветвящейся структуре системы. Такой подход соответствует семантике линейного времени. Чтобы избежать этого недостатка поведение системы описывается древовидными структурами, которые показывают точки недетерминированного выбора при вычислениях, что соответствует семантике ветвящегося времени.

Кроме того, темпоральные логики различаются по набору темпоральных операторов. Часто используются операторы "всегда" □ и "иногда" О (или, с учетом направления времени, — "всегда в прошлом" О, "всегда в будущем" □ , "иногда в прошлом" О, "иногда в будущем" О), являющиеся по существу адаптацией модальных операторов "необходимо" и "возможно". Специфику временной области лучше учитывают оператор Until и двойственный к нему оператор Since. Неформально, формула фЫф истинна, если существует некоторый момент времени, в который истинна формула ф, и во все предшествующие ему моменты времени истинна формула ф. Соответственно, формула фЫф истинна, если ложна формула -iфЫ-^ф. Операторы Оф и Оф при этом могут быть определены как ЬгиеЫф и falseЫф, соответственно. Логики дискретного времени содержат также оператор Next ("в следующий момент"), позволяющий анализировать поведение системы в следующем состоянии.

Чтобы специфицировать количественные временные характеристики функционирования систем реального времени необходимо явно ввести в логический язык понятие времени. Для этих целей, как правило, используется один из следующих приемов: операторы с временными границами [31, 20, 8, 11], полукванторы по времени (freeze quantification) [11, 27,13] и явные ссылки на таймер [38, 40, 11]. При первом подходе темпоральная логика реального времени содержит множество темпоральных операторов с явно заданными временными интервалами. Например, формула фЩ^ истинна, если в некоторый момент времени из интервала I истинна формула и во все предшествующие моменты времени истинна формула ф\. В логике с полукванторами по времени формуле может предшествовать полуквантор х., сопоставляющий переменной х значение текущего временного контекста. Например, формула х.ф(х) истинна в момент времени t тогда и только тогда, когда истинна формула ф{Ь). Такие логики допускают в качестве элементарных формул элементарные временные ограничения такие, как сравнение и простейшие операции со временем (например, сложение). Логика с явной ссылкой на таймер связывает с таймером переменную, областью значений которой является заданная временная область. Данная переменная сопоставляет состоянию системы соответствующий ему момент времени. Сведения о некоторых темпоральных логиках реального времени приведены в таблице 2.

Модель Времени Времеш ой элем юе огрг эл/огр гент сет!у/ шичение S1 S2 1 Интервал/ Длительность сраб'. Принуждение к сраб. Одиночное/ пошаговое сраб. Глобальное/ локальное вр.

Места Перех. Дуги Фишки Шаги

RAMCHANDANI [36] Timed net эл/огр нет нет длительность нет одиночное локальное

SIFAKIS [39] Place timed net огр эл — есть длительность нижняя врем, граница макс, шаг локальное

MERLIN [28] Time net эл/огр нет нет интервал верхняя врем, граница одиночное локальное

ZUBEREK [50] эл нет нет длительность нижняя врем, граница макс, шаг локальное

BERTHOMIEU DIAZ [10) Time net эл нет есть интервал верхняя врем, граница одиночное локальное

VAN DER AALST [42] ITPN эл огр есть есть длительность/ интервал нижняя врем, граница одиночное глобальное

WALTER [47] Arc timed net огр эл есть нет интервал 1 верхняя врем, граница пошаговое локальное

HANISCH [18] Arc timed net эл огр нет нет интервал нижняя врем, граница пошаговое локальное

NEUEDORF [30] Chameleon net эл эл нет нет интервал/ длительность верхняя врем, граница пошаговое локальное

Si - различимость фишек по времени, S2 - автопараллелизм

Таблица 1.

MTL [11] логика линейного времени с операторами с временными границами, в качестве темпоральных операторов используются ограниченные версии операторов Until, Next, Since.

TPTL [10] логика линейного времени, использующая в качестве элементарных временных ограничений сравнение, сравнение по модулю и добавление целого; темпоральные операторы Until, Next.

RTTL [38] логика линейного времени с явной ссылкой на таймер, с теми же временными примитивами и темпоральными операторами, что и TPTL.

XCTL [25] логика линейного времени с явной ссылкой на таймер, со сравнением и сложением в качестве элементарных временных ограничений; разрешает сложение временных переменных, но запрещает явные кванторы по ним.

TCTL [8] логика ветвящегося времени с операторами с временными границами, в качестве темпоральных операторов используется ограниченная версия оператора Until.

Таблица 2.

Алгоритмы анализа параллельных/распределенных систем широко используют темпоральные логики для задания верифицируемых свойств. Известно, что к сетевым моделям могут быть применены эффективные и довольно мощные алгоритмы верификации. В работе [47] на базе темпорального языка СТЬ были предложены дедуктивный и алгоритмический методы верификации свойств элементарных сетевых систем. В статье [28] вводится темпоральная логика для анализа ряда свойств 'справедливости' помеченных сетей Петри. Алгоритм проверки поведенческих свойств сетей высокого уровня с использованием Б-инвариантов, представленных в виде логических формул, разработан в работе [36]. Однако исследования по верификации свойств временных сетей Петри значительно менее продвинуты. Верификационный алгоритм для временных сетей Петри и темпоральной логики линейного времени был предложен в [56]. Интересной задачей является верификация количественных свойств систем реального времени. Так, в работе [8] был предложен алгоритм верификации свойств временных автоматов средствами темпоральной логики реального времени ТСТЬ.

Применение логик реального времени для верификации временных сетей Петри является новой интересной задачей теории параллельных/распределенных систем. Очевидно, что при верификации реальных систем приходится анализировать огромное число состояний. Один из способов преодоления этой проблемы состоит в применении техники частичных порядков [23, 34, 48], которая позволяет редуцировать число верифицируемых состояний за счет параллелизма, присущего системе. Применение данного подхода при верификации временных сетей Петри средствами темпоральной логики реального времени ТСТЬ позволяет опробовать новую, перспективную технику редукции на стандартной, хорошо изученной модели систем реального времени.

Традиционно используемые модели систем реалььного времени (в частнос-сти, временные сети Петри) требуют детальной спецификации временных ограничений и при "настройке" системы каждое изменение временных ограничений влечет новый "прогон" верификационнго алгоритма. Интересной задачей является создание временной модели, допускающей менее подробную спецификацию временных ограничений. Одним из подходов к решению этой задачи является введение параметров во временные спецификации. В качестве средства описания свойств системы при верификации подобной параметрической модели естественно выбрать формализм, позволяющий выражать свойства с параметрическими временными ограничениями. Таким формализмом является, например, параметрическая темпоральная логика реального времени РТСТЬ. Для модификации временных сетей Петри за счет введения параметров задача верификации состоит в нахождении значений параметров, при которых выполнено проверяемое свойство.

Другой задачей, возникающей при верификации систем реального времени является проверка свойств параллелизма. Существующие темпоральные логики реального времени не позволяют напрямую описывать свойства, связанные с параллелизмом, поскольку они не различают точек параллельного ветвления и точек недетерминированного выбора. С другой стороны, поскольку временные сети Петри являются моделью "истинного параллелизма" и позволяют явно выражать параллелизм системы, для их анализа требуется логика, позволяющая выражать как количественные характеристики, так и параллельные свойства.

Таким образом, в области верификации параллельных систем реального времени актуальными являются, с одной стороны, задачи увеличения выразительной мощности временных моделей и темпоральных логик, с другой — задачи повышения эффективности верификационных алгоритмов.

Цель диссертации. Введение и изучение системы формальных понятий, методов и средств спецификации и анализа поведения систем реального времени, представленных сетями Петри с непрерывным временем. Достижение цели связывается с решением следующих задач:

1. Разработка новых темпоральных языков реального времени с элементами параллелизма, позволяющих специфицировать и верифицировать поведение параллельных/распределенных систем реального времени.

2. Увеличение выразительных мощностей средств описания и изучения систем реального времени посредством введения параметров во временные спецификации.

3. Построение эффективных процедур верификации поведенческих свойств параллельных систем реального времени, представленных в виде различных моделей сетей Петри с непрерывным временем.

Методы исследования. В качестве формальной модели параллелизма используются временные сети Петри, а также их подклассы (временные сети, удовлетворяющие прогресс-условию; безопасные временные сети) и расширения (параметрические временные сети). В рамках данной работы используется такой формализм, как аппарат темпоральных логик. Кроме того, применяются методы теории графов, теории множеств и линейного программирования.

Научная новизна состоит в разработке оригинального подхода к решению задач спецификации и верификации систем реального времени средствами различных логических формализмов. Научную новизну раскрывают следующие результаты:

• Введена и исследована новая модель параллельных систем реального времени — параметрические временные сети, которые являются модификацией временных сетей Петри за счет введения параметров в спецификации временных ограничений. Достоинство данной модели состоит в том, что не требуется детальная спецификация временных ограничений.

• Предложена новая темпоральная логика реального времени, содержащая средства для описания свойств параллелизма в системах реального времени. Такая логика позволяет адекватно описывать системы, представленные моделями с семантикой "истинного параллелизма".

• Разработаны алгоритмы верификации поведенческих свойств различных временных сетевых моделей с использованием аппарата темпоральных логик реального времени.

• Предложен метод редукции числа верифицируемых сетевых состояний, позволяющий учитывать как параллелизм сети, так и существенность временных ограничений при проверке заданного свойства.

Практическая ценность данных исследований состоит в возможности их использования при создании автоматизированных систем верификации систем реального времени. В частности, результаты диссертационной работы использовались при создании модуля верификации в системе PEP (Programming Environment based on Petri nets), совместно разрабатываемой Институтом информатики Университета г. Хильдесхайма (Германия) и лабораторией теоретического программирования ИСИ СО РАН.

Во время работы над диссертацией автор участвовал в следующих научных проектах и грантах:

1. Formal methods in design of concurrent/distributed systems. Volkswagen Stiftung (VS), грант 1/70 564, руководители Prof. Dr. elke Best и к.ф.-м.н. и.б. вирбицкайте, 1995-1997. (Публикации [50, 51].)

2. Разработка и исследование семантических методов и средств спецификации и верификации параллельных систем и процессов. РФФИ, грант 96-01-01655, руководитель к.ф.-м.н. И.Б. ВИРБИЦКАЙТЕ, 1995-1997. (Публикации [51].)

3. Methods and Tools for Verification and Analysis of Distributed Systems. INTAS-RFBR, грант 95-0378, руководитель к.ф.-м.н. В.А. НЕПОМНЯЩИЙ, 19971999. (Публикации [2, 3, 41, 50, 52, 42].)

Апробация работы проведена на следующих международных научных конференциях.

1. 4th Workshop on Logic, language, Information and Computation, Fortaleza (Ceara), Brazil, August 1997.

2. Distributed data processing (DDP'98), Novosibirsk, Russia, June 1998.

3. International Workshop on Discrete Event Systems (WODES'98), Cagliari, Italy, August 1998.

4. 1st International conference on practical and theoretical programming (Ukr-Prog'98% Kiev, Ukraine. September 1998.

Кроме того, полученные результаты обсуждались на семинарах лаборатории теоретического программирования ИСИ СО РАН и кафедры вычислительных систем НГУ.

Публикации. По теме диссертации опубликовано 10 научных работ. Из них 4 работы [5, 51, 52, 42] — на международных конференциях, одна [53] —в зарубежных изданиях, 2 работы [2, 3] — в центральных изданиях и 3 работы [б, 41, 50] — в местных изданиях.

Структура работы. В первой главе предлагается метод анализа поведенческих свойств систем реального времени, представленных временными сетями -Петри, основанный на темпоральной логике реального ветвящегося времени TCTL. С целью повышения эффективности метода применяется техника частичных порядков, позволяющая редуцировать число анализируемых сетевых состояний за счет параллелизма, присущего системе. Даны оценки сложности и показана корректность предложенного алгоритма. Основные определения, касающиеся временной сети и ее поведения, даны в разделе 1.1. Синтаксис и семантика темпорального языка реального времени TCTL рассматриваются в разделе 1.2. В разделе 1.3 строится граф обобщенных состояний и приводится базовый алгоритм пометки. Кроме того, вводится понятие временной статтеринг-эквивалентности на графах обобщенных состояний. В разделе 1.4 описано использование техники частичных порядков для редукции числа анализируемых обобщенных состояний временной сети и показана корректность данной редукции. Затемтгриведены некоторые сведения об экспериментальных результатах, подтверждающие эффективность такой редукции.

Во второй главе вводится понятие параметрической временной сети. Предлагается метод параметрического анализа систем реального времени, основанный на параметрической темпоральной логике PTCTL. Основные определения, касающиеся параметрической временной сети и ее поведения, даны в разделе 2.1. Синтаксис и семантика параметрического темпорального языка реального времени PTCTL рассматриваются в разделе 2.2. В разделе 2.3 строится конечное представление поведения параметрической временной сети в виде графа обобщенных состояний, а также вводится понятие кактус-структуры для определения временной длительности путей в графе. В разделе 2.4 приводится алгоритм поведенческого анализа, показывается корректность и дается оценка его временной сложности.

Третья глава посвящена введению новой логики непрерывного времени ТС-CTL и ее использованию для верификации поведения временных сетей. В разделе 3.1 вводится понятие поддерева на состояниях временной сети для представления параллельного поведения системы. Синтаксис и семантика темпоральной логики реального времени ТССТЬ рассматриваются в разделе 3.2. В разделе 3.3 строится конечное представление поведения временной сети в виде структуры обобщенных состояний, а также приводится алгоритм пометки на модели. Далее показывается корректность данного алгоритма и дается оценка его временной сложности.

Заключение

В рамках диссертации были полумены следующие результаты.

1. Разработан алгоритм верификации поведенческих свойств безопасных временных сетей на основе темпоральной логики реального времени ТСТЬ, который позволяет проверять не только качественные, но и количественные свойства сети.

• Построено дискретное представление поведения временной сети в виде графа обобщенных состояний на основе техники регионов.

• Предложен алгоритм пометки графа обобщенных состояний ТСТЬ-формулами.

• Продемонстрирована возможность применения техники "частичных порядков" для повышения эффективности предложенного алгоритма. Одна из отличительных черт данного метода состоит в возможности редукции графового представления поведения временной сети не только за счет ее параллельных переходов, но также и за счет сокращения числа состояний, полученных при истечении времени, не существенного для рассматриваемой ТСТЬ-формулы.

• Введено и исследовано понятие временной статтеринг-эквивалентно-сти для обоснования корректности предложенной редукции.

• Даны оценки сложности предложенных алгоритмов и доказана их корректность.

2. Введена и исследована новая модель параллельных систем реального времени — параметрические временные сети, а также предложены и оценены методы поведенческого анализа данной модели.

• Определено понятие параметрической временной сети, обеспечивающее более гибкую спецификацию временных ограничений системы, чем существующие временные модели.

• Понятие графа обобщенных состояний адаптировано к параметрической природе временных ограничений.

• Предложен и исследован верификационный метод, позволяющий осуществить "настройку" временных ограничений системы относительно проверяемого свойства.

3. Разработан метод верификации поведенческих свойств временных сетей с использованием аппарата параллельного темпорального языка реального ветвящегося времени ТССТЬ, позволяющего специфицировать количественные временные свойства, связанные с параллелизмом системы.

• Введена и исследована новая темпоральная логика реального времени ТССТЬ, содержащая средства для описания "истинного параллелизма" в системах реального времени.

• Предложено понятие поддеревьев на состояниях временной сети для характеристики параллельных выполнений системы.

• Построено конечное представление поведения сети в виде структуры обобщенных состояний, позволяющее различать в выполнениях системы точки параллельного ветвления и точки недетерминированного выбора.

• Предложен алгоритм анализа структуры обобщенных состояний средствами ТССТЬ. Дана оценка сложности алгоритма и доказана его корректность.

1. Ачасова С.М., бандман O.JI. Корректность параллельных вычислительных процессов, Новосибирск, 1990, 252 стр.

2. ВИРБИЦКАЙТЕ И.Б., Покозий Е.А. Использование техники частичных порядков для верификации временных сетей Петри. Программирование, N 1, 1999.

3. ВИРБИЦКАЙТЕ И.Б., Покозий Е.А. Метод параметрической верификации поведения временных сетей Петри. Программирование, N 4, 1999.

4. КОТОВ В.Е. Сети Петри, 1984, 149 с.

5. ПОКОЗИЙ Е.А. Поведенческий анализ параметрических временных сетей Петри. UkrProg'98 (1st International conference on practical and theoretical programming), сентябрь 1998, Киев, Украина, 111-119.

6. ПОКОЗИЙ Е.А. Метод верификации свойств параллелизма временных сетей Петри. Препринт 64, ИСИ, Новосибирск, 1999, 19 стр.

7. УСТИМЕНКО А.П. Отображение временных причинно-следственных структур во временные сети Петри. Кибернетика и системный анализ. Киев, N2, (1997), 44-54.

8. Alur, R., Courcoubetis, С., Dill, D. Model-checking for real-time systems. Proc. 5th IEEE LICS, (1990), 214-225.

9. Alur, R., Dill, D. The theory of timed automata. Lecture Notes in Computer Science 600 (1991) 45-73.

10. Alur, R., Henziger, T.A. A really temporal logic. Proc. of the 30th nnual Symposium on Foundation of Computer Science, IEEE Computer Society Press, (1989), 164-169.

11. Alur, R., henziger, T.A. Real-time logics: complexity and expressiveness. Proc. 5th IEEE LICS, (1990), 390-401.

12. Alur, R., henziger, T.A. Logics and models of real time: a survey. Lecture Notes in Computer Science 600 (1991) 74-106.

13. Alur R. Techniques for Automatic Verification of Real-Time Systems. PhD Thesis, Stanford University, (1991)

14. Best, e., grahlmann, B. PEP — more than a Petri net tool. Lecture Notes in Computer Science 1055 (1996) 397-401.

15. Boyer R.S., Moore J.S. Computation Logic Handbook. Academic Press, Volume 23 of Perspectives in Computing, (1988).

16. Burch, J.R., Clarke, E.M., McMillan, L., Dill, D., Hwang, J. Symbolic model checking: I020 and beyond. Proc. 5th IEEE LICS (1990) 428-439.

17. Clarke, E.M., Emerson, E.A., Sistla, A.P. Automatic verification of finite-state systems using temporal logic specifications. ACM TOPLAS 8(2) (1986) 244-263.

18. Emerson E.A., Мок А.К., Sistla A.P., Srinivasan J. Quantitative temporal reasoning. Proc. Isr Annual Workshop on Computer-aided Verification, (1989).

19. HaNISCH H.-M. Analysis of Timed Petri Nets by mens of Dynamic Graphs. Born, Germany: Gesellschaft fur Informatik (GI), Special Interest Group on Petri Nets and Related System Model, Petry Net Newletter, N36, (1990), 2431.

20. Henzinger, T.A., Manna, Z., Pnueli, A. An interleaving model for real time. Proc. 5th Jerusalem Conference on Information Technology, (1990), 717730.

21. Henzinger, T.A., Manna, Z., Pnueli, A. Timed transition systems. Lecture Notes in Computer Science 600 (1991) 226-251.

22. HENZINGER T.A. Half-order modal logic: how to prove real-time properties. Proc. 9th Annual Symposium on Principles of Distributed Computing, ACM Press, (1990), 281-296.

23. Howell, R.R., Rosier, L.E., Yen, H.-C. A taxonomy of fairness and temporal logic problems for Petri nets. Lecture Notes in Computer Science 324 (1988) 351-359.

24. KATOEN J.-P. Quatitative and Qualitative Extensions of Event Structures. PhD Thesis, Twente University, (1996).

25. Kis T., Neuendorf K.-P., The Benefit of Waiting. Proc. CS&P'97, October 1997, Warsaw, Poland, 93-104.

26. KOYMANS R. Specifying real-time properties with metric temporal logic. Realtime Systems, 2(4), (1990), 255-299.

27. LlLlUS, J. Efficient state space search for time Petri nets. Proc. MFCS'98 Workshop on Concurrency, August 1998, Brno (Czech Republic), FIMU Report Series, FIMU RS-98-06 (1998) 123-130.

28. MARSAN M.A. Stochastic Petri nets: elementary introduction. Lecture Notes in Computer Science 424 (1989) 1-29.

29. Neuendorf K.-P., Kiritsis D., Kis T., Xirouchakis P. Two-level Petri Net Modelling for Integrated Process and Job Shop Production Pinning. ICPTN'97, Proc. workshop Manufcturing nd Petri Nets, (1997), 135-150.

30. OSTROFF J.S. Temporal Logic of Real-time Systems. Research Studies Press. (1990).

31. PENCZEK, W. A concurrent branching time temporal logic. Lecture Notes in Computer Science 440 (1990) 337-354.

32. PNUELY A., HAREL E. Application of temporal logic to the specification of real-time systems. Lecture Notes in Computer Science 331, (1988), 84-98.

33. Roux, J-L., berthomieu, b. Verification of local area network protocol with Tine, a software package for time Petri nets. Proc. 7th European Workshop on Application and Theory of Petri Nets (1986) 183-205.

34. Schneider, S., Davies, J., Jackson, D.M., Reed, G.M., Reed, J.M., Roscoe, A.W. Timed CSP: theory and practice. Lecture Notes in Computer Science 600 (1991) 640-675.

35. VlRBITSKAITE, I.B., Pokozy, E.A., Towards Efficient Verification of Time Petri Nets. Logical Journal of IGPL 5(6) Oxford University Press (1997) 921924.

36. Virbitskaite, I.B., Pokozy, E.A., A partial order algorithm for verifying time Petri nets. Proc. International Workshop on Discrete Event Systems (WODES'98% August 1998, Cagliari, Italy. The IEE Publisher, London, 1998, 514-516.

37. VlRBITSKAITE, I.B., POKOZY, E.A., Parametric Behaviour Analysis for Time Petri Nets. Proc. PaCT-99, September 1999, St .-Petersburg, Russia. (To be published in Lecture Notes in Computer Science)

38. WALTER B. Timed Petri Nets for modelling and Analyzing Protocols with Real-time Characteristics. Protocol Specification, Testing and Verification III, Elsevier Science Publ. B. V., (1983), 149-159.

39. Wang F. Timing behavior analysis for real-time systems. Proc. 10th IEEE LICS (1995) 112—122.

40. Yoneda, T., Shibayama, A., Schlingloff, B.H., Clarke, E.M. Efficient verification of parallel real-time systems. Lecture Notes in Computer Science 697 (1993) 321-333.

41. ZUBEREK W.M. Timed Petri Nets nd Preliminary Performance Evaluation. Proc. 7th Annual Symposium on Comp. Architecture, (1980), 88-96.