О выразительных возможностях некоторых расширений линейной темпоральной логики

Захаров Владимир Анатольевич; Гнатенко Антон Романович

doi:10.18255/1818-1015-2018-5-506-524

Публикации

Статья

О выразительных возможностях некоторых расширений линейной темпоральной логики

Моделирование и анализ информационных систем. 2018. Т. 25. № 5. С. 506-524.

Захаров В. А., Гнатенко А. Р.

О выразительных возможностях некоторых расширений линейной темпоральной логики // Моделирование и анализ информационных систем. — 2018. — Т. 25, № 5. — С. 506–524. Конечные автоматы, задающие преобразования потоков входных сигналов в последовательности элементарных действий, являются простейшей моделью вычислений, пригодной для описания поведения реагирующих систем. Это поведение проявляется в соответствии между потоком входных сигналов и последовательностью элементарных действий, выполняемых системой. Мы полагаем, что для формального описания поведения реагирующих систем такого рода требуются более сложные и выразительные средства спецификации, нежели традиционная темпоральная логика линейного времени LTL. В этой работе рассматривается новый язык формальных спецификаций LP-LTL, представляющий собой расширение темпоральной логики LTL, специально разработанное для описания свойств вычислений автоматов-преобразователей. Темпоральные операторы в формулах LP-LTL снабжены параметрами, в качестве которых используются множества слов (языки), описывающие потоки сигналов управления, поступающих на вход реагирующей системы. Базовые предикаты в формулах LP-LTL также определяются языками в алфавите элементарных действий; эти языки описывают ожидаемую реакцию системы в ответ на воздействия окружающей среды. В более ранних работах авторов этой статьи изучалась задача верификации конечных автоматов-преобразователей относительно спецификаций, представленных формулами логик LP-LTL и LP-CTL. Было показано, что для обеих логик эта задача алгоритмически разрешима. Цель данной работы — оценить выразительные возможности логики LP-LTL и сравнить ее с широко известными логиками, применяющимися в информатике для спецификации реагирующих систем. В логике LP-LTL были выделены два фрагмента LP-1-LTL и LP-n-LTL. Нам удалось установить, что язык спецификаций LP-1-LTL более выразителен, чем LTL, в то время как фрагмент LP-n-LTL обладает точно такими же выразительными возможностями, что и монадическая логика второго порядка S1S.

Научное направление: Компьютерные науки

Приоритетные направления: компьютерно-математическое

Язык: русский

Полный текст (PDF, 703 Кб)

DOI

Текст на другом сайте

Ключевые слова: темпоральная логика верификация моделей программ автомат Бюхи монадическая логика

Публикация подготовлена по результатам проекта: Моделирование информационных систем и анализ их поведения на основе истории событий(2018)

Дискретная математика. Формально-логические системы и языки.

Авдошин С. М., Набебин А. А. М.: ДМК Пресс, 2018.

Книга содержит основные сведения из формально-логических систем. Это функции алгебры логики (булевы функции), теорема Поста о функциональной полноте, k-значные логики, производные булевых функций, аксиоматические исчисления высказываний, предикатов, секвенций, резолюций и язык программирования Пролог. Рассматриваются монадическая логика, конечные автоматы и представимые ими языки, темпоральная логика, аксиоматический язык программирования OBJ3. В основу книги положен многолетний опыт преподавания авторами дисциплины «Дискретная математика» на факультете бизнес-информатики, на факультете компьютерных наук Национального исследовательского университета Высшая школа экономики и на факультете автоматики и вычислительной техники Национального исследовательского университета Московский энергетический институт. Книга предназначена для студентов бакалавриата, обучающихся по направлениям 09.03.01 «Информатика и вычислительная техника», 09.03.02 «Информационные системы и технологии», 09.03.03 «Прикладная информатика», 09.03.04 «Программная инженерия», а также для ИТ-специалистов и разработчиков программных продуктов.

Добавлено: 2 декабря 2017

On the Model Checking of Finite State Transducers over Semigroups

Gnatenko A. R., Zakharov V. Proceedings of the Institute for System Programming of the RAS. 2018. Vol. 30. No. 3. P. 303-324.

Добавлено: 14 июня 2018

Темпоральная логика для верификации автоматов-преобразователей

Захаров В. А., Козлова Д. Г. В кн.: Материалы XII Международного семинара "Дискретная математика и её приложения" имени академика О.Б. Лупанова (Москва, МГУ, 20-25 июня 2016г.). М.: Изд-во механико-математического факультета МГУ, 2016. С. 204-206.

Характерная особенность моделей Крипке и большинства темпоральных логик (PLTL, CTL, PDL, mu-исчисление и др.), используемых в качестве формальных языков спецификации, состоит в том, что элементарные свойства вычислений зависят только от состояний модели, но не от вычислений, которыми достигаются состояния. Однако для стороннего наблюдателя поведение реагирующей системы проявляется в соответствии между последовательностями стимулов (сигналов), которыми внешняя среда воздействует на систему, и откликов (действий), которые вырабатывает или исполняет система в ответ на внешние воздействия. Поэтому при верификации некоторых видов реагирующих систем элементарными свойствами становятся множества конечных последовательностей действий. Это обстоятельство должно быть также учтено при разработке формального языка спецификаций поведения таких систем. В данной статье рассмотрена задача формальной верификации реагирующих систем, моделируемых конечными автоматами-преоб\-разователями. Для спецификации их поведения предложен новый вариант темпоральной логики линейного времени LTL-FL (LTL with Formal Languages). Формальные языки (множества конечных слов фиксированных алфавитов) в формулах LTL-FL используются для представления элементарных свойств вычислений, а также для параметризации темпоральных операторов. Установлено, что задача проверки выполнимости формул регулярного фрагмента FL-LTL на конечных автоматах преобразователях разрешима.

Добавлено: 13 октября 2016

Рождение европейской философии истории и логико-темпоральные схемы ренневизантийских авторов

Каменских А. А. В кн.: . С. 255-275.

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

Добавлено: 5 декабря 2019

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

Захаров В. А., Коннов И. В. Моделирование и анализ информационных систем. 2010. Т. 17. № 4. С. 78-87.

Наиболее значительную трудность для всех инструментальных средств верификации моделей программ создает эффект комбинаторного взрыва. Один из способов сократить размер проверяемой модели $M$ --- выбрать подходящую группу автоморфизмов $G$ размеченной системы переходов $M$ и построить фактор-модель $M/G$. Состояниями фактор-модели $M/G$ служат орбиты состояний модели $M$ относительно группы $G$; также известно, что модели $M/G$ и $M$ находятся в отношении бисимуляции. К сожалению, поиск нетривиальной группы автоморфизмов $G$ произвольной конечной системы переходов $M$ является вычислительно трудной задачей. Для преодоления этой трудности был предложен метод адаптивного упрощения модели на основе симметрии. Этот метод позволяет воспользоваться преимуществами симметричного устройства модели $M$, не обращаясь явно к орбитам ее состояний. В самом начале решения задачи проверки достижимости состояний предполагается, что модель является абсолютно симметричной; далее это предположение корректируется по мере того, как обнаруживаются переходы, несовместные со сложившимся представлением о симметрии в модели. Пространство состояний модели оказывается разбитым на классы эквивалентности, которые называются мета-состояниями; на каждом шаге вычисления при рассмотрении очередного перехода мета-состояния могут подвергаться расщеплению. Мы обнаружили, что метод адаптивного упрощения модели на основе симметрии может быть с равным успехом применен для проверки выполнимости формул LTL. Основной результат работы --- новый теоретико-автоматный подход к верификации моделей программ, сочетающий метод адаптивного упрощения модели на основе симметрии и алгоритм двойного поиска в глубину для проверки пустоты автоматов Бюхи.

Добавлено: 30 сентября 2015

Model for organizing cargo transportation with an initial station of departure and a final station of cargo distribution

Khachatryan N., Akopov A. S. Business Informatics. 2017. No. 1(39). P. 25-35.

Добавлено: 18 апреля 2017

Многомерное хранение журналов событий для извлечения и анализа процессов

Брейман А. Д., Богословский Е. М. Прикаспийский журнал: управление и высокие технологии. 2014. № 2 (26). С. 127-137.

Журналы событий, сохраняемые современными информационными и техническими системами, как правило, содержат достаточно данных для автоматизированного восстановления моделей соответствующих процессов. Разработано множество алгоритмов для построения моделей процессов, проверки соответствия фактического поведения системы модельному, сравнения моделей процессов, и т.д. Однако возможность быстрого анализа выбираемых пользователями частей журнала до сих пор не нашла полноценной реализации. В статье описан метод многомерного хранения журналов событий для извлечения и анализа процессов, основанный на подходе ROLAP. Результатом анализа журнала является направленный невзвешенный граф, представляющий собою сумму возможных последовательностей событий, упорядоченных по вероятности их возникновения с учетом заданных условий. Разработанный инструмент позволяет выполнять совместный анализ моделей подпроцессов, восстановленных из частей журнала путем задания критериев отбора событий и требуемого уровня детализации модели.

Добавлено: 27 февраля 2014

Управление жизненным циклом информационных систем

Зараменских Е. П. Новосибирск: Издательство НГТУ, 2014.

В монографии приведены результаты исследования, посвященного управлению жизненным циклом информационных систем, а также анализу стандартов, сводов знаний и корпоративных методик, использующихся в ИТ-проектах. Приведены характеристики фаз ЖЦИС из практики управления ИТ-проектами, а также практические рекомендации по управлению такими проектами. Книга предназначена для научных работников, сотрудников научно- технических предприятий и работников государственных органов управлений, а также студентов, аспирантов, слушателей бизнес-школ повышения квалификации и переподготовки кадров. Книга содержит практические рекомендации для руководителей ИТ-проектов, а также сотрудников компаний, занимающихся проектной деятельностью в области ИТ-проектов.

Добавлено: 5 августа 2014

Общий обзор китайского рынка облигаций

Афонина С. Г., Ван Ц., Лапшин В. А. Финансовая инженерия, риск-менеджмент и актуарная наука. WP16. Высшая школа экономики, 2013. № WP16/2013/01.

Работа посвящена общему описанию китайского рынка облигаций. В ней содержится обзор западных исследований и история развития китайского рынка облигаций, а также приводится описание структуры, инфраструктуры, регулирования, участников и торгуемых инструментов сегодняшнего рынка облигаций Китая.

Добавлено: 17 апреля 2013

Методика построения кривой безрисковой доходности «спот» и кредитных спрэдов для группы облигаций с неоднородным кредитным качеством эмитентов: стандарт EFFAS-EBC для стран Еврозоны

Смирнов С. Н., Захаров А. В., Рачков Р. В. и др. Финансовая инженерия, риск-менеджмент и актуарная наука. WP16. Высшая школа экономики, 2007. № WP16/2007/03.

Добавлено: 15 марта 2013

Transcultural Empire: Geographic Information System of the 1897 and 1926 General Censuses in the Russian Empire and Soviet Union

Sablin I., Kuchinskiy A., Korobeinikov A. et al. Heidelberg: HeiDATA: Heidelberg Research Data Repository, University of Heidelberg, 2015.

The geographic information system (GIS) is based on the first and only Russian Imperial Census of 1897 and the First All-Union Census of the Soviet Union of 1926. The GIS features vector data (shapefiles) of allprovinces of the two states. For the 1897 census, there is information about linguistic, religious, and social estate groups. The part based on the 1926 census features nationality. Both shapefiles include information on gender, rural and urban population. The GIS allows for producing any necessary maps for individual studies of the period which require the administrative boundaries and demographic information.

Добавлено: 8 декабря 2015

Short lists with short programs in short time

Bauwens B., Makhlin A., Vereshchagin N. et al. Electronic Colloquium on Computational Complexity. Technical report. Hasso-Plattner-Institut, 2013. No. TR13-007.

Добавлено: 14 декабря 2013

Advances in decision technology and intelligent information systems

Iss. 12. Tecumseh: The International Institute for Advanced Studies in Systems Research and Cybernetics, 2011.

Добавлено: 22 февраля 2013

Components of enterprise IT strategy: decision-making model and efficiency measurement

Zelenkov Y. International Journal of Information Systems and Change Management. 2014. Vol. 7. No. 2. P. 150-166.

Добавлено: 29 октября 2017

Сабейские этюды

Коротаев А. В. М.: Восточная литература, 1997.

Добавлено: 9 марта 2013

Program Semantics, Specification and Verification: Theory and Applications. The conference materials. 6th International Computer Science Symposium in Russia

Под науч. редакцией: V. Nepomniaschy, V. Sokolov. Yaroslavl: Yaroslavl State University, 2011.

Добавлено: 23 марта 2013

Разложения решений пятого уравнения Пенлеве вблизи его неособой точки

Брюно А. Д., Парусникова А. В. Институт прикладной математики им. М.В. Келдыша Российской академии наук, 2011. № 18.

В данной работе рассматривается пятое уравнение Пенлеве, которое имеет 4 комплексных параметра. Методами степенной геометрии ищутся асимптотические разложения его решений в окрестности его неособой точки z=z0, z0≠0, z0≠∞, при любых значениях параметров уравнения. Показано, что имеется ровно 10 семейств разложений решений уравнения. Все они - по целым степеням локальной переменной z - z0. Из них одно новое; у него произвольный коэффициент при четвертой степени локальной переменной. Одно из семейств однопараметрическое, остальные - двухпараметрические. Доказано, что все разложения сходятся в окрестности (а являющиеся полюсами - в проколотой окрестности) точки z=z0.

Добавлено: 18 апреля 2012

Многовариантный анализ процессов прокатки на базе компьютерного моделирования

Аксенов С. А., Чумаченко Е. Н., Сырчина О. О. Вестник Воронежского государственного технического университета. 2011. Т. 7. № 11.2. С. 62-64.

В работе рассмотрены два варианта калибровок валков для прокатки прутка круглого сечения диаметром 20 мм из прутка диаметром 55 мм. Первый – классическая калибровка «овал - круг». Второй – комбинация прокатки на гладкой бочке и в круглых калибрах. С помощью аналитических уравнений были рассчитаны черновые варианты калибровок. Полученные формы калибровок использовались при моделировании процесса прокатки в программном комплексе SPLEN(Rolling). По результатам моделирования производилась корректировка зазоров между валками с целью улучшения силовых характеристик и предотвращения переполнения или невыполнение калибров на последнем переходе.

Добавлено: 12 апреля 2012

Асимптотические разложения решений пятого уравнения Пенлеве

Парусникова А. В., Брюно А. Д. Институт прикладной математики им. М.В. Келдыша Российской академии наук, 2010. № 39.

В данной работе рассматривается пятое уравнение Пенлеве, которое имеет 4 комплексных параметра α, β, γ, δ. Методами степенной геометрии ищутся асимптотические разложения его решений при x → ∞. При α≠0 найдено 10 степенных разложений с двумя экспоненциальными добавками каждое. Шесть из них - по целым степеням x (они были известны), и четыре по полуцелым (они новые). При α=0 найдено 4 однопараметрических семейства экспоненциальных асимптотик y(x) и 3 однопараметрических семейства сложных разложений x=x(y). Все экспоненциальные добавки, экспоненциальные асимптотики и сложные разложения найдены впервые. Также уточнена техника вычисления экспоненциальных добавок.

Добавлено: 18 апреля 2012

Локальные разложения решений пятого уравнения Пенлеве

Брюно А. Д., Парусникова А. В. Институт прикладной математики им. М.В. Келдыша Российской академии наук, 2010. № 72.

В данной работе рассматривается пятое уравнение Пенлеве. Методами степенной геометрии ищутся асимптотические разложения его решений при x → 0. Получено 27 семейств разложений решений уравнения. 19 из них получены из разложений решений шестого уравнения Пенлеве. Среди остальных 8 семейств одно было известно раньше, ещё одно может быть получено из разложения решения третьего уравнения Пенлеве. Новыми являются 3 семейства полуэкзотических разложений, 2 семейства сложных разложений и семейство степенно-логарифмических разложений.

Добавлено: 18 апреля 2012

Теория активных систем (ТАС-2014) [Электронный ресурс]: Материалы международной научно-практической конференции, 17–19 нояб. 2014 г, Москва

М.: ИПУ РАН, 2014.

Электронное издание является сборником материалов международной научно-практической конференции "Теория активных систем" (ТАС-2014)

Добавлено: 26 января 2015

Применение информационных и космических технологий в задачах о движении небесных объектов

Чумаченко Е. Н., Кулагин В. П., Назиров Р. Р. и др. Информатизация образования и науки. 2011. № 3 (11). С. 178-187.

Обсуждается одно из направлений деятельности научно-образовательного центра «КОСМОС», созданного Московским государственным институтом электроники и математики (технический университет) и Институтом космических исследований РАН. Рассмотрены общие постановки задач, связанные с разработкой моделей движения астероидов и комет с учетом негравитационных возмущений, построением моделей траекторных измерений, разработкой математического аппарата для полетов в окрестности коллинеарных точек либрации. Обсуждается модель управления орбитальным движением космического аппарата в окрестности точек либрации с применением солнечного паруса с управляемыми отражательными характеристиками.

Добавлено: 12 апреля 2012

Анализ методов компьютерного моделирования механических испытаний

Чумаченко Е. Н., Аксенов С. А., Борхсениус С. С. Вестник Воронежского государственного технического университета. 2011. Т. 7. № 11.2. С. 9-11.

Работа посвящена применению компьютерных технологий при анализе результатов механических испытаний материалов для определения их свойств в условиях горячей деформации. Рассмотрены испытания на кручение, растяжение, сжатие и сжатие с плоской деформацией. Проведен обзор возможностей использования обратного анализа для интерпретации результатов механических испытаний с применением имитационного моделирования на базе метода конечных элементов (МКЭ) в 2D и 3D.

Добавлено: 12 апреля 2012