Журнал
Научно-технический вестник информационных технологий, механики и оптики
УДК:
Номер:6 (64)
Скачать PDF0 Кбайт
MODEL CHECKING AUTOMATA-BASED PROGRAMS USING REDUCED TRANSITION GRAPH CONSTRUCTION
Аннотация:
This article is concentrated on techniques of converting automata-based program models to Kripke models designed for checking properties related to system behavior. The definition of these properties is considered by means of temporal logic formulas. We propose an efficient technique of such converting and property stating that allows construction of small Kripke models and sufficiently fast checking of such models.
Ключевые слова:
Постоянный URL
Статьи в номере
- СТРУКТУРА ОБОБЩЕННОЙ КОМПЬЮТЕРНОЙ МОДЕЛИ ОПТИКО-ЭЛЕКТРОННЫХ СИСТЕМ
- ИЗУЧЕНИЕ ПОГРЕШНОСТЕЙ СОВМЕЩЕНИЯ МАРОК ПРИ ПОПЕРЕЧНЫХ НАВОДКАХ
- УСТАНОВКА ДЛЯ ЭКСПЕРИМЕНТАЛЬНОГО НАБЛЮДЕНИЯ СПЕКТРОВ ХЕМИЛЮМИНЕСЦЕНЦИИ
- ИССЛЕДОВАНИЕ ВРЕМЕНИ ЖИЗНИ ЛЮМИНЕСЦЕНЦИИ CdSe/ZnS КВАНТОВЫХ ТОЧЕК В СЛУЧАЕ ОБРАЗОВАНИЯ И ДИССОЦИАЦИИ КОМПЛЕКСОВ КТ/ОРГАНИЧЕСКАЯ МОЛЕКУЛА В ТОНКИХ ПОЛИМЕРНЫХ ПЛЕНКАХ
- МЕТОД ОПРЕДЕЛЕНИЯ МЕСТОПОЛОЖЕНИЯ ЩЕЛИ И КОНТРОЛЯ КАЧЕСТВА ТЕРМОСОЕДИНЕНИЙ НА ОСНОВЕ МАГНИТНЫХ ИЗМЕРЕНИЙ
- МОДЕЛИРОВАНИЕ ШПИНДЕЛЬНЫХ ГИДРОСТАТИЧЕСКИХ ПОДШИПНИКОВ И ИССЛЕДОВАНИЕ ВОЗМОЖНОСТЕЙ ПОВЫШЕНИЯ ИХ ДИНАМИЧЕСКОГО КАЧЕСТВА
- ПРОГРАММНЫЙ КОМПЛЕКС ИНФОРМАЦИОННОЙ ПОДДЕРЖКИ ПРИНЯТИЯ РЕШЕНИЙ ПРИ ОЦЕНКЕ ТИПОВЫХ ТРАЕКТОРИЙ ПОЛЕТА
- ВЛИЯНИЕ ИЗЛУЧЕНИЯ YLP–ЛАЗЕРА НА ВОЛЬТ-ФАРАДНЫЕ ХАРАКТЕРИСТИКИ СИСТЕМЫ КРЕМНИЙ–ДВУОКИСЬ КРЕМНИЯ
- МНОГОЭЛЕМЕНТНЫЕ ПРИЕМНИКИ НА ОСНОВЕ СЕЛЕНИДА СВИНЦА ДЛЯ ОБЛАСТИ СПЕКТРА 2–5 МКМ
- ИССЛЕДОВАНИЕ ОПТИЧЕСКИХ СВОЙСТВ ПОКРЫТИЙ НА ОСНОВЕ ГИДРОГЕНИЗИРОВАННОГО УГЛЕРОДА, МОДИФИЦИРОВАННОГО НАНОЧАСТИЦАМИ МЕТАЛЛОВ
- ВЛИЯНИЕ ДИСПЕРСИОННОГО НАПОЛНИТЕЛЯ НА ОСНОВЕ АЛЮМИНИЯ НА СТРУКТУРУ И СВОЙСТВА ПОЛИПРОПИЛЕНА
- ВЕРИФИКАЦИЯ АВТОМАТНЫХ МОДЕЛЕЙ МЕТОДОМ РЕДУЦИРОВАННОГО ГРАФА ПЕРЕХОДОВ
- СЕМАНТИЧЕСКАЯ ПАУТИНА И ИСКУССТВЕННЫЙ ИНТЕЛЛЕКТ
- МУЛЬТИАГЕНТНАЯ ТЕХНОЛОГИЯ ФОРМИРОВАНИЯ ВИРТУАЛЬНЫХ БИЗНЕС-ПЛОЩАДОК В ЕДИНОМ ИНФОРМАЦИОННО-КОММУНИКАЦИОННОМ ПРОСТРАНСТВЕ РАЗВИТИЯ ИННОВАЦИЙ
- ОБЕСПЕЧЕНИЕ УСТОЙЧИВОГО РАЗВИТИЯ ПРЕДПРИНИМАТЕЛЬСКИХ СТРУКТУР НА ОСНОВЕ ВЗАИМОДЕЙСТВИЯ МЕХАНИЗМА УПРАВЛЕНИЯ И САМООРГАНИЗАЦИИ
- 4 «РЕ-» ИЗМЕНЕНИЯ БИЗНЕСА: РЕФОРМИРОВАНИЕ,РЕОРГАНИЗАЦИЯ, РЕСТРУКТУРИЗАЦИЯ, РЕИНЖИНИРИНГ
- СОВРЕМЕННОЕ СОСТОЯНИЕ ПРОБЛЕМ УПРАВЛЕНИЯ КОНКУРЕНТОСПОСОБНОСТЬЮ ПРЕДПРИЯТИЙ
- МАКРОЭКОНОМИЧЕСКИЕ ЭФФЕКТЫ РЕАЛИЗАЦИИ КРУПНОМАСШТАБНЫХ ПРОЕКТОВ
- РАЗРАБОТКА ТИПОВОГО WEB-ПОРТАЛА ИННОВАЦИОННОЙ ОБРАЗОВАТЕЛЬНОЙ ПРОГРАММЫ УНИВЕРСИТЕТА И ВНЕДРЕНИЕ ЕГО В УСЛОВИЯХ СЕТЕВОЙ ИНФРАСТРУКТУРЫ УНИВЕРСИТЕТА