Как вычислить достижимое символическое пространство состояний для двоичной диаграммы решений

Question

Этот вопрос о том, как создать символьное пространство состояний для проверки символьной модели. Сначала я перейду к некоторому фону, который заставляет меня хотеть сделать это для MDD, затем я объясню вопрос более подробно.

Эта лекция Эдмунда М. Кларка (одного из основателей проверки моделей) представляет символическую проверку моделей. В нем говорится, что контролеры "промышленной силы" модели используют логическое кодирование (двоичные диаграммы решений, или BDD) для решения проблемы взрыва состояния. Однако, это позволяет только на порядок больше состояний, чем регулярная проверка модели. Я пропустил регулярную проверку модели, которая непосредственно строит график перехода состояния программы, так как я могу представить, что это нецелесообразно немедленно.

Я видел несколько работ, описывающих качества лучше, чем BDD, такие как обработка большего количества состояний 1 (избегая?! проблема взрыва в пространстве состояний), общее ускорение 2 (проверка ограниченной модели), использование методов сопоставления состояний для ограничения поиска в пространстве состояний (помимо проверки ограниченной модели) 3 и использование MDD, которые выполняют на несколько порядков быстрее, чем существующие BDD [4] [5].

BDD увеличил число поддерживаемых штатов в среднем с 10^6 до 10^20. Эта статья также говорит:

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

Таким образом, кажется, что MDD или даже EDD являются лучшим выбором для проверки модели. Существуют также краевые BDD (EVBDD). Но мой вопрос заключается в том, как построить символическое пространство состояний для ~MDD (или того, что лучше). Этот документ представляет его, но, похоже, не объясняет, как на самом деле его генерировать. Они заявляют:

Мы используем квазиредуцированные, упорядоченные, неотрицательные краевые, многозначные диаграммы решений.

Хотите знать, можно ли объяснить алгоритм генерации пространства состояний для MDD на высоком уровне, и каковы структуры данных, которые участвуют в системе, например, каковы свойства node Объект (как структура C). Я думаю, что если я смогу увидеть общую картину структуры данных и примерно, как работает алгоритм, этого будет достаточно для реализации.

Кроме того, я не уверен, что нужно сделать с начальной программой и спецификацией. Так что, если объяснение может быстро описать / представить, как генерировать промежуточные объекты, это было бы полезно. Добавляя это, я видел в одном документе, что у них есть программа в форме сети Петри, которую они затем конвертируют в MDD, и я не уверен, как бы я преобразовал программу в сеть Петри, или если это даже необходимо. В основном, как перейти от исходного кода к MDD на высоком уровне.

Я думаю, что это изображение является алгоритмом генерации пространства состояний, но мне было трудно понять его детали. В частности, о задействованных структурах данных и о том, откуда происходит "состояние", т. Е. Являются ли они логическими предикатами из какой-либо другой модели или как.

Этот также кажется близким:

Вот еще из той же статьи:

---

(1) В этой статье мы показываем, как булевы процедуры принятия решений, такие как метод Штальмарка [16] или процедура Дэвиса и Путнэма [7], могут заменить BDD. Этот новый метод позволяет избежать космического взрыва BDD, гораздо быстрее генерирует контрпримеры, а иногда и ускоряет проверку.

(2) Основным результатом работы является улучшение O(N) во временной сложности проверки формул, ограниченных по времени, где N - число состояний в рассматриваемом CTMC.

(3) Мы опираемся на нашу предыдущую работу, где мы предложили комбинацию символьного выполнения и проверки модели для анализа программ со сложными входными данными [14,19]. В этой работе мы наложили ограничение на входной размер и (или) глубину поиска средства проверки модели. Здесь мы не ограничиваемся проверкой ограниченной модели и изучаем методы сопоставления состояний, чтобы ограничить поиск в пространстве состояний. Мы предлагаем метод проверки, когда символическое состояние относится к другому символическому состоянию.

(4) Мы представляем новый алгоритм генерации пространств состояний асинхронных систем с использованием многозначных диаграмм решений. В отличие от связанной работы, мы кодируем функцию next{state системы не в виде одной булевой функции, а в виде перекрестных {произведений целочисленных функций. Это позволяет применять различные итерационные стратегии для построения пространства состояний системы. В частности, мы представляем новую элегантную стратегию под названием насыщенность и внедряем ее в инструмент SMART. Помимо того, что обычно выполняемые на несколько порядков быстрее, чем существующие генераторы пространства состояний на основе BDD, требуемая пиковая память нашего алгоритма часто близка к конечной памяти, необходимой для хранения общего пространства состояний.

(5) Символьные методы, основанные на двоичных диаграммах принятия решений (BDD), широко используются для рассуждения о временных свойствах аппаратных схем и синхронных контроллеров. Однако они часто плохо работают при работе с огромными пространствами состояний, лежащими в основе систем, основанных на семантике чередования, такой как протоколы связи и распределенное программное обеспечение, которые состоят из независимо действующих подсистем, которые обмениваются данными через общие события... Эта статья показывает, что эффективность методы исследования состояния пространства с использованием диаграмм решений могут быть существенно улучшены путем использования семантики чередования, лежащей в основе многих моделей систем, основанных на событиях и компонентах. Представлен новый алгоритм для символического генерирования пространств состояний, который (i) кодирует векторы состояния модели с помощью многозначных диаграмм решений (MDD), а не объединяет их в BDD.

---

Становится ближе с этим:

Достижимое пространство состояний X_reach можно охарактеризовать как наименьшее решение уравнения с фиксированной точкой X ⊆ X_init ∪ T(X). Алгоритм Bfs реализует именно это вычисление с фиксированной точкой, где множества и отношения хранятся с использованием MDD L-уровня и 2L-уровня соответственно, то есть узел p кодирует набор X_p, имеющий характеристическую функцию v_p, удовлетворяющую

v_p(i_L,...,i_1) = 1 ⇔ (i_L,...,i_1) ∈ X_p.

Объединение множеств просто реализуется путем применения оператора Or к их характеристическим функциям, а вычисление состояний, достижимых за один шаг, реализуется с использованием функции RelProd (конечно, если используются MDD, то должна использоваться версия этих функций MDD). вместо BDD). Поскольку он выполняет поиск символа в ширину, алгоритм Bfs останавливается ровно на таком же количестве итераций, что и максимальное расстояние любого достижимого состояния от начальных состояний.

mdd Bfs(mdd Xinit) is
local mdd p;
  p ← Xinit;
  repeat
    p ← Or(p, RelProd(p, T ));
  until p does not change;
  return p;

bdd Or(bdd a, bdd b) is
local bdd r, r0, r1;
local level k;
  if a = 0 or b = 1 then return b;
  if b = 0 or a = 1 then return a;
  if a = b then return a;
  if Cache contains entry hORcode, {a, b} : ri then return r;
  if a.lvl < b.lvl then
    k ← b.lvl;
    r0 ← Or(a, b[0]);
    r1 ← Or(a, b[1]);
  else if a.lvl > b.lvl then
    k ← a.lvl;
    r0 ← Or(a[0], b);
    r1 ← Or(a[1], b);
  else • a.lvl = b.lvl
    k ← a.lvl;
    r0 ← Or(a[0], b[0]);
    r1 ← Or(a[1], b[1]);
  r ← UniqueTableInsert(k, r0, r1);
  enter hORcode, {a, b} : ri in Cache;
  return r;

bdd RelProd(bdd x, bdd2 t) is • quasi-reduced version
local bdd r, r0, r1;
  if x = 0 or t = 0 then return 0;
  if x = 1 and t = 1 then return 1;
  if Cache contains entry hRELPRODcode, x, t : ri then return r;
  r0 ← Or(RelProd(x[0], t[0][0]), RelProd(x[1], t[1][0]));
  r1 ← Or(RelProd(x[0], t[0][1]), RelProd(x[1], t[1][1]));
  r ← UniqueTableInsert(x.lvl, r0, r1);
  enter hRELPRODcode, x, t : ri in Cache;


mdd Saturation(mdd Xinit) is
  return Saturate(L, Xinit);

mdd Saturate(level k, mdd p) is
local mdd r, r0, ..., rnk−1;
  if p = 0 then return 0;
  if p = 1 then return 1;
  if Cache contains entry hSATcode, p : ri then return r;
  for i = to nk − 1 do
  ri ← Saturate(k − 1, p[i]);
  repeat
  choose e ∈ Ek, i, j ∈ Xk, such that ri 6= 0 and Te[i][j] 6= 0;
  rj ← Or(rj , RelProdSat(k − 1, ri, Te[i][j]));
  until r0, ..., rnk−1 do not change;
  r ← UniqueTableInsert(k, r0, ..., rnk−1);
  enter hSATcode, p : ri in Cache;
  return r;

mdd RelProdSat(level k, mdd q, mdd2 f) is
local mdd r, r0, ..., rnk−1;
  if q = 0 or f = 0 then return 0;
  if Cache contains entry hRELPRODSATcode, q, f : ri then return r;
  for each i, j ∈ Xk such that q[i] 6= 0 and f[i][j] 6= 0 do
  rj ← Or(rj , RelProdSat(k − 1, q[i], f[i][j]));
  r ← Saturate(k, UniqueTableInsert(k, r0, ..., rnk−1));
  enter hRELPRODSATcode, q, f : ri in Cache;
  return r.

Answer 1

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

Все исходные предложения включают кодирование отношения перехода R как подмножества SxS, поэтому переход t из s->s'возможен, если пара (s,s') находится в R. Специальная операция произведения между этим DD и ДД для набора состояний выполняется, получая наследников за один шаг. Но работы Ciardo et al. вы читаете более продвинутые и, как правило, используете формы с уменьшенной MxD/ идентичностью, так что переменные, на которые переход не влияет (не заботится), могут быть пропущены в кодировке. Тем не менее, они заканчиваются DD, который имеет две переменные (до и после) для каждой переменной состояния, так что все еще подмножества SxS.

Поэтому, начиная с программы, вы обычно хотите избавиться от рекурсии / стека, ограничить количество переменных (чтобы вы могли работать с массивом, слишком большим для большинства состояний), сделать все переменные дискретными (например, целые числа),

Если вы можете получить модель в этой форме, но по-прежнему выполнять сложные операции, такие как арифметика и присваивания (то есть вы не можете написать свою задачу в виде сети Петри), возможно, наиболее продвинутые пакеты

• LTSMin (см. Эту статью CAV'10 или, скорее, ее расширенную форму TR). Они вводят непрозрачные функции N переменных в символическую настройку с помощью "PINS").
• Другое усилие в общих переходных отношениях с MDD - это ITS-инструменты и их формализм GAL (см. Статью tacas'15), или CAV'13 для более подробной информации о том, как кодировать арифметику в DD.