Formal methods for control synthesis in partially observed environments : application to autonomous robotic manipulation

Modern robots are increasingly expected to function in uncertain and dynamically challenging environments, often in proximity with humans. In addition, wide scale adoption of robots requires on-the-fly adaptability of software for diverse application. These requirements strongly suggest the need to adopt formal representations of high level goals and safety specifications, especially as temporal logic formulas. This approach allows for the use of formal verification techniques for controller synthesis that can give guarantees for safety and performance. Robots operating in unstructured environments also face limited sensing capability. Correctly inferring a robot's progress toward high level goal can be challenging.

This thesis develops new algorithms for synthesizing discrete controllers in partially known environments under specifications represented as linear temporal logic (LTL) formulas. It is inspired by recent developments in finite abstraction techniques for hybrid systems and motion planning problems. The robot and its environment is assumed to have a finite abstraction as a Partially Observable Markov Decision Process (POMDP), which is a powerful model class capable of representing a wide variety of problems. However, synthesizing controllers that satisfy LTL goals over POMDPs is a challenging problem which has received only limited attention.

This thesis proposes tractable, approximate algorithms for the control synthesis problem using Finite State Controllers (FSCs). The use of FSCs to control finite POMDPs allows for the closed system to be analyzed as finite global Markov chain. The thesis explicitly shows how transient and steady state behavior of the global Markov chains can be related to two different criteria with respect to satisfaction of LTL formulas. First, the maximization of the probability of LTL satisfaction is related to an optimization problem over a parametrization of the FSC. Analytic computation of gradients are derived which allows the use of first order optimization techniques.

The second criterion encourages rapid and frequent visits to a restricted set of states over infinite executions. It is formulated as a constrained optimization problem with a discounted long term reward objective by the novel utilization of a fundamental equation for Markov chains - the Poisson equation. A new constrained policy iteration technique is proposed to solve the resulting dynamic program, which also provides a way to escape local maxima.

The algorithms proposed in the thesis are applied to the task planning and execution challenges faced during the DARPA Autonomous Robotic Manipulation - Software challenge.

Stationary absolute distributions for chains of infinite order

Let {Ƶ_n}^∞_{n = -∞} be a stochastic process with state space S₁ = {0, 1, …, D – 1}. Such a process is called a chain of infinite order. The transitions of the chain are described by the functions

Q_i(i⁽⁰⁾) = Ƥ(Ƶ_n = i | Ƶ_{n - 1} = i ⁽⁰⁾₁, Ƶ_{n - 2} = i ⁽⁰⁾₂, …) (i ɛ S₁), where i⁽⁰⁾ = (i⁽⁰⁾₁, i⁽⁰⁾₂, …) ranges over infinite sequences from S₁. If i⁽ⁿ⁾ = (i⁽ⁿ⁾₁, i⁽ⁿ⁾₂, …) for n = 1, 2,…, then i⁽ⁿ⁾ → i⁽⁰⁾ means that for each k, i⁽ⁿ⁾_k = i⁽⁰⁾_k for all n sufficiently large.

Given functions Q_i(i⁽⁰⁾) such that

(i) 0 ≤ Q_i(i⁽⁰) ≤ ξ ˂ 1

(ii)D – 1/Ʃ/i = 0 Q_i(i⁽⁰⁾) Ξ 1

(iii) Q_i(i⁽ⁿ⁾) → Q_i(i⁽⁰⁾) whenever i⁽ⁿ⁾ → i⁽⁰⁾,

we prove the existence of a stationary chain of infinite order {Ƶ_n} whose transitions are given by

Ƥ (Ƶ_n = i | Ƶ_{n - 1}, Ƶ_{n - 2}, …) = Q_i(Ƶ_{n - 1}, Ƶ_{n - 2}, …)

With probability 1. The method also yields stationary chains {Ƶ_n} for which (iii) does not hold but whose transition probabilities are, in a sense, “locally Markovian.” These and similar results extend a paper by T.E. Harris [Pac. J. Math., 5 (1955), 707-724].

Included is a new proof of the existence and uniqueness of a stationary absolute distribution for an Nth order Markov chain in which all transitions are possible. This proof allows us to achieve our main results without the use of limit theorem techniques.

Zirconocenes as models for homogeneous Ziegler-Natta olefin polymerization catalysts

Using density functional theory, we studied the fundamental steps of olefin polymerization for zwitterionic and cationic Group IV ansa-zirconocenes and a neutral ansa- yttrocene. Complexes [H₂E(C₅H₄)₂ZrMe]ⁿ (n = 0: E = BH₂ (1), BF₂ (2), AlH₂(3); n = +: E = CH₂(4), SiH₂(5)) and H₂Si(C₅H₄)₂YMe were used as computational models. The largest differences among these three classes of compounds were the strength of olefin binding and the stability of the β-agostic alkyl intermediate towards β-hydrogen elimination. We investigated the effect of solvent on the reaction energetics for land 5. We found that in benzene the energetics became very similar except that a higher olefin insertion barrier was calculated for 1. The calculated anion affinity of [CH₃BF₃]^- was weaker towards 1 than 5. The calculated olefin binding depended primarily on the charge of the ansa linker, and the olefin insertion barrier was found to decrease steadily in the following order: [H₂C(C₅H₄)₂ZrMe]⁺ > [F₂B(C₅H₄)₂ZrMe] ≈ [H₂B(C₅H₄)₂ZrMe] > [H₂Si(C₅H₄)₂ZrMe]⁺ > [H₂Al(C₅H₄)₂ZrMe].

We prepared ansa-zirconocene dicarbonyl complexes Me₂ECp₂Zr(CO)₂ (E = Si, C), and t-butyl substituted complexes (t-BuCp)₂Zr(CO)₂, Me₂E(t-BuCp)₂Zr(CO)₂ (E = Si, C), (Me₂Si)₂(t-BuCp)₂Zr(CO)₂ as well as analogous zirconocene complexes. Both the reduction potentials and carbonyl stretching frequencies follow the same order: Me₂SiCp₂ZrCl₂> Me₂CCp₂ZrCl₂> Cp₂ZrCl₂> (Me₂Si)₂Cp₂ZrCl₂. This ordering is a result of both the donating abilities of the cyclopentadienyl substituents and the orientation of the cyclopentadiene rings. Additionally, we prepared a series of analogous cationic zirconocene complexes [LZrOCMe₃][MeB(C₆F₅)₃] (L = CP₂, Me₂SiCp₂, Me₂CCP₂, (Me₂Si)₂Cp₂) and studied the kinetics of anion dissociation. We found that the enthalpy of anion dissociation increased from 10.3 kcal•mol^-1 to 17.6 kcal•mol^-1 as exposure of the zirconium center increased.

We also prepared series of zirconocene complexes bearing 2,2-dimethyl-2-sila-4-pentenyl substituents (and methyl-substituted olefin variants). Methide abstraction with B(C₆F₅) results in reversible coordination of the tethered olefin to the cationic zirconium center. The kinetics of olefin dissociation have been examined using NMR methods, and the effects of ligand variation for unlinked, singly [SiMe₂]-linked and doubly [SiMe₂]-linked bis(cyclopentadienyl) arrangements has been compared (ΔG‡ for olefin dissociation varies from 12.8 to 15.6 kcal•mol^-1). Methide abstraction from 1,2-(SiMe₂)₂(η⁵-C₅H₃)₂Zr(CH₃)-(CH₂CMe₂CH₂CH = CH₂) results in rapid β-allyl elimination with loss of isobutene yielding the allyl cation [{1,2-(SiMe₂)₂(η⁵-C₅H₃)₂Zr(η³-CH₂CH=CH₂)]⁺.

Ancillary ligand effects : from zirconium(IV)-catalyzed homogeneous propylene polymerization to platinum(II)-mediated C-H bond activation

A series of C_s- and C₁-symmetric doubly-linked ansa-metallocenes of the general formula {1,1'-SiMe₂-2,2'-E-('ƞ⁵-C₅H₂-4-R¹)-(ƞ⁵-C₅H-3',5'-(CHMe₂)₂)}ZrC₂ (E = SiMe₂ (1), SiPh₂ (2), SiMe₂ -SiMe₂ (3); R¹ = H, CHMe₂, C₅H₉, C₆H₁₁, C₆H₅) has been prepared. When activated by methylaluminoxane, these are active propylene polymerization catalysts. 1 and 2 produce syndiotactic polypropylenes, and 3 produces isotactic polypropylenes. Site epimerization is the major pathway for stereoerror formation for 1 and 2. In addition, the polymer chain has slightly stronger steric interaction with the diphenylsilylene linker than with the dimethylsilylene linker. This results in more frequent site epimerization and reduced syndiospecificity for 2 compared to 1.

C₁-Symmetric ansa-zirconocenes [1,1 '-SiMe₂-(C₅H₄)-(3-R-C₅H₃)]ZrCl₂ (4), [1,1 '-SiMe₂-(C₅H₄)-(2,4-R₂-C₅H₂)]ZrCl₂ (5) and [1,1 '-SiMe₂-2,2 '-(SiMe₂-SiMe₂)-(C₅H₃)-( 4-R-C₅H₂)]ZrCl₂ (6) have been prepared to probe the origin of isospecificity in 3. While 4 and 3 produce polymers with similar isospecificity, 5 and 6 give mostly hemi-isotactic-like polymers. It is proposed that the facile site epimerization via an associative pathway allows rapid equilibration of the polymer chain between the isospecific and aspecific insertion sites. This results in more frequent insertion from the isospecific site, which has a lower kinetic barrier for chain propagation. On the other hand, site epimerization for 5 and 6 is slow. This leads to mostly alternating insertion from the isospecific and aspecific sites, and consequently, a hemi-isotactic-like polymers. In comparison, site epimerization is even slower for 3, but enchainment from the aspecific site has an extremely high kinetic barrier for monomer coordination. Therefore, enchainment occurs preferentially from the isospecific site to produce isotactic polymers.

A series of cationic complexes [(ArN=CR-CR=NAr)PtMe(L)]⁺[BF₄]⁺ (Ar = aryl; R = H, CH₃; L = water, trifluoroethanol) has been prepared. They react smoothly with benzene at approximately room temperature in trifluoroethanol solvent to yield methane and the corresponding phenyl Pt(II) cations, via Pt(IV)-methyl-phenyl-hydride intermediates. The reaction products of methyl-substituted benzenes suggest an inherent reactivity preference for aromatic over benzylic C-H bond activation, which can however be overridden by steric effects. For the reaction of benzene with cationic Pt(II) complexes, in which the diimine ligands bear 3,5-disubstituted aryl groups at the nitrogen atoms, the rate-determining step is C-H bond activation. For the more sterically crowded analogs with 2,6-dimethyl-substituted aryl groups, benzene coordination becomes rate-determining. The more electron-rich the ligand, as reflected by the CO stretching frequency in the IR spectrum of the corresponding cationic carbonyl complex, the faster the rate of C-H bond activation. This finding, however, does not reflect the actual C-H bond activation process, but rather reflects only the relative ease of solvent molecules displacing water molecules to initiate the reaction. That is, the change in rates is mostly due to a ground state effect. Several lines of evidence suggest that associative substitution pathways operate to get the hydrocarbon substrate into, and out of, the coordination sphere; i.e., that benzene substitution proceeds by a solvent- (TFE-) assisted associative pathway.

Chains of Non-regular de Branges Spaces

We consider canonical systems with singular left endpoints, and discuss the concept of a scalar spectral measure and the corresponding generalized Fourier transform associated with a canonical system with a singular left endpoint. We use the framework of de Branges’ theory of Hilbert spaces of entire functions to study the correspondence between chains of non-regular de Branges spaces, canonical systems with singular left endpoints, and spectral measures.

We find sufficient integrability conditions on a Hamiltonian H which ensure the existence of a chain of de Branges functions in the first generalized Pólya class with Hamiltonian H. This result generalizes de Branges’ Theorem 41, which showed the sufficiency of stronger integrability conditions on H for the existence of a chain in the Pólya class. We show the conditions that de Branges came up with are also necessary. In the case of Krein’s strings, namely when the Hamiltonian is diagonal, we show our proposed conditions are also necessary.

We also investigate the asymptotic conditions on chains of de Branges functions as t approaches its left endpoint. We show there is a one-to-one correspondence between chains of de Branges functions satisfying certain asymptotic conditions and chains in the Pólya class. In the case of Krein’s strings, we also establish the one-to-one correspondence between chains satisfying certain asymptotic conditions and chains in the generalized Pólya class.

Force chains, friction, and flow: Behavior of granular media across length scales

We study the behavior of granular materials at three length scales. At the smallest length scale, the grain-scale, we study inter-particle forces and "force chains". Inter-particle forces are the natural building blocks of constitutive laws for granular materials. Force chains are a key signature of the heterogeneity of granular systems. Despite their fundamental importance for calibrating grain-scale numerical models and elucidating constitutive laws, inter-particle forces have not been fully quantified in natural granular materials. We present a numerical force inference technique for determining inter-particle forces from experimental data and apply the technique to two-dimensional and three-dimensional systems under quasi-static and dynamic load. These experiments validate the technique and provide insight into the quasi-static and dynamic behavior of granular materials.

At a larger length scale, the mesoscale, we study the emergent frictional behavior of a collection of grains. Properties of granular materials at this intermediate scale are crucial inputs for macro-scale continuum models. We derive friction laws for granular materials at the mesoscale by applying averaging techniques to grain-scale quantities. These laws portray the nature of steady-state frictional strength as a competition between steady-state dilation and grain-scale dissipation rates. The laws also directly link the rate of dilation to the non-steady-state frictional strength.

At the macro-scale, we investigate continuum modeling techniques capable of simulating the distinct solid-like, liquid-like, and gas-like behaviors exhibited by granular materials in a single computational domain. We propose a Smoothed Particle Hydrodynamics (SPH) approach for granular materials with a viscoplastic constitutive law. The constitutive law uses a rate-dependent and dilation-dependent friction law. We provide a theoretical basis for a dilation-dependent friction law using similar analysis to that performed at the mesoscale. We provide several qualitative and quantitative validations of the technique and discuss ongoing work aiming to couple the granular flow with gas and fluid flows.