• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • A
  • A
  • A
  • A
  • A
Обычная версия сайта
  • RU
  • EN
  • Национальный исследовательский университет «Высшая школа экономики»
  • Публикации ВШЭ
  • Статьи
  • On the Model Checking Problem for Some Extension of CTL*
  • RU
  • EN
Расширенный поиск
Высшая школа экономики
Национальный исследовательский университет
Приоритетные направления
  • бизнес-информатика
  • государственное и муниципальное управление
  • гуманитарные науки
  • инженерные науки
  • компьютерно-математическое
  • математика
  • менеджмент
  • право
  • социология
  • экономика
по году
  • 2027
  • 2026
  • 2025
  • 2024
  • 2023
  • 2022
  • 2021
  • 2020
  • 2019
  • 2018
  • 2017
  • 2016
  • 2015
  • 2014
  • 2013
  • 2012
  • 2011
  • 2010
  • 2009
  • 2008
  • 2007
  • 2006
  • 2005
  • 2004
  • 2003
  • 2002
  • 2001
  • 2000
  • 1999
  • 1998
  • 1997
  • 1996
  • 1995
  • 1994
  • 1993
  • 1992
  • 1991
  • 1990
  • 1989
  • 1988
  • 1987
  • 1986
  • 1985
  • 1984
  • 1983
  • 1982
  • 1981
  • 1980
  • 1979
  • 1978
  • 1977
  • 1976
  • 1975
  • 1974
  • 1973
  • 1972
  • 1971
  • 1970
  • 1969
  • 1968
  • 1967
  • 1966
  • 1965
  • 1964
  • 1963
  • 1958
  • еще
Тематика
Новости
30 апреля 2026 г.
«Моя цель - стать ординарным профессором»
Михаил Саматов занимается теоретическими исследованиями перовскитных солнечных батарей. В интервью проекту «Молодые ученые Вышки» он рассказал о работе на суперкомпьютере Вышки, сотрудничестве с Пекинским университетом и умении делать мебель.
29 апреля 2026 г.
Научить машину читать прошлое: на ФГН создают нейросеть для расшифровки рукописей
Дневники и письма — бесценный источник для гуманитария-исследователя. Но что делать, если текст невозможно прочитать? На факультете гуманитарных наук (ФГН) ВШЭ эту проблему решили перевести на язык математики: команда филологов, историков и специалистов по машинному обучению создала информационную систему, которая не только распознает неразборчивый почерк, но и помогает анализировать содержание архивов.
29 апреля 2026 г.
8 драйверов технологического будущего: что изменит экономику
Какие отрасли определят облик ближайших десятилетий? Премьер-министр  Михаил Мишустин назвал 8 направлений, которые будут развиваться в ближайшие годы. О том, какие образовательные программы НИУ ВШЭ готовят специалистов по этим направлениям — в материале IQ медиа.

 

Нашли опечатку?
Выделите её, нажмите Ctrl+Enter и отправьте нам уведомление. Спасибо за участие!

Публикации
  • Книги
  • Статьи
  • Главы в книгах
  • Препринты
  • Верификация публикаций
  • Расширенный поиск
  • Правила использования материалов
  • Наука в ВШЭ

?

On the Model Checking Problem for Some Extension of CTL*

Automatic Control and Computer Sciences. 2021. Vol. 55. No. 7. P. 776–785.
Гнатенко А. Р., Захаров В. А.
Переводчик: Захаров В. А.
Научное направление: Компьютерные науки
Язык: английский
Полный текст
DOI
Текст на другом сайте
Ключевые слова: model checkingfinite state transducerконечный автомат-преобразовательверификация моделей программтемпоральные логикиreactive systemреагирующая системаtemporal logic
ПУБЛИКАЦИЯ ПОДГОТОВЛЕНА ПО РЕЗУЛЬТАТАМ ПРОЕКТА:
Модели процессов: проверка соответствия наблюдаемому поведению, автоматический синтез и анализ поведенческих свойств (2021)
Похожие публикации
Proceedings of the 2026 8th International Youth Conference on Radio Electronics, Electrical and Power Engineering (REEPE)
Даюб А., Сулейман Э., IEEE, 2026.
Добавлено: 30 апреля 2026 г.
Bioinspired Method of Agent Redistribution between Groups
Karpova Irina Petrovna, Pattern Recognition and Image Analysis 2025 Vol. 35 No. 4 P. 1138–1144
Добавлено: 29 апреля 2026 г.
Natural hazard database from Internet publications: text mining with a large language model
Деркачева А. А., Сакиркина М. А., Краев Г. Н. и др., /. 2026.
Добавлено: 28 апреля 2026 г.
Influence of the Normal Magnetic Component to Magnetotail Current Sheet Forma
Domrin V. I., Malova H. V., V. Yu. Popov и др., Cosmic Research 2026 Vol. 64 No. 2 P. 238–252
Добавлено: 27 апреля 2026 г.
Asymmetric Equilibrium Structures of Superthin Current Sheets: The Asymmetry of Plasma Sources
Tsareva O. O., Malova H. V., V. Yu. Popov и др., Plasma Physics Reports 2026 Vol. 52 No. 2 P. 179–185
Добавлено: 27 апреля 2026 г.
WWW '26: The ACM Web Conference 2026
NY: Association for Computing Machinery (ACM), 2026.
Добавлено: 23 апреля 2026 г.
Разработка микросервиса ADP для идентификации источников выбросов на основе машинного обучения с подкреплением
Кычкин А. В., Черницин И. А., Прикладная информатика 2026 Т. 21 № 1 С. 40–58
Представлены результаты разработки программного микросервиса, встраиваемого в системы мониторинга качества атмосферного воздуха для поддержки процессов идентификации промышленных источников загрязнений. Выброс и последующее распространение вредных веществ в приземистых слоях атмосферы происходит в динамике и характеризуется высокой неопределенностью из‑за особенностей технологических установок, их режимов работы, влияния рельефа местности, зданий и метеофакторов. Зависимости между местоположением источника выброса и ...
Добавлено: 23 апреля 2026 г.
2026 International Conference on Artificial Intelligence, Computer, Data Sciences and Applications (ACDSA)
IEEE, 2026.
Добавлено: 21 апреля 2026 г.
What Drives Multi-Chain Crypto Forecasting: Model Choice, Feature Selection, and Transferability
Wang M., Xiao Y., Браславский П. И. и др., Mathematics 2026 Vol. 14 No. 8 Article 1286
Добавлено: 20 апреля 2026 г.
Cross-influence of two societies in deterministic evolutionary game
Щур Л. Н., Antonov D., Burovski E., International Journal of Bifurcation and Chaos in Applied Sciences and Engineering 2026 P. 1–9
Добавлено: 20 апреля 2026 г.
Проектирование сети Интернета вещей на основе многокритериальной оптимизации и информационного моделирования здания
Эбрахим А., Информационные процессы 2025 Т. 25 № 4 С. 787–798
В статье предложен метод планирования расположения точек доступа и шлюзов внутри зданий для построения сетей Интернета вещей. Основа метода — использование информации из информационой модели здания, что даёт возможность легко учитывать как геометрию, так и физико-технические характеристики строительных элементов при расчёте распространения радиосигнала. В данной работе для решения задач оптимизации применяется генетический алгоритм U-NSGA-III. Расчёты ...
Добавлено: 19 апреля 2026 г.
Modeling cosolvent effects on solubility in supercritical CO2 using data-driven approaches
Makarov D. M., Каликин Н. Н., Gurikov P. и др., Journal of Supercritical Fluids 2026 Vol. 235 Article 106979
Добавлено: 19 апреля 2026 г.
2026 28th International Conference on Digital Signal Processing and its Applications (DSPA)
IEEE, 2026.
Добавлено: 18 апреля 2026 г.
WWW '26: Proceedings of the ACM Web Conference 2026
NY: Association for Computing Machinery (ACM), 2026.
Добавлено: 17 апреля 2026 г.
Merging Epistemic and Temporal Models: a History-Free Approach
Попова Е. Л., Логико-философские штудии 2022 Vol. 20 No. 1 P. 1–7
Добавлено: 1 августа 2022 г.
On the Modeling of Sequential Reactive Systems by Means of Real Time Automata
Винарский Е. М., Захаров В. А., Automatic Control and Computer Sciences 2021 Vol. 55 No. 7 P. 751–762
Добавлено: 17 января 2022 г.
Efficient Equivalence Checking Technique for Some Classes of Finite-State Machines
Захаров В. А., Automatic Control and Computer Sciences (AC&CS), Switzerland 2021 Vol. 55 No. 7 P. 670–701
Добавлено: 17 января 2022 г.
О верификации моделей и проверке выполнимости формул одного параметрического расширения темпоральной логики линейного времени
Гнатенко А. Р., Захаров В. А., Моделирование и анализ информационных систем 2021 Т. 28 № 4 С. 356–371
К последовательным реагирующим системам относятся компьютерные программы и вычислительные устройства, которые обрабатывают потоки входных данных или сигналов управления и генерируют на выходе последовательности команд или результатов вычислений. Для проектирования таких систем полезно иметь формальные языки спецификаций, способные выражать отношения между входными и выходными потоками данных. В предшествующих работах нами было предложено семейство таких языков спецификаций, ...
Добавлено: 17 января 2022 г.
Reasoning Web. Declarative Artificial Intelligence, 16th International Summer School 2020, Oslo, Norway, June 24-26, 2020, Tutorial Lectures. Article: Temporal Ontology-Mediated Queries and First-Order Rewritability: A Short Course
Захарьящев М. В., Ryzhikov V., Wałęga P., Springer Publishing Company, 2020.
Добавлено: 8 ноября 2021 г.
Branching Time Logics with Multiagent Temporal Accessibility Relations
Рыбаков В. В., Siberian Mathematical Journal 2021 Vol. 62 P. 503–510
Добавлено: 8 ноября 2021 г.
Conference: 28th International Symposium on Temporal Representation and Reasoning, TIME 2021
Захарьящев М. В., Саватеев Ю. В., Ryzhikov V., Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2021.
Добавлено: 6 ноября 2021 г.
Knowledge and Time: Evolutionary Epistemic Model
Попова Е. Л., , in: Двенадцатые Смирновские чтения: материалы Международной научной конференции, Москва, 24–26 июня 2021 г.: М.: Русское общество истории и философии науки, 2021. P. 134–137.
Данная статья посвящена формализации широкого спектра сценариев изменения знаний с течением времени. Мы исследуем комбинации временных и эпистемических модальностей, отражающих различные свойства рассуждений рациональных агентов. Для этой цели вводим модель 𝐸𝐸𝑀 – эволюционную эпистемическую модель. ...
Добавлено: 28 июня 2021 г.
О задаче верификации моделей программ для одного расширения логики CTL*
Гнатенко А. Р., Захаров В. А., Моделирование и анализ информационных систем 2020 Т. 27 № 4 С. 428–441
К последовательным реагирующим системам относятся программы и устройства, которые работают с двумя потоками данных и осуществляют преобразование входных потоков данных в выходные потоки. К числу таких систем обработки информации относятся контроллеры, драйверы устройств, компьютерные интерпретаторы. Результатом работы таких вычислительных систем являются бесконечные последовательности пар событий типа запрос-отклик, и поэтому в качестве математических моделей для них ...
Добавлено: 31 января 2021 г.
Using an extension of CTL* for specification and verification of sequential reactive systems
Гнатенко А. Р., Захаров В. А., Системная информатика 2020 Vol. 17 P. 21–32
Последовательные реагирующие системы, такие как контроллеры, системные драйверы, компьютерные интерпретаторы, работают с двумя потоками данных и преобразуют входные потоки данных (управляющие сигналы, инструкции) в выходные потоки управляющих сигналов (инструкции, данные). Конечные преобразователи широко используются в качестве подходящей формальной модели для подобных систем обработки информации. Поскольку вычисления преобразователей протекают во времени, темпоральная логика, очевидно, может использоваться ...
Добавлено: 9 ноября 2020 г.
  • О ВЫШКЕ
  • Цифры и факты
  • Руководство и структура
  • Устойчивое развитие в НИУ ВШЭ
  • Преподаватели и сотрудники
  • Корпуса и общежития
  • Закупки
  • Обращения граждан в НИУ ВШЭ
  • Фонд целевого капитала
  • Противодействие коррупции
  • Сведения о доходах, расходах, об имуществе и обязательствах имущественного характера
  • Сведения об образовательной организации
  • Людям с ограниченными возможностями здоровья
  • Единая платежная страница
  • Работа в Вышке
  • ОБРАЗОВАНИЕ
  • Лицей
  • Довузовская подготовка
  • Олимпиады
  • Прием в бакалавриат
  • Вышка+
  • Прием в магистратуру
  • Аспирантура
  • Дополнительное образование
  • Центр развития карьеры
  • Бизнес-инкубатор ВШЭ
  • Образовательные партнерства
  • Обратная связь и взаимодействие с получателями услуг
  • НАУКА
  • Научные подразделения
  • Исследовательские проекты
  • Мониторинги
  • Диссертационные советы
  • Защиты диссертаций
  • Академическое развитие
  • Конкурсы и гранты
  • Внешние научно-информационные ресурсы
  • РЕСУРСЫ
  • Библиотека
  • Издательский дом ВШЭ
  • Книжный магазин «БукВышка»
  • Типография
  • Медиацентр
  • Журналы ВШЭ
  • Публикации
  • http://www.minobrnauki.gov.ru/
    Министерство науки и высшего образования РФ
  • https://edu.gov.ru/
    Министерство просвещения РФ
  • http://www.edu.ru
    Федеральный портал «Российское образование»
  • https://elearning.hse.ru/mooc
    Массовые открытые онлайн-курсы
  • НИУ ВШЭ1993–2026
  • Адреса и контакты
  • Условия использования материалов
  • Политика конфиденциальности
  • Правила применения рекомендательных технологий в НИУ ВШЭ
  • Карта сайта
Редактору