Modeling and Analysis of Information Systems / Моделирование и анализ информационных систем (МАИС)
Not a member yet
782 research outputs found
Sort by
О некоторых задачах локализации в триангуляциях Делоне
Get PDFWe study some problems of nodes localization in a Delaunay triangulation and problem-solving procedures. For the problem of the set of nodes the computationally efficient approach that uses Euclidean minimum spanning tree of Delaunay triangulation is proposed. Efficient estimations for computational comlexity of the proposed methods in the average and in the worst cases are proved.computational geometry, geometric search, Delaunay triangulation, merging of overlapping triangulations, unregular discrete mesh, computational complexityРассматриваются постановки задач локализации узлов в триангуляциях Делоне и методы их решения. Для задачи локализации множества узлов предлагается подход, основанный на прослеживании Евклидова минимального остовного дерева триангуляции Делоне. Приводятся и доказываются оценки сложности предложенных методов в среднем и худшем случаях
Формирование волнового нанорельефа при распылении поверхности ионной бомбардировкой. Нелокальная модель эрозии
Get PDFA nanoscale model of surface erosion, simulating the process of surface shaping under ion bombardment is considered. The possibility of a ripple topography is demonstrated by means of bifurcations theory methods for dynamical systems with an infinite dimensional space of initial data. In particular, we use the normal form of Poincare–Dulak.Рассматривается нелокальное уравнение эрозии, которое получено как одна из математических моделей формирования нанорельефа под воздействием потока ионов. Изучен один из механизмов формирования неоднородного нанорельефа. При математическом анализе периодической краевой задачи для нелокального уравнения эрозии использованы методы исследования динамических систем с бесконечномерным фазовым пространством. Вопрос о локальных бифуркациях однородного состояния равновесия сводится к изучению структуры окрестности нулевого решения трехмерной системы обыкновенных дифференциальных уравнений. При этом использован метод интегральных многообразий в сочетании с аппаратом нормальных форм Пуанкаре–Дюлака
О работе семинара «Нелинейная динамика и вычислительная геометрия» (Workshop “Nonlinear Dynamics and Computational Geometry”)
Get PDFС 10 по 14 сентября 2012 года в Ярославском государственном университете им. П.Г. Демидова прошел международный семинар «Нелинейная динамика и вычислительная геометрия» (“Nonlinear Dynamics and Computational Geometry”), организованный лабораторией им. Делоне и научно-образовательным центром «Нелинейная динамика». На семинаре с лекциями выступили ведущие ученые как в области нелинейной динамики, так и в области вычислительной геометрии, были обсуждены вопросы взаимодействия этих дисциплин. Ниже представлены тезисы наиболее интересных докладов, прозвучавших на семинаре. По докладу Н.А. Кудряшова была подготовлена статья, которая публикуется в настоящем номере журнала
Исследование устойчивости решений начально-краевой задачи, моделирующей динамику одной дискретно-континуальной механической системы
Get PDFThe solution stability of an initial boundary problem for a linear hybrid system of differential equations, which models the rotation of a rigid body with two elastic rods located in the same plane is studied in the paper. To an axis passing through the mass center of the rigid body perpendicularly to the rods location plane is applied the stabilizing moment proportional to the angle of the system rotation, derivative of the angle, integral of the angle. The external moment provides a feedback. A method of studying the behavior of solutions of the initial boundary problem is proposed. This method allows to exclude from the hybrid system of differential equations partial differential equations, which describe the dynamics of distributed elements of a mechanical system. It allows us to build one equation for an angle of the system rotation. Its characteristic equation defines the stability of solutions of all the system. In the space of feedback-coefficients the areas that provide the asymptotic stability of solutions of the initial boundary problem are built up
Задача о наибольшем кратном потоке в делимой сети и ее частные случаи
Get PDFIn the article the problem of finding the maximal multiple flow in the network of any natural multiplicity k is studied. There are arcs of three types: ordinary arcs, multiple arcs and multi-arcs. Each multiple and multi-arc is a union of k linked arcs, which are adjusted with each other. The network constructing rules are described. The definitions of a divisible network and some associated subjects are stated. The important property of the divisible network is that every divisible network can be partitioned into k parts, which are adjusted on the linked arcs of each multiple and multi-arc. Each part is the ordinary transportation network. The main results of the article are the following subclasses of the problem of finding the maximal multiple flow in the divisible network. 1. The divisible networks with the multi-arc constraints. Assume that only one vertex is the ending vertex for a multi-arc in k −1 network parts. In this case the problem can be solved in a polynomial time. 2. The divisible networks with the weak multi-arc constraints. Assume that only one vertex is the ending vertex for a multi-arc in s network parts (1 ≤ s < k − 1) and other parts have at least two such vertices. In that case the multiplicity of the multiple flow problem can be decreased to k − s. 3. The divisible network of the parallel structure. Assume that the divisible network component, which consists of all multiple arcs, can be partitioned into subcomponents, each of them containing exactly one vertex-beginning of a multi-arc. Suppose that intersection of each pair of subcomponents is the only vertex-network source x0. If k = 2, the maximal flow problem can be solved in a polynomial time. If k ≥ 3, the problem is NP-complete. The algorithms for each polynomial subclass are suggested. Also, the multiplicity decreasing algorithm for the divisible network with weak multi-arc constraints is formulated
Как разработать простое средство верификации систем реального времени
Get PDFTo verify real-time properties of UML statecharts one may apply a UPPAAL, toolbox for model checking of real-time systems. One of the most suitable ways to specify an operational semantics of UML statecharts is to invoke the formal model of Hierarchical Timed Automata. Since the model language of UPPAAL is based on Networks of Timed Automata one has to provide a conversion of Hierarchical Timed Automata to Networks of Timed Automata. In this paper we describe this conversion algorithm and prove that it is correct w.r.t. UPPAAL query language which is based on the subset of Timed CTL.Исследуется задача верификации систем реального времени (СРВ). Для описания СРВ удобно использовать диаграммы состояний UML с семантикой, определяемой иерархическими автоматами. Для верификации СРВ часто применяется средство UPPAAL, разработанное для проверки формул логики TCTL на сети временных автоматов. Основным результатом данной статьи является алгоритм трансляции иерархических автоматов в сеть временных автоматов и обоснование его корректности
О неглавных идеалах в полурешетке степеней перечислимости
Get PDFThis paper is dedicated to the study of ideals in semi-lattice of the enumeration degrees.Эта статья посвящена изучению неглавных идеалов в полурешетке степеней перечислимости. Построены некоторые неглавные идеалы в верхней полурешетке.
Новые компоненты схемы модулей MP3 (2; -1; 2; 0) стабильных когерентных пучков ранга 2 без кручения на трехмерном проективном пространстве P3
Get PDFIn this paper we consider Giseker-Maruyama moduli scheme M := MP3(2;¡1; 2; 0) of stable coherent torsion free sheaves of rank 2 with Chern classes c1 = -1, c2 = 2, c3 = 0 on 3-dimensional projective space P3. We will de¯ne two sets of sheaves M1 and M2 in M and we will prove that closures of M1 and M2 in M are irreducible components of dimensions 15 and 19, accordingly.Рассматривается схема модулей Гизекера–Маруямы M := MP3 (2;-1; 2; 0) стабильных когерентных пучков без кручения ранга 2 с классами Черна c1 = -1, c2 = 2, c3 = 0 на трехмерном проективном пространстве P³. Мы определяем два множества пучков M1 и M2 в M и доказываем, что их замыкания M1 и M2 – неприводимые компоненты в M размерностей 15 и 19 соответственно
От редакторов специального выпуска
Get PDFДанный выпуск представляет статьи, подготовленные на основе избранных докладов Третьего международного семинара «Семантика, спецификация и верификация программ: теория и приложения» (Third Workshop on Program Semantics, Specification and Verification: Theory and Applications, PSSV 2012) и Международной конференции «Дискретная геометрия», посвященной 100-летию А. Д. Александрова (Yaroslavl International Conference on Discrete Geometry dedicated to the centenary of A. D. Alexandrov)
Элиминация инвариантов циклов для финитной итерации над неизменяемыми структурами данных в Си программах
No full textThe C-program verification is an urgent problem of modern programming. To apply known methods of deductive verification it is necessary to provide loop invariants which might be a challenge in many cases. In this paper we consider the C-light language [18] which is a powerful subset of the ISO C language. To verify C-light programs the two-level approach [19, 20] and the mixed axiomatic semantics method [1, 3, 11] were suggested. At the first stage, we translate [17] the source C-light program into Ckernel one. The C-kernel language [19] is a subset of C-light. The theorem of translation correctness was proved in [10, 11]. The C-kernel has less statements with respect to the C-light, this allows to decrease the number of inference rules of axiomatic semantics during its development. At the second stage of this approach, the verification conditions are generated by applying the rules of mixed axiomatic semantics [10, 11] which could contain several rules for the same program statement. In such cases the inference rules are applied depending on the context. Let us note that application of the mixed axiomatic semantics allows to significantly simplify verification conditions in many cases. This article represents an extension of this approach which includes our verification method for definite iteration over unchangeable data structures without loop exit in C-light programs. The method contains a new inference rule for the deifinite iteration without invariants. This rule was implemented in verification conditions generator. At the proof stage the SMT-solver Z3 [12] is used. An example which illustrates the application of this technique is considered.he article is published in the authors’ wording.Верификация С-программ является актуальной проблемой современного программирования. Для применения известных методов дедуктивной верификации необходимо аннотировать циклы посредством инвариантов, что во многих случаях является трудной задачей. В этой статье мы рассматриваем язык C-light, который является выразительным подмножеством языка C, соответствующего стандарту ISO. Для верификации C-light программ нами были предложены двухуровневый подход [19, 20] и метод смешанной аксиоматической семантики [1, 3, 11]. На первой стадии этого подхода исходная C-light программа транслируется [17] в программу на языке C-kernel [19], который является подмножеством языка C-light. Теорема о корректности этой трансляции была доказана в [10, 11]. По сравнению с C-light в языке C-kernel меньше операторов, что позволяет уменьшить число правил вывода при разработке аксиоматической семантики. На второй стадии этого подхода для программ на языке C-kernel порождаются условия корректности по правилам смешанной аксиоматической семантики [10, 11], которая может содержать несколько правил вывода для одной и той же программной конструкции. В таких случаях правила вывода применяются однозначно в зависимости от контекста. Заметим, что во многих случаях использование смешанной аксиоматической семантики позволяет упростить условия корректности. В этой статье представлено расширение данного подхода, которое включает наш метод верификации для финитной итерации над неизменяемыми структурами данных без выхода из тела цикла в C-light программах. Данный метод содержит новое правило вывода для таких финитных итераций без инвариантов. Это правило было реализовано в генераторе условий корректности. На стадии доказательства используется SMT-решатель Z3 [12]. Рассмотрен пример, иллюстрирующий применение данного подхода.Статья представляет собой расширенную версию доклада на VI Международном семинаре “Program Semantics, Specification and Verification: Theory and Applications”, Казань, 2015.Статья публикуется в авторской редакции