TY - CONF AU - László Erdös ID - 2708 TI - Two dimensional Pauli operator via scalar potential VL - 307 ER - TY - JOUR AB - Polar auxin transport controls multiple aspects of plant development including differential growth, embryo and root patterning and vascular tissue differentiation. Identification of proteins involved in this process and availability of new tools enabling `visualization' of auxin and auxin routes in planta largely contributed to the significant progress that has recently been made. New data support classical concepts, but several recent findings are likely to challenge our view on the mechanism of auxin transport. The aim of this review is to provide a comprehensive overview of the polar auxin transport field. It starts with classical models resulting from physiological studies, describes the genetic contributions and discusses the molecular basis of auxin influx and efflux. Finally, selected questions are presented in the context of developmental biology, integrating available data from different fields. AU - Friml, Jirí AU - Palme, Klaus ID - 2991 IS - 3-4 JF - Plant Molecular Biology TI - Polar auxin transport - Old questions and new concepts? VL - 49 ER - TY - GEN AB - A method of automatic conversion of a physical object into a three-dimensional digital model. The method acquires a set of measured data points on the surface of a physical model. From the measured data points, the method reconstructs a digital model of the physical object using a Delaunay complex of the points, a flow strcuture of the simplicies in the Delaunay complex and retracting the Delaunay complex into a digital model of the physical object using the flow structure. The method then outputs the digital model of the physical object. AU - Edelsbrunner, Herbert AU - Fu, Ping ID - 3508 TI - Methods of generating three-dimensional digital models of objects by wrapping point cloud data points ER - TY - CONF AU - Mallick, Sanhita AU - Krishnendu Chatterjee AU - Merchant, Arif N AU - Dasgupta, Pallab ID - 3448 TI - Implementation of shape grammar for plan analysis ER - TY - THES AB - This dissertation investigates game-theoretic approaches to the algorithmic analysis of concurrent, reactive systems. A concurrent system comprises a number of components working concurrently; a reactive system maintains an ongoing interaction with its environment. Traditional approaches to the formal analysis of concurrent reactive systems usually view the system as an unstructured state-transition graphs; instead, we view them as collections of interacting components, where each one is an open system which accepts inputs from the other components. The interactions among the components are naturally modeled as games. Adopting this game-theoretic view, we study three related problems pertaining to the verification and synthesis of systems. Firstly, we propose two novel game-theoretic techniques for the model-checking of concurrent reactive systems, and improve the performance of model-checking. The first technique discovers an error as soon as it cannot be prevented, which can be long before it actually occurs. This technique is based on the key observation that "unpreventability" is a local property to a module: an error is unpreventable in a module state if no environment can prevent it. The second technique attempts to decompose a model-checking proof into smaller proof obligations by constructing abstract modules automatically, using reachability and "unpreventability" information about the concrete modules. Three increasingly powerful proof decomposition rules are proposed and we show that in practice, the resulting abstract modules are often significantly smaller than the concrete modules and can drastically reduce the space and time requirements for verification. Both techniques fall into the category of compositional reasoning. Secondly, we investigate the composition and control of synchronous systems. An essential property of synchronous systems for compositional reasoning is non-blocking. In the composition of synchronous systems, however, due to circular causal dependency of input and output signals, non-blocking is not always guaranteed. Blocking compositions of systems can be ruled out semantically, by insisting on the existence of certain fixed points, or syntactically, by equipping systems with types, which make the dependencies between input and output signals transparent. We characterize various typing mechanisms in game-theoretic terms, and study their effects on the controller synthesis problem. We show that our typing systems are general enough to capture interesting real-life synchronous systems such as all delay-insensitive digital circuits. We then study their corresponding single-step control problems --a restricted form of controller synthesis problem whose solutions can be iterated in appropriate manners to solve all LTL controller synthesis problems. We also consider versions of the controller synthesis problem in which the type of the controller is given. We show that the solution of these fixed-type control problems requires the evaluation of partially ordered (Henkin) quantifiers on boolean formulas, and is therefore harder (nondeterministic exponential time) than more traditional control questions. Thirdly, we study the synthesis of a class of open systems, namely, uninitialized state machines. The sequential synthesis problem, which is closely related to Church's solvability problem, asks, given a specification in the form of a binary relation between input and output streams, for the construction of a finite-state stream transducer that converts inputs to appropriate outputs. For efficiency reasons, practical sequential hardware is often designed to operate without prior initialization. Such hardware designs can be modeled by uninitialized state machines, which are required to satisfy their specification if started from any state. We solve the sequential synthesis problem for uninitialized systems, that is, we construct uninitialized finite-state stream transducers. We consider specifications given by LTL formulas, deterministic, nondeterministic, universal, and alternating Buechi automata. We solve this uninitialized synthesis problem by reducing it to the well-understood initialized synthesis problem. While our solution is straightforward, it leads, for some specification formalisms, to upper bounds that are exponentially worse than the complexity of the corresponding initialized problems. However, we prove lower bounds to show that our simple solutions are optimal for all considered specification formalisms. The lower bound proofs require nontrivial generic reductions. AU - Mang, Freddy ID - 4414 TI - Games in open systems verification and synthesis ER -