Modeling and Analysis of Information Systems / Моделирование и анализ информационных систем (МАИС)
Not a member yet
782 research outputs found
Sort by
Замечания о последних достижениях в доказательстве устойчивости с использованием KeYmaeraX
Get PDFKeYmaeraX is a Hoare-style theorem prover for hybrid systems. A hybrid system can be seen as an aggregation of both discrete and continuous variables, whose values can change abruptly or continuously, respectively. KeYmaeraX supports only variables having the primitive type bool or real. Due to the mixture of discrete and continuous system elements, one promising application area for KeYmaeraX are closed-loop control systems. A closed-loop control system consists of a plant and a controller. While the plant is basically an aggregation of continuous variables whose values change over time accordingly to physical laws, the controller can be seen as an algorithm formulated in a classical programming language. In this paper, we review some recent extensions of the proof calculus applied by KeYmaeraX that make formal proofs on the stability of dynamic systems more feasible. Based on an example, we first introduce to the topic and prove asymptotic stability of a given system in a hand-written mathematical style. This approach is then compared with a formal encoding of the problem and a formal proof established in KeYmaeraX. We also discuss open problems such as the formalization of asymptotic stability.KeYmaeraX -- это доказательство теорем в стиле Хоара для гибридных систем. Гибридную систему можно рассматривать как совокупность дискретных, так и непрерывных переменных, значения которых могут изменяться резко или непрерывно соответственно. KeYmaeraX поддерживает только переменные, имеющие примитивный тип bool или real. Благодаря сочетанию дискретных и непрерывных элементов системы, одной из перспективных областей применения KeYmaeraX являются системы управления с замкнутым контуром. Система управления с замкнутым контуром состоит из установки и контроллера. В то время как установка в основном представляет собой совокупность непрерывных переменных, значения которых меняются со временем в соответствии с физическими законами, контроллер можно рассматривать как алгоритм, сформулированный на классическом языке программирования. В этой статье мы рассмотрим некоторые недавние расширения исчисления доказательств, применяемые KeY\\-maeraX, которые делают формальные доказательства устойчивости динамических систем более выполнимыми. Основываясь на примере, мы сначала познакомимся с темой и докажем асимптотическую устойчивость данной системы
Классификация текстов по жанрам на основе ритмических характеристик
Get PDFThe article is devoted to the analysis of the rhythm of texts of different genres: fiction novels, advertisements, scientific articles, reviews, tweets, and political articles. The authors identified lexico-grammatical figures in the texts: anaphora, epiphora, diacope, aposiopesis, etc., that are markers of the text rhythm. On their basis, statistical features were calculated that describe quantitatively and structurally these rhythm features.The resulting text model was visualized for statistical analysis using boxplots and heat maps that showed differences in the rhythm of texts of different genres. The boxplots showed that almost all genres differ from each other in terms of the overall density of rhythm features. Heatmaps showed different rhythm patterns across genres. Further, the rhythm features were successfully used to classify texts into six genres. The classification was carried out in two ways: a binary classification for each genre in order to separate a particular genre from the rest genres, and a multi-class classification of the text corpus into six genres at once. Two text corpora in English and Russian were used for the experiments. Each corpus contains 100 fiction novels, scientific articles, advertisements and tweets, 50 reviews and political articles, i.e. a total of 500 texts. The high quality of the classification with neural networks showed that rhythm features are a good marker for most genres, especially fiction. The experiments were carried out using the ProseRhythmDetector software tool for Russian and English languages. Text corpora contains 300 texts for each language.Статья посвящена анализу ритма текстов различных жанров: художественных романов, рекламы, научных статей, отзывов, твитов и политических статей. Авторы выделили в текстах лексико-грамматические средства: анафору, эпифору, диакопу, апозиопезу и т. п., которые являются маркерами ритма текста. На их основе были подсчитаны статистические характеристики, описывающие количественно и структурно данные ритмические средства.Полученная модель текста была визуализирована для статистического анализа с помощью диаграмм размаха и тепловых карт, которые показали отличия в ритме текстов различных жанров. Диаграммы размаха показали, что практически все жанры отличаются друг от друга по общей плотности ритмических характеристик. Тепловые карты показали различную структуру ритма у жанров.Далее ритмические характеристики успешно использовались для классификации текстов по шести жанрам. Высокое качество классификации показало, что ритмические характеристики являются хорошим маркером для большинства жанров, в особенности для художественной литературы. Эксперименты проводились с помощью программного инструмента ProseRhythmDetector для русского и английского языков. Корпуса текстов содержат по 300 текстов для каждого языка
NP-полнота задачи о минимальном остовном дереве в кратном графе кратности k ≥ 3
Get PDFIn this paper, we study undirected multiple graphs of any natural multiplicity k > 1. There are edges of three types: ordinary edges, multiple edges and multi-edges. Each edge of the last two types is a union of k linked edges, which connect 2 or (k + 1) vertices correspondingly. The linked edges should be used simultaneously. If a vertex is incident to a multiple edge, it can be also incident to other multiple edges and it can be the common end of k linked edges of some multi-edge. If a vertex is the common end of some multi-edge, it cannot be the common end of another multi-edge. A multiple tree is a connected multiple graph with no cycles. Unlike ordinary trees, the number of edges in a multiple tree is not fixed. The problem of finding the spanning tree can be set for a multiple graph. Complete spanning trees form a special class of spanning trees of a multiple graph. Their peculiarity is that a multiple path joining any two selected vertices exists in the tree if and only if such a path exists in the initial graph. If the multiple graph is weighted, the minimum spanning tree problem and the minimum complete spanning tree problem can be set. Also we can formulate the problems of recognition of the spanning tree and complete spanning tree of the limited weight. The main result of this article is the proof of NPcompleteness of such recognition problems for arbitrary multiple graphs as well as for divisible multiple graphs in the case when multiplicity k ≥ 3. The corresponding optimization problems are NP-hard.В статье рассматриваются неориентированные кратные графы произвольной натуральной кратности k > 1. Кратный граф содержит ребра трех типов: обычные, кратные и мультиребра. Ребра последних двух типов представляют собой объединение k связанных ребер, которые соединяют 2 или (k + 1) вершину соответственно. Связанные ребра могут использоваться только согласованно. Если вершина инцидентна кратному ребру, то она может быть инцидентна другим кратным ребрам, а также она может быть общим концом k связанных ребер мультиребра. Если вершина является общим концом мультиребра, то она не может быть общим концом никакого другого мультиребра. Кратное дерево определяется как связный кратный граф без циклов. В отличие от обычных деревьев количество ребер в кратных деревьях не фиксировано. Для кратного графа можно поставить задачу поиска его остовного дерева. Среди всех остовных деревьев в кратном графе выделяется особый класс – полные остовные деревья. Кратный путь между любой парой вершин в таком дереве существует тогда и только тогда, когда кратный путь между ними существует в исходном графе. Если кратный граф является взвешенным, то для него можно поставить задачу о минимальном остовном дереве, а также о минимальном полном остовном дереве. Кроме того, можно сформулировать задачи распознавания остовного и полного остовного дерева ограниченного веса. Основным результатом данной статьи является доказательство того, что указанные задачи распознавания являются NP-полными как в случае произвольных, так и в случае делимых кратных графов, если кратность k ≥ 3. Соответствующие оптимизационные задачи являются NP-трудными
Алгоритм корректировки уровней полезных сигналов при расшифровке вихретоковых дефектограмм
Get PDFTo ensure traffic safety of railway transport, non-destructive tests of rails are regularly carried out by using various approaches and methods, including eddy-current flaw detection methods. An automatic analysis of large data sets (defectograms) that come from the corresponding equipment is an actual problem. The analysis means a process of determining the presence of defective sections along with identifying structural elements of railway tracks in defectograms. This article continues the cycle of works devoted to the problem of automatic recognizing images of defects and structural elements of rails in eddy-current defectograms. In the process of forming these images, only useful signals are taken into account, the threshold levels of amplitudes of which are determined automatically from eddy-current data. The previously used algorithm for finding threshold levels was focused on situations in which the vast majority of signals coming from the flaw detector is a rail noise. A signal is considered useful and is subject to further analysis if its amplitude is twice the corresponding noise threshold. The article is devoted to the problem of correcting threshold levels, taking into account the need to identify extensive surface defects of rails. An algorithm is proposed for finding the values of threshold levels of rail noise amplitudes with their subsequent correction in the case of a large number of useful signals from extensive defects. Examples of the algorithm’s operation on real eddy-current data are given.Для обеспечения безопасности движения на железнодорожном транспорте регулярно проводится неразрушающий контроль рельсов с применением различных подходов и методов, включая методы вихретоковой дефектоскопии. Актуальной задачей является автоматический анализ больших массивов данных (дефектограмм), которые поступают от соответствующего оборудования. Под анализом понимается процесс определения по дефектограммам наличия дефектных участков наряду с выявлением конструктивных элементов рельсового пути. Данная статья продолжает цикл работ, посвященных задаче автоматического распознавания образов дефектов и конструктивных элементов железнодорожных рельсов по вихретоковым дефектограммам. При формировании этих образов принимаются в расчет только полезные сигналы, пороговые уровни амплитуд которых определяются автоматически по вихретоковым данным. Применяемый ранее алгоритм нахождения пороговых уровней был ориентирован на ситуации, при которых подавляющее большинство поступающих от дефектоскопа сигналов составляет рельсовый шум. Сигнал считается полезным и подлежит дальнейшему анализу, если его амплитуда в два раза превосходит соответствующий пороговый уровень шума. Статья посвящена задаче корректировки пороговых уровней с учётом необходимости выявления протяжённых поверхностных дефектов рельсов. Предлагается алгоритм нахождения значений пороговых уровней амплитуд рельсового шума с их последующей корректировкой в случае наличия большого количество полезных сигналов от протяженных дефектов. Приводятся примеры работы алгоритма на реальных вихретоковых данных
Подход к автонастройке параллельных программ методом проверки моделей
Get PDFThe paper presents a new approach to autotuning data-parallel programs. Autotuning is a search for optimal program settings which maximize its performance. The novelty of the approach lies in the use of the model checking method to find the optimal tuning parameters by the method of counterexamples. In our work, we abstract from specific programs and specific processors by defining their representative abstract patterns. Our method of counterexamples implements the following four steps. At the first step, an execution model of an abstract program on an abstract processor is described in the language of a model checking tool. At the second step, in the language of the model checking tool, we formulate the optimality property that depends on the constructed model. At the third step, we find the optimal values of the tuning parameters by using a counterexample constructed during the verification of the optimality property. In the fourth step, we extract the information about the tuning parameters from the counter-example for the optimal parameters. We apply this approach to autotuning parallel programs written in OpenCL, a popular modern language that extends the C language for programming both standard multi-core processors (CPUs) and massively parallel graphics processing units (GPUs). As a verification tool, we use the SPIN verifier and its model representation language Promela, whose formal semantics is good for modelling the execution of parallel programs on processors with different architectures.В этой статье представлен новый подход к автонастройке программ, параллельных по данным. Автонастройка -- это поиск оптимальных параметров настройки программы, при которых её производительность оказывается максимальной. Новизна подхода состоит в использовании метода проверки моделей для поиска оптимальных параметров настройки методом контрпримеров. В нашей работе мы абстрагируемся от конкретных программ и конкретных процессоров, задавая их представительные абстрактные шаблоны. Наш метод контрпримеров состоит в реализации следующих четырёх шагов. На первом шаге на языке инструмента проверки моделей задаётся модель исполнения абстрактной программы на абстрактном процессоре. На втором шаге на языке инструмента проверки моделей формулируем свойство оптимальности, зависящее от построенной модели. На третьем шаге подбираем оптимальные значения параметров настройки посредством использования контрпримеров, построенных в ходе верификации свойства оптимальности. На четвёртом шаге извлекаем информацию о параметрах настройки из контрпримера для оптимальных параметров. Мы применяем этот подход к автонастройке параллельных программ, написанных на языке OpenCL -- современном популярном языке, который расширяет язык C для программирования как обычных многоядерных процессоров (CPU), так и массивно-параллельных графических процессоров (GPU). В качестве инструмента верификации мы используем верификатор SPIN и его язык представления моделей Promela, формальная семантика которого позволяет моделировать исполнение параллельных программ на процессорах с различной архитектурой
Сравнение стилистических характеристик для верификации авторов художественных текстов
Get PDFThe article compares character-level, word-level, and rhythm features for the authorship verification of literary texts of the 19th-21st centuries. Text corpora contains fragments of novels, each fragment has a size of about 50 000 characters. There are 40 fragments for each author. 20 authors who wrote in English, Russian, French, and 8 Spanish-language authors are considered.The authors of this paper use existing algorithms for calculation of low-level features, popular in the computer linguistics, and rhythm features, common for the literary texts. Low-level features include n-grams of words, frequencies of letters and punctuation marks, average word and sentence lengths, etc. Rhythm features are based on lexico-grammatical figures: anaphora, epiphora, symploce, aposiopesis, epanalepsis, anadiplosis, diacope, epizeuxis, chiasmus, polysyndeton, repetitive exclamatory and interrogative sentences. These features include the frequency of occurrence of particular rhythm figures per 100 sentences, the number of unique words in the aspects of rhythm, the percentage of nouns, adjectives, adverbs and verbs in the aspects of rhythm. Authorship verification is considered as a binary classification problem: whether the text belongs to a particular author or not. AdaBoost and a neural network with an LSTM layer are considered as classification algorithms. The experiments demonstrate the effectiveness of rhythm features in verification of particular authors, and superiority of feature types combinations over single feature types on average. The best value for precision, recall, and F-measure for the AdaBoost classifier exceeds 90% when all three types of features are combined.В статье сравниваются характеристики уровней символов, слов и ритма для верификации авторства художественных текстов 19-21-го веков. Корпуса текстов содержат фрагменты романов, каждый фрагмент имеет размер около 50 000 знаков. Для каждого автора приводится 40 фрагментов. Рассматриваются по 20 авторов, писавших на английском, русском, французском языках, и 8 испаноязычных авторов.Авторы статьи используют существующие алгоритмы для вычисления популярных в современной компьютерной лингвистике низкоуровневых характеристик и распространённых в художественной литературе ритмических характеристик. Низкоуровневые характеристики включают в себя n-граммы слов, частоты встречаемости букв и знаков пунктуации, среднюю длину слова и предложения и т. д. Ритмические характеристики основаны на лексико-грамматических средствах: анафоре, эпифоре, симплоке, апозиопезе, эпаналепсисе, анадиплозисе, диакопе, эпизевксисе, хиазме, многосоюзие, повторяющихся восклицательных и вопросительных предложениях. Данные характеристики включают в себя частоты появления отдельных ритмических средств на 100 предложений, количество уникальных слов в аспектах ритма, доли существительных, прилагательных, наречий и глаголов в аспектах ритма. Верификация авторов рассматривается как задача бинарной классификации: принадлежит текст конкретному автору или нет. В качестве алгоритмов классификации рассматриваются AdaBoost и нейросеть со слоем LSTM. Эксперименты демонстрируют эффективность ритмических характеристик при верификации конкретных авторов и превосходство комбинаций типов характеристик над отдельными типами характеристик в среднем. Лучшее значение точности, полноты и F-меры для классификатора AdaBoost превышает 90%, когда комбинируются все три типа характеристик
Онлайн тестирование динамических реконфигураций по отношению к политикам адаптации
Get PDFSelf-adaptation of complex systems is a very active domain of research with numerous application domains. Component systems are designed as sets of components that may reconfigure themselves according to adaptation policies, which describe needs for reconfiguration. In this context, an adaptation policy is designed as a set of rules that indicate, for a given set of configurations, which reconfiguration operations can be triggered, with fuzzy values representing their utility. The adaptation policy has to be faithfully implemented by the system, especially w.r.t. the utility occurring in the rules, which are generally specified for optimizing some extra-functional properties (e.g. minimizing resource consumption). In order to validate adaptive systems’ behaviour, this paper presents a model-based testing approach, which aims to generate large test suites in order to measure the occurrences of reconfigurations and compare them to their utility values specified in the adaptation rules. This process is based on a usage model of the system used to stimulate the system and provoke reconfigurations. As the system may reconfigure dynamically, this online test generator observes the system responses and evolution in order to decide the next appropriate test step to perform. As a result, the relative frequencies of the reconfigurations can be measured in order to determine whether the adaptation policy is faithfully implemented. To illustrate the approach the paper reports on experiments on the case study of platoons of autonomous vehicles.Самоадаптация сложных систем является активной областью теоретических и прикладных исследований, имеющей чрезвычайно широкий спектр применения. Компонентно-ориентированные адаптивные системы разрабатываются на базе компонент, которые могут перенастроиться в соответствии с политиками адаптации, описывающими потребности в реконфигурировании. В этом контексте политика адаптации представляет собой набор правил, которые указывают для данного множества конфигураций, какие операции реконфигурирования могут быть инициированы, при этом их полезность представлена нечеткими значениями. Правила обычно разрабатываются для оптимизации некоторых нефункциональных свойств, например, минимизации потребления ресурсов, поэтому реализация системы с политиками адаптации должна быть точной, особенно по отношению к описанной в правилах полезности реконфигурирования. С целью валидации поведения адаптивных систем в этой статье представлен модельно-ориентированный подход к тестированию, который направлен на создание больших наборов тестов для оценки случаев реконфигурирования и сравнения частоты этих случаев со значениями полезности, описанными в правилах адаптации. Этот процесс основан на модели использования системы в ее среде, для стимулирования ее реконфигурирований. Поскольку система может динамически изменять свою архитектуру, этот генератор тестов наблюдает за откликами системы на события и ее изменениями в режиме онлайн, чтобы решить каким будет следующий подходящий шаг теста. В результате относительные частоты реконфигурирований могут быть измерены, чтобы определить, правильно ли реализована политика адаптации. Чтобы проиллюстрировать предложенный подход, статья описывает эксперименты по моделированию поведения колонн автономных машин
Математическая модель параллельных программ и основанный на ней подход к верификации MPI-программ
Get PDFThe paper presents a new mathematical model of parallel programs, on the basis of which it is possible, in particular, to verify parallel programs presented on a certain subset of the parallel programming interface MPI. This model is based on the concepts of a sequential and distributed process. A parallel program is modeled as a distributed process in which sequential processes communicate by asynchronously sending and receiving messages over channels. The main advantage of the described model is the ability to simulate and verify parallel programs that generate an indefinite number of sequential processes. The proposed model is illustrated by the application of verification of the matrix multiplication MPI program.В работе излагается новая математическая модель параллельных программ, на базе которой можно в частности верифицировать параллельные программы, представленные на некотором подмножестве программного интерфейса параллельного программирования MPI. Данная модель основана на понятиях последовательного и распределенного процесса. Параллельная программа моделируется распределенным процессом, в котором последовательные процессы взаимодействуют путем асинхронной передачи и приема сообщений через каналы. Главным преимуществом изложенной модели является возможность моделирования и верификации параллельных программ, порождающих неопределенное число последовательных процессов. Изложенная модель проиллюстрирована применением к верификации MPI программы перемножения матриц
На пути к автоматической дедуктивной верификации C-программ с Sisal-циклами в системе C-lightVer
Get PDFThe C-lightVer system is developed in IIS SB RAS for C-program deductive verification. C-kernel is an intermediate verification language in this system. Cloud parallel programming system (CPPS) is also developed in IIS SB RAS. Cloud Sisal is an input language of CPPS. The main feature of CPPS is implicit parallel execution based on automatic parallelization of Cloud Sisal loops. Cloud-Sisal-kernel is an intermediate verification language in the CPPS system. Our goal is automatic parallelization of such a superset of C that allows implementing automatic verification. Our solution is such a superset of C-kernel as C-Sisal-kernel. The first result presented in this paper is an extension of C-kernel by Cloud-Sisal-kernel loops. We have obtained the C-Sisal-kernel language. The second result is an extension of C-kernel axiomatic semantics by inference rule for Cloud-Sisal-kernel loops. The paper also presents our approach to the problem of deductive verification automation in the case of finite iterations over data structures. This kind of loops is referred to as definite iterations. Our solution is a composition of symbolic method of verification of definite iterations, verification condition metageneration and mixed axiomatic semantics method. Symbolic method of verification of definite iterations allows defining inference rules for these loops without invariants. Symbolic replacement of definite iterations by recursive functions is the base of this method. Obtained verification conditions with applications of recursive functions correspond to logical base of ACL2 prover. We use ACL2 system based on computable recursive functions. Verification condition metageneration allows simplifying implementation of new inference rules in a verification system. The use of mixed axiomatic semantics results to simpler verification conditions in some cases.В Институте систем информатики СО РАН разрабатывается система C-lightVer для дедуктивной верификации C-программ. C-kernel является промежуточным языком верификации в данной системе. Система облачного параллельного программирования (CPPS) также разрабатывается в Институте систем информатики СО РАН. Cloud Sisal является входным языком системы CPPS. Главной особенностью системы CPPS является неявное параллельное исполнение, основанное на автоматическом распараллеливании циклов Cloud Sisal. Cloud-Sisal-kernel является промежуточным языком верификации в системе CPPS. Нашей целью является автоматическое распараллеливание такого надмножества языка C, которое позволяет реализовать автоматическую верификацию. Нашим решением является такое надмножество языка C-kernel, как язык C-Sisal-kernel. Первым результатом, представленным в данной статье, является расширение языка C-kernel циклами языка Cloud-Sisal-kernel. В результате был разработан язык C-Sisal-kernel. Вторым результатом, представленным в данной статье, является расширение аксиоматической семантики языка C-kernel правилом вывода для циклов языка Cloud-Sisal-kernel. В данной статье также представлен наш подход к проблеме автоматизации дедуктивной верификации в случае финитных итераций над структурами данных. Такие циклы называются финитными итерациями. Нашим решением является композиция символического метода верификации финитных итераций, метагенерации условий корректности и смешанной аксиоматической семантики. Символический метод верификации финитных итераций позволяет задавать правила вывода для таких циклов без инвариантов. Символическая замена финитных итераций рекурсивными функциями является основой данного метода. Полученные условия корректности с применениями рекурсивных функций соответствуют логической основе системы доказательства ACL2. Мы используем систему ACL2, основанную на вычислимых рекурсивных функциях. Метагенерация условий корректности позволяет упростить реализацию новых правил вывода в системе верификации. Использование смешанной аксиоматической семантики приводит в некоторых случаях к более простым условиям корректности
Алгоритм нахождения обратной связи в задаче с ограничениями для одного класса нелинейных управляемых систем
Get PDFFor a continuous nonlinear control system on a finite time interval with control constraints, where the right-hand side of the dynamics equations is linear in control and linearizable in the vicinity of the zero equilibrium position, we consider the construction of a feedback according to the Kalman algorithm. For this, the solution of an auxiliary optimal control problem with a quadratic functional is used by analogy with the SDRE approach.Since this approach is used in the literature to find suboptimal synthesis in optimal control problems with a quadratic functional with formally linear systems, where all coefficient matrices in differential equations and criteria can contain state variables, then on a finite time interval it becomes necessary to solve a complicated matrix differential Riccati equations, with state-dependent coefficient matrices. This circumstance, due to the nonlinearity of the system, in comparison with the Kalman algorithm for linear-quadratic problems, significantly increases the number of calculations for obtaining the coefficients of the gain matrix in the feedback and for obtaining synthesis with a given accuracy. The proposed synthesis construction algorithm is constructed using the extension principle proposed by V. F. Krotov and developed by V. I. Gurman and allows not only to expand the scope of the SDRE approach to nonlinear control problems with control constraints in the form of closed inequalities, but also to propose a more efficient computational algorithm for finding the matrix of feedback gains in control problems on a finite interval. The article establishes the correctness of the application of the extension principle by introducing analogs of the Lagrange multipliers, depending on the state and time, and also derives a formula for the suboptimal value of the quality criterion. The presented theoretical results are illustrated by calculating suboptimal feedbacks in the problems of managing three-sector economic systems.Для непрерывной нелинейной управляемой системы на конечном интервале времени с ограничениями на управление, где правая часть уравнений динамики линейна по управлению и линеаризуема в окрестности нулевого положения равновесия рассматривается построение обратной связи по схеме алгоритма Калмана. Для этого используется решение вспомогательной задачи оптимального управления c квадратичным функционалом по аналогии с подходом SDRE.Так как этот подход в литературе применяется для нахождения субоптимального синтеза в задачах оптимального управления с квадратичным функционалом с формально линейными системами, где все матрицы коэффициентов в дифференциальных уравнениях и в критерии могут содержать переменные состояния, то на конечном интервале времени здесь появляется необходимость решения усложненного матричного дифференциального уравнения Риккати, с матрицами коэффициентов зависящими от состояния. Это обстоятельство вследствие нелинейности системы, по сравнению с алгоритмом Калмана для линейно-квадратичных задач, значительно увеличивает количество вычислений для получения коэффициентов матрицы коэффициентов усиления в обратной связи и для получения синтеза с заданной точностью. Предложенный в работе алгоритм построения синтеза строится с помощью принципа расширения, предложенного В. Ф. Кротовым и развитого В. И. Гурманом, и позволяет не только расширить сферу использования подхода SDRE на нелинейные задачи управления с ограничениями на управление в виде замкнутых неравенств, но и предложить более эффективный вычислительный алгоритм нахождения матрицы коэффициентов усиления обратной связи в задачах управления на конечном интервале. В работе устанавливается корректность применения принципа расширения с помощью введения аналогов множителей Лагранжа, зависящих от состояния и времени, а также выводится формула субоптимального значения критерия качества. Приведенные теоретические результаты иллюстрируются на расчетах субоптимальных обратных связей в задачах управления трехсекторными экономическими системами