Как CGAAL проверяет модели: более глубокое понимание

:::информация Этот документ доступен на arxiv под лицензией CC 4.0.

Авторы:

(1) Фальке Б. О. Карлсен, факультет компьютерных наук, Ольборгский университет, Дания, & falkeboc@cs.aau.dk;

(2) Ларс Бо П. Фриденсков, факультет компьютерных наук, Ольборгский университет, Дания, & larsbopark@gmail.com;

(3) Николай О. Йенсен, факультет компьютерных наук, Ольборгский университет, Дания, & noje@cs.aau.dk;

(4) Йенер Расмуссен, jener@jener.dk;

(5) Матиас М. Соренсен, mathiasmehlsoerensen@gmail.com;

(6) Асгер Г. Вейрсе, asger@weircon.dk;

(7) Матиас К. Йенсен, факультет компьютерных наук, Ольборгский университет, Дания, & mcje@cs.aau.dk;

(8) Ким Г. Ларсен, факультет компьютерных наук, Ольборгский университет, Дания, & кгl@cs.aau.dk.

:::

Таблица ссылок

Введение

Определения

Проверка модели

Обзор инструмента

Оценка

Выводы и ссылки

3 Проверка модели

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

Расширенные графы зависимостей Расширенный граф зависимостей (EDG) представляет собой кортеж G = ⟨C,E,N⟩, где

C — конечное множество конфигураций (вершин), E ⊆C×P(C) — конечное множество гиперребер и N ⊆C×C — конечное множество ребер отрицания.

3.1 Кодирование ATL в EDG

Сначала мы установим некоторые определения, относящиеся к подмножествам векторов ходов, индуцированных коалицией игроков.

Учитывая это обозначение, мы определяем функцию pmoves. Функция pmoves возвращает набор всех

возможные частичные ходы, которые следуют от игроков множества A ⊆ Σ, совершающих комбинацию ходов в состоянии q ∈ Q:

Например, если D(q) = {1,2}×{1,2} в игре с двумя игроками и A = {1}. Тогда pmoves(q,A) = {{1}× {1,2},{2}×{1,2}} содержит два частичных хода. В одном игрок 1 выбирает действие 1, а в другом игрок 1 выбирает действие 2. Другими словами, функция pmoves создает частичные ходы, из которых набор игроков A может выбирать при совместной работе в состоянии в. Если A выбирает V ∈ pmoves(q,A), то V содержит все векторы ходов, полученные в результате того, что оставшиеся игроки Σ/A также сделали выбор.

Мы определяем частичную функцию перехода ∆, которая создает набор возможных состояний-преемников при условии состояния q ∈ Q и частичного перемещения V. Это

С введением EDG, присвоений и частичных ходов мы теперь можем определить, как отношение удовлетворения ⊧ может быть закодировано как EDG.

Кодировка. Учитывая CGS S, состояние q состояния S и формулу состояния ATL φ, мы теперь создаем EDG, где каждая конфигурация представляет собой либо пару состояния и формулы, либо тройку состояния, частичного хода и формулы. Тройки представляют частично оцененные состояния, в которых ходы некоторых игроков уже заданы. Начиная с исходной пары ⟨q,φ⟩, строится граф зависимостей согласно рисункам с 1 по 6. На рисунках показано, какие исходящие ребра имеет каждая конфигурация, и целевые конфигурации этих ребер.

Доказательство теоремы 3.1 можно найти в расширенной версии этой статьи.

3.2 Стратегии поиска

Алгоритм CERTAINZERO управляется стратегией поиска, которая определяет, в каком порядке исследуются и оцениваются ребра. Наши стратегии поиска для CGAAL включают общие стратегии поиска в ширину (BFS) и поиска в глубину (DFS), а также несколько стратегий поиска, основанных на эвристике. Некоторые из них обсуждаются в следующих подразделах. Какая стратегия лучше, во многом зависит от формы EDG, которая определяется рассматриваемой формулой CGS и ATL. Оценку стратегий можно найти в разделе 5. Стратегия BFS является стратегией по умолчанию.

Эвристический поиск зависимостей (DHS) PageRank [15] — это алгоритм, созданный для оценки важности веб-сайта на основе количества других веб-сайтов, имеющих на него ссылки. С тех пор эта идея использовалась в других областях, таких как системы рекомендаций по графам [13] или измерение сходства структурного контекста с помощью SimRank [7]. Наш эвристический поиск зависимостей (DHS) использует аналогичную идею, предполагая, что важны конфигурации со многими входящими ребрами. Нахождение их назначений приводит к увеличению обратного распространения ошибки, приближая нас к завершению. Другими словами, эвристика фокусируется на стволе EDG, где определенные назначения имеют высокую ценность. В частности, DHS отдает приоритет ребрам, где исходная конфигурация имеет большое количество входящих ребер. То есть, если e является ребром с исходной конфигурацией c, то:

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

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

Эвристический поиск нестабильности (IHS) Средство проверки модели сети Петри TAPAAL [8] также реализует алгоритм CERTAINZERO. Их конфигурации состоят из маркировки (состояния) и свойства, а их стратегия поиска по умолчанию использует эвристику, которая оценивает расстояние между маркировкой конфигурации и маркировкой, удовлетворяющей формуле конфигурации. Наша новая эвристика нестабильности основана на их эвристике, но мы отличаемся тем, что признаем, что, поскольку в EDG есть отрицательные ребра, мы не всегда можем искать состояние, которое удовлетворяет формуле. То есть, если состояние уже удовлетворяет связанной формуле, вместо этого мы оцениваем расстояние до состояния, которое не удовлетворяет. Это направляет поиск в сторону конфигураций, в которых назначение нестабильно и, следовательно, может иметь большое влияние. Алгоритмы 1 и 2 находят описанное выше distIHS для ребра. В алгоритмах используется абстрактная метрика BiDist, которая для пар состояние-свойство находит ⟨tˆ, ˆf⟩, где tˆ — расстояние до истинного свойства, а ˆf — расстояние до ложного свойства.

Этот документ доступен на Arxiv по лицензии CC 4.0.