Tracking in object action space

In this paper we focus on the joint problem of tracking humans and recognizing human action in scenarios such as a kitchen scenario or a scenario where a robot cooperates with a human, e.g., for a manufacturing task. In these scenarios, the human directly interacts with objects physically by using/manipulating them or by, e.g., pointing at them such as in “Give me that…”. To recognize these types of human actions is difficult because (a) they ought to be recognized independent of scene parameters such as viewing direction and (b) the actions are parametric, where the parameters are either object-dependent or as, e.g., in the case of a pointing direction convey important information. One common way to achieve recognition is by using 3D human body tracking followed by action recognition based on the captured tracking data. For the kind of scenarios considered here we would like to argue that 3D body tracking and action recognition should be seen as an intertwined problem that is primed by the objects on which the actions are applied. In this paper, we are looking at human body tracking and action recognition from a object-driven perspective. Instead of the space of human body poses we consider the space of the object affordances, i.e., the space of possible actions that are applied on a given object. This way, 3D body tracking reduces to action tracking in the object (and context) primed parameter space of the object affordances. This reduces the high-dimensional joint-space to a low-dimensional action space. In our approach, we use parametric hidden Markov models to represent parametric movements; particle filtering is used to track in the space of action parameters. We demonstrate its effectiveness on synthetic and on real image sequences using human-upper body single arm actions that involve objects.     

State agnostic planning graphs: deterministic,non-deterministic,and probabilistic planning

Planning graphs have been shown to be a rich source of heuristic information for many kinds of planners. In many cases, planners must compute a planning graph for each element of a set of states, and the naive technique enumerates the graphs individually. This is equivalent to solving a multiple-source shortest path problem by iterating a single-source algorithm over each source.We introduce a data-structure, the state agnostic planning graph, that directly solves the multiple-source problem for the relaxation introduced by planning graphs. The technique can also be characterized as exploiting the overlap present in sets of planning graphs. For the purpose of exposition, we first present the technique in deterministic (classical) planning to capture a set of planning graphs used in forward chaining search. A more prominent application of this technique is in conformant and conditional planning (i.e., search in belief state space), where each search node utilizes a set of planning graphs; an optimization to exploit state overlap between belief states collapses the set of sets of planning graphs to a single set. We describe another extension in conformant probabilistic planning that reuses planning graph samples of probabilistic action outcomes across search nodes to otherwise curb the inherent prediction cost associated with handling probabilistic actions. Finally, we show how to extract a state agnostic relaxed plan that implicitly solves the relaxed planning problem in each of the planning graphs represented by the state agnostic planning graph and reduces each heuristic evaluation to counting the relevant actions in the state agnostic relaxed plan. Our experimental evaluation (using many existing International Planning Competition problems from classical and non-deterministic conformant tracks) quantifies each of these performance boosts, and demonstrates that heuristic belief state space progression planning using our technique is competitive with the state of the art.     

A Partial Order Approach to Branching Time Logic Model Checking

Partial order techniques enable reducing the size of the state space used for model checking, thus alleviating the “state space explosion” problem. These reductions are based on selecting a subset of the enabled operations from each program state. So far, these methods have been studied, implemented, and demonstrated for assertional languages that model the executions of a program as computation sequences, in particular the linear temporal logic. The present paper shows, for the first time, how this approach can be applied to languages that model the behavior of a program as a tree. We study here partial order reductions for branching temporal logics, e.g., the logics CTL and CTL* (with the next time operator removed) and process algebra logics such as Hennesy–Milner logic (withτactions). Conditions on the selection of subset of successors from each state during the state-space construction, which guarantee reduction that preserves CTL* properties, are given. The experimental results provided show that the reduction is substantial.     

Approximate dynamic programming with a fuzzy parameterization

Dynamic programming (DP) is a powerful paradigm for general, nonlinear optimal control. Computing exact DP solutions is in general only possible when the process states and the control actions take values in a small discrete set. In practice, it is necessary to approximate the solutions. Therefore, we propose an algorithm for approximate DP that relies on a fuzzy partition of the state space, and on a discretization of the action space. This fuzzy Q-iteration algorithm works for deterministic processes, under the discounted return criterion. We prove that fuzzy Q-iteration asymptotically converges to a solution that lies within a bound of the optimal solution. A bound on the suboptimality of the solution obtained in a finite number of iterations is also derived. Under continuity assumptions on the dynamics and on the reward function, we show that fuzzy Q-iteration is consistent, i.e., that it asymptotically obtains the optimal solution as the approximation accuracy increases. These properties hold both when the parameters of the approximator are updated in a synchronous fashion, and when they are updated asynchronously. The asynchronous algorithm is proven to converge at least as fast as the synchronous one. The performance of fuzzy Q-iteration is illustrated in a two-link manipulator control problem.     

First-order logical filtering

Logical filtering is the process of updating a belief state (set of possible world states) after a sequence of executed actions and perceived observations. In general, it is intractable in dynamic domains that include many objects and relationships. Still, potential applications for such domains (e.g., semantic web, autonomous agents, and partial-knowledge games) encourage research beyond intractability results.In this paper we present polynomial-time algorithms for filtering belief states that are encoded as First-Order Logic (FOL) formulas. Our algorithms are exact in many cases of interest. They accept belief states in FOL without functions, permitting arbitrary arity for predicates, infinite universes of elements, and equality. They enable natural representation with explicit references to unidentified objects and partially known relationships, still maintaining tractable computation. Previous results focus on more general cases that are intractable or permit only imprecise filtering. Our algorithms guarantee that belief-state representation remains compact for STRIPS actions (among others) with unbounded-size domains. This guarantees tractable exact filtering indefinitely for those domains. The rest of our results apply to expressive modeling languages, such as partial databases and belief revision in FOL.     

Using Assumptions to Distribute CTL Model Checking

In this work we discuss the problem of performing distributed CTL model checking by splitting the given state space into several “partial state spaces” . The partial state space is modelled as a Kripke structure with border states. Each computer involved in the distributed computation owns a partial state space and performs a model checking algorithm on this incomplete structure. To be able to proceed, the border states are augmented by assumptions about the truth of formulas and the computers exchange assumptions about relevant states as they compute more precise information. In the paper we give the basic definitions and present the distributed algorithm.     

Priority conflict-free Petri nets

A number of problems concerning priority conflict-free Petri nets are investigated in this paper. We show the reachability problem for such Petri nets to be NP-complete. (Using a similar technique, the NP-completeness result applies to the class of priority BPP-nets as well.) As for the boundedness problem, an NP-completeness result is demonstrated for priority conflict-free Petri nets with two types of prioritized transitions. (In contrast, the problem is known to be P-complete for conflict-free Petri nets without priorities.) We also investigate the home state problem, i.e., the problem of determining whether home states exist in a given a Petri net, for conflict-free Petri nets with and without priorities. As it turns out, home states always exist for bounded conflict-free Petri nets without priorities. If an additional liveness constraint is imposed, such Petri nets are guaranteed to be ‘reversible’ (i.e., their initial states are home states). For priority conflict-free Petri nets, being bounded and live is sufficient for the existence of home states. However, if the liveness assumption is dropped, the existence of home states is no longer guaranteed. Received: 1 April 1997 / 8 December 1997     

Descriptions of Game Actions

To describe simultaneous knowledge updates for different subgroups we propose anepistemic language with dynamic operators for actions. The language is interpreted onequivalence states (S5 states). The actions are interpreted as state transformers. Two crucial action constructors are learning and local choice. Learning isthe dynamic equivalent of common knowledge. Local choice aids in constraining theinterpretation of an action to a functional interpretation (state transformer).Bisimilarity is preserved under execution of actions. The language is applied todescribe various actions in card games.     

Optimization of rule-based systems using state space graphs

Embedded rule-based expert systems must satisfy stringent timing constraints when applied to real-time environments. The paper describes a novel approach to reduce the response time of rule-based expert systems. The optimization method is based on a construction of the reduced cycle-free finite state space graph. In contrast with traditional state space graph derivation, the optimization algorithm starts from the final states (fixed points) and gradually expands the state space graph until all of the states with a reachable fixed point are found. The new and optimized system is then synthesized from the constructed state space graph. The authors present several algorithms implementing the optimization method. They vary in complexity as well as in the usage of concurrency and state-equivalency-both targeted toward minimizing the size of the optimized state space graph. Though depending on the algorithm used, optimized rule-based systems: (1) in general have better response time in that they require fewer rule firings to reach the fixed point; (2) are stable, i.e., have no cycles that would result in the instability of execution; and (3) have no redundant rules. They also address the issue of deterministic execution and propose optimization algorithms that generate the rule-bases with single corresponding fixed points for every initial state. The synthesis method also determines the tight response time bound of the new system and can identify unstable states in the original rule-base     

Improving swarming using genetic algorithms

The verification of temporal properties against a given system may require the exploration of its full state space. In explicit model checking, this exploration uses a depth-first search and can be achieved with multiple randomized threads to increase performance. Nonetheless, the topology of the state space and the exploration order can cap the speedup up to a certain number of threads. This paper proposes a new technique that aims to tackle this limitation by generating artificial initial states, using genetic algorithms. Threads are then launched from these states and thus explore different parts of the state space. Our prototype implementation is 10% faster than state-of-the-art algorithms on a general benchmark and 40% on a specialized benchmark. Even if we expected a decrease in an order of magnitude, these results are still encouraging since they suggest a new way to handle existing limitations. Empirically, our technique seems well suited for “linear” topology, i.e., the one we can obtain when combining model checking algorithms with partial-order reduction techniques.

     

Partial-order reduction for general state exploring algorithms

Partial-order reduction is one of the main techniques used to tackle the combinatorial state explosion problem occurring in explicit-state model checking of concurrent systems. The reduction is performed by exploiting the independence of concurrently executed events, which allows portions of the state space to be pruned. An important condition for the soundness of partial-order-based reduction algorithms is a condition that prevents indefinite ignoring of actions when pruning the state space. This condition is commonly known as the cycle proviso. In this paper, we present a new version of this proviso, which is applicable to a general search algorithm skeleton that we refer to as the general state exploring algorithm (GSEA). GSEA maintains a set of open states from which states are iteratively selected for expansion and moved to a closed set of states. Depending on the data structure used to represent the open set, GSEA can be instantiated as a depth-first, a breadth-first, or a directed search algorithm such as Best-First Search or A*. The proviso is characterized by reference to the open and closed set of states of the search algorithm. As a result, it can be computed in an efficient manner during the search based on local information. We implemented partial-order reduction for GSEA based on our proposed proviso in the tool HSF-SPIN, an extension of the explicit-state model checker SPIN for directed model checking. We evaluate the state space reduction achieved by partial-order reduction using the proposed proviso by comparing it on a set of benchmark problems to the use of other provisos. We also compare the use of breadth-first search (BFS) and A*, two algorithms ensuring that counterexamples of minimal length will be found, together with the proviso that we propose.     

A Database Approach to Distributed State Space Generation

We study distributed state space generation on a cluster of workstations. It is explained why state space partitioning by a global hash function is problematic when states contain variables from unbounded domains, such as lists or other recursive datatypes. Our solution is to introduce a database which maintains a global numbering of state values. We also describe tree-compression, a technique of recursive state folding, and show that it is superior to manipulating plain state vectors.This solution is implemented and linked to the μCRL toolset, where state values are implemented as maximally shared terms (ATerms). However, it is applicable to other models as well, e.g., PROMELA models via the NIPS virtual machine. Our experiments show the trade-offs between keeping the database global, replicated, or local, depending on the available network bandwidth and latency.     

Minimizing user intervention in registering 2D images to 3D models

This paper proposes a novel technique to speed up the registration of 2D images to 3D models. This problem often arises in the process of digitalization of real objects, because pictures are often taken independently from the 3D geometry. Although there are a number of methods for solving the problem of registration automatically, they all need some further assumptions, so in the most general case the process still requires the user to provide some information about how the image corresponds to geometry, for example providing point-to-point correspondences. We propose a method based on a graph representation where the nodes represent the 2D photos and the 3D object, and arcs encode correspondences, which are either image–to–geometry or image–to–image point pairs. This graph is used to infer new correspondences from the ones specified by the user and from successful alignment of single images and to factually encode the state of the registration process. After each action performed by the user, our system explores the states space to find the shortest path from the current state to a state where all the images are aligned, i.e. a final state and, therefore, guides the user in the selection of further alignment actions for a faster completion of the job. Experiments on empirical data are reported to show the effectiveness of the system in reducing the user workload considerably.     

Ultimate bound and optimal measurement for estimation of coupling constant in Tavis–Cummings model

We seek to study the problem of estimating the atoms-field coupling constant in Tavis–Cummings model for interaction between two atoms and an electromagnetic field by means of local estimation theory. We calculate the quantum Fisher information (QFI) for the most general pure probe state that undergoes evolution generated by the Hamiltonian of the Tavis–Cummings model; then, proper probe states which maximize the QFI are determined. Furthermore, we consider subspaces separately and show that QFI for atomic subspace (contains both qubits) and cavity field subspace can reach the maximum value of QFI in the whole space by choosing proper initial state. Finally, the optimal measurement that saturates the Cramer–Rao bound, i.e., the measurement with Fisher information equal to QFI, for considered states are determined in the whole space and the subspaces, separately.     

Past‐Free[ze] reachability analysis: reaching further with DAG‐directed exhaustive state‐space analysis

Model‐checking enables the automated formal verification of software systems through the explicit enumeration of all the reachable states. While this technique has been successfully applied to industrial systems, it suffers from the state‐space explosion problem because of the exponential growth in the number of states with respect to the number of interacting components. In this paper, we present a new reachability analysis algorithm, named Past‐Free[ze], that reduces the state‐space explosion problem by freeing parts of the state‐space from memory. This algorithm relies on the explicit isolation of the acyclic parts of the system before analysis. The parallel composition of these parts drives the reachability analysis, the core of all model‐checkers. During the execution, the past states of the system are freed from memory making room for more future states. To enable counter‐example construction, the past states can be stored on external storage. To show the effectiveness of the approach, the algorithm was implemented in the OBP Observation Engine and was evaluated both on a synthetic benchmark and on realistic case studies from automotive and aerospace domains. The benchmark, composed of 50 test cases, shows that in average, 75% of the state‐space can be dropped from memory thus enabling the exploration of up to 14 times more states than traditional approaches. Moreover, in some cases, the reachability analysis time can be reduced by up to 25%. In realistic settings, the use of Past‐Free[ze] enabled the exploration of a state‐space 4.5 times larger on the automotive case study, where almost 50% of the states are freed from memory. Moreover, this approach offers the possibility of analyzing an arbitrary number of interactions between the environment and the system‐under‐verification; for instance, in the case of the aerospace example, 1000 pilot/system interactions could be analyzed unraveling an 80 GB state‐space using only 10 GB of memory. Copyright © 2016 John Wiley & Sons, Ltd.     

Solution of the input-constrained LQR problem using dynamic programming

The input-constrained LQR problem is addressed in this paper; i.e., the problem of finding the optimal control law for a linear system such that a quadratic cost functional is minimised over a horizon of length N subject to the satisfaction of input constraints. A global solution (i.e., valid in the entire state space) for this problem, and for arbitrary horizon N, is derived analytically by using dynamic programming. The scalar input case is considered in this paper. Solutions to this problem (and to more general problems: state constraints, multiple inputs) have been reported recently in the literature, for example, approaches that use the geometric structure of the underlying quadratic programming problem and approaches that use multi-parametric quadratic programming techniques. The solution by dynamic programming proposed in the present paper coincides with the ones obtained by the aforementioned approaches. However, being derived using a different approach that exploits the dynamic nature of the constrained optimisation problem to obtain an analytical solution, the present result complements the previous methods and reveals additional insights into the intrinsic structure of the optimal solution.     

Cluster-Based Partial-Order Reduction

The verification of concurrent systems through an exhaustive traversal of the state space suffers from the infamous state-space-explosion problem, caused by the many interleavings of actions of different processes in the system. Partial-order reduction is a well-known technique to tackle this problem. In this paper, we present an enhancement of the partial-order-reduction scheme of Holzmann and Peled that uses the hierarchical structure of concurrent systems. Our technique tries to contain dependencies between actions within clusters of processes, capitalizing on the independence of actions in different clusters to reduce the state space to be verified while preserving properties of interest. The paper starts with a formalization of the partial-order-reduction technique and continues with a presentation of our enhanced technique, including a correctness argument. The new technique has been implemented in the verification tool SPIN. We present implementation details, some small experiments, and one larger case study using a cache coherency protocol. The experimental results are encouraging. Compared to standard partial-order reduction, improvements in reductions are obtained from 21% up to 98% in the number of states and 34% up to 99% in the number of state transitions.     

The inhibition spectrum and the achievement of causal consistency

Summary.  We consider the problem of distinguishing causally-consistent global states in asynchronous distributed systems. Such states are fundamental to asynchronous systems, because they correspond to possible simultaneous global states; their detection arises in a variety of distributed applications, including global checkpointing, deadlock detection, termination detection, and broadcasting. A consistent-cut protocol is a protocol which in every run will designate for each processor a state, in such a way that these states together form a consistent cut. We analyze the cost of achieving causal consistency in terms of the extent to which a consistent-cut protocol delays events of the underlying system. We refer to the delaying action of a protocol as inhibition. A protocol using local inhibition may cause the delay of some of a processor’s events until that processor has performed some number of local actions; a protocol using global inhibition may force the delay of some of a processor’s events until that processor has received some communication from other processors. Based on a variety of system and protocol characteristics, including the ability to locally or globally inhibit particular types of events, we give three impossibility results and examine some existing protocols. We are then able to present a thirty-six case summary of protocols and impossibility results for the determination of causally-consistent states as a function of those characteristics. In particular, we demonstrate that local inhibition is necessary and sufficient to solve this problem for general FIFO systems, while global send inhibition is necessary and sufficient for general non-FIFO systems. Received: January 1993 / Accepted: January 1996     

基于节点生长k-均值聚类算法的强化学习方法

处理连续状态强化学习问题,主要方法有两类:参数化的函数逼近和自适应离散划分.在分析了现有对连续状态空间进行自适应划分方法的优缺点的基础上,提出了一种基于节点生长k均值聚类算法的划分方法,分别给出了在离散动作和连续动作两种情况下该强化学习方法的算法步骤.在离散动作的MountainCar问题和连续动作的双积分问题上进行仿真实验.实验结果表明,该方法能够根据状态在连续空间的分布,自动调整划分的精度,实现对于连续状态空间的自适应划分,并学习到最佳策略.