CTL * - это надмножество логики вычислительного дерева (CTL) и линейной временной логики (LTL). Он свободно комбинирует кванторы путей и временные операторы. Как и CTL, CTL * - это логика времени ветвления. Формальная семантика формул CTL * определяется по отношению к данной структуре Крипке .
LTL был предложен для проверки компьютерных программ первым Амиром Пнуэли в 1977 году. Четыре года спустя, в 1981 году, Э.М. Кларк и Е.А. Эмерсон изобрели проверку моделей CTL и CTL . CTL * был определен EA Emerson и Joseph Y. Halpern в 1983 г. [1]
CTL и LTL были разработаны независимо до CTL *. Обе подлогики стали стандартами в сообществе проверяющих моделей , в то время как CTL * имеет практическое значение, поскольку обеспечивает выразительную тестовую площадку для представления и сравнения этих и других логик. Это удивительно [ необходима цитата ], потому что вычислительная сложность проверки модели в CTL * не хуже, чем у LTL: они оба лежат в PSPACE .
Язык из хорошо сформированных CTL * формул генерируется следующим однозначным (относительно скобки) контекстно-свободной грамматики :
где колеблется по набору атомарных формул . Действительные CTL * -формулы построены с использованием нетерминального. Эти формулы называются формулами состояний , а формулы , созданные с помощью символаназываются формулами пути . (Вышеупомянутая грамматика содержит некоторые избыточности; например,а также импликации и эквивалентности может быть определена как только для булевых алгебр (или логики ) от отрицания и конъюнкции, и временные операторы Х и У являются достаточными для определения двух других .)
Операторы в основном такие же, как в CTL . Однако в CTL каждый темпоральный оператор () должен непосредственно предшествовать квантификатор, в то время как в CTL * этого не требуется. Квантор универсального пути может быть определен в CTL * таким же образом, как и для классического исчисления предикатов. , хотя это невозможно во фрагменте CTL.
Примеры формул
- Формула CTL *, которой нет ни в LTL, ни в CTL:
- Формула LTL, которой нет в CTL:
- Формула CTL, которой нет в LTL:
- Формула CTL *, которая находится в CTL и LTL:
Примечание: при использовании LTL в качестве подмножества CTL * любая формула LTL неявно имеет префикс универсального квантификатора пути. .
Семантика CTL * определяется относительно некоторой структуры Крипке . Как следует из названий, формулы состояний интерпретируются по отношению к состояниям этой структуры, а формулы путей интерпретируются по путям на ней.
Формулы состояний
Если государство структуры Крипке удовлетворяет формуле состояния это обозначено . Это отношение определяется индуктивно следующим образом:
- для всех путей начиная с
- на какой-то путь начиная с
Формулы пути
Отношение удовлетворения для формул пути и путь также определяется индуктивно. Для этого пусть обозначить подпуть :
Проверка модели CTL * является PSPACE-полной [2], а проблема выполнимости - 2EXPTIME-полной . [2] [3]