Warning: session_start(): open(C:\Windows\temp\sess_trfgrh5ddp16a15igljfqm91n0, O_RDWR) failed: No space left on device (28) in C:\www\lemma4.1php\login.php on line 15 Warning: session_commit(): open(C:\Windows\temp\sess_trfgrh5ddp16a15igljfqm91n0, O_RDWR) failed: No space left on device (28) in C:\www\lemma4.1php\login.php on line 36 Warning: session_commit(): Failed to write session data (files). Please verify that the current setting of session.save_path is correct (C:\Windows\temp) in C:\www\lemma4.1php\login.php on line 36 Сети Петри: модификации и расширения

3.1.3 Непрерывно-временные СП (НВСП)

Рассмотрим ряд понятий, связанных со структурой и поведением временной сети модели Мерлина, которую будем называть непрерывно-временной СП (НВСП). Под НВСП понимается СП, где с каждым переходом связан некоторый временной интервал (нижняя и верхняя временные границы) срабатывания перехода.

Пусть N — множество натуральных чисел, R — множество неотрицательных действительных чисел и R+ — множество положительных действительных чисел. Определим множество Interv={[d1,d2]R|d1,d2N,d1d2}.

Определение 45 Непрерывно-временная сеть Петри (НВСП) — это кортежCTN=(S,T,F,M0,D), гдеN=(S,T,F,M0)ординарная СП, D:TInterv — временная функция, сопоставляющая каждому переходуtTинтервалD(t)из множества Interv.

Пример НВСП приведен на рис. 3.7, где с каждым переходом связан его временной интервал.

В целях упрощения представления полагаем, что базовая сеть СП N является чистой, т.е. xx= для каждого xST. Напомним, что через En(M) обозначается множество переходов, готовых к срабатыванию при маркировке M.

Пусть V=[TR] — множество наборов значений часов, связанных с переходами из T. Для заданных νV и δR обозначим через ν+δ набор значений часов, равных ν(t)+δ для каждого перехода t из T.

Определение 46 Состоянием в CTN называется параq=<M,ν>, где M  маркировка в CTN иνV. Hачальное состояние в CTN  это параq0=<M0,ν0> такая, чтоν0(t)=0для всехtT.

В НВСП смена одного состояния другим осуществляется либо при истечении некоторого времени, либо при срабатывании некоторого перехода сети.

Будем говорить, что в состоянии q=<M,ν> может пройти времяδR+, если существует δ'δ такое, что ν(t)+δ'D(t) для всех tEn(M). Тогда состояние q'=<M',ν'> получается при истечении времениδ из состояния q (обозначаем qδq'), если

  • M'=M и
  • ν'(t)=ν(t)+δ для всех tT.

Будем говорить, что в состоянии q=<M,ν> переход tTможет сработать, если tEn(M) и δ(t)D(t). Тогда состояние q'=<M',ν'> получается при срабатывании перехода t из состояния q (обозначаем q0q'), если

  • M[t>M' и
  • t'Tν'(t')=0,t'En(M')\En(M),ν(t'),иначе.

Только в некоторых случаях, когда существенно, что q' получается из q при срабатывании конкретного перехода t, будем писать qtq'.

Достижимость состояний в CTN посредством прохождения времени или срабатывания перехода определяется стандартным образом. Через [q0> обозначим множество всех состояний, достижимых в НВСП CTN, а через [q> — множество всех состояний, достижимых из состояния q в CTN.

Назовем q-путем r в CTN бесконечную последовательность состояний qi[q0> и моментов времени δiR вида: q=q1δ1q2δ2...qnδn... Пусть time(r,n)=1inδi. В качестве иллюстрации построим q0-путь r1 в НВСП CTN1 (см. рис. 3.7): {s1,s2},ν00δ1=0.7{s1,s2},ν10.7δ2=0.3{s1,s2},ν21δ3=0{s1,s5},ν31δ4=1{s1,s5},ν42δ5=0{s4,s5},ν5δ6=0,ν6δ7=3 …, где ν5(ti)=2(1i4),ν5(t5)=0, ν5(t5)=0 и ν5=ν6. Тогда time(r1,7)=1i<7δi=2.

Будем говорить, что CTN безопасна, если для любого достижимого состояния <M,ν>[q0> и для любого места sS верно M(s)1. Для того, чтобы исключить ситуацию, когда на некотором q-пути в CTN может сработать бесконечное число переходов за конечный отрезок времени, рассмотрим следующее условие, которое назовем прогресс-условием: для всякого множества переходов {t1,t2,...,tn} таких, что 1i<n    titi+1 и tnt1, существует 1jn такой, что 0D(tj). НВСП CTN1 (см. рис. 3.7) удовлетворяет прогресс-условию, так как имеем 0D(t1).

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

TCTL: синтаксис и семантика

В данном пункте рассматривается темпоральная логика реального времени TCTL (Timed Computation Tree Logic) [3], которая является расширением известного языка ветвящегося времени CTL за счет добавления временных ограничений в его операторы.

Опишем формально синтаксис и семантику языка TCTL. Пусть AS — множество элементарных формул. Для наших целей удобно взять AS = S.

Определение 47TCTL-формулаφиндуктивно определяется следующим образом:

φ:=s|¬φ1|φ1φ2|φ1Ucφ2|&exists;φ1Ucφ2,

гдеsAS, cN, φ1иφ2 — TCTL-формулы, ~  одно из бинарных отношений из множества{<,,=,,>}.

Для TCTL-формулы φ обозначим через cφ максимальную константу, встречающуюся в φ. Пусть I(~c) обозначает интервал действительных чисел, соответствующий '~c'.

Интуитивно формула &exists;φ1U<cφ2 означает, что для некоторого вычисления системы существует начальный префикс такой, что его временная длительность меньше, чем c, и формула φ1 истинна на всех состояниях префикса, кроме последнего состояния, где истинна формула φ2.

Условимся, что неиндексированные темпоральные операторы соответствуют TCTL-операторам с индексом '0 '. В языке TCTL также можно определять темпоральные операторы, индексированные временными интервалами. Например, формула &exists;(a,b)φ может быть записана как &exists;=a&exists;<(b-a)φ. Далее приведен ряд общепринятых сокращений: ~cφtrueU~cφ, &exists;~cφ&exists;trueU~cφ, ~cφ¬&exists;~c¬φ, &exists;~cφ¬~c¬φ.

Определение 48 Для заданного состоянияq=<M,ν>[q0>и TCTL-формулыφ отношение выполнимости (обозначаетсяq=φ) определяется индуктивно следующим образом:

q=ssM;

q=¬φ1qφ1;

q=φ1φ1qφ1илиq=φ2;

q=&exists;φ1U<cφ2для некоторого q-пути r в CTN верноr=φ1U<cφ2;

q=φ1U<cφ2 для всякого q-пути r в CTN верноr=φ1U<cφ2.

Для q-пути r : <M,ν>=<M1,ν1>δ1<M2,ν2>δ2в CTN выполняетсяr=φ1U<cφ2тогда и только тогда, когда существует k иδδkтакие, что:

  1. (δ+time(r,k))~c;
  2. <Mk,νk+δ>=φ2;
  3. 1i<k(<Mi,νi>=φ10<δ'<δi<Mi,νi+δ'>=φ1);
  4. 0<δ'<δ<Mk,νk+δ'>=φ1).

Будем говорить, что CTN удовлетворяет TCTL-формуле φ (обозначается CTN=φ), если q0=φ. Тогда TCTL-формула φ выполнима, если существует CTN такая, что CTN=φ.

В качестве примера рассмотрим формулу φ1=&exists;2(s4s5). НВСП CTN1 (см. рис. 3.7) удовлетворяет этой формуле, так как в CTN1 существует q0-путь, на котором фишки присутствуют в местах s4 и s5 (т.е. переход t5 может сработать) в момент времени, больший или равный двум единицам времени. Следовательно, формула φ1 выполнима.

Теорема 30Проблема TCTL-выполнимости11-сложна.

Доказательство. Следует из определения отношения выполнимости и теоремы о неразрешимости TCTL [3].      □

Построение графа регионов

Поскольку понятие НВСП базируется на модели непрерывного времени, то число ее состояний бесконечно. Чтобы получить конечное представление сетевого поведения, введем понятие региона [3]. Два состояния НВСП принадлежат одному и тому же региону, если они в некотором смысле эквивалентны, т.е. их маркировки совпадают и значения соответствующих часов согласованы по целым частям и порядку дробных частей.

Для некоторого числа δR обозначим через [δ] его целую часть, a через {δ} — его дробную часть. Пусть ν,ν'V. Тогда νν', если и только если выполнены следующие условия:

  • для любого tT верно:
    • ([ν(t)]=[ν'(t)]) или
    • (ν(t)>maxD(t)ν'(t)>maxD(t));
  • для любых t,t'T таких, что ν(t)maxD(t) и ν(t')maxD(t') верно:
    • {ν(t)}{ν(t')}{ν'(t)}{ν'(t')} и
    • {ν(t)}=0{ν'(t)}=0

В качестве примера рассмотрим НВСП CTN2 (см. рис. 3.8) и следующие наборы значений часов ее переходов: ν1=(1.99,1.99,0.13), ν2=(1.1,1.1,0.05), ν3=(1.1,1.1,0.8). Имеем ν1ν2, однако ¬(ν1ν3), поскольку ({ν1(t3)}<{ν1(t1)} и {ν3(t3)}>{ν3(t1)}).

Лемма 15Пусть<M,ν>,<M,ν'>[q0> такие, чтоνν'. Тогда для всякой TCTL-формулыφ верно<M,ν>=φ<M,ν'>=φ.

Доказательство. Прежде, чем доказывать лемму, покажем, что в CTN существуют <M,ν>- и <M,ν'>-пути, которые являются эквивалентными в определенном ниже смысле. Рассмотрим <M,ν>-путь r:

<M,ν>=<M1,ν1>δ1<M2,ν2>...<Mi,νi>δi<Mi+1,νi+1>...

Покажем, что существует <M,ν'>-путь r' такой, что

<M,ν'>=<M1,ν1'>δ1'<M2,ν2'>...<Mi,νi'>δi'<Mi+1,νi+1'>...

и для каждого i1 выполнены следующие условия эквивалентности между (νi,time(r,i)) и  (νi',time(r',i)) (обозначается (νi,time(r,i))(νi',time(r',i)):

  • νiνi';
  • значения time(r,i) и time(r',i) согласованы по целым частям, т.е.
    • [time(r,i)]=[time(r',i)],
    • {time(r,i)}=0{time(r',i)}=0
  • дробные части значений time(r,i) и time(r',i) находятся в одном и том же отношении с дробными частями значений νi и νi' соответственно, т.е. для всякого перехода tT верно:
    • {νi(t)}<{time(r,i)}{νi'(t)}<{time(r',i)},
    • {νi(t)}>{time(r,i)}{νi'(t)}>{time(r',i)}.

Путь r' будем строить пошагово по заданному пути r. Базис индукции очевиден, так как νν' и time(r,1)=time(r',1)=0. Пусть путь r' построен до i-ого состояния. Теперь покажем, что по заданному δi можно найти δi' такое, что r' может быть продолжен до состояния <Mi+1,νi+1'> без нарушения приведенных выше условий эквивалентности.

Определим множество Δ для пути r следующим образом:

Δ={time(r,i)}{νi(t)|tT}.

Множество Δ' для пути r' определяется аналогично. Так как до i-ого состояния путь r' построен корректно, то необходимое и достаточное требование к значению δi' заключается в том, чтобы значение каждого элемента множества Δ' пересекало некоторую целочисленную границу, если и только если эту границу пересекает значение соответствующего элемента множества Δ. Очевидно, что выбор δi' зависит только от порядка дробных частей значений элементов в Δ', который совпадает с порядком дробных частей значений элементов в Δ. Cледовательно, существование δi гарантирует существование δi'.

Теперь покажем справедливость леммы индукцией по структуре формулы φ. Для базиса индукции (атомарных формул) и логических связок справедливость очевидна. Рассмотрим случай φ=&exists;φ1U~cφ2. Предположим <M,ν>=φ. Тогда, по определению 48, в CTN существует <M,ν>-путь r такой, что r=φ1U~cφ2, т.е. существует k и δδk такие, что:

  1. (δ+time(r,k))~c;
  2. <Mk,νk+δ>=φ2;
  3. 1i<k(<Mi,νi>=φ10<δ<δi<Mi,νi+δ'>=φ1);
  4. 0δ<δ ◊ <Mk,νk+δ'>=φ1.

Построим <M,ν'>-путь r', как описано выше. Покажем, что r'=φ1U~cφ2. Необходимо рассмотреть четыре случая:

  1. Так как (νk,time(r,k))(νk',time(r',k)), то, согласно построению r' по заданному δ, можно найти δ' такое, что (νk+δ,time(r,k)+δ)(νk'+δ',time(r',k)+δ'). Тогда исходя из того, что (δ'+time(r',k))~c имеем (δ+time(r,k))~c.
  2. Так как <Mk,νk+δ>=φ2, то, по предположению индукции, верно <Mk,νk'+δ'>=φ2.
  3. Пусть 1i<k и 0<δ'<δi'. Поскольку верно, что (νi,time(r,i))(νi',time(r',i)), то, согласно построению r', существует 0<δ<δi такое, что (νi+δ,time(r,i)+δ)(νi'+δ',time(r',i)+δ'). Исходя из того, что <Mi,νi+δ>=φ1 и <Mi,νi>=φ1, то, по предположению индукции, имеем <Mi,νi'>=φ1 и <Mi,νi'+δ'>=φ1;
  4. Аналогично пункту 3.

Таким образом, r'=φ1U~cφ2. Следовательно, <M,ν'>=φ, по определению 48. □

Чтобы проверить истинность временных ограничений TCTL-формулы φ, необходимо ввести дополнительный переход t*T, который не готов к срабатыванию ни при одной маркировке в N, и поэтому его часы будут хранить значение времени, прошедшего с некоторого фиксированного начального момента. Пусть T*=T{t*} и V*=[T{t*}R]. Определим отношение φ* как расширение отношения на переход t*, полагая maxD(t*) равным cφ. Будем использовать [ν]φ* для обозначения класса эквивалентности по V*, к которому принадлежит ν. Для νV и xR обозначим через [x]ν набор значений часов из V*, в котором часам, соответствующим переходу t*, сопоставлено значение x, а значения остальных часов совпадают с ν. Для произвольного tT* введем следующее обозначение: [ν(t)]φ*={ν(t)|ν[ν]φ*}.

Лемма 16Число классов эквивалентности по V*(CTN), порожденных отношениемφ*, ограничено величиной

|T*|!22|T*|t|T*|(maxD(t)+1).

Доказательство. Класс эквивалентности [ν]φ* по V*(CTN) относительно φ* можно представить тройкой массивов <α,β,γ>, определенных ниже.

Массив α — T*-индексированный массив, в котором каждому переходу tT* сопоставлен один из интервалов [0,0], (0,1), [1,1], ... , [maxD(t*), maxD(t*)], (maxD(t*), ). Таким образом, массив α представляет набор значений счетчиков ν, если и только если ν(t)α(t) для любого tT*.

Пусть Tα* — множество переходов таких, что α(t) имеет вид (i,i+1) для некоторого imaxD(t). Таким образом Tα* — множество переходов с ненулевыми дробными частями значений счетчиков.

Массив β:Tα*{1...|Tα*|} является перестановкой множества Tα*, задающей порядок по отношению дробных частей значений счетчиков, связанных с переходами из Tα*. Таким образом, массив β представляет набор значений счетчиков ν, если и только если для любой пары t1,t2Tα* верно {ν(t1)}{ν(t2)}, если β(t1)β(t2).

Массив γ — булевозначный Tα*-индексированный массив, определяющий переходы из Tα* с одинаковыми дробными частями. Для перехода tTα*γ(t) определяет, равна ли дробная часть значения его счетчика дробной части значения счетчика перехода, расположенного справа от t в массиве β. Таким образом, массив γ представляет набор значений счетчиков ν, если и только если для любого t1Tα* верно γ(t1)=0, если существует t2Tα* такой, что β(t2)=β(t1)+1 и {ν(t1)}={ν(t2)}.

Легко видеть, что число классов эквивалентности по V*(CTN) относительно φ* ограничено числом троек <α,β,γ> описанной выше формы. Число способов выбора α оценивается как tT*(2maxD(t)+2). Для заданного α число способов выбора β ограничено числом перестановок над Tα*, которое равно |T*|!, а число способов выбора γ ограничено числом булевозначных массивов над Tα*, оцениваемым как 2|T*|. □

Определение 49 Регионом в CTN относительно TCTL-формулыφ называется параv=<M,[ν]φ*>, где<M,ν>[q0>. Начальный регион в CTN относительноφ — это параv0=<M0,[[0]ν0]φ*>. Обозначим черезR(CTN,φ) множество всех регионов в CTN относительноφ.

Регионы в CTN1 (см. рис. 3.7) относительно TCTL-формулы φ1=&exists;2(s4s5) показаны на рис. 3.9.

Лемма 17Число регионов в CTN относительно формулы φограничено величиной

|T*|!22|T*|+|P|t|T*|(maxD(t)+1).

Доказательство. Предположим <M,[ν]φ*> — регион в CTN относительно формулы φ. Так как маркировка M — множество мощностью |P|, состоящее из '0' и '1', то число различных маркировок в CTN равно 2|P|. Число классов эквивалентности по V*(CTN), порожденных отношением φ*, ограничено величиной |T*|!22|T*|t|T*|(maxD(t)+1), по лемме 16. Таким образом, число регионов в CTN относительно формулы φ, ограничено величиной |T*|!22|T*|+|P|t|T*|(maxD(t)+1).

Пусть <M,[ν]φ*>, <M',[ν']φ*> — различные регионы из множества R(CTN,φ). Будем говорить, что <M',[ν']φ*> — преемник по времени для <M,[ν]φ*> (обозначается <M',[ν']φ*>=succδ(<M,[ν]φ*>)), если для некоторого положительного δR+ верно: M=M', ν+δ[ν']φ* и {ν+δ'|0δ'δ}[ν]φ*[ν']φ*. Также будем говорить, что <M',[ν']φ*> — преемник по срабатыванию для <M,[ν]φ*> (обозначается <M',[ν']φ*>=succt(<M,[ν]φ*>)), если для некоторого δR верно {ν+δ'|0δ'δ}[ν]φ* и <M,ν+δ>t<M',ν'>. Тогда fireable(<M,[ν]φ*>)={tT|succt(<M,[ν]φ*>)R(CTN,φ)}{δ|succδ(<M,[ν]φ*>)R(CTN,φ)}.

Чтобы проиллюстрировать данные определения, рассмотрим НВСП CTN2 (см. рис. 3.8) и некоторые ее регионы относительно формулы φ2=2s4. Имеем v0={s1,s2},{ν'|ν'(t1)=ν'(t2)=ν'(t3)=ν'(t*)[0,0]}, v1=succδ(v0)={s1,s2},{ν'|ν'(t1)=ν'(t2)=ν'(t3)=ν'(t*)(0,1)}, v2=succt1(v1)={s2,s3},{ν'|ν'(t1)=ν'(t2)=ν'(t*)(0,1),ν'(t3)[0,0]}, v3=succδ(v2)={s2,s3},{ν'|ν'(t1)=ν'(t2)=ν'(t*)(0,1),ν'(t3)(0,1)} и т.д. Кроме того, fireable(v0)={t1,δ}, fireable(v1)={t1,δ}, fireable(v2)={t3,δ} и т.д.

Алгоритм построения графа регионов G(CTN,φ)=(V,E,l) состоит в следующем.

Инициализация: St:=, H:=;

V:={v0};

E:=;

l:=;

поместить v0 в St;

пока St выполнить {

взять v из St;

если v не принадлежит H то {

добавить v в H;

TS:=fireable(v);

для всех tTS выполнить {

v':=succt(v),tT,succδ(v),else.

V:=V{v'};

E:=E{(v,v')};

l(v,v')=t;

добавить v' в St}}}.

Здесь St представляет собой множество регионов, которые должны быть рассмотрены, H — множество уже рассмотренных регионов.

Граф регионов для НВСП CTN1 (см. рис. 3.7) и формулы φ1=&exists;2(s4s5) показан на рис. 3.10.

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

Цель данного пункта разработать алгоритм, проверяющий удовлетворяет ли НВСП своей спецификации, заданной в виде TCTL-формулы.

Алгоритм проверки, верно ли CTN=φ, состоит в следующем: сначала строится граф регионов G(CTN,φ), а затем выполняется алгоритм пометки этого графа. НВСП CTN удовлетворяет TCTL-формуле φ, если и только если M0,[[0]v0]φ* помечена φ.

Рассмотрим алгоритм пометки графа G(CTN,φ). Будем помечать вершины графа G(CTN,φ) подформулами формулы φ или их отрицанием, начиная с подформул длины 1, затем длины 2 и т.д. Пусть v=<M,[ν]φ*> — вершина графа G(CTN,φ).

Для каждого индекса '~c', встречающегося в φ, введем новую элементарную формулу s~c. Помечаем v=<M,[ν]φ*> формулой s~c, если <M,ν>=ν(t*)~c, иначе помечаем v — ¬s~c.

Пусть ψ — подформула формулы φ. Предположим, что все вершины графа G(CTN,φ) уже помечены всеми подформулами формулы ψ или их отрицанием. Рассмотрим структуру формулы ψ.

  • ψAS. Если ψM, то помечаем v формулой ψ, иначе — формулой ¬ψ.
  • ψ=¬φ. Если v помечена формулой φ, то помечаем v формулой ¬ψ, иначе — формулой ψ.
  • ψ=φ1φ2. Если v помечена формулами ¬φ1 или φ2, то помечаем v формулой ψ, иначе — формулой ¬ψ.
  • ψ=Qφ1U~cφ2, где Q — либо квантор существования, либо квантор всеобщности. Заметим, что вершины в G(CTN,φ) уже помечены φ1 или ее отрицанием, а также φ2 или ее отрицанием. Вершина v помечается формулой ψ, если некоторый или всякий, в зависимости от квантора Q путь в G(CTN,φ), начинающийся в v, имеет префикс v=v1,v2,...vn такой, что vi помечена формулой φ1 для любого 1i<n, vn помечена формулами φ2 и s~c.

Результат применения алгоритма пометки к графу G(CTN1,φ1) при φ1=&exists;2(s4s5) показан на рис. 3.11. Таким образом, получаем CTN1=φ1.

Следующая лемма устанавливает корректность алгоритма пометки.

Лемма 18Пусть<M,[ν]φ*>G(CTN,φ)иψ — подформула формулыφ или ее отрицание. Приведенный выше алгоритм помечает<M,[ν]φ*>формулойψ тогда и только тогда, когда<M,ν>=ψ.

Доказательство. Будем доказывать справедливость леммы индукцией по структуре формулы ψ. Случаи ψAS, ψ=¬φ1 и ψ=φ1φ2 очевидны. Покажем, что алгоритм помечает <M,[ν]φ*> формулой ψ=&exists;φ1U~cφ2 тогда и только тогда, когда <M,ν>=ψ. Случай ψ=φ1U~cφ2 доказывается аналогично.

(): Предположим, что <M,ν>=ψ. Тогда, по определению 48, в CTN существует путь r : <M,ν>=<M1,ν1>δ1<M2,ν2>... такой, что r=φ1U~cφ2, т.е. существует k и δδk такие, что:

  1. (δ+time(r,k))~c;
  2. <Mk,νk+δ>=φ2;
  3. 1i<k(<Mi,νi>=φ10<δ<δi<Mi,νi+δ'>=φ1);
  4. 0δ<δ<Mk,νk+δ'>=φ1.

Для заданного пути r в CTN строим соответствующий ему путь в G(CTN,φ). Для каждого i1 можно найти конечный путь ωi в G(CTN,φ) следующим образом: ωi={<Mi,[νi]φ*>=<Mi0,[νi0]φ*>,<Mi1,[νi1]φ*>, ... , <Miji,[νiji]φ*>=<Mi+1,[νi+1]φ*>} такой, что для всех 0l<ji верно <Mil+1,[νil+1]φ*>=succδ(<Mil,[νil]φ*>), если <Mi+1,νi+1> получается при истечении времени δi из <Mi,νi>, иначе ji=1 и <Mi1,[νi1]φ*>=succt(<Mi0,[νi0]φ*>) для некоторого tfireable(<Mi,[νi]φ*>). Заметим, что 0δ'δi&exists;0ljiνi+δ'φ*νil. Пусть ω — путь в G(CTN,φ), получаемый конкатенацией путей ωi.

Покажем, что ω удовлетворяет формуле φ1U(φ2s~c), т.е. существуют k и l<jk такие, что: а) <Mkl,[νkl]φ*> помечено формулой s~c, б) <Mkl,[νkl]φ*> помечено формулой φ2 и в) любое <Mk'l',[νk'l']φ*>, стоящее в ω раньше, чем <Mkl,[νkl]φ*>, помечено формулой φ1. По построению ωk, имеем &exists;0ljkνk+δ'φ*νkl. Далее:

а) так как time(r,k)=νk(t*), то δ+νk(t*)~c. Следовательно, νkl~c, т.е. <Mkl,[νkl]φ*> помечено формулой s~c;

б) так как <Mk,νk+δ>=φ2, то <Mkl,νkl>=φ2. Тогда, по предположению индукции, <Mkl,[νkl]φ*> помечено формулой φ2.

в) рассмотрим <Mk'l',[νk'l']φ*>, стоящее в ω раньше <Mkl,[νkl]φ*> (т.е. либо k'<k, либо k'=k и l'<l). По построению ωk', существует 0δ'δk' такое, что νk'+δ'φ*νk'l'. Так как <Mk',νk'+δ'>=φ1, то <Mk'l',νk'l'>=φ1. Следовательно, по предположению индукции, <Mk'l',[νk'l']φ*> помечено формулой φ1.

Таким образом, <M,[ν]φ*> помечено формулой ψ.

(): Предположим, что <M,[ν]φ*> помечено формулой ψ=&exists;φ1U~cφ2. Тогда существуют путь {<M,[ν]φ*>=<M1,[ν1]φ*><M2,[ν2]φ*>...} в G(CTN,φ) и n N такие, что <Mi,[νi]φ*> помечено формулой φ1 для любого 1i<n, <Mn,[νn]φ*> помечено формулами φ2 и s~c. Cтроим соответствующий <M,ν>-путь r в CTN: <M,ν>=<M1,ν1>δ1<M2,ν2>δ2... такой, что для каждого i1 существует δiR такое, что <Mi,νi>δi<Mi+1,νi+δi> и νi+δi[νi+1]φ*. Далее, рассуждая, как в первой части доказательства, можно показать, что <M,ν>=ψ. □

Теорема 31Пустьφ — TCTL-формула. Существует алгоритм проверки, чтоCTN=φ, который удовлетворяет следующей оценке:

O[|φ|cφ|T|2|S|+2|T|tT(maxD(t)+1)].

Доказательство. Имеем |V|=O[cφT!2|P|+2TtT(Lft(t)+1)], в силу леммы 17. Для вершины v графа G(CTN,φ) существует не более |T| выходных дуг, представляющих срабатывания переходов и одна дуга, представляющая течение времени. Отсюда получаем следующее: |E|=O[cφT!2|P|+2TtT(Lft(t)+1)]. Далее, G(CTN,φ) может быть построен за время O[|V|+|E|]. Таким образом, алгоритм проверки имеет сложность O[|φ|(|V|+|E|)]=O[|φ|cφT!2|P|+2TtT(Lft(t)+1)]. □

Редукция графа регионов методом частичных порядков

Далее показывается, как уменьшить размер графа регионов для заданных НВСП и TCTL-формулы, сохранив корректность алгоритма проверки на графе. Корректность такой редукции основана на понятии временной статтеринг-эквивалентности.

Для TCTL-формулы φ обозначим через S(φ) множество мест, встречающихся в φ, а через cφ максимальную константу, встречающуюся в φ. Введем понятие временной статтеринг-эквивалентности (timed stuttering equivalence) для графов регионов.

Определение 50Пустьφ — TCTL-формула иG=G(N, φ') = (V', E', l'), G=G(N, φ'') = (V'', E'', l'') — графы регионов такие, чтоS(φ)=S(φ')=S(φ'') и cφ=cφ'=cφ''. Пустьv0', v0'' — начальные вершины вG', G''соответственно. ОтношениеφV'×V'' называется временной статтеринг-эквивалентностью относительно φмеждуG'иG'', если(v0',v0'')φи для всех(v'=M',[ν']φ*,v''=M'',[ν'']φ*)φверно:

  1. M'S(φ)=M''S(φ) иν'(t*)~cν''(t*)~cдля всех'~c'вφ;
  2. если(v',v1')E', то существуютv0,...,vnV''(n0) такие, чтоv''=v0, ((vi,vi+1)E''(v',vi)φ) для всех0i<n, и(v1',vn)φ;
  3. аналогично п. 2, но множестваV' иE' поменены местами с множествамиV'' иE'' соответственно.

ТогдаG'φG'', если между графамиG' иG'' существует отношениеφ.

Теорема 32Пустьφ — TCTL-формулаφ иG'=G(CTN,φ'), G''=G(CTN,φ'') — графы регионов такие, чтоG'φG''. Далее, пустьv'иv'' — вершины вG' иG''соответственно. Если(v',v'')φ, тоv' помеченаφтогда и только тогда, когдаv''помеченаφ.

Доказательство. Пусть (v'=<M',[ν']φ*>,v''=<M'',[ν'']φ*>)φ и вершина v' помечена TCTL-формулой φ. Индукцией по структуре формулы покажем, что v'' помечена TCTL-формулой φ.

  • φAS

    (а) φS. Тогда φM' и φS(φ). По определению 50, верно M'S(φ)=M''S(φ). Следовательно, φM''. Значит, v'' помечена φ.

    (б) φ=s~c. Так как ν'(t*)~c, то ν''(t*)~c, по определению 50. Следовательно, v'' помечена φ.

  • φ=¬φ1. Так как v' помечена φ, то, согласно алгоритму пометки, v' не помечена φ1. По предположению индукции, v' помечена φ1 тогда и только тогда, когда v'' помечена φ1. Следовательно, v'' не помечена φ1. Значит, v'' помечена φ.
  • φ=φ1φ2. Так как v' помечена φ, то, согласно алгоритму пометки, v' помечена формулами φ1 и φ2. Тогда, по предположению индукции, v'' помечена формулами φ1 и φ2. Следовательно, v'' помечена φ.
  • φ=&exists;φ1U~cφ2. Так как v' помечена φ, то, согласно алгоритму пометки, в G' существует путь ω':v'=v1'v2'...vn'...(n0) такой, что вершина vi' помечена формулой φ1 для любого 1i<n и вершина vn' помечена формулами φ2 и s~c. Путь ω'' в G'' будем строить пошагово по заданному пути ω' в G'. Базис индукции очевиден. Пусть ω'' построен до i-ого состояния. Расширим ω'' дугой (vi',vi+1') из E'. По определению 50, существуют вершины vi0,...,vimiV''(mi0) такие, что vi''=vi0,((vij,vij+1)E''(vi',vij)φ) для всех 0j<mi и (vi+1',vimi)φ. Так как (vi',vij)φ для всех j<mi и vi' помечена φ1 для всех 0i<n, то, по предположению индукции, vij помечена φ1. В случае 0i<n-1, по предположению индукции, vimi помечена φ1, поскольку (vi+1',vimi)φ и vi+1' помечена φ1. В случае i=n-1, по предположению индукции, vn-1mn-1 помечена φ2 и s~c, так как (vn',vn-1mn-1)φ и vn' помечена φ2 и s~c. Таким образом, на пути ω'':v''=v00...v0m0v01...v1m1...vn-10...vn-1mn-1... все вершины до vn-1mn-1 помечены φ1, а vn-1mn-1 помечена φ2 и s~c. Следовательно, v'' помечена φ.
  • φ=φ1U~cφ2. Аналогично случаю φ=&exists;φ1U~cφ2. □

Теперь введем ряд вспомогательных определений, необходимых для построения редуцированного графа НВСП CTN и TCTL-формулы φ. Пусть tT и v=<M,[ν]φ*>R(CTN,φ). Тогда

  • t' находится в конфликте с переходом t, если tt' и tt'. Пусть conflict(t) обозначает множество переходов, конфликтных с t;
  • t' — предшественник перехода t в регионе v, если t'F*t и t'M, где F* — транзитивное рефлексивное замыкание отношения F. Пусть pred(t,v) обозначает множество предшественников перехода t в регионе v;
  • t' — +-предшественник перехода t в регионе v, если t' — предшественник перехода t'', находящегося в конфликте с предшественником t''' перехода t, и справедливо, что dist(t',t'')maxD(t'''), где dist(t˜,tˆ) — минимальная сумма минимальных значений функции D(t) переходов на пути из t˜ в tˆ, не включая minD(tˆ). Пусть pred+(t,v) обозначает множество +-предшественников перехода t в регионе v;
  • t — видимый переход относительно TCTL-формулы φ, если (tt)S(φ). Пусть visible(φ) обозначает множество переходов, видимых относительно φ;
  • visible+(v,φ)=tvisible(φ)(pred(t,v)pred+(t,v));
  • δ — видимое время относительно TCTL-формулы φ в v, если значение часов перехода t* принадлежит интервалу I'(~c), где
    I'(~c)=[0,c), ~=<,[0,c]I(~c),иначе;
  • visibleδ+(v,φ)={δ|δ — видимое относительно формулы φ в v};
  • dependent(v,φ)=visible+(v,φ)visibleδ+(v,φ).

Для НВСП CTN1, показанной на рис. 3.7, и формулы φ=&exists;2(s4s5) имеем: conflict(t2)={t1}, pred(t2,v0)={t2}, conflict+(t2,v0)={t1}, pred+(t5,v0)={t1}, visible(φ)={t2,t3,t5}, visible+(v0,φ)={t1,t2,t3,t5}, visibleδ+(v0,φ)={δ} и dependent(v0,φ)={δ,t1,t2,t3,t5}. А для НВСП CTN2, показанной на рис. 3.8, и формулы φ=2s4 получаем следующее: conflict(t2)=, pred(t2,v0)={t2}, conflict+(t2,v0)=, pred+(t5,v0)=, visible(φ)={t2}, visible+(v0,φ)={t2}, visibleδ+(v0,φ)={δ} и dependent(v0,φ)={δ,t2}.

Определим множество ready(v,φ) как минимальное подмножество переходов из fireable(v) такое, что

fireable(v)dependent(v,φ)ready(v,φ)

Для НВСП CTN2 и формулы φ=2s4 имеем fireable(v0)={δ,t1} тогда, как ready(v0,φ)={δ}. Сложность конструирования множества ready(v,φ) равна O(|S||T|2).

Алгоритм построения редуцированного графа GR(CTN,φ) тот же, что и алгоритм построения графа G(CTN,φ), за исключением того, что множество TS определяется как ready(v,φ).

Теорема 33G'=G(CTN,φ) — граф регионов, G''=G(CTN,φ) — редуцированный граф регионов. Тогда φ*V'×V''.

Доказательство. Построим отношение φ*V'×V'' следующим образом: φ*={(v'=<M',[ν']φ*>,v''=<M'',[ν'']φ*>)|dependent(v',φ)=dependent(v'',φ), M'S(φ)=M''S(φ) и ν'(t*)~cν''(t*)~c для всех '~c' в φ}. Покажем, что отношение φ* является временной статтеринг-эквивалентностью относительно φ между G' и G''. Пусть v0' и v0'' — начальные вершины в G' и G'' соответственно. По построению графов G' и G'', имеем (v0',v0'')φ*, поскольку v0' = v0''. Предположим (v',v'')φ*. Справедливость п. 1 в определении 50 следует из построения φ*. Рассмотрим п. 2 в определении 50 (п. 3 симметричен). Предположим, что (v',v1')E'. Покажем, что существуют v0'',...,vn''V''(n0) такие, что v''=v0'', ((vi'',vi+1'')E''(v',vi'')φ*) для всех 0i<n и (v1',vn'')φ*. Пусть vi'=<Mi',[νi']φ*> и vi''=<Mi'',[νi'']φ*> для всех 0in.

Предложение. Пусть (v',v1')E'E''. Тогда:

1) если v1'=succt(v')tvisible+(v',φ), то visible+(v',φ)=visible+(v1',φ), M'S(φ)=M1'S(φ) и ν'(t*)~cν1'(t*)~c для всех '~c' в φ;

2) если v1'=succδ(v')δvisibleδ+(v',φ), то visibleδ+(v',φ)=visibleδ+(v1',φ), M'S(φ)=M1'S(φ) и ν'(t*)~cν1'(t*)~c для всех '~c' в φ.

Доказательство.

1) v1'=succt(v'). Тогда существует δR такое, что {ν'+δ'|0δ'δ}[ν']φ* и <M',ν'+δ>t<M1',ν1'>. По определению t, имеем ν'(t*)~cν1'(t*)~c для всех '~c' в φ. Так как tvisibleδ+(v',φ), то t˜visible(φ)¬(tF*t˜tM')[tˆ(tˆF*t˜tˆM'),t¯(t¯tˆt¯tˆ)¬(tF*t¯tM'dist(t,t¯)maxD(tˆ)))]. Заметим, что tM'. Тогда имеем: а) для всех t˜visible(φ) выполнено ¬(tF*t˜) и б) для всех t˜visible(φ) выполнено ¬(tF*t¯dist(t,t¯)maxD(tˆ)) для всех tˆ(tˆF*t˜tˆM') и для всех (t¯tˆt¯tˆ). Из пункта а) следует, что tvisible(φ) и source(t˜,v')=source(t˜,v1') для всех t˜visible(φ). Далее, из пункта б) следует, что source+(t˜,v')=source+(t˜,v1') для всех t˜visible(φ). Таким образом, visibleδ+(v',φ)=visibleδ+(v1',φ). Так как tvisible(φ) и tt=, то tS(φ)t=. Следовательно, M'S(φ)=M1'S(φ), по определению t.

2) v1'=succδ(v'). Непосредственно следует из определения succδ(v') и I'.

Далее будем доказывать индукцией по i.

i=0. По построению G'', имеем ready(v0'',φ)= и, следовательно, fireable(v0'')=. Тогда, по определению региона, ν0''(t')>maxD(t') для любого t'T*. Сначала покажем, что dependent(v',φ)=dependent(v1',φ), M'S(φ)=M1'S(φ) и ν'(t*)~cν1'(t*)~c для всех '~c' в φ. Возможны два случая.

  • v1'=succt(v'). Покажем, что tvisiblet+(v',φ). Предположим обратное, т.е. tvisiblet+(v',φ). Тогда tvisibleδ+(v0'',φ), по построению φ*. Следовательно, &exists;t~visible(φ)(tF*t~tM0'')[&exists;tˆ(tˆF*t~tˆM0''),&exists;t¯(t¯tˆt¯tˆ)(tF*t¯tM0''dist(t,t¯)maxD(tˆ)))]. Далее, так как tfireable(v0''), то δR({ν0''+δ'|0δ'δ}[ν0'']φ*)(t⊂⃒M0''ν0''(t)+δ<Eft(t)). Следовательно, ν0''(t)+δ<Eft(t) для всех δR таких, что {ν0''+δ'|0δ'δ}[ν0'']φ*. Пришли к противоречию, поскольку ν0''(t')>maxD(t') для всех t'T*. Таким образом, имеем tvisiblet+(v',φ). Утверждение непосредственно следует из предложения.
  • v1'=succδ(v'). Если δvisibleδ+(v',φ), утверждение непосредственно следует из предложения. Рассмотрим случай δvisibleδ+(v',φ). Так как v1'=succδ(v'), то M'=M1' и существует δR такое, что ν'+δ[ν1']φ* и {ν'+δ'|0δ'δ}[ν']φ*[ν1']φ*. Тогда M'S(φ)=M1'S(φ).
    Теперь покажем, что ν'(t*)~cν1'(t*)~c для всех '~c' в φ. Предположим обратное, возможны два случая: а) ν'(t*)~c¬(ν1'(t*)~c) для некоторого '~c' в φ и б) ¬(ν'(t*)~c)ν1'(t*)~c для некоторого '~c' в φ. Случай а) противоречит либо тому, что ν1'(t*)>ν'(t*), если ~{>,}, либо тому, что ν'(t*)~cν0''(t*)~c, поскольку ν0''(t*)>cφ,, если ~{<,,=}. Случай б) противоречит либо тому, что ν1'(t*)>ν'(t*), если ~{<,}, либо тому, что ν'(t*)~cν0''(t*)~c, поскольку ν0''(t*)>cφ,, если ~{>,}, либо тому, что (v',v0'')φ*, поскольку ν'(t*)<c and ν0''(t*)>c, если ~{=}.
    Наконец покажем, что δvisibleδ*(v1',φ), поскольку δvisibleδ*(v',φ). Предположим обратное, т.е. ν'(t*)I'(~c) для некоторого '~c' в φ и ν1'(t*)I'(~c) для всех '~c' в φ. Это противоречит либо определению I'(~c), поскольку ν1'(t*)>ν'(t*), если ~{>,}, либо ν'(t*)~cν0''(t*)~c, поскольку ν0''(t*)>cφ, если ~{<,,=}.

Таким образом, dependent(v',φ)=dependent(v1',φ), M'S(φ)=M1'S(φ) и ν'(t*)~cν1'(t*)~c для всех '~c' в φ. Так как (ν',ν0'')φ*, то (ν1',ν0'')φ*, по построению φ*.

i>0 По предположению индукции, имеем (v',vi-1'')φ*. Рассмотрим случай i<n. Покажем, что существует vi+1''V'' такая, что ((vi'',vi+1'')E''(v',vi'')φ*). Легко показать, что l''(vi-1'',vi'')visible+(vi-1''),φ) и νi-1''(t*)~cνi''(t*)~c для всех ~c в φ. Тогда утверждение непосредственно следует из построения φ* и требования, поскольку (v',vi-1'')φ*. Рассмотрим случай i=n. Покажем, что (v1',vn'')φ*. Пусть l'(v',v1')=t и l''(vn-1'',vn'')=t'. По построению G', G'' и φ*, возможны только два случая.

  1. tdependent(v',φ)t'dependent(vn-1'',φ). Не уменьшая общности, положим t=t'. Тогда утверждение получается непосредственно, поскольку (v',vn-1'')φ*.
  2. tdependent(v',φ)t'dependent(vn-1'',φ). Утверждение следует из предложения, поскольку (v',vn-1'')φ*.

Таким образом, существуют v0'',...,vn''V''(n0) такие, что v''=v0'', ((vi'',vi+1'')E''(v',vi'')φ*) для всех 0i<n, и (v',vn'')φ*. Значит, φ* является временной статтеринг-эквивалентностью относительно φ между G' и G''. □

Следовательно, можем сделать вывод, что алгоритм проверки на G(CTN,φ) сводится к алгоритму проверки на GR(CTN,φ).