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

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

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

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

conditions -> action

e.g. 

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

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

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

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

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

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


logic tla+ model-checking ctl
person nanoquack    schedule 03.03.2014    source источник

Ответы (2)


arrow_upward
8
arrow_downward

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

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

Но… имейте в виду, Temporal Logic — это не просто так, и вам нужно будет потратить некоторое время на чтение и тщательное обдумывание.

person marcmagransdeabril    schedule 03.05.2014

arrow_upward
4
arrow_downward

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

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

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

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

person Ioannis Filippidis    schedule 02.12.2015