Modeling and Analysis of Information Systems / Моделирование и анализ информационных систем (МАИС)
Not a member yet
782 research outputs found
Sort by
О гипотезах Тэйта для дивизоров на расслоенном многообразии и его общем схемном слое в случае конечной характеристики
Get PDFWe investigate interrelations between the Tate conjecture for divisors on a fibred variety over a finite field and the Tate conjecture for divisors on the generic scheme fibre under the condition that the generic scheme fibre has zero irregularity. Let be a surjective morphism of smooth projective varieties over a finite field of characteristic , is a curve and the generic scheme fibre of is a smooth variety over the field of rational functions of the curve , is an algebraic closure of the field , is its separable closure, is the N\'eron - Severi group of classes of divisors on the variety modulo algebraic equivalence, and assume that the following conditions hold: If, for a prime number not dividing and different from the characteristic of the field , the following relation holds in other words, if the Tate conjecture for divisors on holds, then for any prime number the Tate conjecture holds for divisors on : In particular, it follows from this result that the Tate conjecture for divisors on an arithmetic model of a surface over a sufficiently large global field of finite characteristic different from 2 holds as well.В работе изучаются взаимоотношения между гипотезой Тэйта для дивизоров на расслоенном многообразии над конечным полем и гипотезой Тэйта для дивизоров на общем схемном слое при условии, что общий схемный слой имеет иррегулярность нуль. Пусть -- сюръективный морфизм гладких проективных многообразий над конечным полем характеристики , -- кривая, общий схемный слой морфизма является гладким многообразием над полем рациональных функций кривой , -- алгебраическое замыкание поля , -- его сепарабельное замыкание, -- группа Нерона -- Севери классов дивизоров на многообразии по модулю алгебраической эквивалентности, причем выполнены следующие условия: \; Если для простого числа , не делящего и отличного от характеристики поля , верно соотношение \; другими словами, если верна гипотеза Тэйта для дивизоров на , то для любого простого числа гипотеза Тэйта верна для дивизоров на : В частности, из этого результата следует гипотеза Тэйта для дивизоров на арифметической модели K3 -- поверхности над достаточно большим глобальным полем конечной характеристики, отличной от 2
Декодирование тензорного произведения MLD-кодов и приложения к кодовым криптосистемам
Get PDFFor the practical application of code cryptosystems such as McEliece, it is necessary that the code used in the cryptosystem should have a fast decoding algorithm. On the other hand, the code used must be such that finding a secret key from a known public key would be impractical with a relatively small key size. In this connection, in the present paper it is proposed to use the tensor product of group codes and in a McEliece-type cryptosystem. The algebraic structure of the code in the general case differs from the structure of the codes and , so it is possible to build stable cryptosystems of the McEliece type even on the basis of codes for which successful attacks on the key are known. However, in this way there is a problem of decoding the code . The main result of this paper is the construction and justification of a set of fast algorithms needed for decoding this code. The process of constructing the decoder relies heavily on the group properties of the code . As an application, the McEliece-type cryptosystem is constructed on the code and an estimate is given of its resistance to attack on the key under the assumption that for code cryptosystems on codes an effective attack on the key is possible. The results obtained are numerically illustrated in the case when , are Reed--Muller--Berman codes for which the corresponding code cryptosystem was hacked by L. Minder and A. Shokrollahi (2007).Для практического применения кодовой криптосистемы типа Мак-Элиса необходимо, чтобы используемый в основе криптосистемы код имел быстрый алгоритм декодирования. С другой стороны, используемый код должен быть таким, чтобы нахождение секретного ключа по известному открытому ключу было практически неосуществимо при относительно небольшом размере ключа. В связи с этим в настоящей работе предлагается в криптосистеме типа Мак-Элиса использовать тензорное произведение групповых -кодов и . Алгебраическая структура кода в общем случае отличается от структуры кодов и , поэтому представляется возможным построение стойких криптосистем типа Мак-Элиса даже на основе кодов , для которых известны успешные атаки на ключ. Однако на этом пути возникает проблема декодирования кода . Основной результат настоящей работы -- построение и обоснование набора необходимых для декодирования этого кода быстрых алгоритмов. Процесс построения декодера существенно опирается на групповые свойства кода . В качестве приложения в работе построена криптосистема типа Мак-Элиса на коде и приводится оценка ее стойкости к атаке на ключ в предположении, что для кодовых криптосистем на кодах возможна эффективная атака на ключ. Полученные результаты численно проиллюстрированы в случае, когда , -- коды Рида--Маллера--Бермана, для которых соответствующая кодовая криптосистема взломана Л. Миндером и А. Шокроллахи (2007 г.)
Устойчивость решений дискретных краевых задач для уравнения двумерной фильтрации
Get PDFThe stability of the solutions of the linear equations arising in the theory of twodimensional digital filtration is studied. The different statements of the initial value problem are analysed. As the basic results, the corresponding stability criterion is obtained for each of them. Исследуется устойчивость решений линейных уравнений, возникающих в теории двумерной цифровой фильтрации. Анализируются различные постановки начальной задачи. В качестве основных результатов для каждой из них получен соответствующий критерий устойчивости в терминах корней характеристического уравнения. Для краевых условий типа Дирихле, Неймана или для периодических краевых условий обоснован переход к системе линейных уравнений первого порядка в конечномерном пространстве. Кроме этого, рассмотрены краевые условия, определяющие поведение решений на «бесконечности». Здесь речь идет об анализе линейных бесконечномерных систем.
О задаче минимизации последовательных программ
Get PDFFirst-order program schemata is one of the simplest models of sequential imperative programs intended for solving verification and optimization problems. We consider the decidable relation of logical-thermal equivalence of these schemata and the problem of their size minimization while preserving logical-thermal equivalence. We prove that this problem is decidable. Further we show that the first-order program schemata supplied with logical-thermal equivalence and finite state deterministic transducers operating over substitutions are mutually translated into each other. This relationship implies that the equivalence checking problem and the minimization problem for these transducers are also decidable. In addition, on the basis of the discovered relationship, we have found a subclass of firstorder program schemata such that their minimization can be performed in polynomial time by means of known techniques for minimization of finite state transducers operating over semigroups. Finally, we demonstrate that in general case the minimization problem for finite state transducers over semigroups may have several non-isomorphic solutions.Стандартные схемы программ — это одна из наиболее простых моделей последовательных императивных программ, предназначенная для решения задач оптимизации и верификации программ. Мы рассматриваем разрешимое отношение логико-термальной эквивалентности стандартных схем программ и задачу минимизации их размера при условии сохранения отношения логико-термальной эквивалентности. Нами доказано, что эта задача является алгоритмически разрешимой. Далее показано, что стандартные схемы программ с отношением логико-термальной эквивалентности и конечные детерминированные автоматы-преобразователи, работающие над полугруппами подстановок, взаимно транслируются друг в друга. Отсюда следует, что также разрешимы задачи проверки эквивалентности и минимизации для преобразователей указанного вида. Кроме того, на основе обнаруженной взаимосвязи выделен подкласс стандартных схем программ, минимизация которых осуществима за полиномиальное время при помощи ранее известных методов минимизации автоматов-преобразователей, работающих над полугруппами. В заключении приведен пример, свидетельствующий о том, что в общем случае задача минимизации автоматов- преобразователей над полугруппой подстановок может иметь несколько неизоморфных решений.
Прототип статического тайп-чекера для языка программирования Jolie
No full textStatic verification of a program source code correctness is an important element of software reliability. Formal verification of software programs involves proving that a program satisfies a formal specification of its behavior. Many languages use both static and dynamic type checking. With such approach, the static type checker verifies everything possible at compile time, and the dynamic one checks the remaining. The current state of the Jolie programming language includes a dynamic type system. Consequently, it allows avoidable run-time errors. A static type system for the language has been formally defined on paper but lacks an implementation yet. In this paper, we describe a prototype of Jolie Static Type Checker (JSTC), which employs a technique based on a SMT solver. We describe the theory behind and the implementation, and the process of static analysis. The article is published in the authors’ wording. Статическая верификация исходного кода программы является важным элементом надежности программного обеспечения. Под верификацией предполагается доказательство соответствия поведения программы ее спецификации. Во многих языках программирования используется как статическая, так и динамическая проверка типов. Таким образом, статический тайп-чекер старается проверить все возможное во время компиляции, а динамический проверяет оставшееся. На данный момент язык программирования Jolie имеет динамическую систему типов, что позволяет обнаруживать ошибки только во время выполнения программы. Статическая система типов для языка была формально определена на бумаге, но пока не реализована. В этой статье мы представим прототип статического тайп-чекера для языка программирования Jolie (JolieStaticTypeChecker или JSTC), основанный на SMT-решателе. Мы опишем базовую теорию, необходимую для реализации тайп-чекера, саму реализацию, а также процесс статического анализа программы. Статья публикуется в авторской редакции
Асимптотическое исследование решения уравнения теплопроводности вблизи границы раздела двух сред
Get PDFPhysical phenomena that arise near the boundaries of media with different characteristics, for example, changes in temperature at the water-air interface, require the creation of models for their adequate description. Therefore, when setting model problems one should take into account the fact that the environment parameters undergo changes at the interface. In particular, experimentally obtained temperature curves at the water-air interface have a kink, that is, the derivative of the temperature distribution function suffers a discontinuity at the interface. A function with this feature can be a solution to the problem for the heat equation with a discontinuous thermal diffusivity and discontinuous function describing heat sources. The coefficient of thermal diffusivity in the water-air transition layer is small, so a small parameter appears in the equation prior to the spatial derivative, which makes the equation singularly perturbed. The solution of the boundary value problem for such an equation can have the form of a contrast structure, that is, a function whose domain contains a subdomain, where the function has a large gradient. This region is called an internal transition layer. The existence of a solution with the internal transition layer of such a problem requires justification that can be carried out with the use of an asymptotic analysis. In the present paper, such an analytic investigation was carried out, and this made it possible to prove the existence of a solution and also to construct its asymptotic approximation.Физические явления, возникающие вблизи границы раздела сред с различными характеристиками, требуют учета некоторых особенностей при их моделировании. Необходимо учитывать тот факт, что на границе раздела параметры окружающей среды претерпевают изменения. Например, экспериментально полученные графики распределения температуры среды вблизи границы раздела вода-воздух имеют излом на границе, поэтому при моделировании производная функции распределения температуры должна быть разрывной. Функция, обладающая такой особенностью, может являться решением задачи для уравнения теплопроводности с разрывным коэффициентом температуропроводности и разрывной функцией, описывающей источники тепла. Поскольку коэффициент температуропроводности в переходном слое вода-воздух является малым, в уравнении перед пространственной производной возникает малый параметр, что делает уравнение сингулярно возмущенным. Решение краевой задачи для такого уравнения может иметь вид контрастной структуры, то есть функции, в области определения которой содержится подобласть, где функция обладает большим градиентом. Такая подобласть называется внутренним переходным слоем. Из экспериментальных наблюдений известно, что в случае перепада температур между водой и воздухом (летний день) вблизи границы раздела возникает подобный переходный слой с резким изменением температуры. Существование решения задачи с внутренним переходным слоем нуждается в обосновании, которое можно провести при помощи асимптотического анализа. В настоящей работе было проведено подобное аналитическое исследование, и это позволило доказать существование решения, а также построить его асимптотическое приближение
Автоматизированная Обучающая Система для обучения курсу анализа сложности алгоритмов
No full textThis article describes problems of designing automated teaching system for “Computational complexity of algorithms” course. This system should provide students with means to familiarize themselves with complex mathematical apparatus and improve their mathematical thinking in the respective area. The article introduces the technique of algorithms symbol scroll table that allows estimating lower and upper bounds of computational complexity. Further, we introduce a set of theorems that facilitate the analysis in cases when the integer rounding of algorithm parameters is involved and when analyzing the complexity of a sum. At the end, the article introduces a normal system of symbol transformations that allows one both to perform any symbol transformations and simplifies the automated validation of such transformations. The article is published in the authors’ wording.В данной работе исследуются вопросы построения автоматизированной обучающей системы “Анализ сложности алгоритмов”, которая позволит учащемуся освоить сложный математический аппарат и развить логико-математическое мышление в этом направлении. Вводится технология символьной прокрутки алгоритма, позволяющая получать верхние и нижние оценки вычислительной сложности. Приводятся утверждения, облегчающие анализ в случае целочисленного округления параметров алгоритма, а также при оценке сложности сумм. Вводится нормальная система символьных преобразований, позволяющая, с одной стороны, делать учащемуся любые символьные преобразования, а с другой стороны – упростить автоматический контроль корректности таких преобразований. Статья публикуется в авторской редакции.
Семантически-ориентированная миграция Java-программ: опыт практического применения
Get PDFThe purpose of the study is to demonstrate the feasibility of automated code migration to a new set of programming libraries. Code migration is a common task in modern software projects. For example, it may arise when a project should be ported to a more secure or feature-rich library, a new platform or a new version of an already used library. The developed method and tool are based on the previously created by the authors a formalism for describing libraries semantics. The formalism specifies a library behaviour by using a system of extended finite state machines (EFSM). This paper outlines the metamodel designed to specify library descriptions and proposes an easy to use domainspecific language (DSL), which can be used to define models for particular libraries. The mentioned metamodel directly forms the code migration procedure. A process of migration is split into five steps, and each step is also described in the paper. The procedure uses an algorithm based on the breadth- first search extended for the needs of the migration task. Models and algorithms were implemented in the prototype of an automated code migration tool. The prototype was tested by both artificial code examples and a real-world open source project. The article describes the experiments performed, the difficulties that have arisen in the process of migration of test samples, and how they are solved in the proposed procedure. The results of experiments indicate that code migration can be successfully automated. Данная статья посвящена разработке процедуры автоматизированной миграции Java-программ на новый набор библиотек. Задача миграции (портирования) кода часто встречается в современных программных проектах. Например, такая задача может возникнуть, когда проект необходимо перенести на более безопасную или функциональную библиотеку, на новую платформу или на новую версию уже используемой в проекте библиотеки. В данной работе представлена процедура автоматизированной миграции, основанная на семантическом подходе. Для процедуры миграции была разработана метамодель библиотеки, использующая предложенный ранее авторами формализм и предназначенная для описания библиотек на объектно-ориентированных языках. Формализм описывает поведение библиотек с помощью системы расширенных конечных автоматов (РКА). Процедура миграции разбита на пять шагов, каждый шаг подробно описан в тексте статьи. В процедуре используется алгоритм вычисления эквивалентной трассы на основе поиска в ширину, расширенный для решения задач миграции. Предложенная процедура реализована в прототипе инструмента миграции. Инструмент включает в себя модули извлечения трассы выполнения программ, визуализации моделей библиотек, взаимодействия с пользователем и непосредственно миграции. Для инструмента был разработан язык описания библиотек. Прототип инструмента был протестирован как на искусственных примерах, так и на существующем проекте. В статье подробно описаны проведенные эксперименты, отдельно отмечены сложности, возникающие в процессе миграции тестовых примеров, и то, как они решаются в предложенной процедуре. В качестве библиотек в экспериментах используются реализации протокола HTTP и библиотеки протоколирования. Результаты тестирования показали, что миграция кода может быть успешно автоматизирована с использованием разработанной процедуры.
Замечание об области притяжения стационарного решения одного сингулярно возмущённого параболического уравнения
Get PDFWe consider a boundary-value problem for a singularly perturbed parabolic equation with an initial function independent of a perturbation parameter in the case where a degenerate stationary equation has smooth possibly intersecting roots. Before, the existence of a stable stationary solution to this problem was proved and the domain of attraction of this solution was investigated — due to exchange of stabilities, the stationary solution approaches the non-smooth (but continuous) composite root of the degenerate equation as the perturbation parameter gets smaller, and its domain of attraction contains all initial functions situated strictly on one side of the other non-smooth (but continuous) composite root of the degenerate equation. We show that if the initial function is out of the boundary of this family of initial functions near some point, the problem cannot have a solution inside the domain of the problem, i.e. this boundary is the true boundary of the attraction domain. The proof uses ideas of the nonlinear capacity method.В работе рассмотрена начально-краевая задача для одного сингулярно возмущённого параболического уравнения с не зависящей от малого параметра начальной функцией в случае, когда вырожденное стационарное уравнение имеет гладкие, возможно, пересекающиеся корни. Ранее было доказано существование устойчивого стационарного решения этой задачи и исследована его область притяжения вследствие смены устойчивости стационарное решение асимптотически приближается к некоторому негладкому (но непрерывному) составному корню вырожденного уравнения при уменьшении параметра возмущения, а его области притяжения принадлежат все начальные функции, находящиеся строго по одну сторону от другого негладкого (но непрерывного) составного корня вырожденного уравнения. В работе показано, что если начальная функция выходит за границу указанного семейства начальных функций вблизи некоторой точки, то исходная задача не имеет решения внутри области определения переменных задачи, т.е. эта граница в действительности является границей области притяжения. Доказательство этого факта основано на идеях метода нелинейной ёмкости