Unbounded Petri nets (UPNs) can describe and analyze discrete event systems with infinite states (DESIS). Due to the infinite state space and the combination explosion problem, the reachability ...analysis of UPNs is an NP-Hard problem. The existing reachability analysis methods cannot achieve an accurate result at reasonable costs (computational time and space) due to the finite reachability tree with <inline-formula> <tex-math notation="LaTeX">\omega</tex-math> </inline-formula>-numbers. Based on the idea of approximating infinite space with finite states, given some limited reachable markings of a UPN, we propose a method that can quantitatively solve the UPN's reachability problem with machine learning. Firstly, we define the probabilistic reachability of markings and transform the UPN's reachability problem into the prediction problem of markings. The proposed method based on positive and unlabeled learning (PUL) and bagging trains a classifier to predict the probabilistic reachability of unknown markings. Finally, to predict the markings outside the positive sample set and unlabeled sample set, an iterative strategy is designed to update the classifier. Based on seven general UPNs, the results of the experiments show that the proposed method has a good performance in the accuracy and time consumption for the UPN's reachability problem. Note to Practitioners -In discrete event systems, the reachability problem mainly studies reachable states of the system and the relationship between states, which is the basis of the system's states, behaviors, attributes and performance analysis. For discrete event systems with infinite states, it is hard to analyze the reachable relationship between states within a finite time due to the infinite state space and the combination explosion problem. The main motivation of the paper is to propose a method that can predict the reachable relationship between the states with a probability value within a finite time. By machine learning algorithms, the method learns the feature information of the known reachable states. The reachability of unknown states in the infinite state space can be predicted approximately. The proposed approximation method can be applied to analyze the reachability properties of general discrete event systems with infinite states, such as checking whether a fault occurs in operating systems, whether a message is delivered in communication and so on.
Backward reachability analysis is essential to synthesizing controllers that ensure the correctness of closed-loop systems. This paper is concerned with developing scalable algorithms that ...under-approximate the backward reachable sets, for discrete-time uncertain linear and nonlinear systems. Our algorithm sequentially linearizes the dynamics, and uses constrained zonotopes for set representation and computation. The main technical ingredient of our algorithm is an efficient way to under-approximate the Minkowski difference between a constrained zonotopic minuend and a zonotopic subtrahend, which consists of all possible values of the uncertainties and the linearization error. This Minkowski difference needs to be represented as a constrained zonotope to enable subsequent computation, but, as we show, it is impossible to find a polynomial-size representation for it in polynomial time. Our algorithm finds a polynomial-size under-approximation in polynomial time. We further analyze the conservatism of this under-approximation technique, and show that it is exact under some conditions. Based on the developed Minkowski difference technique, we detail two backward reachable set computation algorithms to control the linearization error and incorporate nonconvex state constraints. Several examples illustrate the effectiveness of our algorithms.
We study the synthesis of a policy in a Markov decision process (MDP) following which an agent reaches a target state in the MDP while minimizing its total discounted cost. The problem combines a ...reachability criterion with a discounted cost criterion and naturally expresses the completion of a task with probabilistic guarantees and optimal transient performance. We first establish that an optimal policy for the considered formulation may not exist but that there always exists a near-optimal stationary policy. We additionally provide a necessary and sufficient condition for the existence of an optimal policy. We then restrict our attention to stationary deterministic policies and show that the decision problem associated with the synthesis of an optimal stationary deterministic policy is NP-complete. Finally, we provide an exact algorithm based on mixed-integer linear programming and propose an efficient approximation algorithm based on linear programming for the synthesis of an optimal stationary deterministic policy.
Autonomous coverage of a specified area by robots operating in close proximity with each other has many potential applications such as real-time monitoring of rapidly changing environments, and ...search and rescue; however, coordination and safety are two fundamental challenges. For coordination, we propose a distributed controller for covering moving, compact domains which consists in a double integrator with bounded input forces. This control policy is based on artificial potentials and alignment forces designed to promote desired vehicle-domain and intervehicle separations and relative velocities. We prove that certain coverage configurations are locally asymptotically stable. For safety, we establish energy conditions for collision-free motion and utilize Hamilton-Jacobi (HJ) reachability theory for last-resort pairwise collision avoidance. We derive an analytical solution to the associated HJ partial differential equation corresponding to the collision avoidance problem between two double integrator vehicles. We demonstrate our approach in several numerical simulations involving vehicles covering convex and nonconvex moving domains.
Object-sensitive pointer analysis (denoted k obj under <inline-formula><tex-math notation="LaTeX">k</tex-math> <mml:math><mml:mi>k</mml:mi></mml:math><inline-graphic ...xlink:href="he-ieq1-3162236.gif"/> </inline-formula>-limiting) for an object-oriented program can be accelerated if context-sensitivity can be selectively applied to only some precision-critical variables/objects in a program. Existing pre-analyses for making such selections, which are performed as whole-program analyses to a program, are developed based on two broad approaches. One approach preserves the precision of object-sensitive pointer analysis but achieves limited speedups by reasoning about all the possible value flows in the program conservatively, while the other approach achieves greater speedups but sacrifices precision (often unduly) by examining only some but not all the value flows in the program heuristically. In this paper, we introduce a new pre-analysis approach, Turner <inline-formula><tex-math notation="LaTeX">^{\mathcal{m}}</tex-math> <mml:math><mml:msup><mml:mrow/><mml:mi mathvariant="script">m</mml:mi></mml:msup></mml:math><inline-graphic xlink:href="he-ieq2-3162236.gif"/> </inline-formula> (where <inline-formula><tex-math notation="LaTeX">\mathcal {m}</tex-math> <mml:math><mml:mi mathvariant="script">m</mml:mi></mml:math><inline-graphic xlink:href="he-ieq3-3162236.gif"/> </inline-formula> stands for modularity), that represents a sweet spot between these two existing ones, as it is designed to enable k obj to run significantly faster than the former approach and achieve significantly better precision than the latter approach. Turner <inline-formula><tex-math notation="LaTeX">^{\mathcal{m}}</tex-math> <mml:math><mml:msup><mml:mrow/><mml:mi mathvariant="script">m</mml:mi></mml:msup></mml:math><inline-graphic xlink:href="he-ieq4-3162236.gif"/> </inline-formula> is simple, lightweight yet effective due to two novel aspects in its design. First, we exploit a key observation that some precision-uncritical objects in the program can be approximated based on the object-containment relationship pre-established (from Andersen's analysis). In practice, this approximation introduces only a small degree of imprecision into k obj . Second, leveraging this initial approximation, we apply a novel object reachability analysis to the program by pre-analyzing its methods according to a reverse topological order of its call graph. When pre-analyzing each method, we make use of a simple DFA (Deterministic Finite Automaton) to reason about object reachability intra-procedurally from its entry to its exit along all the possible value flows established by its statements to identify its precision-critical variables/objects. In practice, this new modular object reachability analysis, which runs linearly in terms of the number of statements in the program, introduces again only a small loss of precision into k obj . We have validated Turner <inline-formula><tex-math notation="LaTeX">^{\mathcal{m}}</tex-math> <mml:math><mml:msup><mml:mrow/><mml:mi mathvariant="script">m</mml:mi></mml:msup></mml:math><inline-graphic xlink:href="he-ieq5-3162236.gif"/> </inline-formula> with an open-source implementation in Soot (already publicly available) against the state of the art by using a set of 12 widely used Java benchmarks and applications.
In this paper, the set reachability and observability of probabilistic Boolean networks (PBNs) are investigated. Using a parallel extension technique, we proved that the observability problem of a ...PBN can be recast as a set reachability problem of an interconnected PBN. For set reachability analysis, we designed a random logic dynamical system (RLDS) from the PBN under consideration by reconstructing the state transfer graph (STG). We proved that, for a PBN, a target subset is reachable from an initial subset if and only if all solutions to the corresponding RLDS starting from the initial subset converge to the zero state. Based on the STG reconstruction technique and using the largest invariant subset algorithm, the necessary and sufficient conditions for finite-time set reachability with probability one and asymptotical set reachability in distribution were obtained. All the results are expressed in terms of the transition probability matrix between non-zero states of the RLDS. Further, the results related to set reachability were applied to the observability problem of PBNs. The necessary and sufficient conditions for finite-time observability with probability one and asymptotical observability in distribution were obtained. Finally, examples were presented to illustrate the effectiveness of the proposed method.
In this work, we develop a time-optimal path planning algorithm for a mobile robot constrained by a minimum turning radius in an environment cluttered with an arbitrary number of moving and deforming ...obstacles. The algorithm builds on our previous work and involves substantial extensions to handle the turning radius constraint by adding the heading angle of the robot to the state space in addition to its location in a 2-D plane. The developed planner involves two stages: 1) forward propagation of the reachable set in the state space to preset destination through a newly derived variational inequality (VI) which encodes the obstacle avoidance and 2) backtracking to obtain the waypoints of the optimal path (corresponding to optimal control of the turning rate and speed), solved through an ODE-based scheme or a new and more robust backward-set-based scheme. The planned path represents a rigorous global optimal solution (except numerical errors) to the problem that can be used as a benchmark for other simplified planners or implemented together with a receding horizon for path planning with limited perception ability. We demonstrate both applications in several test cases.
The main objective of the present article is to employ the ψ-Hilfer pseudo-fractional derivative (HPFD) to examine the reachability criteria for fractional dynamical systems with mixed delays in ...control of order ϑ∈(0,1) and type ϱ∈0,1. we derived the sufficient and necessary conditions for the reachability criterion of fractional linear dynamical systems by utilizing the positiveness of Grammian matrices, which are defined by the Mittag-Leffler functions. The sufficient conditions for the reachability criteria of fractional nonlinear dynamical systems are obtained by using Banach’s fixed point theorem. To help grasp the theoretical results, only a limited number of numerical examples are provided.
•To examine the reachability of dynamical systems with mixed delays in control.•To describe the dynamics of systems with mixed delays in control using ψ-HPFD.•To get necessary and sufficient conditions for the reachability of linear systems.•To derive sufficient conditions for the reachability of nonlinear systems.
PDF
