LTL, CTL или TLA для моделирования для моей модели (подробное описание внутри)?

В настоящее время я пишу магистерскую диссертацию и сталкиваюсь с определением и проверкой моего подхода во временной логике.

Какую временную логику лучше всего использовать в моих обстоятельствах? Мне бы очень хотелось получить отзыв о моем подходе и о том, как действовать

Моя модель состоит из участников, которые будут выполнены одновременно. Для каждого участника можно зарегистрировать правила. Они выглядят примерно так:

conditions -> action

например

received(a, c) ^ received(b,c) -> allowed(c,d) 

это означает, что c должен был получить сообщение от b и один от c, чтобы иметь возможность отправить сообщение d.

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

  1. Если не существует правила, условия которого выполняются: запретить действие

  2. Если существует правило, условия которого выполняются, и оно запрещает действие: запретите действие

  3. Если существует правило, условия которого выполняются, оно разрешает действие, и не существует другого правила, условие которого выполняется и которое запрещает действие: разрешить действие

2 ответа

Решение

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

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

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

Существует неправильное представление о сравнении этих трех логик. И TLA+, и LTL являются линейными логиками. TLA+ является аксиоматической теорией, основанной на теории множеств Цермело-Френкеля, и синтаксически обеспечивает инвариантность заикания (для обеспечения практичности уточнения). LTL - логика высказываний.

CTL кардинально отличается от LTL, потому что CTL - логика времени ветвления, тогда как LTL - логика линейного времени. Отдельная последовательность представляет собой модель для линейной формулы времени. Напротив, дерево является моделью для формулы времени ветвления. Последовательность представляет отдельное выполнение, тогда как дерево представляет много выполнений, которые начинаются в некотором состоянии. Количественная оценка пути доступна в CTL, а в LTL отсутствует. Существует общее подмножество LTL и CTL, но они несопоставимы (= некоторые свойства выражаются только в LTL, другие - только в CTL). CTL* - их общий суперсет.

Для приложения, которое вы рисуете, линейная семантика времени представляется более подходящей. Я бы порекомендовал использовать TLA+, потому что он предлагает хорошую дисциплину для описания систем и является достаточно выразительным во времени, что вам, вероятно, не понадобится LTL (наоборот: если вы не можете указать систему с формулой, инвариантной к заиканию в TLA+, тогда более вероятно, что система нуждается в пересмотре, а не в необходимости полной выразительной мощности LTL).

Книга TLA+ - очень читаемое введение для всех уровней спецификаторов.

Другие вопросы по тегам