Временная логика действий - Temporal logic of actions

Эта статья включает Список ссылок, связанное чтение или внешняя ссылка, но его источники остаются неясными, потому что в нем отсутствует встроенные цитаты. Пожалуйста, помогите улучшать эта статья введение более точные цитаты. (Январь 2011 г.) (Узнайте, как и когда удалить этот шаблон сообщения)

Временная логика действий (TLA) - логика, разработанная Лесли Лэмпорт, который объединяет темпоральная логика с логика действий. Он используется для описания поведения параллельные системы.

Подробности

Утверждения темпоральной логики имеют форму ${ displaystyle [A] _ {t}}$, куда А это действие и т содержит подмножество переменных, входящих в А. Действие - это выражение, содержащее переменные со штрихом и без него, такие как ${ displaystyle x + x '* y = y'}$. Значение переменных без штрихов: значение переменной в этом состоянии. Значение переменных со штрихом: значение переменной в следующем состоянииВышеприведенное выражение означает значение Икс сегодня, плюс значение Икс завтра умноженное на значение y сегодня, равняется значению у завтра.

Значение ${ displaystyle [A] _ {t}}$ состоит в том, что либо A действителен сейчас, либо переменные, фигурирующие в t, не меняются. Это позволяет делать шаги с заиканием, когда ни одна из переменных программы не меняет своих значений.

Смотрите также

• Динамическая логика (модальная логика)
• Временная логика
• PlusCal
• TLA +

Рекомендации

• Лэмпорт, Лесли (2002). Определение систем: TLA⁺ Язык и инструменты для инженеров по аппаратному и программному обеспечению. Эддисон-Уэсли. ISBN  0-321-14306-X. Получено 2007-02-02.
• Лесли Лэмпорт (16 декабря 1994 г.), Введение в TLA (PDF), получено 2010-09-17

внешняя ссылка

• Официальный веб-сайт
• «Система подтверждения TLA +». INRIA.
• Лэмпорт, Лесли (2014). «Мышление для программистов». Мягкое вступление к TLA + на Строить

Этот формальные методы -связанная статья является заглушка. Вы можете помочь Википедии расширяя это.