О применении композиционно-номинативных логик в инсерционном моделировании

Рассмотрена возможность применения композиционно-номинативных логик как инструмента проведения формально-логических рассуждений в рамках технологии инсерционного моделирования. Обоснована теоретическая база такого применения – сформулирована задача проверки выполнимости формул в многосортных компози...

Ausführliche Beschreibung

Gespeichert in:

Bibliographische Detailangaben
Datum:	2012
Hauptverfasser:	Никитченко, Н.С., Тимофеев, В.Г.
Format:	Artikel
Sprache:	Russian
Veröffentlicht:	Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України 2012
Schriftenreihe:	Управляющие системы и машины
Schlagworte:	Дедуктивные методы
Online Zugang:	http://dspace.nbuv.gov.ua/handle/123456789/83109
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!
Назва журналу:	Digital Library of Periodicals of National Academy of Sciences of Ukraine
Zitieren:	О применении композиционно-номинативных логик в инсерционном моделировании / Н.С. Никитченко, В.Г. Тимофеев // Управляющие системы и машины. — 2012. — № 6. — С. 57-63. — Бібліогр.: 12 назв. — рос.

Institution

Digital Library of Periodicals of National Academy of Sciences of Ukraine

id	irk-123456789-83109
record_format	dspace
spelling	irk-123456789-831092015-06-15T03:02:09Z О применении композиционно-номинативных логик в инсерционном моделировании Никитченко, Н.С. Тимофеев, В.Г. Дедуктивные методы Рассмотрена возможность применения композиционно-номинативных логик как инструмента проведения формально-логических рассуждений в рамках технологии инсерционного моделирования. Обоснована теоретическая база такого применения – сформулирована задача проверки выполнимости формул в многосортных композиционно-номинативных логиках первого порядка. Предложен редукционный подход к ее решению. The possibility is considered of using the composition-nominative logics as an instrument for formal reasoning in the insertion modeling technology. Theoretical foundations are established for such an application: we formulate the satisfiability problem for the first-order many-sorted composition-nominative logics and suggest a reductional approach for solving this problem. Розглянуто можливість застосування композиційно-номінативних логік як інструменту проведення формально-логічних суджень в рамках технології інсерційного моделювання. Обґрунтовано теоретичну базу такого застосування – сформульовано задачу перевірки виконуваності формул у багатосортних композиційно-номінативних логіках предикатів першого порядку та подано редукційний підхід до її розв’язання. 2012 Article О применении композиционно-номинативных логик в инсерционном моделировании / Н.С. Никитченко, В.Г. Тимофеев // Управляющие системы и машины. — 2012. — № 6. — С. 57-63. — Бібліогр.: 12 назв. — рос. 0130-5395 http://dspace.nbuv.gov.ua/handle/123456789/83109 004.02 ru Управляющие системы и машины Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України
institution	Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection	DSpace DC
language	Russian
topic	Дедуктивные методы Дедуктивные методы
spellingShingle	Дедуктивные методы Дедуктивные методы Никитченко, Н.С. Тимофеев, В.Г. О применении композиционно-номинативных логик в инсерционном моделировании Управляющие системы и машины
description	Рассмотрена возможность применения композиционно-номинативных логик как инструмента проведения формально-логических рассуждений в рамках технологии инсерционного моделирования. Обоснована теоретическая база такого применения – сформулирована задача проверки выполнимости формул в многосортных композиционно-номинативных логиках первого порядка. Предложен редукционный подход к ее решению.
format	Article
author	Никитченко, Н.С. Тимофеев, В.Г.
author_facet	Никитченко, Н.С. Тимофеев, В.Г.
author_sort	Никитченко, Н.С.
title	О применении композиционно-номинативных логик в инсерционном моделировании
title_short	О применении композиционно-номинативных логик в инсерционном моделировании
title_full	О применении композиционно-номинативных логик в инсерционном моделировании
title_fullStr	О применении композиционно-номинативных логик в инсерционном моделировании
title_full_unstemmed	О применении композиционно-номинативных логик в инсерционном моделировании
title_sort	о применении композиционно-номинативных логик в инсерционном моделировании
publisher	Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України
publishDate	2012
topic_facet	Дедуктивные методы
url	http://dspace.nbuv.gov.ua/handle/123456789/83109
citation_txt	О применении композиционно-номинативных логик в инсерционном моделировании / Н.С. Никитченко, В.Г. Тимофеев // Управляющие системы и машины. — 2012. — № 6. — С. 57-63. — Бібліогр.: 12 назв. — рос.
series	Управляющие системы и машины
work_keys_str_mv	AT nikitčenkons oprimeneniikompozicionnonominativnyhlogikvinsercionnommodelirovanii AT timofeevvg oprimeneniikompozicionnonominativnyhlogikvinsercionnommodelirovanii
first_indexed	2025-07-06T09:50:37Z
last_indexed	2025-07-06T09:50:37Z
_version_	1836890653385031680
fulltext	УСиМ, 2012, № 6 57 Дедуктивные методы УДК 004.02 Н.С. Никитченко, В.Г. Тимофеев О применении композиционно-номинативных логик в инсерционном моделировании Рассмотрена возможность применения композиционно-номинативных логик как инструмента проведения формально-логических рассуждений в рамках технологии инсерционного моделирования. Обоснована теоретическая база такого применения – сформули- рована задача проверки выполнимости формул в многосортных композиционно-номинативных логиках первого порядка. Предло- жен редукционный подход к ее решению. The possibility is considered of using the composition-nominative logics as an instrument for formal reasoning in the insertion modeling tech- nology. Theoretical foundations are established for such an application: we formulate the satisfiability problem for the first-order many-sorted composition-nominative logics and suggest a reductional approach for solving this problem. Розглянуто можливість застосування композиційно-номінативних логік як інструменту проведення формально-логічних суджень в рамках технології інсерційного моделювання. Обґрунтовано теоретичну базу такого застосування – сформульовано задачу перевірки виконуваності формул у багатосортних композиційно-номінативних логіках предикатів першого порядку та подано редукційний підхід до її розв’язання. Введение. Инсерционное моделирование [1–3] – это технология проектирования систем, основан- ная на теории взаимодействий агентов и сред, успешно примененная к задачам верификации спецификаций для распределенных систем ре- ального времени в различных предметных об- ластях [4, 5]. Одно из главных применений этой технологии – система VRS (Verification of Requi- rement Specifications) [2, 5]. Программный ком- плекс VRS предоставляет возможности провер- ки требований к программным и аппаратным системам путем автоматического доказатель- ства теорем, использования техник символьной и дедуктивной проверки моделей, а также ге- нерации трасс для тестирования с различными критериями покрытия. Идеология инсерционного моделирования, представленная в VRS, предполагает, что ис- ходные данные для анализа системы предложе- ны в виде спецификации на языке базовых про- токолов [6]. Каждая такая спецификация со- стоит из двух частей: из описания среды и множества базовых протоколов. Описание сре- ды доопределяет сигнатуру языка специфика- ции и возможные ограничения интерпретации этой сигнатуры. Множество базовых протоко- лов определяет требования к поведению сис- темы. В процессе верификации система VRS использует специализированный решатель как средство для проверки выполнимости форму- лы–свойства, сформулированной в специаль- ном логическом языке. В частности, это требу- ется на этапе проверки условия применимости базового протокола в состоянии. На низком уровне это реализуется путем проверки вы- полнимости формул в логическом языке, кото- рый представляет собой фрагмент языка клас- сической многосортной логики первого поряд- ка. Этот язык включает в себя комбинацию теории линейной арифметики над целыми и рациональными числами [7] и теории неинтер- претированных функциональных символов с равенством [8]. В ограниченном виде в форму- лах допускается квантификация и перемены кванторов. Использование классической логики как ин- струмента для рассуждений накладывает ограни- чения на исходный язык спецификации, его вы- разительную мощность. Это отражается на про- цессе моделирования и на адекватности постро- енных моделей. Так, в рамках классической ло- гики функциональные символы всегда имеют фиксированное число аргументов и интерпрети- руются как всюду определенные (тотальные) функции, что, конечно, не всегда соответствует особенностям формализуемых систем. Преодо- леть эти ограничения можно, переходя к другим, более выразительным логикам. 58 УСиМ, 2012, № 6 К таким логикам, в частности, относятся ло- гики, разработанные в рамках композиционно- номинативного подхода и называемые компо- зиционно-номинативными логиками (КНЛ) [9]. Последние основываются на алгебрах частич- ных предикатов и строятся в семантико-син- таксическом стиле. Они могут рассматриваться как обобщения традиционных логик на классы частичных функций и предикатов, не имеющих фиксированной арности (квазиарные функции и предикаты). Основные инструменты системы VRS разде- лены на две группы: статические и динамичес- кие. Статические инструменты предусматрива- ют проверку непротиворечивости и полноты спецификаций. Эти инструменты используют специальную процедуру–решатель (solver), обес- печивающую проверку выполнимости формул в логическом языке. Задача проверки выполнимости – одна из главных задач, которую приходится решать в процессе верификации. Эта задача неразреши- ма в общем случае для многих логических тео- рий, представляющих практический интерес. Например, задача выполнимости для комбина- ции теории линейной целочисленной арифме- тики и теории неинтерпретированных функ- циональных символов с равенством разрешима для подмножества бескванторных формул, но неразрешима для формул произвольного вида. Поэтому при разработке языка спецификации всегда приходится искать компромисс между его выразительными возможностями и слож- ностью соответствующих решателей. Таким об- разом, одним из первых вопросов, требующих рассмотрения при переходе к другим логикам, будет задача проверки выполнимости формул в этих логиках и методы ее решения. Цель настоящей статьи – показать, что про- блема выполнимости в многосортных компози- ционно-номинативных логиках первого поряд- ка может быть сведена к проблеме выполни- мости в классических логиках. Предлагаемые редукционные методы решения задачи выпол- нимости для КНЛ позволяют решать ее, поль- зуясь арсеналом средств, разработанных для решения аналогичной задачи в классических логиках. Это облегчает использование КНЛ для проведения логических рассуждений при спе- цификации и верификации систем, и обосно- вывает возможность применения КНЛ для за- дач инсерционного моделирования при расши- рении языка спецификации в направлении под- держки частичных квазиарных функций. В статье дано определение многосортных композиционно-номинативных логик (МКНЛ) квазиарных функций и предикатов первого по- рядка, сформулирована проблема выполнимости для этих логик и показан редукционный способ решения задачи проверки выполнимости фор- мул. Понятия и обозначения, не определяемые в данной статье, трактуются согласно [10]. Многосортная алгебра квазиарных функ- ций и предикатов Семантической базой многосортных КНЛ первого порядка выступают специальные ал- гебры функций и предикатов. Пусть S – множество сортов, V – множе- ство имен, v – тотальная функция : t V V S  . Имена из V по традиции также называются пе- ременными. Функция v сопоставляет каждой переменной v  V некоторый сорт s  S, s = N (v). В таком случае будем говорить, что v – пере- менная (имя) сорта s. Пусть A – класс множеств значений, IS – тотальная функция интерпретации сортов ASI t S : . Функция IS сопоставляет каждо- му сорту некоторое множество допустимых значений для этого сорта (носитель, тип, до- мен). Для v  V обозначим Dom (v) = IS (v(v)). Обозначим  класс номинативных (именных) множеств  =  (V, S, v, A, IS), состоящий из всех (в том числе частичных) однозначных отобра- жений множества V в элементы множеств Ai  A таких, что для любых d  , v  V из d(v) = a следует, что a  Aj, Aj = IS (v(v)). Пусть Bool = {F, T} – множество истинност- ных (булевых) значений. Обозначим Pr = Pr (V, S, v, A, IS) множество всех (частичных) отобра- жений, имеющих тип Boolp . Обозначим iAFn = ( , , , , , )V S iFn V S A I A множество всех (ча- стичных) отображений типа i p A , ai  A. УСиМ, 2012, № 6 59 Пусть Fn = i i A A A Fn   . Область значений функ- ции f  Fn обозначим Cod (f). Множества Fn и Pr называются множествами многосортных квазиарных функций и предикатов соответст- венно. Для номинативного множества d   и предиката p  Pr пишем p(d) = b, если значе- ние предиката p на d определено и равняется b  Bool; запись p(d) означает, что значение предиката p на множестве d не определено. Аналогичное обозначение вводится для функ- ций. Для двух номинативных множеств d1 и d2 определим множество d = d1d2, состоящее из всех именованных пар из d2 и тех пар из d1, имена которых не имеют значений в d2. Запись dx  a обозначает d[x  a]. Рассмотрим базовые композиции квазиар- ных функций и предикатов (p, q  Pr, d  ). Пропозициональные композиции задаются следующим образом: , если ( ) или ( ) , ( )( ) , если ( ) и ( ) , не определено в остальных случаях. T p d T q d T p q d F p d F q d F          , если ( ) , ( )( ) , если ( ) , не определено, если ( ) . T p d F p d F p d T p d        Композиции nvv FS ,...,1 (сокращенно: v FS ) и nvv PS ,...,1 (сокращенно: v PS ) называются компози- циями суперпозиции в квазиарную функцию и предикат соответственно. Эти композиции за- даются следующим образом. Для f  Fn, p  Pr, vi  V, gi  Fn таких, что Dom (vi) = Cod (gi), i = 1,...,n , nvv FS ,...,1 (f, g1,..., gn)(d) = f (d[v1g1(d),  ..., vngn(d)]), nvv PS ,...,1 (p, g1,..., gn)(d) = p(d[v1 g1(d), ...,vngn(d)]). Интуитивный смысл этих формул заключается в изменении для номина- тивного множества d значений имен v1,..., vn на g1(d),..., gn(d) соответственно. Нульарная композиция (функция) деномина- ции с параметром xV определяется формулой: 'x (d) = d(x). Унарная композиция экзистенциальной кван- тификации x с параметром xV определяется так: , ( ) для некоторого ( ), ( )( ) , ( ) для всех ( ), не определено в остальных случаях. T p d x b T b Dom x x p d F p d x a F a Dom x              Бинарная композиция равенства = задается следующим образом: (f = g) (d) , если ( ) , ( ) и ( ) ( ), , если ( ) и ( ) , в остальных случаях. T f d g d f d g d T f d g d F          Производные композиции (конъюнкция &, композиция универсальной квантификации x ) определяются традиционным способом. Обозначим A = (V, S, V, A, IS). Алгебра AMS( A ) = <Pr, Fn;  , , v FS , v PS , x, x, = > служит семантической базой логики, рассмат- риваемой в настоящей статье. Кортеж A = (V, S, v, A, IS) – сигнатура этой алгебры. Повторим, что композиции v FS , v PS , x, x – параметризи- рованные, поэтому эти обозначения здесь – сокращение для всего набора композиций, кото- рые отличаются параметрами (именами из V). Многосортная композиционно-номинатив- ная логика квазиарных функций и преди- катов первого порядка Язык логики будем строить индуктивно, ис- пользуя понятия термов и формул. Термы и фор- мулы языка строятся на основе простейших (ато- марных) термов и формул с помощью символов композиций. Для простоты обозначений отож- дествляем символы композиций в языке логики и соответствующие им операции в алгебре AMS. Пусть Ps – множество предикатных симво- лов, Fs – множество функциональных символов, F – всюду определенная функция, : t F Fs S  , сопоставляющая каждому функциональному символу его сорт (сорт значений). Кортеж  = (V, S, Fs, Ps, V , F , {, , v PS , v FS , x' , x, = }) определяет сигнатуру логики. Для задания языка логики L() определяем класс термов Tr() и класс формул Fr() этого языка. С каждым термом t  Tr() ассоцииру- ется его сорт T(t). 60 УСиМ, 2012, № 6 Множество Tr() задается так:  если F Fs, то F Tr(), T(F) = F(F);  если x  V, то x  Tr(), T(x) = V(x);  если ),...,( 1 nvvv  – список попарно различ- ных переменных, t, t1,…, tn  Tr(), T(ti) = V(vi), i = 1,, n, то ),...,,( 1 n v F tttS Tr(), 1( ( , ,..., ))v T F nS t t t  = T(ti). Множество Fr() задается следующим об- разом:  если P Ps, то P  Fr();  если ,  Fr(), то ()Fr() и  Fr();  если )( Fr , ),...,( 1 nvvv  – список по- парно различных переменных, t1,…,tnTr(), ( ) ( )T i V it v  , ni ,...,1 , то  ),...,,( 1 n v P ttS Fr();  если xV,  Fr(), то x Fr();  если t1, t2 Tr(), 1 2( ) ( )T Tt t   , то t1= t2   Fr(). Множество формул Fr() (МКНЛ-формул) определяет язык логики L(). Наконец, определим понятие интерпретации логики L(). Пусть IS – отношение интерпрета- ции сортов, определенное ранее. Поскольку ком- позиционные символы интерпретированы, необ- ходимо задать интерпретацию функциональных и предикатных символов. Это делается с помо- щью отображений FI :Fs t Fn и PI :Ps t Pr соответственно. При этом допустимые интер- претации IF удовлетворяют ограничению: для каждого F Fs Cod(IF(F) = IS(F(F)). Определив интерпретацию функциональных и предикатных символов, интерпретация термов и формул оп- ределяется индуктивно, согласно определениям композиций в алгебре AMS. Тройка (AMS(A), IF, IP) называется моделью логики L(). Мо- дель определяется тройкой J = (A, IF, IP), на- зываемой интерпретацией. Для формулы    Fr() и интерпретации J значение формулы  на интерпретации J обозначается J. Поскольку в КНЛ не имеет места дистрибу- тивность композиции квантора существования относительно композиций суперпозиции, для проведения эквивалентных преобразований фор- мул необходимо иметь бесконечное множество имен каждого сорта. Будем считать, что такое множество U содержится в множестве V (U  V). Неформально говоря, это ограничивает класс рассматриваемых интерпретаций. Но такое ог- раничение естественно и несущественно при рассмотрении проблемы выполнимости [11]. Проблема выполнимости в МКНЛ и ее редукция Формула  называется выполнимой на ин- терпретации J, если существует d   такое, что J (d)↓= T. Это будем обозначать J \|≈ . Формула  называется выполнимой, если су- ществует интерпретация J, на которой  вы- полнима. Это будем обозначать \|≈ . Формулы  и  эквивыполнимы, если они одновременно выполнимы или одновременно невыполнимы. Задача проверки выполнимости состоит в проверке факта \| для произвольной форму- лы   Fr(). В рамках данной статьи предла- гается решать эту задачу редукционными ме- тодами: по данной МКНЛ-формуле  строить эквивыполнимую ей формулу CL классической логики с тем, чтобы применять существующие методы решения задачи проверки выполнимо- сти, разработанные для классических логик. Для этого формула  предварительно при- водится к нормальной форме usnf [], унифи- цированной по операции суперпозиции. Будем говорить, что формула  находится в унифицированной по суперпозиции нормальной форме, если выполняются следующие условия:  для любой подформулы вида v PS (, t ) име- ем Ps;  для любой подформулы вида v FS (r, t ) име- ем, что rFs;  все вхождения операции суперпозиции параметризированы одним списком перемен- ных w ;  для каждого вхождения квантора  y в формулу  имеем, что y содержится в w (см. предыдущий пункт). Рассмотрим набор правил T1–T12 преобра- зований формул вида rl   , l , r  Fr(). Эти правила – эквивалентные преобразования формул в КНЛ [10]. УСиМ, 2012, № 6 61 T1) v PS (, t )  v PS (, t )  v PS (, t ) . T2) v PS (, t )   v PS (, t ). T3) v PS (x, t )  u v PS ( x PS (,'u), t ), u – несущественная переменная, не встречающая- ся в v PS (x, t ), , ( ) ( ).V Vu U u x    T4) S xu P , (S vx P , (, sr , ), wt , )  vxu PS ,, (, t , xu FS , (r1, t , w ), ... xu FS , (rk , t , w ), xu FS , (s1, t , w ), ... , xu FS , (sm, t , w )), здесь и в T5 u = u1, ..., un; t = t1, ..., tn; x = х1, ..., xk; r = r1, ..., rk; w = w1, ... , wk; v = v1, ..., vm; s = s1, ..., sm, ,i ju v i = 1, , n, j = 1, , m. T5) xu FS , ( vx FS , (t, sr , ), wt , ) vxu FS ,, (t, t , xu FS , (r1, t , w ), ..., xu FS , (rk , t , w ), xu FS , (s1, t , w ), ... , xu FS , (sm , t , w )). T6) v PS (r = s, t )  v FS (r, t ) = v FS (s, t ). T 7) v PS (, t )  vx PS , (,'x, t ), x не встреча- ется в v . В частности,  x PS (, 'x). T8) v FS (t, t )  vx FS , (t, 'x, t ), x не встречает- ся в v . В частности, t x FS (t, 'x). T9) vxu PS ,, (, srq ,, ) vux PS ,, (, r, sq , ). T10) vxu FS ,, (t, srq ,, ) vux FS ,, (t, r, sq , ). T11) trtxS vx F ),,(', . T12) xrxS v F '),('  , x не встречается в v . Правила T3 и T 7 позволяют без ограниче- ния общности считать, что в формуле все кван- тифицируемые переменные (параметры опера- ции квантификации) различны. Для произвольной формулы   Fr(V, Fs, Ps) можно (не однозначным образом) построить ее унифицированную нормальную форму usnf[] путем применения правил T1–T12. При этом полученная формула будет эквивыполнима ис- ходной. С целью сведения проблемы выполнимости для многосортных композиционно-номинатив- ных логик к аналогичной проблеме многосорт- ных логик первого порядка рассмотрим синтак- сическое преобразование clf. Это преобразова- ние переводит МКНЛ-формулы в унифициро- ванной нормальной форме к формулам клас- сической логики и задается индуктивно: 1. clf['x] x. 2. 1 ,..., 1 1[ ( , ,..., )] ( [ ],...nw w F nclf S F t t F clf t , [ ])nclf t FFs. 3. ])[][()][( 2121  clfclfclf  . 4. ][][  clfclf  . 5. )()(][ 2121 tclftclfttclf   . 6. 1 ,..., 1 1[ ( , ,..., )] ( ( ),..., ( )),nw w P n nclf S P t t P clf t clf t n  0. 7. [ ] ( & [ ]), ( ) ( ).j V j Vclf x x x e clf e x        .Здесь каждому сорту s  S соответствует одна заданная наперед переменная es, не встречаю- щаяся в исходной формуле. Разные применения правила 7 для кванторов по переменным одно- го сорта вводят одну и ту же переменную ej. Описанная редукция переводит формулу в язык классической логики, но сохраняет при этом свойство выполнимости формулы. Теорема. Пусть   Fr(). Тогда  выпол- нима в МКНЛ тогда и только тогда, когда фор- мула clf [usnf []] выполнима в классической многосортной логике первого порядка. Теорема постулирует редукцию проблемы выполнимости в многосортной композиционно- номинативной логике первого порядка к пробле- ме выполнимости в классической многосорт- ной логике первого порядка. Опишем схему доказательства теоремы. От- личительными особенностями композиционно- номинативных логик есть свойства классов пре- дикатов: КНЛ строятся на алгебрах частичных квазиарных предикатов, в то время как класси- ческие логики строятся на классах тотальных n-арных предикатов. Возможность предикатов разграничивать присутствие и отсутствие компо- нент номинативных множеств также вносит от- личия в трактовку истинности формул. Так, в КНЛ формула  = (xP) P выполнима. Чтобы построить интерпретацию, на которой  истин- на, можно рассмотреть такую интерпретацию предикатного символа P: IP (P)(d) = «имя х оп- ределено в d». Эти особенности следует учесть при переходе в классические логики. Для этого: 1. При использовании свойства монотон- ности композиций КНЛ показано, что фор- мула   Fr() выполнима в КНЛ тогда и толь- 62 УСиМ, 2012, № 6 ко тогда, когда она выполнима в классе то- тальных интерпретаций. 2. Использование унифицированной нормаль- ной формы позволяет выделить во множестве имен V те имена, значение которых меняется при вычислении значений отдельных термов формулы и ее подформул; поскольку таких имен конечное число, оказывается возможным про- моделировать процесс вычисления значения МКНЛ-формулы при переходе в класс n-арных интерпретаций. 3. При переходе в класс n-арных интерпре- таций следует расширить каждый класс мно- жеств значений Ai  A дополнительным значе- нием i , которое используется для моделиро- вания неопределенного значения имен в номи- нативных множествах. 4. С учетом пп. 1–3 по формуле   Fr(), находящейся в унифицированной нормальной форме, выполнимой в МКНЛ-интерпретации на номинативном множестве d, несложно по- строить классическую n-арную интерпретацию такую, что каждая подформула  формулы  и формула clf []принимают в соответствующих интерпретациях одинаковые значения на неко- торой «окрестности» множества d. Доказатель- ство этого (и обратного) утверждения проводит- ся индукцией по структуре формулы. Заключение. Многосортные логики перво- го порядка широко используются для проведе- ния формальных рассуждений в процессе ве- рификации и при других применениях фор- мальных методов, в частности, такие логики используются в системе верификации требова- ний VRS. Одна из главных задач, которую при- ходится при этом решать – задача проверки истинности и, дуальная к ней, – задача провер- ки выполнимости формул. В данной статье описан класс многосортных композиционно-номинативных логик и пока- зано, как проблема выполнимости в таких ло- гиках может быть сведена к аналогичной про- блеме для соответствующих им классических многосортных логик первого порядка. Возмож- ность редукции проблемы выполнимости по- зволяет использовать расширенные выразитель- ные возможности композиционно-номинатив- ных логик в сравнении с традиционными ло- гиками n-арных предикатов, и, в то же время, использовать имеющиеся методы решения про- блемы выполнимости, разработанные для клас- сических логик. Результаты обосновывают воз- можность применения КНЛ при обобщении используемых в технологии инсерционного мо- делирования языков спецификации на классы частичных квазиарных функций. Статья есть продолжением [11], где постро- ены редукционные методы решения задачи про- верки выполнимости для композиционно-но- минативных логик кванторно-эквационального уровня. Предложенные в [11] методы обобща- ются на класс многосортных КНЛ. Таким об- разом, проблему выполнимости в МКНЛ мож- но решать имеющимися средствами для клас- сических логик. Дальнейшая работа предполагает исследо- вание проблемы выполнимости для более вы- разительных классов композиционно-номина- тивных логик – логик над иерархическими но- минативными данными. Иерархические данные позволяют задавать такие структуры данных как списки, стеки, массивы и др. Логики над таки- ми данными более удобны для рассуждений над программными моделями со сложными струк- турами данных. Другое направление исследо- ваний связано с идентификацией классов фор- мул в композиционно-номинативных логиках разных типов, для которых задача проверки вы- полнимости может решаться эффективно. Осо- бенный интерес представляет проблема выпол- нимости для логических теорий, в которых часть предикатов имеет фиксированную интер- претацию, задаваемую определенными аксио- мами. В литературе эта проблема известна как проблема выполнимости относительно теорий (satisfiability modulo theory (SMT) problem) [12]. Также необходимо построить прототипы про- граммных систем для проверки выполнимости в композиционно-номинативных логиках, по- зволяющих формализовать семантику логиче- ских языков, используемых в системе VRS. 1. Letichevsky A.А. Algebra of behavior transformations and its applications / V.B. Kudryavtsev, I.G. Rosenberg (Eds.). Structural theory of Automata, Semigroups, and Univer- УСиМ, 2012, № 6 63 sal Algebra, NATO Sci. Series II // Mathematics, Physics and Chemistry. – 2005. – 207. – Springer. – P. 241–272. 2. Insertion Modeling in Distributed System Design / A. Le- tichevsky, Ju. Kapitonova, V. Kotlyarov et al. // Problems of Programming. – 2008. – 4. – P. 13–39. 3. Letichevsky A.A., Letychevskyi A.A. (jr), Peschanenko V.S. Insertion Modeling System // Lecture Notes in Com- puter Science. – Springer. – 2011. – 7162. – P. 262–274. 4. System Validation / Ju. Kapitonova, A. Letichevsky, V. Volkov et al. / R. Zurawski (Ed.) // The Embedded Systems Handbook. Ch.6. – Miami: CRC Press, 2005. – P. 1–57. 5. Basic Protocols, Message Sequence Charts, and the Veri- fication of Requirements Specifications / A. Letichev- sky, Ju. Kapitonova, A. Letichevsky (jr) et al. / Computer Networks. – 2005. – № 47. – P. 662–675. 6. Сертификация систем с помощью базовых протоко- лов / А.А. Летичевский, Ю.В. Капитонова, В.А. Вол- ков и др. / Кибернетика и системный анализ. – 2005. – № 4. – C. 256–268. 7. Weispfenning V. Mixed Real-Integer Linear Quantifier Elimination // Proc. of the int. symp. Symbolic and al- gebraic computation ISSAC’99, 1999. – P. 129–136. 8. Kroening D., Strichman O. Decision Procedures – an Algorithmic Point of View. – Berlin: Springer-Verlag, 2008. – 304 p. 9. Nikitchenko N. A composition-nominative approach to program semantics // Technical report ITTR 1998-020, Technical University of Denmark, 1998. – 103 p. 10. Нікітченко М.С., Шкільняк С.С. Математична ло- гіка та теорія алгоритмів. – К.: Вид-полігр. центр «Київський університет», 2008. – 528 с. 11. Nikitchenko M.S., Tymofieiev V.G. Satisfiability Prob- lem in Composition-Nominative Logics of Quantifier- Equational Level // ICT in Education, Research and Indu- strial Applications: Integration, Harmonization and Know- ledge Transfer: int. conf., June 6–10, 2012, Kherson, Uk- raine: Proc. – CEUR-WS.org. – 2012. – N 848. – P. 56–70. 12. Satisfiability Modulo Theories / C. Barrett, R. Sebasti- ani, A. Seshia et al. / A. Biere, M. Heule., H. van Maaren, T. Walsh (Eds.). Handbook of Satisfiability. – IOS Press. – 2009. – P. 737–797. Тел. для справок: +38 044 259-0519 (Киeв) E-mail: nikitchenko@unicyb.kiev.ua, tvalentyn@univ.kiev.ua © Н.С. Никитченко, В.Г. Тимофеев, 2012 

О применении композиционно-номинативных логик в инсерционном моделировании

Institution

Ähnliche Einträge