T-satisfiability test problem for the VL1 logical language of the VRS system
In this paper we give a short introduction to the satisfiability modulo theories (SMT) problem and demonstrate how the methods developed in the SMT research field can be applied in the requirement verification tool VRS, which supports insertion modelling methodology. We formalize the logical languag...
Збережено в:
Дата: | 2015 |
---|---|
Автор: | |
Формат: | Стаття |
Мова: | Ukrainian |
Опубліковано: |
Інститут програмних систем НАН України
2015
|
Теми: | |
Онлайн доступ: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/78 |
Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
Назва журналу: | Problems in programming |
Репозитарії
Problems in programmingid |
pp_isofts_kiev_ua-article-78 |
---|---|
record_format |
ojs |
resource_txt_mv |
ppisoftskievua/41/f07c7ab39b21bee21f5dcb8772a11041.pdf |
spelling |
pp_isofts_kiev_ua-article-782018-09-18T15:10:04Z T-satisfiability test problem for the VL1 logical language of the VRS system Задача проверки Т-выполнимости для логического языка VL1 системы VRS Завдання перевірки Т-здійсненності для логічнї мови VL1 системи VRS Timofeev, V.G. UDC 004.02 УДК 004.02 УДК 004.02 In this paper we give a short introduction to the satisfiability modulo theories (SMT) problem and demonstrate how the methods developed in the SMT research field can be applied in the requirement verification tool VRS, which supports insertion modelling methodology. We formalize the logical language VL1 used for formal reasoning in VRS and justify decidability of satisfiability problem in that language. Besides we discuss the context of the problem being solved and indicate possible methods that can be used on different stages of solution. Finally, we present a satisfiable conjunction search method, which is based on a set-representation of logical connectives in formulas. В данной работе дается короткое введение в задачу проверки T-выполнимости формул относительно логических теорий, и показывается, что разработанные методы решения этой задачи могут применяться в технологии инсерционного моделирования, которая представлена в системе верификации требований VRS. Дается формализация логического языка, используемого в VRS для проведения формальных рассуждений, и показывается разрешимость проблемы выполнимости формул в этом языке. Обсуждаются особенности применения используемых методов, и описывается альтернативный алгоритм поиска выполнимой конъюнкции, основанный на множественном представлении операций в формулах. У даній роботі дається короткий введення в задачу перевірки T-виконуваності формул щодо логічних теорій, і показується, що розроблені методи вирішення цього завдання можуть застосовуватися в технології інсерційного моделювання, яка представлена в системі верифікації вимог VRS. Дається формалізація логічної мови, використовуваного в VRS для проведення формальних міркувань, і показується можливість розв'язання проблеми здійсненності формул в цій мові. Обговорюються особливості застосування використовуваних методів, і описується альтернативний алгоритм пошуку здійсненним кон'юнкції, заснований на множині поданні операцій в формулах. Інститут програмних систем НАН України 2015-09-10 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/78 PROBLEMS IN PROGRAMMING; No 2-3 (2012) ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2-3 (2012) ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2-3 (2012) 1727-4907 uk https://pp.isofts.kiev.ua/index.php/ojs1/article/view/78/78 Copyright (c) 2015 ПРОБЛЕМИ ПРОГРАМУВАННЯ |
institution |
Problems in programming |
baseUrl_str |
https://pp.isofts.kiev.ua/index.php/ojs1/oai |
datestamp_date |
2018-09-18T15:10:04Z |
collection |
OJS |
language |
Ukrainian |
topic |
UDC 004.02 |
spellingShingle |
UDC 004.02 Timofeev, V.G. T-satisfiability test problem for the VL1 logical language of the VRS system |
topic_facet |
UDC 004.02 УДК 004.02 УДК 004.02 |
format |
Article |
author |
Timofeev, V.G. |
author_facet |
Timofeev, V.G. |
author_sort |
Timofeev, V.G. |
title |
T-satisfiability test problem for the VL1 logical language of the VRS system |
title_short |
T-satisfiability test problem for the VL1 logical language of the VRS system |
title_full |
T-satisfiability test problem for the VL1 logical language of the VRS system |
title_fullStr |
T-satisfiability test problem for the VL1 logical language of the VRS system |
title_full_unstemmed |
T-satisfiability test problem for the VL1 logical language of the VRS system |
title_sort |
t-satisfiability test problem for the vl1 logical language of the vrs system |
title_alt |
Задача проверки Т-выполнимости для логического языка VL1 системы VRS Завдання перевірки Т-здійсненності для логічнї мови VL1 системи VRS |
description |
In this paper we give a short introduction to the satisfiability modulo theories (SMT) problem and demonstrate how the methods developed in the SMT research field can be applied in the requirement verification tool VRS, which supports insertion modelling methodology. We formalize the logical language VL1 used for formal reasoning in VRS and justify decidability of satisfiability problem in that language. Besides we discuss the context of the problem being solved and indicate possible methods that can be used on different stages of solution. Finally, we present a satisfiable conjunction search method, which is based on a set-representation of logical connectives in formulas. |
publisher |
Інститут програмних систем НАН України |
publishDate |
2015 |
url |
https://pp.isofts.kiev.ua/index.php/ojs1/article/view/78 |
work_keys_str_mv |
AT timofeevvg tsatisfiabilitytestproblemforthevl1logicallanguageofthevrssystem AT timofeevvg zadačaproverkitvypolnimostidlâlogičeskogoâzykavl1sistemyvrs AT timofeevvg zavdannâperevírkitzdíjsnennostídlâlogíčnímovivl1sistemivrs |
first_indexed |
2025-07-17T09:58:44Z |
last_indexed |
2025-07-17T09:58:44Z |
_version_ |
1838410132566835200 |
fulltext |
Формальні методи програмування
УДК 004.02
ЗАДАЧА ПРОВЕРКИ Т-ВЫПОЛНИМОСТИ ДЛЯ ЛОГИЧЕСКОГО
ЯЗЫКА VL1 СИСТЕМЫ VRS
В.Г. Тимофеев
Киевский национальный университет имени Тараса Шевченко,
кафедра теории и технологии программирования,
01601 Киев, Украина, ул. Владимирская 64, e-mail: tvalentyn@univ.kiev.ua
В данной работе дается короткое введение в задачу проверки T-выполнимости формул относительно логических теорий, и
показывается, что разработанные методы решения этой задачи могут применяться в технологии инсерционного моделирования,
которая представлена в системе верификации требований VRS. Дается формализация логического языка, используемого в VRS для
проведения формальных рассуждений, и показывается разрешимость проблемы выполнимости формул в этом языке. Обсуждаются
особенности применения используемых методов, и описывается альтернативный алгоритм поиска выполнимой конъюнкции,
основанный на множественном представлении операций в формулах.
In this paper we give a short introduction to the satisfiability modulo theories (SMT) problem and demonstrate how the methods developed
in the SMT research field can be applied in the requirement verification tool VRS, which supports insertion modelling methodology. We
formalize the logical language VL1 used for formal reasoning in VRS and justify decidability of satisfiability problem in that language.
Besides we discuss the context of the problem being solved and indicate possible methods that can be used on different stages of solution.
Finally, we present a satisfiable conjunction search method, which is based on a set-representation of logical connectives in formulas.
Введение
Задача проверки выполнимости логических формул является одной из фундаментальных и прикладных
задач в математической логике. В терминах проверки выполнимости могут быть сформулированы некоторые
задачи верификации программных и аппаратных систем, задачи теории графов, теории расписаний,
статического анализа, автоматической генерации тестов и др. Для этого может быть достаточно даже
простейшего языка логики высказываний. Однако применения формальных методов в разработке
программного и аппаратного обеспечения, и задачах искусственного интеллекта требуют выразительных
возможностей, которые уже выходят за рамки пропозициональной логики. Необходимость решения задачи
выполнимости для более выразительных фрагментов логик в различных предметных областях привело к
появлению задачи Т-выполнимости, ее активному изучению и значительному прорыву в решении с точки
зрения эффективности инструментальных средств и выразительных возможностей поддерживаемых языков. Об
этом свидетельствуют ежегодные конференции, симпозиумы и соревнования программных комплексов в
области исследований, которая получила название Satisfiability Modulo Theories (SMT) [1 – 3]. Название
отражает главную особенность рассматриваемых проблем: приложения формальных методов требуют решения
задачи выполнимости в логике первого порядка относительно одной или нескольких теорий Т,
ограничивающих допустимые интерпретации функциональных и предикатных символов. Например, говоря о
выполнимости формулы линейной арифметики 110 +≥+→=+ yxyx мы заинтересованы только в
стандартных интерпретациях символов 0, 1, + и на множестве действительных чисел. ≥
Актуальность и практическая потребность в решении задачи SMT обосновывается и в данной работе, где
эта задача ставится в контексте технологии инсерционного моделирования, которая разрабатывается в
Институте кибернетики им. В.М. Глушкова НАН Украины.
Инсерционное моделирование [4 – 6] – это технология проектирования систем, основанная на теории
взаимодействий агентов и сред. Этот подход был успешно применен к задачам верификации спецификаций для
распределенных систем реального времени в различных предметных областях [7, 8]. Одно из главных
применений технологии инсерционного моделирования реализуется в системе VRS (Verification of Requirement
Specifications) [5, 8]. Эта система предоставляет возможность проверки требований путем автоматического
доказательства теорем, использованием техник символьной и дедуктивной проверки моделей, а также
генерацией трасс для тестирования с различными критериями покрытия. Основные инструменты системы VRS
разделены на две группы: статические и динамические. Статические инструменты включают проверку
непротиворечивости и полноты спецификаций. Эти инструменты используют специальную процедуру-
решатель (solver), которая обеспечивает проверку выполнимости формул в логическом языке, фрагменте
логики первого порядка. В данной работе мы показываем, что задача, которая ставится перед VRS-решателем,
является типичным примером задачи SMT. Это свидетельствует о том, что достижения в этой области могут
быть использованы для решения задач инсерционного моделирования. Для этого в статье формулируется
проблема проверки выполнимости формулы относительно теории (satisfiability modulo theorу). Затем строится
формализация логического языка VL1, используемого решателем VRS. Далее показывается разрешимость
проблемы выполнимости в этом языке. Также приводится короткий обзор основных подходов, вариации
которых используются в современных SMT-решателях и показывается, как они могут быть применяться для
251
©В.Г. Тимофеев, 2012
ISSN 1727-4907. Проблеми програмування. 2012. № 2-3. Спеціальний випуск
Формальні методи програмування
решения проблемы выполнимости в языке VL1. Из достаточно большого арсенала средств разработанных в
области SMT мы указываем конкретные методы и оценки сложности используемых алгоритмов. Наконец,
описывается альтернативный эвристический метод поиска выполнимой конъюнкции и приводятся данные
результатов экспериментов, демонстрирующие его применимость в контексте системы VRS. Этот метод,
насколько нам известно, не исследовался в SMT-литературе.
Статья структурирована следующим образом. В разделе 1 дается необходимый логический формализм и
описание языка VL1. В разделе 2 формулируется задача выполнимости относительно теории. Основные методы
решения этой задачи, а также особенности их применения в контексте системы VRS, обсуждаются в разделе 3.
В разделе 4 описывается метод поиска выполнимой конъюнкции, основанный на представлении формул с
множественными операциями.
1. Логический язык VL1
Идеология инсерционного моделирования, представленная в системе VRS, предполагает, что исходные
данные для анализа системы представлены в виде спецификации на языке базовых протоколов [9]. Каждая
такая спецификация состоит из двух частей: описание среды и множество базовых протоколов. Описание среды
доопределяет сигнатуру базового языка и возможные ограничения интерпретации этой сигнатуры. Множество
базовых протоколов определяет требования к поведению системы. Во время процесса верификации, система
VRS использует специализированный решатель как средство для проверки выполнимости формулы-свойства,
сформулированной в специальном базовом языке. В частности, это требуется на этапе проверки условия
применимости базового протокола в состоянии. На низком уровне это может быть реализовано путем проверки
выполнимости формул в некотором логическом языке первого порядка. Мы делаем формализацию этого языка
в виде языка VL1.
Анализ практических требований, которые ставятся к решателю системы VRS, показывает, что язык VL1
можно задать в терминах языка многосортной логики предикатов первого порядка.
Язык многосортной логики (ЯМЛ) предикатов первого порядка определяется своей сигнатурой.
Сигнатура языка задается четверкой , где ( , , , )S C F PΣ = Σ Σ Σ Σ SΣ – непустое конечное множество сортов, CΣ ,
FΣ , PΣ – счетные множества констант, функциональных и предикатных символов соответственно. Каждый
символ константы ассоциируется с некоторым сортом σ , каждый функциональный символ ассоциируется с его
типом – объектом вида 1 nσ σ× × →L σ , каждый предикатный символ ассоциируется с типом вида 1 nσ σ× ×L ;
здесь , ,i Sσ σ ∈ 1 . i n≤ ≤
Пусть Var – счетное множество переменных. Каждая переменная ассоциируется с некоторым сортом σ .
Для каждого из сортов в множестве Var имеется бесконечное число переменных этого сорта.
Для данной сигнатуры Σ множества Σ-термов, Σ-атомов и Σ-формул определяются индуктивно. Каждая
переменная x сорта σ есть Σ-терм сорта σ . Каждая константа c сорта σ , Cc∈Σ , есть Σ-терм сорта σ .
Если Ff ∈Σ – функциональный символ типа 1 nσ σ σ× × →L , – Σ-термы сортов 1,..., nt t 1,..., nσ σ
соответственно, то 1( ,..., )nf t t – терм сорта σ .
Множество Σ-атомов состоит из выражений где ),...,( 1 nttp Pp∈Σ – предикатный символ типа
1 nσ σ× ×L , – Σ-термы сортов 1,..., nt t 1,..., nσ σ соответственно.
Каждый Σ-атом является Σ-формулой. Формулы полученные применением к Σ-формулам
пропозициональных связок ( , , , , )¬ ∨ ∧ → ↔ являются Σ-формулами. Если ϕ – Σ-формула, x – переменная сорта
σ , то xσ ϕ∀ и xσ ϕ∃ – Σ-формулы. Приоритеты операций традиционные, для точного указания порядка
применения операций могут использоваться скобки.
Формула ψ называется Σ-литералом, если ψ = ϕ или ψ = ¬ϕ для некоторого атома ϕ.
Множество переменных сорта σ , встречающихся в терме t, обозначается varsσ(t), множество всех
переменных, встречающихся в терме t, обозначается vars(t). Для формулы ϕ обозначим varsσ(ϕ) множество
свободных (не связанных кванторами) переменных сорта σ . Множество всех свободных переменных в
формуле обозначим vars(ϕ). Если vars(ϕ) = ∅, то ϕ считается замкнутой формулой.
Семантика ЯМЛ сигнатуры Σ задается с помощью понятия Σ-интерпретации. Пусть Σ – сигнатура языка,
X – множество переменных, сорта которых принадлежат SΣ . Σ-интерпретация I над X – это отображение,
которое ставит в соответствие каждому сорту Sσ ∈Σ непустое множество Iσ (область значений, носитель
сорта), каждой переменной x X∈ сорта σ – элемент Ix Iσ∈ , каждому символу константы сорта Cc∈Σ σ –
элемент Ic Iσ∈ , каждому функциональному символу Ff ∈Σ типа 1 nσ σ σ× × →L – тотальную функцию
1
:
n
If I I Iσ σ σ× × →L , каждому предикатному символу Pf ∈Σ типа 1 nσ σ× ×L – некоторое
подмножество
1
:
n
I Ip p I Iσ σ⊆ × ×L . В случае, когда множество X ясно из контекста либо пусто, будем говорить
просто о Σ-интерпретации.
252
Формальні методи програмування
Если I – Σ-интерпретация над X, t – Σ-терм такой, что vars(t) ⊆ X, то можно определить понятие
истинностной оценки терма t в интерпретации I (обозначается [ ]It ). Для переменной x полагаем [ ]Ix = Ix , для
константы c полагаем [ ]I Ic c= , для 1( ,..., )nf t t полагаем . )][,,]([)],...,([ 11
I
n
III
n ttfttf K=
Пусть I, J – Σ-интерпретации над X, x X∈ . Будем говорить, что J x-варианта I, если I Jσ σ= для всех
и Sσ ∈Σ I Jr r= для всех объектов . ( \{ })C F Pr X∈Σ ∪Σ ∪Σ ∪ x
Будем считать, что множество истинностных значений состоит из двух элементов {false, true}. Если I –
Σ-интерпретация над X, ϕ – Σ-формула такая, что vars(ϕ) ⊆ X, то можно говорить об истинностной оценке
формулы ϕ в интерпретации I (обозначается [ ]Iϕ ). Для предикатного символа p, и термов t1,…, tn
тогда и только тогда, когда . 1[ ( , , )]I
np t t true=K II
n
I ptt ∈)][,,]([ 1 K [ ]Ix trueσ ϕ∀ = тогда и только тогда, когда
для любой x-варианты J интерпретации I; [ ]trueJ =][ϕ Ix trueσ ϕ∃ = тогда и только тогда, когда для
некоторой x-варианты J интерпретации I; [ ] тогда и только тогда, когда = false. Истинностная
оценка формулы, построенной с помощью бинарных пропозициональных связок ( , , определяется
естественным образом.
trueJ =][ϕ
I trueϕ¬ = I][ϕ
, , )∨ ∧ → ↔
Пусть I – Σ-интерпретация над X, ϕ – Σ-формула такая, что vars(ϕ) ⊆ X. Будем писать I |= ϕ для
обозначения того, что = true. Будем говорить в таком случае, что ϕ истинна в интерпретации I, или что I –
модель формулы ϕ .
I][ϕ
Пусть ϕ – Σ-формула, X = vars(ϕ). Формула ϕ всюду истинна, если I |= ϕ для любой Σ- интерпретации I
над X. Это будем обозначать |=ϕ . Формула ϕ выполнима, если существует Σ-интерпретация I над X такая, что
I |= ϕ . Это будем обозначать |≈ϕ .
Пусть ϕ – Σ-формула, X = vars(ϕ), M – множество Σ-интерпретаций над X. Будем говорить, что ϕ M-
истинна, если I |= ϕ для всех Σ-интерпретаций I M∈ . Это будем обозначать | M ϕ= . Будем говорить, что ϕ M-
выполнима, если существует Σ-интерпретация I M∈ такая, что I |= ϕ . Это будем обозначать | M ϕ≈ . Формула
M-невыполнима если она не M-выполнима.
Пусть S – множество Σ-формул. Будем писать I |= S, если I |= ϕ для каждой формулы ϕ ∈ S.
Проблема выполнимости для ЯМЛ сигнатуры Σ состоит в определении выполняется ли |≈ϕ для
произвольной Σ-формулы ϕ .
Когда сигнатура языка фиксирована, символ Σ будем опускать, говоря просто о термах, формулах,
интерпретациях и т. д.
Теперь в терминах ЯМЛ можно определить язык VL1 и рассматриваемые интерпретации этого языка.
Язык VL1 используется для проведения рассуждений о формулах, выражающих свойства в линейной
арифметике с равенством, линейным порядком, неинтерпретированными символами: неинтерпретированными
константами и неинтерпретированными функциональными символами. Линейная арифметика в VL1 должна
поддерживать переменные над целыми и рациональными числами.
Язык VL1 является подмножеством ЯМЛ сигнатуры ( , , , )S C F PΣ = Σ Σ Σ Σ , где содержит три сорта
= <int, rat, symb>. Множество констант = C
SΣ
SΣ CΣ rat∪ Csymb. Множество констант Crat используется для задания
целых и рациональных коэффициентов в формулах VL1. Считаем, что Crat состоит из всех рациональных чисел,
представленных в виде несократимых дробей. Множество констант Csymb состоит из всех идентификаторов, т. е.,
последовательностей из букв латинского алфавита и цифр, которые начинаются с буквы. Символы констант
можно считать неинтерпретированными символами. Переменные сорта int называем целыми переменными,
переменные сорта rat называем рациональными переменными, переменные сорта symb называем символьными
переменными.
Множество функциональных символов следующее: FΣ = { int int int× →+ , int rat rat× →+ , intrat rat , rat rat rat× →+ × →+ ,
, } . Формулы VL1 могут также содержать неинтерпретированные функциональные символы,
которые мы не включаем явно в
rat rat→− int int→−
FΣ . Конечное множество таких функциональных символов доопределяется,
когда фиксирован контекст языка. В терминах системы VRS, для заданного описания среды [10], можно
указать конечное множество неинтерпретированных функциональных символов UF явно.
Множество предикатных символов PΣ = { int int×< , int rat×< , intrat×< , rat rat×< , int int×= , , , int rat×= intrat×= rat rat×= ,
symb symb×= }.
Язык VL1 состоит из замкнутых Σ-формул вида
1 1 ( )
n nq qσ σ ϕ∃ ∃K , где ϕ – бескванторная формула, n ≥ 0.
2. Задача выполнимости относительно теорий
Особенность задачи проверки выполнимости относительно теории (теорий) состоит в ограничении
возможных интерпретаций логических символов в формулах. Материал этой главы кратко излагаем на
основе [11, 12], куда отсылаем заинтересованного читателя для получения исчерпывающей информации по
данной теме.
253
Формальні методи програмування
Для данного ЯМЛ сигнатуры , любое множество T замкнутых Σ-формул называется Σ-теорией. Σ-
интерпретация I называется Σ-моделью T, если эта интерпретация является моделью каждой формулы ϕ в T.
Множество M всех Σ-моделей для данной теории T называется классом Σ-моделей T. С другой стороны, для
данной интерпретации I можно разделить множество всех замкнутых Σ-формул на две группы в зависимости
от того, являются ли они истинными в интерпретации I. Множество замкнутых формулы, истинных в I,
составляет теорию для интерпретации I. Если множество интерпретаций M является классом моделей теории
T, то T – множество аксиом для M. Если две теории имеют один и тот же класс моделей, они эквивалентны. В
частности, две замкнутые формулы эквивалентны, если они истинны в точности на одних и тех же
интерпретациях. Отметим что в литературе иногда теория определяется как (возможно бесконечное) множество
Σ-моделей. В контексте данной работы различие в этих способах определения не является существенным.
Σ
Зафиксировав некоторую Σ-теорию T можно сформулировать задачу выполнимости относительно
теории T, или, задачу T-выполнимости следующим образом: для данной замкнутой Σ-формулы ϕ выяснить,
существует ли в классе Σ-моделей теории T такая интерпретация, в которой формула ϕ истинна. Другими
словами, проверить, существует ли такая интерпретация I, что }{| ϕ∪= TI . В англоязычной литературе это
называют satisfiability with respect to theory T, satisfiability modulo theory T, T-satisfiability problem, SMT problem.
С другой стороны, если теория задается классом своих Σ-моделей M, можно сформулировать задачу
выполнимости относительно М так: для произвольной замкнутой Σ-формулы ϕ проверить справедливость
ϕM≈| . Проблема выполнимости для множества Σ-формул S относительно класса Σ-моделей M разрешима, если
существует алгоритм, который проверяет справедливость ϕM≈| для любой формулы S∈ϕ . Выполнимость
формулы относительно теории T будем обозначать ϕT≈| .
По аналогии с задачей пропозициональной выполнимости (propositional satisfiability problem, SAT),
процедуры решения задачи SMT называются SMT-решателями (SMT-solvers). Для процедур, решающих задачу
выполнимости для конкретных теорий употребляется также термин разрешающие процедуры (decision
procedures). Часто в SMT интерес представляет задача выполнимости относительно Σ-теории Т для множества
формул S, содержащих неинтерпретированные символы, т. е., дополнительные символы, не принадлежащие Σ.
Например, множество констант может не ограничиваться CΣ , с тем чтобы, для технического удобства, считать
свободные переменные константами. В таких случаях можно рассматривать расширение исходной теории.
Пусть – произвольная сигнатура, включающая Σ. Расширение Σ-модели A на Σ′ Σ′ – это такая -модель Σ′ A′ ,
которая имеет тот же носитель и интерпретирует символы Σ таким же образом. Тогда класс моделей теории T ′
определяется как множество всех возможных расширений моделей T на Σ′ . Для простоты обычно говорят о
выполнимости относительно теории Т, подразумевая ее подходящее расширение ,T ′ где это необходимо.
Рассмотрим примеры распространенных теорий, широко встречающихся при использовании SMT в
различных формальных методах.
Теории линейной арифметики. Сигнатура ArΣ таких теорий включает константы 0, 1, предикатный
символ ≤, функциональные символы +, –. Теория линейной целочисленной арифметики определяется
стандартной интерпретацией сигнатуры над множеством целых чисел. Теория линейной арифметики над
рациональными числами определяется стандартной интерпретацией той же сигнатуры над множеством
рациональных чисел.
IntT
ArΣ
RealT
Пример 1. Пусть )*2&4&2(:1 xyxxyx =<>∃∃=Φ . Формула 1Φ невыполнима относительно , но
выполнима относительно .
IntT
RealT
Рассматривается также теория смешанной линейной арифметики, в которой вводятся два
отдельных сорта (int, rat) для целых и рациональных чисел.
RealIntT −
Пример 2. Формула ))*2(&34&2(:2 xyyxxxx =∃=→<>∀=Φ не выполнима в теориях и ,
но формула
IntT RealT
))*2(&34&2(: xyyxxxx ratint =∃=→<>∀=Φ′ выполнима в теории . RealIntT −
Отметим, что дополнительные символы выражаются через имеющиеся символы сигнатуры ArΣ .
Например, 2*y = y+y, 4 = 1+1+1+1 и т. д.
Теория массивов. Сигнатура содержит два функциональных символа read, write. Терм read(a, i)
обозначает значение, находящееся по индексу i в массиве a. Терм write(a, i, v) обозначает массив, идентичный a
для всех значений индекса за исключением i, которому соответствует элемент v. Класс моделей для
является классом моделей для следующего множества аксиом:
ArrΣ
ArrT
)).,()),,,(()((
),)),,,(((
jareadjviawritereadjivjia
viviawritereadvia
=→=¬∀∀∀∀
=∀∀∀
Иногда к ним добавляется аксиома экстенсиональности: )))),(),(((( baibreadiareadiba =→=∀∀∀ .
Теория массивов используется для моделирования массивов как структур данных. Несмотря на NP-
полноту разрешающей процедуры в общем случае, разработанные -решатели хорошо показывают себя на
практике.
ArrT
254
Формальні методи програмування
Иногда неинтерпретированные функциональные символы рассматриваются в контексте отдельной
теории неинтерпретированных функций с равенством. Теория также называется чистой теорией (pure
theory of equality with uninterpreted functions) и не фиксирует в своей сигнатуре никаких
интерпретированных функциональных/предикатных символов. Класс ее моделей состоит из множества всех
EUFT
EUFΣ
Σ -
моделей.
Пример 3. Для формул
))()(&&(:3 zfxfzyyxyx ≠==∃∃=Φ , ))()()()(&(: 3121213214 xfxfxfxfxxxxx =∨≠=∃∃∃=Φ имеем,
что невыполнима относительно , в то время как 3Φ EUFT 4Φ – выполнима.
Подмена интерпретированных функций неинтерпретированными иногда позволяет упростить процесс
доказательство выполнимости некоторых формул. В то же время такая абстракция не сохраняет свойство всюду
истинности. Теория может также использоваться для доказательства эквивалентности программ. EUFT
Практические применения SMT также включают использование теории битовых векторов для
проведения рассуждений в области проектирования схем и программ, индуктивных типов данных для
моделирования структур данных, теории строк, позволяющие, например, выражать свойства принадлежности к
регулярным языкам конечной длины и многие другие теории.
3. Задача выполнимости для языка VL1
Возвращаясь к языку VL1 следует отметить, что нас интересуют не произвольные интерпретации
символов VL1, а стандартные интерпретации, представляющие практическую ценность для решения задач
верификации в контексте инсерционного моделирования, и того, как оно реализуется в VRS. Таким образом,
будем рассматривать только такие интерпретации I формул VL1, которые удовлетворяют нижеследующим
ограничениям (VL1-интерпретации).
1. Областью значений сорта int является множество целых чисел, область значений сорта rat –
множество рациональных чисел. Область значений сорта symb – некоторое счетное бесконечное множество.
2. Независимо от типа функциональные символы + и – интерпретируются как сложение и унарный
минус над рациональными числами. Предикат < имеет стандартную интерпретацию над множеством
рациональных чисел, symb symb×= интерпретируется как равенство над областью значений сорта symb, остальные
предикаты равенства интерпретируются как равенство над множеством рациональных чисел.
3. Константы Crat интерпретируются как соответствующие им рациональные константы. Константы
Csymb интерпретируются произвольным образом так что , , I I
symba b C a b a b∈ ≠ ⇒ ≠ .
Итак, чтобы задать конкретную VL1-интерпретацию необходимо предоставить:
- область значений для сорта symb;
- интерпретацию функциональных символов UF;
- интерпретацию констант Csymb.
Обозначим V класс всех VL1-интерпретаций. Задача проверки выполнимости в VL1, рассматриваемая в
данной работе, заключается в проверке справедливости | V ϕ≈ для произвольной формулы ϕ языка VL1.
Таким образом, задача проверки выполнимости формул в языке VL1 является задачей SMT.
Действительно, задача заключается в проверке выполнимости формул этого языка как формул языка логики
первого порядка, относительно следующих теорий:
- линейная смешанная арифметика (сорта int, rat);
- теория неинтерпретированных функциональных символов с равенствами (сорта int, rat, symb).
Для решения задачи выполнимости в VL1 мы используем известные методы решения задачи SMT, и, тем
самым, показываем, что задача проверки выполнимости VL1-формул относительно класса VL1 интерпретаций
разрешима.
Бóльшую часть SMT-методов, согласно устоявшейся терминологии [11], можно разделить на две группы
– «жадные» (eager) и «ленивые» (lazy).
«Жадный» подход заключается в построении по формуле логики первого порядка эквивыполнимой
пропозициональной формулы. Для многих логических теорий, использующихся в практических задачах SMT,
это возможно. Правда, кодирование всех существенных формул-выводов теории может приводить к
значительному увеличению размера формулы. Преимуществом данного подхода является возможность
использования уже разработанных SAT-решателей, способных справиться с достаточно большими формулами.
Эффективность подхода будет зависеть, в том числе, от особенностей работы алгоритма SAT-решателя над
ограничениями, которые получаются в процессе кодирования формул рассматриваемой теории.
«Ленивый» подход состоит в создании процедур построения логического вывода, специализированных
для данной теории Т. Данный подход позволяет учитывать особенности конкретных теорий, использовать
наиболее эффективные для рассматриваемой теории алгоритмы и структуры данных, что положительно влияет
на производительность. Общепринятая практика состоит в разработке решателей для конъюнкции литералов
теории T. С помощью решателя для конъюнкции литералов простейший алгоритм проверки выполнимости
формулы заключается в построении дизъюнктивной нормальной формы, и решении задачи для каждого
255
Формальні методи програмування
конъюнкта по отдельности. Это называется синтаксическим разделением на подзадачи (syntactic case-splitting).
Действительно,
1 1 1| (
n nI v vσ σ 2 )ϕ ϕ≈ ∃ ∃ ∨K тогда и только тогда, когда
1 1 1|
n nI v vσ σ ϕ≈ ∃ ∃K либо
1 1 2|
n nI v vσ σ ϕ≈ ∃ ∃K .
Реализация такого алгоритма, конечно, не отличается эффективностью как с точки зрения временных
затрат, так и с точки зрения объемов потребляемой оперативной памяти. Существует много различных
вариантов «ленивых» SMT-решателей. Одна из центральных идей в их разработке состоит в интегрировании
решателей для теории в процедуры решения задачи пропозициональной выполнимости (SAT engines). Известна
следующая схема. Пусть pϕ – пропозициональная абстракция входной формулы ϕ . Формула pϕ получаемая
путем замены атомов формулы ϕ пропозициональными символами отдается на вход SAT решателю. Если
pϕ невыполнима, значит ϕ тоже невыполнима. В противном случае SAT-решатель возвращает некоторое
решение, которое можно представить в виде конъюнкции pμ проп иональных литералов. Этой конъюнкции
соответствует некоторая конъюнкция
озиц
μ атомов из ϕ или их отрицаний. Затем μ проверяется на
выполнимость уже Т-решателем. Если μ выполнима относительно Т, то ϕ тоже выполнима. В противном
случае, к формуле ϕ конъюнктивно добавляется μ¬ и процесс проверки продолжается.
Более эффективные (соответственно, более сложные) схемы предполагают встраивание T-решателя
непосредственно в алгоритмы SAT-решателя, наиболее популярным из которых является алгоритм DPLL
(Davis-Putnam-Logemann-Loveland) [13]. Схемы такого вида получили обозначение DPLL(T) [14]. При этом, для
эффективной интеграции T-решатель должен обладать дополнительными функциями, которые позволят DPLL-
алгоритму сузить пространство перебора, используя дополнительную информацию из теории Т. Важными
являются следующие функции.
1. Способность генерации модели для выполнимой конъюнкции литералов μ .
2. Способность генерации противоречивого подмножества невыполнимой конъюнкции μ .
3. Свойство инкрементности: пусть решателем доказана выполнимость конъюнкции 1μ , и на следующем
шаге необходимо проверить выполнимость 21 & μμ . Инкрементность означает, что выполнимость последней
формулы будет проверяться с учетом имеющейся информации, полученной при проверке выполнимости 1μ , с
целью сокращения вычислительных затрат. Для этого T-решатель поддерживает некоторое состояние,
меняющееся с учетом формул, которые ему приходится доказывать.
4. Способность отката: Т-решатель может эффективно возвращаться к предыдущему состоянию в
процессе доказательств.
При решении практических SMT задач часто приходится сталкиваться с формулами, которые
принадлежат сразу нескольким логическим теориям. В особенности это касается верификации, когда
формулировки, требующие доказательства, накладывают ограничения, характеризующимися несколькими
типами данных, где каждый тип данных моделируется своей собственной теорией.
Пример 4 [15]. Формула )1())2),3,,(((&2:5 +−≠−=+=Φ bcfcbawritereadfcb содержит символы
сигнатуры теории (–, +), теории (read, write), (неинтепретированный символ f). Рассматривая
интерпретацию функциональных и предикатных символов формулы согласно определениям соответствующих
теорий можно убедиться, что формула не выполнима. Действительно, рассмотрим цепочку преобразований
сохраняющих выполнимость:
IntT ArrT EUFT
5Φ
)1())2),3,,(((&2 +−≠−=+ bcfcbawritereadfcb ⇒
)12())22),3,,(((&2 +−+≠−+=+ bbfbbawritereadfcb ⇒
)3())),3,,(((&2 fbbawritereadfcb ≠=+ ⇒
)3()3(&2 ffcb ≠=+ .
Для указанных теорий, или их бескванторных фрагментов, проблема выполнимости разрешима. Для них
построены относительно эффективные Т-решатели. Возникает вопрос: возможно ли комбинировать решатели
для нескольких теорий так, чтобы получить решатель, проверяющий выполнимость формулы относительно
объединенной теории? В общем случае ответ отрицательный, поскольку существуют теории выполнимые по
отдельности, но не выполнимые в комбинации. Например, проблема выполнимости относительно комбинации
и разрешима для бескванторного фрагмента, но не разрешима в общем случае. IntT EUFT
Для -теории и -теории их комбинация 1Σ 1T 2Σ 2T 21 TTT ⊕= определяется как -теория такая,
что , а T задается множеством аксиом . В терминах моделей в несколько упрощенном виде
можно сказать, что класс
Σ
21 Σ∪Σ=Σ 21 TT ∪
Σ -моделей T совпадает с классом Σ -моделей для . Понятие комбинации
может быть расширено на несколько теорий.
21 TT ∪
Наложив некоторые ограничения на теории можно построить комбинированный решатель для
, используя решатели для Т
21, TT
21 TTT ⊕= 1 и Т2. Большинство методов комбинирования теорий в SMT являются
расширениями и усовершенствованиями метода Нельсона – Оппена [16]. Ограничения, налагаемые методом, на
256
Формальні методи програмування
практике не являются чрезмерно строгими, и это позволят строить эффективные имплементации. Один из
вариантов метода комбинирования налагает следующие ограничения на теории [12]:
- теории Т1 и Т2 являются бескванторными теориями с равенством;
- для Т1 и Т2 существует решатели;
- сигнатуры Т1 и Т2 не пересекаются;
- теории Т1 и Т2 интерпретируются на бесконечном носителе.
Без ограничения общности метод опишем для случая конъюнкции литералов 21 TT ⊕∈ϕ . Сначала
производится разделение термов в исходной формуле ϕ путем введения дополнительных переменных. После
этого получается эквивыполнимая формула 21 &ϕϕϕ =′ , где каждый литерал уже принадлежит какой-то одной
из теорий, т. е., 11 T∈ϕ и .22 T∈ϕ Рассмотрим для примера формулу 0)( 11 >+ xfx . В этой формуле
единственный предикат содержит символы сигнатуры двух теорий Int и UF . Введением новой переменн
2x получаем форму ), гд
T T ой
лу е
E
(&0 1221 xfxxx =>+ EUFTxfx ∈= )( 12 и .021 IntTxx ∈>+ Обозначим
множество переменных встречающихся одновременно в },...,{ 1 nvvVar = 1ϕ и .2ϕ На абстрактном уровне метод
комбинации Нельсона – Оппена состоит в поиске такой формулы , что одновременно
выполняется
ji
nji
vv ≅=
∈
&
},...,1{,
ψ
ψϕ &| 11T≈ и ψϕ &| 22T≈ . Это будет означать, что ϕ′≈T| , и следовательно, ϕT≈| . Если такую
формулу ψ построить нельзя, то ϕ не выполнима в Т. Формула ψ состоит из атомов вида для каждой
пары переменных , , где каждый такой атом может входить в чистом виде, либо с отрицанием
.
ji vv =
iv Varv j ∈
)( ji vv =¬
Более детальное обсуждение общих методов решения SMT задачи выходит за рамки данной работы, но
хотелось бы отметить следующие выводы:
- при построении Т-решателей достаточно иметь в наличии алгоритм проверки выполнимости для
конъюнкции литералов теории Т;
- если , то для установления ∅=Var ϕT≈| достаточно проверить 11
| ϕT≈ и 22
| ϕT≈ ;
- поскольку алгоритмы DPLL-решателей рассчитаны на запись формулы в виде конъюнктивной
нормальной формы (КНФ), на практике исходная формула вначале приводится к эквивыполнимой формуле
представленной в КНФ.
Рассмотрим специализированные SMT методы решения проблемы выполнимости в языке VL1. Пусть
ϕ – формула языка VL1. Проверка выполнимости ϕ может быть произведена следующим образом.
Сначала исходная формула ϕ может быть приведена к эквивыполнимой формуле без
неинтерпретированных функциональных символов. Для этого рассмотрим каждую (синтаксически различную)
пару термов 1( ,..., )nf t t и 1( ,..., )nf u u , типаUFf ∈ 1 nσ σ σ× × →L , и конъюнктивно добавим к ϕ формулу
11 1 & &
nn nt u t uσ σ= = →K 1 1( ,..., ) ( ,..., )n nf t t f u uσ= . В полученной формуле заменим каждый (самый внешний)
терм 1( ,..., )nf t t сорта σ , новой переменной
1( ,..., )nf t tv сорта σ . Синтаксически идентичные термы заменяются
одной и той же переменной. Хотя для вложенных термов, содержащих неинтерпретированные функциональные
символы, новой переменной заменяется только внешний терм, вложенные подтермы тоже рассматриваются при
построении импликаций. В итоге, каждую новодобавленную переменную необходимо связать квантором
существования в префиксе формулы. Полученную формулу обозначим ϕ′ . Эквивыполнимость ϕϕ ′≈⇔≈ VV ||
может быть доказана непосредственно: для данной интерпретации I V∈ такой, что |I ϕ′≈ , мы всегда можем
построить интерпретацию J V∈ такую, что |J ϕ≈ и наоборот. Это преобразование известно под названием
редукция Аккермана [17]. Отметим, что после применения редукции атомы, содержащие переменные или
константы сорта symb. не содержат термов других сортов в качестве своих подтермов.
Без ограничения общности будем считать ϕ конъюнкцией литералов. Пусть ϕ имеет вид
1 1 1 1 1( &...& & &...& )
k k symb symb l n mv v s sσ σϕ χ χ ψ ψ= ∃ ∃ ∃ ∃K K , где k, l, n, m ≥ 0, },{ ratinti ∈σ , литералы iχ не
содержат термов сорта symb, а литералы iψ представляют собой равенства термов типа symb или отрицания
таковых. Обозначим
1 1 1( &...& )
k k nv vσ σχ χ χ= ∃ ∃K и 1 1( &...& )symb symb l ms sψ ψ ψ= ∃ ∃K . Формулы χ и ψ
являются замкнутыми. Поскольку в формулах χ и ψ не может быть общих переменных, имеем | V ϕ≈ тогда и
только тогда, когда | V χ≈ и | V ψ≈ .
Задача проверки выполнимости | V χ≈ может быть решена с помощью обобщенного симплекс-
метода [18] или алгоритмов элиминации кванторов в теории смешанной арифметики над целыми и
вещественными числами [19]. Обработка целочисленных переменных является более дорогостоящей по
вычислительной сложности. Известно [20], что проверка непротиворечивости системы линейных неравенств в
рациональных числах может быть выполнена за полиномиальное время, в то время как аналогичная задача в
целых числах является NP-полной. В [19] утверждается, что проверка выполнимости замкнутых формул в
257
Формальні методи програмування
языке смешанной арифметики может быть выполнена за время , где l – длина формулы, n – число
переменных, a – число перемен кванторов в пренексной нормальной форме формулы.
)(
2
aOnl
Задача проверки выполнимости | V ψ≈ может быть решена построением фактор-множества по
отношению эквивалентности следующим образом. Сначала для каждой пары различных констант c1, c2
встречающихся в ψ конъюнктивно добавим к ψ дополнительный литерал 1( symbc c2 )¬ = . Полученную
формулу обозначим ψ ′ . Пусть }– множество переменных и констант формулы ,...,{ 1 qwwW = ψ ′ . Ассоциируем
с каждым элементом класс эквивалентности , состоящий из этого элемента. Затем, для каждого
литерала в формуле
iw }{ iw
jsymbi ww = ψ объединяем классы и . Далее, пока это возможно, объединяем
классы эквивалентности содержащие общие элементы. Впрочем, исходная формула
}{ iw }{ jw
ψ выполнима тогда и
только тогда, когда в ψ для каждого литерала вида )( jsymbi ww =¬ имеем, что и принадлежат разным
классам эквивалентности. Расширение этого метода может использоваться для проверки выполнимости
конъюнкции формул теории . Можно построить соответствующий алгоритм [21], имеющий сложность
O(n log n) для конъюнкции длины n.
iw jw
EUFT
Вместо редукции Аккермана могут также использоваться SMT-методы, решающие задачу комбинации
теорий.
4. Метод поиска выполнимой конъюнкции для формулы с множественными
операциями
В разделе 3 мы ограничились решением задачи выполнимости для конъюнкции литералов языка VL1.
Как было отмечено, при решении проблемы выполнимости общепринятой практикой считаются переборные
методы, использующие предварительное представление исходной формулы в КНФ. Это мотивируется
использованием требующей КНФ достаточно развитой схемы DPLL(T), для которой разработаны
многочисленные эвристики и усовершенствования. В то же время, для дизъюнктивной нормальной формы
задача выполнимости решается проще, и сводится к простой проверке выполнимости каждого конъюнкта, а в
случае пропозициональной формулы задача вообще решается тривиально. На этой почве возник вопрос: всегда
ли имеет смысл проводить поиск выполнимой конъюнкции, выполняя безоговорочное приведение формулы к
КНФ, в особенности, если представление формулы близко к дизъюнктивной нормальной форме?
Этот вопрос послужил мотивацией для разработки альтернативного подхода к поиску выполнимой
конъюнкции литералов, являющейся импликантой исходной формулы. Суть подхода состоит в следующем.
Формула представляется в виде дерева, вершинами которого являются множественные операции конъюнкции
(&) и дизъюнкции (∨), а листами – литералы либо их отрицания. Множественность подчеркивает то, что
количество аргументов операции (арность) не ограничивается, а порядок аргументов не устанавливается. С
каждой (∨)-вершиной ассоциируется индекс, определяющий одного из ее потомков. Комбинация значений всех
индексов (∨)-вершин однозначно определяет конъюнкцию предикатов, которая проверяется на предмет
выполнимости. На множестве возможных комбинаций вводится линейный порядок, согласно которому
производится последовательный поиск выполнимой конъюнкции.
При этом, для сокращения поиска, каждая невыполнимая конъюнкция анализируется с целью
нахождения противоречивого подмножества ее литералов. Задача состоит в обнаружении противоречивого
подмножества, встречающегося в как можно большем числе конъюнкций, еще не проанализированных, в
соответствии с порядком их рассмотрения алгоритмом. После выделения такого подмножества, часть
конъюнкций удается отбросить, как заведомо противоречивые.
Рассмотрено несколько реализаций предлагаемого подхода, которые отличались способом
упорядочивания множества аргументов (∨)-вершин. В первом варианте порядок вершин был произвольным и
определялся представлением исходной формулы. Во втором и третьем варианте аргументы сортировались в
порядке возрастания и, соответственно, убывания числа вершин в своих поддеревьях. Для обнаружения
противоречивого подмножества предикатов для невыполнимой конъюнкции литералов p1&…&pn бинарным
поиском находился такой индекс i, что формула pi&...&pn не выполнима, но pi+1&...&pn выполнима.
Непосредственно следующие конъюнкции, содержащие все предикаты pi...pn исключались из рассмотрения.
Реализации алгоритмов были опробованы в процессе работы системы VRS. При этом оценивалось соотношение
числа дополнительных вызовов разрешающей процедуры для выделения противоречивого подмножества
предикатов, и количество обнаруженных противоречивых конъюнктов исходной формулы. Для лучшей из
реализаций (третий вариант) число вызовов разрешающей процедуры для выполнимых формул составило 2%
от общего числа конъюнктов, составляющих ДНФ, для невыполнимых формул – 4%.
В данный момент было бы не совсем адекватно считать предложенный метод конкурентом схеме
DPLL(T), которая активно совершенствуется более 10 лет, но отметим, что оба метода являются переборными и
имеют выраженную эвристическую природу. Построение множественного представления выполняется за
линейное время. Преимуществом предложенного метода поиска выполнимой конъюнкции является линейная
сложность проверки выполнимости формулы для ДНФ-представления, без учета сложности разрешающей
процедуры. Проведенные эксперименты продемонстрировали возможность применения предложенного
258
Формальні методи програмування
подхода на практических примерах из системы верификации требований VRS. Показатели эффективности
различных способов его реализации отличаются, поэтому вопрос об эффективности конкретных реализаций и
эвристик может быть исследован дополнительно.
Выводы
В настоящей работе мы описали логический язык VL1 и показали, что задача выполнимости в этом
языке разрешима. Предложена схема разрешающей процедуры для этого языка, которая использует
вспомогательные методы такие, как редукция Аккермана, обобщенный симплекс метод, процедура построения
замыкания по отношению эквивалентности. Указанная схема может применяться в комбинации с
пропозициональными решателями согласно «ленивому» подходу к решению задачи выполнимости
относительно теории. Также мы предложили альтернативный метод поиска выполнимой конъюнкции для
формулы с множественными операциями, не требующей приведения формулы к конъюнктивной нормальной
форме. Метод позволяет существенно сократить число вызов разрешающей процедуры в процессе поиска
выполнимой конъюнкции и может использоваться для решения типичной задачи SMT при наличии решателя
для конъюнкции литералов.
Язык VL1 используется в системе верификации требований VRS как язык для проведения формальных
рассуждений. Отметим, что требования, предъявляемые новой версией системы VRS к SMT-решателю,
требуют усовершенствования выразительных возможностей языка VL1. В частности, предполагается
использовать операции-конструкторы для символьных термов и ограниченную операцию универсальной
квантификации. В последующих работах планируется исследовать вопросы выполнимости в расширенном
языке, находя компромисс между выразительными возможностями и сложностью разрешающих процедур.
Поскольку введение универсальной квантификации уже делает проблему выполнимости неразрешимой в
общем случае, мы заинтересованы в изучении и выделении разрешимых фрагментов языка, которые будут
достаточными для проведения рассуждений для при практическом использовании системы VRS.
В заключение отметим, что современные успехи исследований в направлении выполнимости
относительно теорий (satisfiability modulo theories, SMT) свидетельствуют о широком спектре применимости
разработанных в этой области методов. Построены разрешающие процедуры для теорий конечных множеств,
мультимножеств, решеток, конечных, регулярных и бесконечных деревьев, списков, записей, очередей,
свободных термов, хэш-таблиц, массивов, линейной арифметики [1, 11]. Разработаны эффективные решатели,
среди которых отметим программные системы Z3, CVC4, Barcelogic, MathSAT, OpenSMT, SatEEn, STP, UCLID,
Yices. Некоторые из них являются свободно распространяемыми системами с открытым кодом. Список
решателей и поддерживаемых ими теорий продолжает увеличиваться, и, безусловно, достижения в области
SMT не могут оставаться без внимания при разработке систем верификации. Некоторые из указанных
разрешающих процедур планируется применить и в системе VRS.
1. de Moura L., Bjørner N. Satisfiability Modulo Theories: Introduction and Applications // Communications of the ACM. –2011. – Vol. 54 (9). –
P. 69–77.
2. The 15-th International Conference on Theory and Applications of Satisfiability Testing – Режим доступа: http://sat2012.fbk.eu/
3. Satisfiability Modulo Theories Competition (SMT-COMP) – Режим доступа: http://www.smtcomp.org
4. Letichevsky A. Algebra of behavior transformations and its applications // in V.B. Kudryavtsev and I.G. Rosenberg editors. Structural theory of
Automata, Semigroups, and Universal Algebra, NATO Science Series II. Mathematics, Physics and Chemistry. – Springer. – 2005. – Vol. 207.
– P. 241–272.
5. Letichevsky A., Kapitonova J., Kotlyarov V. et al. Insertion Modeling in Distributed System Design // Problems of Programming. – 2008. – Vol.
4. – P. 13–39.
6. Letichevsky A.A., Letychevskyi O.A., Peschanenko V.S. Insertion Modeling System // Lecture Notes in Computer Science. – Springer. – 2011. –
Vol. 7162. – P. 262–274.
7. Kapitonova J., Letichevsky A., Volkov V. et al. System Validation // In R. Zurawski, editor. The Embedded Systems Handbook. – Miami: CRC
Press, 2005 – P. 6.1 – 6 – 57. .
8. Letichevsky A., Kapitonova J., Letichevsky A. (jr). et al. Basic Protocols, Message Sequence Charts, and the Verification of Requirements
Specifications // Computer Networks. – 2005. – N 47. – P. 662– 675.
9. Летичевский А.А., Капитонова Ю.В., Волков В.A. и др. Сертификация систем с помощью базовых протоколов // Кибернетика и
системный анализ. – 2005. – № 4. – C. 256–268.
10. Letichevsky A., Gilbert D. A Model for Interaction of Agents and Environments // In D. Bert, C. Choppy, P. Moses, editors. Recent Trends in
Algebraic Development Techniques. Lecture Notes in Computer Science. – Springer. – 1999. – Vol. 1827. – P. 311–328.
11. Barrett C., Sebastiani R., Seshia S. A., Tinelli C. Satisfiability Modulo Theories // In: A. Biere, M. Heule., H. van Maaren, T. Walsh editors.
Handbook of Satisfiability. – IOS Press. – 2009. – P. 737–797.
12. Kroening D., Strichman O. Decision Procedures – an Algorithmic Point of View. – Berlin: Springer-Verlag, 2008. – 304 p.
13. Davis M., Logemann G., Loveland D. Machine Program for Theorem-Proving // Comm. of the ACM. –1962. – № 5(7). – P. 7:394–397.
14. Ganzinger H., Hagen G., Nieuwenhuis R. et al. DPLL (T): Fast decision procedures // Proc. of the 16-th Intl. Conf. on Computer Aided
Verification, Lecture Notes in Computer Science, 3114. – 2004. – P. 175–188.
15. de Moura L., Bjørner N. Satisfiability Modulo Theories: An Appetizer // Lecture Notes in Computer Science. –2009. – Vol. 5902. – P. 23–36.
16. Nelson G., Oppen D.C. Simplification by cooperating decision procedures // ACM Transactions on Programming Languages and Systems. –
1979. – Vol. 1. – P. 245–257.
17. Ackermann W. Solvable cases of the Decision Problem. – Amsterdam: North-Holland, 1954. – 114 p.
18. Dutertre B., de Moura L. Integrating Simplex with DPLL(T) // Technical report, CSL-06-01, SRI International. – 2006. – 35 p.
19. Weispfenning V. Mixed Real-Integer Linear Quantifier Elimination // Proceedings of the international symposium on Symbolic and algebraic
computation ISSAC’99. – 1999. – P. 129–136.
20. Schrijver A. Theory of Linear and Integer Programming. – John Wiley & sons. – 1998. – 471 p.
21. Nieuwenhuis R., Oliveras R. Fast Congruence Closure and Extensions // Information and Computation. – 2007. – Vol. 205(4). – P. 557–580.
259
http://sat2012.fbk.eu/
http://www.smtcomp.org/
ЗАДАЧА ПРОВЕРКИ Т-ВЫПОЛНИМОСТИ ДЛЯ ЛОГИЧЕСКОГО ЯЗЫКА VL1 СИСТЕМЫ VRS
Введение
1. Логический язык VL1
2. Задача выполнимости относительно теорий
3. Задача выполнимости для языка VL1
4. Метод поиска выполнимой конъюнкции для формулы с множественными операциями
Выводы
|