Препринты Института систем информатики СО РАН 1999 г.

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

В данной работе изучаются иерархии регулярных “беззвездных” языков, индуцируемые иерархиями предложений подходящих сигнатур по числу перемен кванторов в предваренной нормальной форме. Доказано, что все уровни этих иерархий не обладают свойством редукции, но два первых уровня обладают свойством отделимости. Установлены включения между уровнями этих иерархий, а также некоторых утончений этих иерархий. Ключевые слова: беззвездные регулярные языки, иерархия, редукция, отделимость, утончение.

Представляем новый, логический подход к проблеме разрешимости иерархий Страубинга и Бржозовского, основанный на теореме сохранения из теории моделей, на теореме Хигмана и на теореме о дереве Рабина. Таким образом мы получаем чисто логические краткие доказательства некоторых известных фактов о разрешимости, которые могут представлятьмет одологический интерес. Наш подход также применим к некоторым другим похожим ситуациям, скажем, к "словам" над плотными порядками, относящимся к непрерывному времени и гибридным системам. Ключевые слова: беззвездные регулярные языки, иерархии, определимость, разрешимость.

Эта работа адресована ученикам первого и второго классов. Два раздела информатики ("Внутреннее устройство компьютера" и "Компьютер и здоровье") излагаются методом микрооткрытий.

Для разработки распределенных систем широко используются методы формального описания (МФО), такие как Specification and Description Language (SDL), Extended State Transition Language (ESTELLE), Language of Temporal Ordering Specification (LOTOS). Верификация МФО-спецификаций (доказательство свойствбезопасности , прогресса, etc.) — актуальная научная проблема. Логический подход к этой проблеме подразумевает разработку точной математической семантики дляМФО, выбор логического языка представления свойств и выбор соответствующей методики доказательства. Предлагаемый подход к верификации SDL-спецификаций использует двухуровневую схему. На первом этапе SDL-спецификации транслируются в модельный язык высокого уровня, а на втором этапе верифицируются свойства модельных спецификаций. В качестве модельного языка используется специально разработанный язык Basic-REAL (bREAL). Этот язык имеет точную математическую семантику и является версией ранее описанного языка REAL, который основан на SDL и CTL. В препринте на формальном и неформальном уровне описаны синтаксис и семантика языка bREAL, доказано несколько математических свойств этой семантики (включая устойчивость к заиканию и интерливинговый характер параллелизма), приведен пример спецификации и верификации системы “Касса-Пассажир”.

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

В работе предложен метод верификации количественных свойств параллелизма в системах реального времени. Для этой цели вводится новая темпоральная логика реального времени TCCTL, которая является расширением языка ветвящегося времени CCTL, предложенного Пенчеком, за счет добавления временных ограничений на его операторы. Предложенная логика позволяет как различать точки параллельного ветвления и точки недетерминированного выбора, так и выражать временные аспекты поведения системы. Таким образом, TCCTL позволяет адекватно описывать системы, представленные моделями с семантикой “истинного параллелизма”. В качестве модели параллельных систем реального времени используются временные сети Петри. Предлагается алгоритм анализа поведенческих свойств временных сетей Петри, основанный на темпоральной логике TCCTL. Алгоритм линеен по размеру формулы и экспоненциален по размеру сети.

Предлагаются средства формального определения родовых типов объектов, сатегорий родовых типов, годовых функций и родовых процедур в объектно-ориентированных машинах абстрактных состояний. Эти средства позволяют специфицировать алгоритмы над сложными структурами данных, абстрагируясь как от типа компонентов структуры, так и самой структуры. Использование предложенных средств демонстрируется примерами спецификаций некоторых важных компонентов библиотеки стандартных шаблонов для языка программирования С++.

В последнее десятилетие словосочетание "корпоративная сеть" приобрело большую популярность. Стремительный рост вычислительной мощи компьютерной техники и удешевление средств телекоммуникаций сделали реальными замыслы соединения территориально распределенных источни ков и потребителей информации относительно недорогими высокоскоростными каналами связи и организации работы на основе современных технологий (распределенные базы данных, клиент-сервер и т. д.). Данная работа ставит своей целью, с одной стороны, провести краткий обзор существующих методов передачи данных с помощью широкополосного сигнала, а с другой - представить идею нового метода, использующего понятие обратной пространственной связи.

Рассматривается проблема анализа циклов и отбора кандидатов на распараллеливание, осуществляемого распараллеливающим компилятором. Предварительно дано описание с этой точки зрения известных распараллеливающих компиляторов и соответствующих инструментальных систем.

В данной работе собраны задания для детей 6-10 лет, которые могут быть использованы на уроках информатики при изучении тем "Информация" и "Алгоритмы".