Modeling and Analysis of Information Systems / Моделирование и анализ информационных систем (МАИС)
Not a member yet
782 research outputs found
Sort by
Равномерность векторных расслоений конечного ранга на полных пересечениях конечной коразмерности в линейных инд-грассманианах
Get PDFA linear projective ind-variety X is called 1-connected if any two points on it can be connected by a chain of lines l1, l2, ..., lk in X, such that li intersects li+1. A linear projective ind-variety X is called 2-connected if any point of X lies on a projective line in X and for any two lines l and l 0 in X there is a chain of lines l = l1, l2, ..., lk = l 0 , such that any pair (li , li+1) is contained in a projective plane P 2 in X. In this work we study an ind-variety X that is a complete intersection in the linear ind-Grassmannian G = lim−→G(km, nm). By definition, X is an intersection of G with a finite number of ind-hypersufaces Yi = lim−→Yi,m, m ≥ 1, of fixed degrees di , i = 1, ..., l, in the space P∞, in which the ind-Grassmannian G is embedded by Pl¨ucker. One can deduce from work [17] that X is 1-connected. Generalising this result we prove that X is 2-connected. We deduce from this property that any vector bundle E of finite rank on X is uniform, i. e. the restriction of E to all projective lines in X has the same splitting type. The motiavtion of this work is to extend theorems of Barth - Van de Ven - Tjurin - Sato type to complete intersections of finite codimension in ind-Grassmannians
Равномерная асимптотика верхней границы дисперсии для случайного многогранника
No full textThe present paper contains a sketch of the proof of an upper bound for the variance of the number of hyperfaces of a random polytope when the mother body is a simple polytope. Thus we verify a weaker version of the result in [1] stated without a proof. The article is published in the author’s wording.Содержится развернутый план доказательства равномерной оценки дисперсии числа гиперграней случайного многогранника в случае, если объемлющее тело — простой многогранник. Таким образом, доказана ослабленная версия результата, оставленного в [1] без доказательства. Статья публикуется в авторской редакции
Модель безопасности информационных потоков для программно-конфигурируемых сетей
No full textSoftware-defined networks (SDN) are a novel paradigm of networking which became an enabler technology for many modern applications such as network virtualization, policy-based access control and many others. Software can provide flexibility and fast-paced innovations in the networking; however, it has a complex nature. In this connection there is an increasing necessity of means for assuring its correctness and security. Abstract models for SDN can tackle these challenges. This paper addresses to confidentiality and some integrity properties of SDNs. These are critical properties for multi-tenant SDN environments, since the network management software must ensure that no confidential data of one tenant are leaked to other tenants in spite of using the same physical infrastructure. We define a notion of end-to-end security in context of software-defined networks and propose a semantic model where the reasoning is possible about confidentiality, and we can check that confidential information flows do not interfere with non-confidential ones. We show that the model can be extended in order to reason about networks with secure and insecure links which can arise, for example, in wireless environments.The article is published in the authors’ wording.Программно-конфигурируемые сети (ПКС, SDN, Software-defined Networks) являются новой парадигмой организации сетей, которая используется во многих современных приложениях, таких как виртуализация сети, управление доступом на основе политик безопасности и многих других. Программное обеспечение ПКС обеспечивает гибкость и быстрый темп инноваций в сети, однако оно имеет сложную природу, в связи с чем возникает необходимость в средствах обеспечения его корректности и безопасности. Абстрактные модели для ПКС могут решить эти задачи. Данная работа направлена на разработку моделей безопасного взаимодействия в ПКС, акцентируя внимание на таких свойствах безопасности, как конфиденциальность и, частично, целостность. Это критические свойства безопасности многопользовательских сетей, поскольку программное обеспечение, управляющее сетью, должно гарантировать, что конфиденциальные данные одного пользователя не будут переданы другим (нежелательным) пользователям. Мы определили понятие сквозной безопасности в контексте ПКС и предложили семантическую модель, позволяющую сделать обоснованный вывод о соблюдении конфиденциальности, и мы можем проверить, что конфиденциальные информационные потоки не смешиваются с не конфиденциальными. Мы показываем, что модель может быть расширена до обоснования соблюдения конфиденциальности в сетях с безопасными и небезопасными каналами связи, которые могут возникнуть, например, в беспроводных средах.Статья представляет собой расширенную версию доклада на VI Международном семинаре “Program Semantics, Specification and Verification: Theory and Applications”, Казань, 2015.Статья публикуется в авторской редакции
Верификация вычислительных решеток с особыми краевыми условиями бесконечными сетями Петри
Get PDFA technique of the computing grid verification using invariants of infinite Petri nets was presented. Models of square grid structures in the form of parametric Petri nets for such edge conditions as connection of edges and truncated devices were constructed. Infinite systems of linear algebraic equations were composed on parametric Petri nets for calculating p-invariants; their parametric solutions were obtained. P-invariant Petri nets are structuraly conservative and bounded that together with liveness are the properties of ideal systems. Liveness investigation based on siphons and traps can be implemented by using p-invariants of modified nets.Представлена методика верификации вычислительных решеток с помощью нахождения инвариантов бесконечных сетей Петри. Построены модели структур квадратных решеток в форме параметрических сетей Петри для таких краевых условий, как соединение краев и усеченные устройства. По параметрическим сетям Петри построены бесконечные системы линейных алгебраических уравнений для вычисления p-инвариантов и получены их параметрические ре- шения. P-инвариантные сети Петри являются структурно консервативными и ограниченными, что, вместе с живостью, является свойствами моделей идеальных систем. Исследование живости модели на основе анализа сифонов и ловушек может быть выполнено с помощью p-инвариантов модифицированных сетей
Формальная верификация программ, написанных на функционально-потоковом языке параллельного программирования
Get PDFThe article is devoted to the methods of proving parallel programs correctness that are based on the axiomatic approach. Formal system for functional data-flow parallel programming language Pifagor is described. On the basis of this system programs correctness could be proved.Работа посвящена доказательству корректности параллельных программ на основе аксиоматического подхода. Описана формальная система для функционально-потокового языка параллельного программирования Пифагор, в рамках которой можно проводить доказательства
Алгоритмы для мажоритарного декодирования групповых кодов
Get PDFWe consider a problem of constructive description and justification of the algorithms necessary for a practical implementation of the majority decoder for group codes specified as left ideals of groupalgebras. In addition to the algorithms needed to implement a classical decoder of J. Massey, it is built a generalization of the classical decoder for codes with unequal protection of characters, which in some cases could be better than the classic one. For use as a classical decoder of J. Massey and its generalization to group codes it was developed an algorithm for constructing decoding trees that lie at the core of these algorithms for majority decoding. Because group codes are defined as left ideals of group algebras, the decoding algorithm for constructing decoding trees allows to build all decoding trees from one tree. On the basis of the generalized decoding algorithm it was developed an algorithm for decoding group codes induced on the subgroup. Application of the developed decoders was illustrated by an example of Reed-Muller-Berman codes and group codes induced by them on a non-Abelian group of affine transformations. In particular, for Reed–Muller–Berman code description and justification of the algorithm for constructing one decoding tree are provided. This three is used for constructing all decoding trees and then it is a built decoder for Reed-Muller-Berman codes and codes induced by them
Локальная динамика уравнения второго порядка с большим экспоненциально распределенным запаздыванием и существенным трением
Get PDFWe study local dynamics of a nonlinear second order differential equation with a large exponentially distributed delay in the vicinity of the zero solution under the condition γ>√ 2. The parameter γ can be interpreted as a friction coefficient. We find such parameter values that critical cases in the stability problem are realized. We show that the characteristic equation for zero solution stability can have arbitrary many roots in the vicinity of imaginary axis. So, the critical case of an infinite dimension is realized. We construct normal forms analogues to describe dynamics of the origin equation. We formulate results about the correspondence of solutions of received PDE and second order DDE with a large exponentially distributed delay. The received asymptotic formulas allow us to evidently find characteristics of origin problem local regimes that are close to the zero solution and also to obtain domains of parameters and initial conditions, where the appearance of any given-type solution is possible
Моделирование счетчиковых машин двухголовочными автоматами
Get PDFA method of modeling the Minsky counter machine behaviour by a two-head finite automaton is proposed.Проводится моделирование работы счетчиковых машин Минского с помощью двухголовочных автоматов
Динамика комплексного пространственно-распределенного уравнения Хатчинсона
Get PDFIn the article the complex Hutchinson equation is studied. New results on numerically observable space-inhomogenious solutions are obtained.Исследуется комплексный вариант уравнения Хатчинсона с запаздыванием в одномерной и двумерной пространственных областях. В то время как характерные режимы действительного распределенного уравнения Хатчинсона достаточно подробно изучены с помощью асимптотических и численных методов в работах М. Бестехорна, Е.В. Григорьевой, С.А. Кащенко, динамика комплексного уравнения требует отдельного исследования. В работе получены новые результаты о численно наблюдаемых пространственно-неоднородных решениях задачи с условиями непроницаемости и периодическими краевыми условиями
Метод логистической функции для нахождения аналитических решений нелинейных дифференциальных уравнений
No full textThe method of the logistic function is presented for finding exact solutions of nonlinear differential equations. The application of the method is illustrated by using the nonlinear ordinary differential equation of the fourth order. Analytical solutions obtained by this method are presented. These solutions are expressed via exponential functions.logistic function, nonlinear wave, nonlinear ordinary differential equation, Painlev´e test, exact solutionДля нахождения точных решений нелинейных дифференциальных уравнений используется метод логистической функции. Применение метода иллюстрируется на примере нелинейного обыкновенного дифференциального уравнения четвертого порядка. Представлены аналитические решения, полученные с помощью этого метода. Как оказалось, эти решения выражаются через экспоненциальные функции