Участник:Soshial
Материал из eSyr's wiki.
(Различия между версиями)
м (tmp) |
м |
||
Строка 10: | Строка 10: | ||
* '' <math>\tau</math> - невидимое действие '' | * '' <math>\tau</math> - невидимое действие '' | ||
* <math>\overset{a}{\rightarrow} \subseteq S \times Act \times S </math> - тотальное отношение переходов. Тотальность означает, что из каждого состояния ведёт какое-то действие. | * <math>\overset{a}{\rightarrow} \subseteq S \times Act \times S </math> - тотальное отношение переходов. Тотальность означает, что из каждого состояния ведёт какое-то действие. | ||
- | * <math>s_0 \in S</math> - начальное состояние | + | * <math>s_0 \in S</math> - начальное состояние, либо <math>I</math> - множество начальных состояний |
* AP - множество атомарных высказываний | * AP - множество атомарных высказываний | ||
* <math>L:S \rightarrow 2^{AP}</math> - функция разметки | * <math>L:S \rightarrow 2^{AP}</math> - функция разметки | ||
Строка 27: | Строка 27: | ||
* '''по действиям''' тогда и только тогда, когда | * '''по действиям''' тогда и только тогда, когда | ||
** <math>|I| \leqslant 1</math> | ** <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>|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>\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> | # '''Начальный фрагмент вычисления''' - фрагмент вычисления, для которого <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> | '''Достижимое состояние''' (из начального) в системе переходов 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> | * Свойство <math>\varphi</math> определяет набор допустимых трасс: <math>\varphi \subseteq (2^{AP})^\omega</math> | ||
- | * Система переходов TS удовлетворяет свойству линейного времени <math>\varphi</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> - | |
- | * | + |
Текущая версия
Содержание |
[править] Моделирование программ. Размеченные системы переходов. Детерминизм и недетерминизм. Вычисления и трассы. Свойства линейного времени. Выполнимость свойства на трассе.
Лекция 2, Слайды 39-50
[править] Размеченная система переходов (LTS)
- S - множество состояний
- Act - множество действий
- τ - невидимое действие
- - тотальное отношение переходов. Тотальность означает, что из каждого состояния ведёт какое-то действие.
- - начальное состояние, либо I - множество начальных состояний
- AP - множество атомарных высказываний
- - функция разметки
S, Act - конечные или счётные множества
Пример LTS: Лекция 2, слайды 40-41
Прямые потомки
- - такие состояния s', которые непосредственно вытекают из s через переход a
- - все возможные состояния s', которые непосредственно вытекают из s
Система детерминирована:
- по действиям тогда и только тогда, когда
- (количество потомков не больше одного)
- по атомарным высказываниям
- (количество одинаково размеченных потомков не больше одного)
Недетерминизм - это фича! Полезен для:
- моделирования параллельного выполнения в режиме чередования (интерливинга)
- позволяет не указывать скорость выполнения процессов
- моделирования прототипа системы
- не ограничивает реализацию заданным порядком выполнения операторов
- построения абстракции реальной системы
- модель может быть построена по неполной информации
[править] Вычисления
- Конечный фрагмент вычисления σ системы переходов TS - это конечная последовательность чередующихся состояний и действий, заканчивающаяся состоянием:
- Бесконечный (максимальный) фрагмент вычисления ρ -
- Начальный фрагмент вычисления - фрагмент вычисления, для которого
- Вычисление - начальный максимальный фрагмент вычисления (описывает последовательность состояний и действий)
Достижимое состояние (из начального) в системе переходов TS - такое состояние , для которого существует конечный фрагмент вычисления
Reach(TS) - множество всех достижимых состояний в TS
Трасса
[править] Свойства линейного времени
- Свойство определяет набор допустимых трасс:
- Система переходов TS удовлетворяет свойству линейного времени , если:
- по определению программа удовлетворяет свойству φ, если её система переходов удовлетворяет этому свойству: -