Причинно-следственная семантика для непрерывно-временных сетей Петри со слабой временной стратегией

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