Редактирование: Участник:Soshial

Материал из eSyr's wiki.

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.

=== Моделирование программ. Размеченные системы переходов. Детерминизм и недетерминизм. Вычисления и трассы. Свойства линейного времени. Выполнимость свойства на трассе.===

'' Лекция 2, Слайды 39-50 ''

====Размеченная система переходов (LTS)====

<math>TS = \langle S, Act, \overset{a}{\rightarrow} ,s_0, AP, L \rangle </math>
* S - множество состояний
* Act - множество действий
* '' <math>\tau</math> - невидимое действие ''
* <math>\overset{a}{\rightarrow} \subseteq S \times Act \times S </math> - тотальное отношение переходов. Тотальность означает, что из каждого состояния ведёт какое-то действие.
* <math>s_0 \in S</math> - начальное состояние ('''!!!''')
* AP - множество атомарных высказываний 
* <math>L:S \rightarrow 2^{AP}</math> - функция разметки

S, Act - конечные или счётные множества

<math>\langle s, a, s' \rangle \in \overset{a}{\rightarrow} \equiv s \overset{a}{\rightarrow} s' </math>

''Пример LTS: Лекция 2, слайды 40-41''

'''Прямые потомки'''
* <math>Post(s, a) = \{s' \in S, s \overset{a}{\rightarrow} s'\}</math> - такие состояния s', которые <u>непосредственно вытекают</u> из s через переход a
* <math>Post(s) = \bigcup_{a \in Act} Post(s, a)</math> - все возможные состояния s', которые <u>непосредственно вытекают</u> из s

Система <math>TS = \langle S, Act, \overset{a}{\rightarrow} ,I, AP, L \rangle</math> '''детерминирована''':
* '''по действиям''' тогда и только тогда, когда 
** <math>|I| \leqslant 1</math>
** <math>\forall s \in S, \forall a \in Act \Rightarrow |Post(s, a)| \leqslant 1</math> ('''!!!''')
* '''по атомарным высказываниям'''
** <math>|I| \leqslant 1</math>
** <math>\forall s \in S, \forall A \in 2^{AP} ~ \Rightarrow ~ |Post(s) \cap \{s' \in S, L(s') = A\}| \leqslant 1</math> ( количество одинаково размеченных потомков не больше одного )

'''Недетерминизм''' - это фича! Полезен для:
* моделирования параллельного выполнения в режиме чередования (интерливинга)
** позволяет не указывать скорость выполнения процессов
* моделирования прототипа системы
** не ограничивает реализацию заданным порядком выполнения операторов
* построения абстракции реальной системы
** модель может быть построена по неполной информации

====Вычисления====
# '''Конечный фрагмент вычисления <math>\sigma</math>''' системы переходов TS - это конечная последовательность чередующихся состояний и действий, заканчивающаяся состоянием: <math>\sigma = s_0 a_1 s_1 a_2 s_2 \dots a_n s_n, \forall i \in [0,n)  \Rightarrow  s_i \overset{a_{i+1}}{\rightarrow} s_{i+1}</math>
# '''Бесконечный (максимальный) фрагмент вычисления <math>\rho</math>''' - <math>\rho = s_0 a_1 s_1 a_2 s_2 \dots, \forall i \geqslant 0 \Rightarrow s_i \overset{a_{i+1}}{\rightarrow} s_{i+1}</math>
# '''Начальный фрагмент вычисления''' - фрагмент вычисления, для которого <math>s_0 \in I</math>
# '''Вычисление''' - начальный максимальный фрагмент вычисления

'''Достижимое состояние''' (из начального) в системе переходов TS - такое состояние <math>s \in S</math>, для которого существует конечный фрагмент вычисления <math>s_0 a_1 s_1 a_2 s_2 \dots a_n s_n = s</math>

'''Reach(TS)''' - множество всех достижимых состояний в TS

'''Трасса''' <math>tr = L(s_0) L(s_1) \dots \in (2^{AP})^\omega</math>

====Свойства линейного времени====
* Свойство <math>\varphi</math> определяет набор допустимых трасс: <math>\varphi \subseteq (2^{AP})^\omega</math>
* Система переходов TS удовлетворяет свойству линейного времени <math>\varphi</math>
** <math>TS \models \varphi ~~ \Leftrightarrow ~~ Traces(TS) \subseteq \varphi</math>
** <math>P \models \varphi ~~ \equiv ~~ TS(P) \models \varphi </math> - по определению программа удовлетворяет свойству &phi;, если её система переходов удовлетворяет этому свойству

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!

Описание изменений:

Отменить | Справка по редактированию (в новом окне)

Получено с http://esyr.org/wiki/%D0%A3%D1%87%D0%B0%D1%81%D1%82%D0%BD%D0%B8%D0%BA:Soshial

Редактирование: Участник:Soshial

Материал из eSyr's wiki.

Просмотры

Личные инструменты

Навигация

инструменты

Разделы

Спецкурсы

9 семестр

7 семестр

5 семестр

3 семестр

Поиск

Инструменты

@@ Строка 10: / Строка 10: @@
 * '' <math>\tau</math> - невидимое действие ''
 * <math>\overset{a}{\rightarrow} \subseteq S \times Act \times S </math> - тотальное отношение переходов. Тотальность означает, что из каждого состояния ведёт какое-то действие.
-* <math>s_0 \in S</math> - начальное состояние, либо <math>I</math> - множество начальных состояний
+* <math>s_0 \in S</math> - начальное состояние ('''!!!''')
 * AP - множество атомарных высказываний
 * <math>L:S \rightarrow 2^{AP}</math> - функция разметки
@@ Строка 27: / Строка 27: @@
 * '''по действиям''' тогда и только тогда, когда
 ** <math>|I| \leqslant 1</math>
-** <math>\forall s \in S, \forall a \in Act \Rightarrow |Post(s, a)| \leqslant 1</math> (количество потомков не больше одного)
+** <math>\forall s \in S, \forall a \in Act \Rightarrow |Post(s, a)| \leqslant 1</math> ('''!!!''')
 * '''по атомарным высказываниям'''
 ** <math>|I| \leqslant 1</math>
-** <math>\forall s \in S, \forall A \in 2^{AP} ~ \Rightarrow ~ |Post(s) \cap \{s' \in S, L(s') = A\}| \leqslant 1</math> (количество '''одинаково размеченных''' потомков не больше одного)
+** <math>\forall s \in S, \forall A \in 2^{AP} ~ \Rightarrow ~ |Post(s) \cap \{s' \in S, L(s') = A\}| \leqslant 1</math> ( количество одинаково размеченных потомков не больше одного )
@@ Строка 45: / Строка 45: @@
 # '''Бесконечный (максимальный) фрагмент вычисления <math>\rho</math>''' - <math>\rho = s_0 a_1 s_1 a_2 s_2 \dots, \forall i \geqslant 0 \Rightarrow s_i \overset{a_{i+1}}{\rightarrow} s_{i+1}</math>
 # '''Начальный фрагмент вычисления''' - фрагмент вычисления, для которого <math>s_0 \in I</math>
-# '''Вычисление''' - начальный максимальный фрагмент вычисления (описывает последовательность состояний и действий)
+# '''Вычисление''' - начальный максимальный фрагмент вычисления
 '''Достижимое состояние''' (из начального) в системе переходов TS - такое состояние <math>s \in S</math>, для которого существует конечный фрагмент вычисления <math>s_0 a_1 s_1 a_2 s_2 \dots a_n s_n = s</math>
@@ Строка 55: / Строка 55: @@
 ====Свойства линейного времени====
 * Свойство <math>\varphi</math> определяет набор допустимых трасс: <math>\varphi \subseteq (2^{AP})^\omega</math>
-* Система переходов TS удовлетворяет свойству линейного времени <math>\varphi</math>, если: <math>TS \models \varphi ~~ \Leftrightarrow ~~ Traces(TS) \subseteq \varphi</math>
+* Система переходов TS удовлетворяет свойству линейного времени <math>\varphi</math>
-* по определению программа удовлетворяет свойству &phi;, если её система переходов удовлетворяет этому свойству: <math>P \models \varphi ~~ \equiv ~~ TS(P) \models \varphi </math> -
+** <math>TS \models \varphi ~~ \Leftrightarrow ~~ Traces(TS) \subseteq \varphi</math>
+** <math>P \models \varphi ~~ \equiv ~~ TS(P) \models \varphi </math> - по определению программа удовлетворяет свойству &phi;, если её система переходов удовлетворяет этому свойству