Cost Problems for Parametric Time Petri Nets*

We investigate the problem of parameter synthesis for time Petri nets with a cost variable that evolves both continuously with time, and discretely when firing transitions. More precisely, parameters are rational symbolic constants used for time constraints on the firing of transitions and we want to synthesise all their values such that some marking is reachable, with a cost that is either minimal or simply less than a given bound. We first prove that the mere existence of values for the parameters such that the latter property holds is undecidable. We nonetheless provide symbolic semi-algorithms for the two synthesis problems and we prove them both sound and complete when they terminate. We also show how to modify them for the case when parameter values are integers. Finally, we prove that these modified versions terminate if parameters are bounded. While this is to be expected since there are now only a finite number of possible parameter values, our algorithms are symbolic and thus avoid an explicit enumeration of all those values. Furthermore, the results are symbolic constraints representing finite unions of convex polyhedra that are easily amenable to further analysis through linear programming. We finally report on the implementation of the approach in Romeo, a software tool for the analysis of time Petri nets.

Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems

Semi-algebraic abstraction is an approach to the safety verification problem for polynomial dynamical systems where the state space is partitioned according to the sign of a set of polynomials. Similarly to predicate abstraction for discrete systems, the number of abstract states is exponential in the number of polynomials. Hence, semi-algebraic abstraction is expensive to explicitly compute and then analyze (e.g., to prove a safety property or extract invariants).In this paper, we propose an implicit encoding of the semi-algebraic abstraction, which avoids the explicit enumeration of the abstract states: the safety verification problem for dynamical systems is reduced to a corresponding problem for infinite-state transition systems, allowing us to reuse existing model-checking tools based on Satisfiability Modulo Theory (SMT). The main challenge we solve is to express the semi-algebraic abstraction as a first-order logic formula that is linear in the number of predicates, instead of exponential, thus letting the model checker lazily explore the exponential number of abstract states with symbolic techniques. We implemented the approach and validated experimentally its potential to prove safety for polynomial dynamical systems.

Gradient-Based Optimization for Bayesian Preference Elicitation

Effective techniques for eliciting user preferences have taken on added importance as recommender systems (RSs) become increasingly interactive and conversational. A common and conceptually appealing Bayesian criterion for selecting queries is expected value of information (EVOI). Unfortunately, it is computationally prohibitive to construct queries with maximum EVOI in RSs with large item spaces. We tackle this issue by introducing a continuous formulation of EVOI as a differentiable network that can be optimized using gradient methods available in modern machine learning computational frameworks (e.g., TensorFlow, PyTorch). We exploit this to develop a novel Monte Carlo method for EVOI optimization, which is much more scalable for large item spaces than methods requiring explicit enumeration of items. While we emphasize the use of this approach for pairwise (or k-wise) comparisons of items, we also demonstrate how our method can be adapted to queries involving subsets of item attributes or “partial items,” which are often more cognitively manageable for users. Experiments show that our gradient-based EVOI technique achieves state-of-the-art performance across several domains while scaling to large item spaces.

An Exact Enumeration Method to Find d-MPs in Multistate Networks

The enumeration approaches are important topics in network reliability calculation. For general purposes, the explicit enumeration (EE) is the popular method to apply. However, the low-cost feature of EE sacrifices its efficiency. A great improvement of EE is the invention of fast enumeration (FE), which creates a low-cost way of general purpose enumeration method with very good efficiency for applications. But for the enumeration in network reliability calculation, the optimal number of enumerations can be shown to be [Formula: see text], where [Formula: see text] is the number of minimal paths and [Formula: see text] is the demand of flow. FE still has the complexity far greater than the optimal one. This paper proposes an exact enumeration method for network reliability calculation, which has the complexity no greater than [Formula: see text]. This method greatly improves the enumeration efficiency than FE. So, it is believed to be very valuable to the large real-life applications. Benchmarks are made to show the efficiency of the proposed method.

Bayesian Active Edge Evaluation on Expensive Graphs

We consider the problem of real-time motion planning that requires evaluating a minimal number of edges on a graph to quickly discover collision-free paths. Evaluating edges is expensive, both for robots with complex geometries like robot arms, and for robots sensing the world online like UAVs. Until now, this challenge has been addressed via laziness, i.e. deferring edge evaluation until absolutely necessary, with the hope that edges turn out to be valid. However, all edges are not alike in value - some have a lot of potentially good paths flowing through them, and some others encode the likelihood of neighbouring edges being valid. This leads to our key insight - instead of passive laziness, we can actively choose edges that reduce the uncertainty about the validity of paths. We show that this is equivalent to the Bayesian active learning paradigm of decision region determination (DRD). However, the DRD problem is not only combinatorially hard but also requires explicit enumeration of all possible worlds. We propose a novel framework that combines two DRD algorithms, DIRECT and BISECT, to overcome both issues. We show that our approach outperforms several state-of-the-art algorithms on a spectrum of planning problems for mobile robots, manipulators and autonomous helicopters.

A Merge Search Approach to Find Minimal Path Vectors in Multistate Networks

A new approach namely merge search (MS) is proposed to search for minimal path vectors (MPV) in multistate networks (MSN). Also, a new advance in solving integer programming problems namely fast enumeration (FE) is integrated in this approach. Such an integrated approach can greatly improve the time efficiency of searching for MPV in MSN. Traditionally, searching for MPV in MSN involves three steps: (a) enumerate all feasible flow vectors; (b) transform these vectors to corresponding state vectors; (c) filter out MPV from these state vectors. Steps (a) and (c) are bottlenecks. Explicit enumeration is usually engaged in solving Step (a), and pairwise comparison is usually employed in solving Step (c). The integrated approach uses FE to solve Step (a), and MS to solve Step (c) instead. Some numerical examples are explored to show the superior time efficiency of the proposed approach. The results show that the proposed new approach is valuable in solving the search of MPV in MSN.

Construction and Enumeration of Circuits Capable of Guiding a Miniature Vehicle

In contrast to traditional toy tracks, a patented system allows the creation of a large number of tracks with a minimal number of pieces, and whose loops always close properly. These circuits strongly resemble traditional self-avoiding polygons (whose explicit enumeration has not yet been resolved for an arbitrary number of squares) yet there are numerous differences, notably the fact that the geometric constraints are different than those of self-avoiding polygons. We present the methodology allowing the construction and enumeration of all of the possible tracks containing a given number of pieces. For small numbers of pieces, the exact enumeration will be treated. For greater numbers of pieces, only an estimation will be offered. In the latter case, a randomly construction of circuits is also given. We will give some routes for generalizations for similar problems.

Blip-summed quantum–classical path integral with cumulative quantum memory

The quantum-classical path integral (QCPI) offers a rigorous methodology for simulating quantum mechanical processes in condensed-phase environments treated in full atomistic detail. This paper describes the implementation of QCPI on system–bath models, which are frequently employed in studying the dynamics of reactive processes. The QCPI methodology incorporates all effects associated with stimulated phonon absorption and emission as its crudest limit, thus can (in some regimes) converge faster than influence functional-based path integral methods specifically designed for system–bath Hamiltonians. It is shown that the QCPI phase arising from a harmonic bath can be summed analytically with respect to the discrete bath degrees of freedom and expressed in terms of precomputed influence functional coefficients, avoiding the explicit enumeration of forced oscillator trajectories, whose number grows exponentially with the length of quantum memory. Further, adoption of the blip decomposition (which classifies the system paths based on the time length over which their forward and backward components are not identical) and a cumulative treatment of the QCPI phase between blips allows elimination of the majority of system paths, leading to a dramatic increase in efficiency. The generalization of these acceleration techniques to anharmonic environments is discussed.