Базовый формализм для моделирования концептуально сложных динамических систем

Размещено на http://www.allbest.ru/

Базовый формализм для моделирования концептуально сложных динамических систем

Ануреев Игорь Сергеевич

Институт Систем Информатики

Аннотация

В статье предлагается базовый математический формализм для спецификации и моделирования концептуально сложных динамических систем -- контекстные машины. Рассмотрены предопределенные контексты интерпретации, часто используемые при построении моделей динамических систем. Использование данного формализма иллюстрируется на примере построения модели системы светофоров, представленной на языке описания контекстных систем CML.

Ключевые слова: динамические системы, спецификация, моделирование, семантика, системы переходов, онтология, контекстные машины

Введение

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

Для простых динамических систем таким формализмом являются системы переходов (§1) и их расширение -- помеченные системы переходов (§2).

§1. Система переходов -- это пара (st, tr), где st -- множество состояний, tr -- подмножество декартова произведения st Ч st, называемое отношением перехода. Факт (s, s?) ? tr означает, что из состояния s можно перейти в состояние s?.

§2. Помеченная система переходов -- это тройка (st, lab, tr), где st -- множество состояний, lab -- множество меток, tr -- подмножество декартова произведения st Ч lab Ч st, называемое отношением помеченных переходов. Факт (s, l, s?) ? tr означает, что из состояния s можно перейти в состояние s? по метке l. Метки могут интерпретироваться как действия, агенты и т. д.

Однако при моделировании концептуально сложных динамических систем использовать такой формализм становится неудобным.

Логико-алгебраический подход к решению этой задачи, основанный на машинах абстрактных состояний, был предложен Гуревичем [1]. Машины абстрактных состояний -- специальный вид систем переходов, состояниями в которых являются алгебраические системы. Выбор подходящей сигнатуры алгебраической системы позволяет приблизить формальное описание динамической системы к ее естественной концептуальной структуре. Примеры приложений этого формализма могут быть найдены в [2]. Этот подход реализован в языках ASML [3] и XASM [4].

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

Этот формализм является обобщением онтологических систем переходов [5, 6] -- гибрида систем переходов и онтологических моделей.

Работа имеет следующую структуру. В разделе 2 дано определение контекстной машины. Раздел 3 описывает виды контекстов интерпретации. Раздел 4 посвящен построению модели простой системы светофоров. На примере спецификации этой модели рассмотрены некоторые конструкции разрабатываемого в настоящее время языка описания контекстных машин CML. Язык CML -- это дальнейшее развитие языка описания онтологических систем OTSL [7, 8, 9].

Работа частично поддержана грантом РФФИ 08-01-00899-а и интеграционным проектом РАН № 2/12.

1. Контекстные машины

Контекстные машины предназначены для спецификации и моделирования динамических систем, состояния и переходы которых имеют сложную концептуальную структуру.

Этот формализм обогащает системы переходов за счет добавления интерпретируемых форм и различных контекстов их (форм) интерпретации.

Формально контекстная машина есть пятерка

(st, frm, fvs, ic, {sem_{фф ? ic})},

где st -- множество состояний (§4), frm -- множество форм (§5), fvs -- множество значений форм (§6), ic -- множество контекстов интерпретации (§7), {sem_ф}_{ф ? ic} -- семейство интерпретаций форм в соответствии с контекстами интерпретации (§8).

§4. Множество st специфицирует множество состояний моделируемой системы.

§5. Множество форм frm представляет сущности, которые могут тем или иным образом проинтерпретированы. Форма -- это способ получения информации о системе. При этом способе информация извлекается как результат интерпретации формы в том или ином контексте.

§6. Множество fvs определяет значения, которые могут принимать формы.

§7. Множество контекстов интерпретации ic специфицирует названия контекстов, в которых может быть проинтерпретирована форма.

§8. Функции из семейства интерпретаций форм отображают frm Ч st в fvs. Они определяют способы интерпретации форм в соответствии с контекстами интерпретации. Значение sem_{ф(A, s)} называется значением (или семантикой) формы A в состоянии s в контексте ф.

2. Предопределенные контексты интерпретации

Определим ряд предопределенных контекстов интерпретации (§9), которые часто встречаются при моделировании систем, и соответствующих им интерпретаций форм (§10). Также опишем относящуюся к ним терминологию (§11).

§9. Множество предопределенных контекстов интерпретации включает:

1) fr (или form) -- форма интерпретируется как форма;

2) o (или object) -- форма интерпретируется как объект;

3) f (или formula) -- форма интерпретируется как формула;

4) c (или concept) -- форма интерпретируется как понятие;

5) t (или transition) -- форма интерпретируется как переход;

6) to (или transition-effect object) -- форма интерпретируется как объект с эффектом перехода;

7) tf (или transition-effect formula) -- форма интерпретируется как формула с эффектом перехода;

8) tc (или transition-effect concept) -- форма интерпретируется как понятие с эффектом перехода;

9) ot (или object-effect transition) -- форма интерпретируется как переход с эффектом объекта;

10) ft (или formula-effect transition) -- форма интерпретируется как переход с эффектом формулы;

11) ct (или concept-effect transition) -- форма интерпретируется как переход с эффектом понятия.

§10. Пусть A -- интерпретируемая форма, s -- состояние, в котором A интерпретируется, bool -- множество с формами true и false в качестве элементов. Интерпретации для предопределенных контекстов задаются следующим образом:

1) sem_fr(A, s) = A;

2) sem_o(A, s) ? frm;

3) sem_f(A, s) ? bool;

4) sem_c(A, s) ? pset(frm);

5) sem_o(A, s) ? pset(st);

6) sem_to(A, s) ? frm Ч pset(st);

7) sem_tf(A, s) ? bool Ч pset(st);

8) sem_tc(A, s) ? pset(frm) Ч pset(st);

9) sem_ot(A, s) ? pset(frm Ч st);

10) sem_ft(A, s) ? pset(bool Ч st);

11) sem_ct(A, s) ? pset(pset(frm) Ч st).

Здесь pset(M) обозначает множество всех подмножеств множества M.

§11. Будем говорить, что объект (формула и т. д.) A имеет значение sem_{o(A, s)} (sem_{f(A, s)} и т. д.) в состояние s.

Форма A называется экземпляром понятия B в состояние s, если A ? sem_{c(B, s)}. Значение понятия A в состоянии s называется содержимым понятия A в состоянии s.

Переход (переход с эффектом объекта и т. д.) A называется невыполнимым в состоянии s, если множество sem_{t(A, s)} (sem_{ot(A, s)} и т. д.) пусто.

Объект (формула, понятие) с эффектом перехода могут изменять состояние системы. Однако их значение не зависит от того, в какое новое состояние переходит система.

Для переходов с эффектом объекта (формулы, понятия) каждому изменению состояния соответствует свое значение объекта (формулы, понятия).

3. Модель системы светофоров

Опишем модель системы светофоров, состоящую из двух светофоров A и B и таймера T, который управляет временем переключения светофоров. Эта модель включает спецификации светофора (§12), таймера (§13) и начальной инициализации (запуска) системы светофоров (§14), представленные на языке CML.

§12. Спецификация светофора состоит из определений двух понятий -- светофор и цвет светофора.

Понятие цвет светофора определяется переходом

1 (concept: цвет светофора;

2 body:

3 (one of: this;

4 sequence: красный желтый-после-красного зеленый желтый-после-зеленого))

Форма вида A: B; в этом переходе называется полем с именем A (или просто полем A) и значением B. Поле concept (1) задает имя понятия. Поле body (2) задает формулу (3), определяющую множество экземпляров понятия цвет светофора. Некоторая форма является экземпляром этого понятия в состоянии s, если ее подстановка в формулу на место this дает в результате формулу, истинную в состоянии s. Поле one of (3) в формуле определяет элемент, который проверяется на принадлежность последовательности. Эта последовательность задается полем sequence. Таким образом, понятие цвет светофора включает 4 экземпляра: красный, желтый-после-красного, зеленый и желтый-после-зеленого.

Понятие светофор задается переходом

(concept: светофор;

1 (object: сигнал; type: цвет светофора)

2 (transition: переключиться;

body:

(if: (=: this.цвет; красный);

then: (object: this.цвет; value: желтый-после-красного);

elseif: (=: this.цвет; желтый-после-красного);

then: (object: this.цвет; value: зеленый);

elseif: (=: this.цвет; зеленый);

then: (object: this.цвет; value: желтый-после-зеленого);

else: (object: this.цвет; value: красный)))

3 (input signal: переключиться; body: this.переключиться))

Это понятие определяется таким образом, что с любым его экземпляром связывается объект сигнал (1), переход переключиться (2) и входной сигнал переключиться (3).

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

Переход переключиться (2) описывает порядок переключения сигналов светофора. Он содержит переходы вида

(if: A; then: B; elseif: C₁; then: D₁; ...; elseif: C_n; then: D_n; else: E)

И (object: A; value: B)

Первый из них имеет стандартную семантику условного оператора, а второй устанавливает значение объекта A равным B.

До сих пор рассматривались предопределенные контексты интерпретации форм такие, как формулы, понятия, объекты и переходы. Переход input signal (3) определяет новый контекст интерпретации с именем input signal. Интерпретация формы A.переключиться в контексте input signal заключается в проверке факта, что светофор A получил сигнал переключиться. Если такой сигнал получен, то выполняется переход переключиться. В противном случае, ничего не происходит.

§13. Спецификация таймера состоит из определения понятия таймер. Это понятие задается переходом

(concept: таймер;

1 (object: интервал; type: integer)

2 (object: интервал для зеленого; type: integer)

3 (object: интервал для желтого; type: integer)

4 (object: время; type: integer; value: 0)

5 (object: такт; type: integer; value: 1)

6 (object: число тиков; type: integer; value: 0)

7 (transition: сменить интервал;

body:

(if: (=: this.интервал; this.интервал для зеленого);

then: (object: this.интервал; value: this. интервал для желтого)

else: (object: this.интервал; value: this. интервал для зеленого)))

8 (transition: тик;

body:

(object: this.число тиков; value: (+: this.число тиков; 1))

(if: (=: this.число тиков; this.такт);

then: (object: this.время; value: (+: this.время, this.тик))

(if: (>=: this.время; this.интервал);

then:

(object: this.время; value: 0)

(send: переключиться)

this.сменить интервал)))

9 (input signal: тик; body: this.тик))

Таким образом, с каждым экземпляром понятия таймер связаны: объекты интервал (1), интервал для зеленого (2), интервал для желтого (3), время (4), такт (5) и число тиков (6); переходы сменить интервал (7) и тик (8) и входной сигнал тик (9).

Время таймера подразделяется на внешнее и внутреннее. Внешнее время таймера измеряется в тактах. Внутреннее время таймера измеряется в тиках. Объект такт (5) определяет число тиков, соответствующее одному такту. Объект число тиков (6) хранит количество тиков, произошедших после последнего такта.

Объект интервал (1) определяет число тактов, по завершении которых таймер сработает и пошлет светофорам сигнал переключиться. Объект интервал для зеленого (2) определяет число тактов, установленное для переключения зеленого или красного сигнала светофора. Объект интервал для желтого (3) определяет число тактов, установленное для переключения желтого сигнала светофора. Объект время (4) определяет количество тактов, выполненных после последнего запуска таймера.

Поле value определений объектов время, такт и число тиков задает значения этих объектов по умолчанию: 0, 1 и 0, соответственно.

Переход сменить интервал (7) меняет значение объекта интервал при смене сигнала светофора.

Переход тик (8) выполняет действия, инициируемые тиком. Поля + и >= в этом переходе определяют операции сложения и «больше или равно» на целых числах. Переход с полем send посылает сигнал переключиться светофорам A и B.

Переход (9) определяет, что при получении таймером сигнала тик выполнится переход тик.

§14. Инициализация системы из двух светофоров A и B и таймера T задается следующим образом:

1 (concept: светофор; value: A)

2 (object: A.сигнал; value: зеленый)

3 (concept: светофор; value: B)

4 (object: B.сигнал; value: красный)

5 (concept: таймер; value: T)

6 (object: T.единица измерения; value: 1000)

7 (object: T.интервал для зеленого; value: 10)

8 (object: T.интервал для желтого; value: 2)

Переход (1) определяет A как экземпляр понятия светофор. Переход (2) устанавливает значение объекта сигнал, связанного со светофором A равным зеленый. Переход (3) определяет B как экземпляр понятия светофор. Переход (4) устанавливает значение объекта сигнал, связанного со светофором A равным красный. Переход (5) определяет T как экземпляр понятия таймер. Переходы (6, 7, 8) устанавливают значения объектов единица измерения, интервал для зеленого и интервал для желтого равными 1000, 10 и 2, соответственно. Таким образом, если тик равен миллисекунде, то один такт таймера соответствует одной секунде (1000 миллисекунд), а время ожидания смены зеленого и желтого сигналов светофора равно 10 и 2 секундам, соответственно.

Заключение

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

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

В настоящее время ведется доработка формальной спецификации языка CML и разрабатываются примеры его применения для моделирования концептуально сложных динамических систем. Одним из классов таких систем являются абстрактные машины, задающие формальную семантику современных языков программирования [10, 11, 12]. Другой класс подобных систем -- малые (light-weight) информационные системы, которые при относительно простом поведении имеют достаточно сложную концептуальную структуру [5, 8, 13].

Литература

[1] Гуревич Ю. Последовательные машины абстрактных состояний // Сборник научных трудов «Формальные методы и модели информатики». Серия «Системная информатика», Новосибирск, Издательство СО РАН. 2004. № 9. C. 7-50.

[2] Huggins J. Abstract State Machines Web Page. http://www.eecs.umich.edu/gasm.

[3] AsmL: The Abstract State Machine Language. -- Reference Manual. 2002. http://research.microsoft.com/fse/asml/doc/AsmL2\_Reference.doc.

[4] XasM An Extensible, Component-Based Abstract State Machines Language. http://xasm.sourceforge.net/XasmAnl00/XasmAnl00.html.

[5] Ануреев И.С. Онтологии и системы переходов // Материалы 11 национальной конференции по искусственному интеллекту с международным участием (КИИ-08), Дубна, 2008. -- Том 3. -- С. 173-180.

[6] Anureev I.S. Ontological Transition Systems // Joint NCC&IIS Bulletin, Series Computer Science. -- 2007. -- Vol. 26 -- P. 1-18.

[7] Anureev I.S. A Language of Actions in Ontological Transition Systems // Joint NCC&IIS Bulletin, Series Computer Science. -- 2007. -- Vol. 26. -- P. 19-38.

[8] Ануреев И.С. Язык описания онтологических систем переходов OTSL как средство формальной спецификации программных систем // Вестник НГУ, серия «Информационные технологии», Т. 6, вып. 3. -- С. 24-34. -- 2008.

[9] Anureev I.S. Ontological models in OTSL // Problems in Programming. -- 2008. -- № 2-3. -- P. 41-49.

[10] Ануреев И.С. Операционно-онтологический подход к формальной спецификации языков программирования // Программирование. -- № 1. -- 2009. -- С. 1-11.

[11] Ануреев И.С. Операционно-онтологическая семантика обработки исключений // Тезисы докладов международной конференции “Космос, астрономия и программирование» (Лавровские чтения). -- Санкт-Петербургский государственный университет, Санкт-Петербург,

[12] Ануреев И.С. Операционно-онтологическая семантика операторов безусловной передачи управления в языке C# // Тезисы докладов международной конференции “Космос, астрономия и программирование» (Лавровские чтения). -- Санкт-Петербургский государственный университет, Санкт-Петербург, 2008. -- С. 259-266.2008. -- С. 15-22.

[13] Ануреев И.С. Онтологические системы переходов // Труды XIII Байкальской Всероссийской конференции «Информационные и математические технологии в науке и управлении», Том 1, 2008. -- С. 307-315.

Размещено на Allbest.ru