WikiDer > Модальное μ-исчисление

Modal μ-calculus

В теоретическая информатика, то модальное μ-исчисление (, Lμ, иногда просто μ-исчисление, хотя это может иметь более общее значение) является расширением пропозициональный модальная логикамного модальностей) добавив наименьшая фиксированная точка оператор μ и оператор наибольшая фиксированная точка оператор , таким образом логика с фиксированной точкой.

(Пропозициональное, модальное) μ-исчисление происходит от Дана Скотт и Жако де Баккер,[1] и был развит Декстер Козен[2] в наиболее используемую в настоящее время версию. Он используется для описания свойств маркированные переходные системы и для проверка эти свойства. Много темпоральная логика можно закодировать в μ-исчислении, включая CTL * и его широко используемые фрагменты -линейная темпоральная логика и вычислительная древовидная логика.[3]

Алгебраическая точка зрения - рассматривать это как алгебра из монотонные функции через полная решетка, с операторами, состоящими из функциональный состав плюс операторы наименьшей и наибольшей фиксированной точки; с этой точки зрения модальное μ-исчисление находится над решеткой алгебра степенных множеств.[4] В семантика игры μ-исчисления связано с игры для двух игроков с идеальная информация, особенно бесконечное паритетные игры.[5]

Синтаксис

Позволять п (предложения) и А (действия) - два конечных набора символов, и пусть V - счетно бесконечное множество переменных. Набор формул (пропозиционального, модального) μ-исчисления определяется следующим образом:

  • каждое предложение и каждая переменная - это формула;
  • если и формулы, то это формула.
  • если формула, то это формула;
  • если это формула и это действие, то это формула; (произносится либо: коробка или после обязательно )
  • если это формула и переменная, тогда является формулой при условии, что каждое свободное вхождение в происходит положительно, т.е. в рамках четного числа отрицаний.

(Понятия свободных и связанных переменных как обычно, где - единственный оператор привязки.)

Учитывая приведенные выше определения, мы можем обогатить синтаксис:

  • смысл
  • (произносится либо: алмаз или после возможно ) смысл
  • средства , куда означает замену за в целом бесплатные вхождения из в .

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

Обозначение (и его дуал) вдохновлены лямбда-исчисление; цель состоит в том, чтобы обозначить наименьшую (и, соответственно, наибольшую) фиксированную точку выражения где «минимизация» (и, соответственно, «максимизация») находятся в переменной , как в лямбда-исчислении - функция с формулой в связанная переменная ;[6] подробнее см. денотационную семантику ниже.

Денотационная семантика

Модели (пропозиционального) μ-исчисления задаются как маркированные переходные системы куда:

  • набор состояний;
  • сопоставляется с каждой меткой бинарное отношение на ;
  • , отображается в каждое предложение множество состояний, в которых утверждение верно.

Учитывая помеченную систему перехода и интерпретация переменных из -исчисление, , это функция, определяемая следующими правилами:

  • ;
  • ;
  • ;
  • ;
  • ;
  • , куда карты к при сохранении отображений где-либо еще.

По двойственности интерпретация других основных формул такова:

  • ;
  • ;

Менее формально это означает, что для данной переходной системы :

  • выполняется во множестве состояний ;
  • выполняется в каждом состоянии, где и оба держатся;
  • выполняется в каждом состоянии, где не держит.
  • держит в состоянии если каждый -переход, ведущий из приводит к состоянию, когда держит.
  • держит в состоянии если существует -переход, ведущий из что приводит к состоянию, когда держит.
  • выполняется в любом состоянии в любом наборе так что, когда переменная установлен на , тогда относится ко всем . (От Теорема Кнастера – Тарского следует, что это наибольшая фиксированная точка из , и это наименьшая фиксированная точка.)

Интерпретации и на самом деле "классические" из динамическая логика. Дополнительно оператор можно интерпретировать как живость («рано или поздно происходит что-то хорошее») и в качестве безопасность («ничего плохого никогда не происходит») в Лесли ЛэмпортНеофициальная классификация.[7]

Примеры

  • интерпретируется как " верно на каждом а-дорожка".[7] Идея в том, что " верно на каждом а-path "можно аксиоматически определить как это (самое слабое) предложение что подразумевает и которое остается верным после обработки любого а-метка. [8]
  • интерпретируется как наличие пути по а-переходы в состояние, когда держит.[9]
  • Свойство системного существа тупик-свободно, означающее отсутствие состояний без исходящих переходов и, кроме того, что путь к такому состоянию не существует, выражается формулой[9]

Проблемы с решением

Удовлетворенность формулы модального μ-исчисления EXPTIME-завершено.[10] Что касается линейной временной логики,[11] проверка модели, выполнимости и валидности линейного модального μ-исчисления являются PSPACE-полный.[12]

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

Примечания

  1. ^ Скотт, Дана; Баккер, Якобус (1969). «Теория программ». Неопубликованная рукопись.
  2. ^ Козен, Декстер (1982). «Результаты по μ-исчислению высказываний». Автоматы, языки и программирование. ИКАЛП. 140. С. 348–359. Дои:10.1007 / BFb0012782. ISBN 978-3-540-11576-2.
  3. ^ Кларк стр.108, теорема 6; Эмерсон П. 196
  4. ^ Арнольд и Нивинский, стр. Viii-x и глава 6
  5. ^ Арнольд и Нивинский, стр. Viii-x и глава 4
  6. ^ Арнольд и Нивиньски, стр. 14
  7. ^ а б Брэдфилд и Стирлинг, стр. 731
  8. ^ Брэдфилд и Стирлинг, стр. 6
  9. ^ а б Эрих Гредель; Фокион Г. Колайтис; Леонид Либкин; Маартен Маркс; Джоэл Спенсер; Моше Й. Варди; Yde Venema; Скотт Вайнштейн (2007). Теория конечных моделей и ее приложения. Springer. п. 159. ISBN 978-3-540-00428-8.
  10. ^ Клаус Шнайдер (2004). Верификация реактивных систем: формальные методы и алгоритмы. Springer. п. 521. ISBN 978-3-540-00296-3.
  11. ^ Sistla, A. P .; Кларк, Э. М. (1 июля 1985 г.). «Сложность пропозициональной линейной темпоральной логики». J. ACM. 32 (3): 733–749. Дои:10.1145/3828.3837. ISSN 0004-5411.
  12. ^ Варди, М. Ю. (1988-01-01). «Временное исчисление фиксированных точек». Материалы 15-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования. ПОПЛ '88. Нью-Йорк, Нью-Йорк, США: ACM: 250–259. Дои:10.1145/73560.73582. ISBN 0897912527.

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

  • Кларк младший, Эдмунд М .; Орна Грумберг; Дорон А. Пелед (1999). Проверка модели. Кембридж, Массачусетс, США: MIT press. ISBN 0-262-03270-8., глава 7, Проверка моделей для μ-исчисления, стр. 97–108
  • Стирлинг, Колин. (2001). Модальные и временные свойства процессов.. Нью-Йорк, Берлин, Гейдельберг: Springer Verlag. ISBN 0-387-98717-7., глава 5, Модальное μ-исчисление, стр. 103–128
  • Андре Арнольд; Дамиан Нивинский (2001). Зачатки μ-исчисления. Эльзевир. ISBN 978-0-444-50620-7., глава 6, μ-исчисление над алгебрами степенных множеств, стр. 141–153 посвящена модальному μ-исчислению.
  • Иде Венема (2008) Лекции по модальному μ-исчислению; был представлен на 18-й Европейской летней школе по логике, языку и информации
  • Брэдфилд, Джулиан и Стирлинг, Колин (2006). «Модальные мю-исчисления». У П. Блэкберна; J. van Benthem & F. Wolter (ред.). Справочник по модальной логике. Эльзевир. С. 721–756.
  • Эмерсон, Э. Аллен (1996). «Проверка моделей и Мю-исчисление». Описательная сложность и конечные модели. Американское математическое общество. С. 185–214. ISBN 0-8218-0517-7.
  • Козен, Декстер (1983). «Результаты по μ-исчислению высказываний». Теоретическая информатика. 27 (3): 333–354. Дои:10.1016/0304-3975(82)90125-6.

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