Reachability types: tracking aliasing and separation in higher-order functional programs

Ownership type systems, based on the idea of enforcing unique access paths, have been primarily focused on objects and top-level classes. However, existing models do not as readily reflect the finer aspects of nested lexical scopes, capturing, or escaping closures in higher-order functional programming patterns, which are increasingly adopted even in mainstream object-oriented languages. We present a new type system, λ * , which enables expressive ownership-style reasoning across higher-order functions. It tracks sharing and separation through reachability sets, and layers additional mechanisms for selectively enforcing uniqueness on top of it. Based on reachability sets, we extend the type system with an expressive flow-sensitive effect system, which enables flavors of move semantics and ownership transfer. In addition, we present several case studies and extensions, including applications to capabilities for algebraic effects, one-shot continuations, and safe parallelization.

Stability Analysis of Semi-active Suspension Systems Using a Data-driven Approach

The modern vehicles are getting equipped with more and more sensors, which allows the engineers to collect more information about the states of the vehicle and its environment during its operation. This information can be used to increase the capacity and the performances of the control systems. In this paper, a novel data-driven approach is presented to compute the reachability sets of the vehicles, which are equipped with a semi-active suspension system. The dataset, which is used in this paper, is provided by the high fidelity vehicle simulation software, CarSim. Firstly, the dataset is categorized using a stability criterion. Then, a machine-learning algorithm (C4.5 decision tree) is trained, which can categorize a given instance using only the onboard signals of the vehicle. Finally, a possible application of the reachability sets is presented to show the use of the computed sets.

ALGORITHM FOR CONSTRUCTING A REACHABILITY TREE FOR STOCHASTIC PETRI NETS

Описываются основные определения дерева достижимости сетей Петри. Также рассматриваются различные примеры стохастических сетей Петри, в которых после выставления начальных маркировок в первых позициях определяются значения во всех остальных позициях. Показаны примеры определения маркировок при помощи высчитывания вектора диагональной свертки. Для каждого примера стохастической сети Петри проводится анализ данной сети. Данный анализ необходим для различных распределительных систем и процессов, особенно на заключительном этапе. Основными методами анализа являются дерево достижимости и матричные уравнения. Рассматривается один из таких методов анализа сетей Петри. С использованием дерева достижимости можно проанализировать, выявить и исправить сбои в процессах, которые могут произойти при наличии тупиковых состояний и при неправильной последовательности срабатывания переходов. Исходя из рассмотренных примеров предлагается обобщенный алгоритм построения дерева достижимости для стохастических сетей Петри. Предложенный алгоритм построения дерева достижимости стохастических сетей Петри можно применять для всех сетей как с конечным, так и с бесконечным множеством достижимости. Данный алгоритм будет являться полезным инструментом при анализе стохастических сетей Петри The article describes the basic definitions of the reachability tree of Petri nets. It also considers various examples of stochastic Petri nets, in which, after setting the initial markings in the first positions, the values in all other positions are determined. The work shows examples of determining markings by calculating the vector of the diagonal convolution. Each example of a stochastic Petri net is analyzed. This analysis is necessary for various distribution systems and processes, especially in the final stage. The main analysis methods are reachability tree and matrix equations. I consider one of such methods for analyzing Petri nets. Using the reachability tree, you can analyze, identify, and correct process failures that can occur when there are deadlocks and when transitions are fired incorrectly. Based on the examples considered, I propose a generalized algorithm for constructing a reachability tree for stochastic Petri nets. The proposed algorithm for constructing the reachability tree of stochastic Petri nets can be applied to all nets with both finite and infinite reachability sets. This algorithm will be a useful tool for analyzing stochastic Petri nets

Optimizing Reachability Sets in Temporal Graphs by Delaying

A temporal graph is a dynamic graph where every edge is assigned a set of integer time labels that indicate at which discrete time step the edge is available. In this paper, we study how changes of the time labels, corresponding to delays on the availability of the edges, affect the reachability sets from given sources. The questions about reachability sets are motivated by numerous applications of temporal graphs in network epidemiology and scheduling problems in supply networks in manufacturing. We introduce control mechanisms for reachability sets that are based on two natural operations of delaying time events. The first operation, termed merging, is global and batches together consecutive time labels in the whole network simultaneously. This corresponds to postponing all events until a particular time. The second, imposes independent delays on the time labels of every edge of the graph. We provide a thorough investigation of the computational complexity of different objectives related to reachability sets when these operations are used. For the merging operation, we prove NP-hardness results for several minimization and maximization reachability objectives, even for very simple graph structures. For the second operation, we prove that the minimization problems are NP-hard when the number of allowed delays is bounded. We complement this with a polynomial-time algorithm for the case of unbounded delays.

External Estimators of the Reachability Set of Nonlinear Discrete Systems

On the one hand, nonlinear discrete systems are natural generalization of linear discrete systems. On the other hand, various economic and, especially, technical systems have, basically, a nonlinear nature. Therefore, research of mathematical models of these systems is a relevant issue for implementing various procedures of systems analysis and decision making. Clusters of trajectories of the considered systems can be generated both by the parameters interpreted as control circuits, and by the parameters interpreted as perturbations. Quite general results of reachability sets estimation of nonlinear discrete systems, including a number of well-known achievements in this field as a consequence, are offered. As specification of these approaches, quadratic estimators of the reachability set of nonlinear discrete systems are received.