bluuebunny/crossref_metadata_2025 huggingface dataset:
An Integrated Geologic and Engineering Assessment of Fracture-Flow Potential in the Ratawi Reservoir of the Wafra Field, Partitioned Neutral Zone
Authors: Whitaker A. E. , Kabir C. S. , Narr W.
Published: January 2009

The extent to which fractures affect fluid pathways is a vital component of understanding and modeling fluid flow in any reservoir. We examined the Wafra Ratawi grainstone for which production extending for 50 years, including recent horizontal drilling, has provided some clues about fractures, but their exact locations, intensity, and overall effect have been elusive. In this study, we find that a limited number of total fractures affect production characteristics of the Ratawi reservoir. Although fractures occur throughout the Wafra field, fracture-influenced reservoir behavior is confined to the periphery of the field where the matrix permeability is low. This work suggests that for the largest part of the field, explicit fractures are not necessary in the next-generation Earth and flow-simulation models.

The geologic fracture assessment included seismic fault mapping and fracture interpretation of image logs and cores. Fracture trends are in the northeast and southwest quadrants, and fractures are mineralized toward the south and west of the field. Pressure-falloff tests on some peripheral injectors indicate partial barriers, and most of these wells lie on seismic-scale faults in the reservoir, suggesting partial sealing. A few wells show fractured-reservoir production characteristics, and rate-transient analysis on a few producers indicates localized dual-porosity behavior. Producers proximal to dual-porosity wells display single-porosity behavior, however, to attest to the notion of localized fracture response. The spatially restricted fracture-flow characteristics appear to correlate with fracture or vug zones in a low-permeability reservoir.

Presence of fracture-flow behavior was tested by constructing the so-called flow-capacity index (FCI), the ratio of khwell (well test-derived value) to khmatrix (core-derived property). Data from 80 wells showed khmatrix to be consistently higher than khwell, a relationship that suggests insignificant fracture production in these wells.
Economic Decision Making and the Application of Nonparametric Prediction Models
Authors: Attanasi E. D. , Coburn T. C. , Freeman P. A.
Published: January 2009

Sustained increases in energy prices have focused attention on gas resources in low-permeability shale or in coals that were previously considered economically marginal. Daily well deliverability is often relatively small, although the estimates of the total volumes of recoverable resources in these settings are often large. Planning and development decisions for extraction of such resources must be areawide because profitable extraction requires optimization of scale economies to minimize costs and reduce risk. For an individual firm, the decision to enter such plays depends on reconnaissance-level estimates of regional recoverable resources and on cost estimates to develop untested areas.

This paper shows how simple nonparametric local regression models, used to predict technically recoverable resources at untested sites, can be combined with economic models to compute regional-scale cost functions. The context of the worked example is the Devonian Antrim-shale gas play in the Michigan basin. One finding relates to selection of the resource prediction model to be used with economic models. Models chosen because they can best predict aggregate volume over larger areas (many hundreds of sites) smooth out granularity in the distribution of predicted volumes at individual sites. This loss of detail affects the representation of economic cost functions and may affect economic decisions. Second, because some analysts consider unconventional resources to be ubiquitous, the selection and order of specific drilling sites may, in practice, be determined arbitrarily by extraneous factors. The analysis shows a 15-20% gain in gas volume when these simple models are applied to order drilling prospects strategically rather than to choose drilling locations randomly.
Key Aspects of Project Design for Polymer Flooding at the Daqing Oilfield
Authors: Wang Dongmei , Seright R. S. , Shao Zhenbo , Wang Jinmei
Published: January 2009

This paper describes the design procedures that led to favorable incremental oil production and reduced water production during 12 years of successful polymer flooding in the Daqing oil field. Special emphasis is placed on some new design factors that were found to be important on the basis of extensive experience with polymer flooding. These factors include (1) recognizing when profile modification is needed before polymer injection and when zone isolation is of value during polymer injection, (2) establishing the optimum polymer formulations and injection rates, and (3) time-dependent variation of the molecular weight of the polymer used in the injected slugs.

For some Daqing wells, oil recovery can be enhanced by 2 to 4% of original oil in place (OOIP) with profile modification before polymer injection. For some Daqing wells with significant permeability differential between layers and no crossflow, injecting polymer solutions separately into different layers improved flow profiles, reservoir sweep efficiency, and injection rates, and it reduced the water cut in production wells. Experience over time revealed that larger polymer-bank sizes are preferred. Bank sizes grew from 240–380 mg/L.PV during the initial pilots to 640 to 700 mg/L.PV in the most recent large-scale industrial sites [pore volume (PV)]. Economics and injectivity behavior can favor changing the polymer molecular weight and polymer concentration during the course of injecting the polymer slug. Polymers with molecular weights from 12 to 35 million Daltons were designed and supplied to meet the requirements for different reservoir geological conditions. The optimum polymer-injection volume varied around 0.7 PV, depending on the water cut in the different flooding units. The average polymer concentration was designed approximately 1000 mg/L, but for an individual injection station, it could be 2000 mg/L or more. At Daqing, the injection rates should be less than 0.14–0.20 PV/year, depending on well spacing.
The Application of Cutoffs in Integrated Reservoir Studies
Authors: Worthington Paul F.
Published: January 2009

Methodologies have been developed for applying net reservoir and thence net pay cutoffs in cases of primary and waterflood depletion. The cutoffs are dynamically-conditioned to be reservoir-specific (i.e., they are tied back to a reference permeability parameter in a way that is driven by the reservoir data themselves). They also honor scale, where feasible, and are conformable with any pertinent rock-typing. For primary depletion, the Leverett equivalent circular pore diameter has been used to distinguish between reservoir and nonreservoir rock. This composite parameter can incorporate mobility for multiphase work. It is linked to a discrete core porosity under simulated reservoir conditions, so the adopted net reservoir cutoff is expressed as a limiting porosity. For waterflood depletion, an extrapolated endpoint relative permeability to oil has proved effective for the same purpose. Here, the zero endpoint relative permeability is linked to a conventional "absolute" core permeability corrected to reservoir conditions. Porosity is tied back to this limiting absolute permeability so that the net reservoir cutoff is again expressed in terms of porosity. Consequently, in both cases, the discrete porosity cutoffs have a dynamic significance. Other cutoff parameters, such as shale volume fraction and water saturation, can be tied back to these. A proposed workflow for applying dynamically-conditioned cutoffs allows data character to drive their use in integrated reservoir studies. The workflow constitutes a basis for greater technical consistency in the estimation of ultimate hydrocarbon recovery. However, the treatment is not exclusive, and other approaches to the determination of net pay will emerge as more reservoirs are considered.
A Survey of Factors Involved in Crop Maturity
Authors: Bruns H. Arnold
Published: January 2009

The time necessary for crops to successfully complete reproduction is species and environment dependent. Lifecycles can be completed in a few weeks or take several years depending on the plant species. Crop development is divided into phenophases that are affected primarily by light and temperature changes, interacting with phytohormones. Some species are influenced more by light and others by temperature. This review focuses on factors that influence maturation in several important agronomic crops.
Nitrogen and Plant Growth Regulator Influence on ‘Champion’ Bermudagrass Putting Green under Reduced Sunlight
Authors: Baldwin Christian M. , Liu Haibo , McCarty Lambert B. , Luo Hong , Toler Joe E.
Published: January 2009

Managing warm‐season turfgrasses with reduced sunlight is challenging due to C4 plant morphological limitations, such as reduced lateral stem growth. Adjusting cultural management practices, such as N and trinexapac‐ethyl (TE) [4‐(cyclopropyl‐a‐hydroxy‐methylene)‐3,5‐dioxocyclohexanecarboxylic acid ethyl ester], application may benefit turfgrass performance when sunlight is reduced. Therefore, a 2‐yr field study from 15 June to 15 September in 2006 and 2007 at Clemson University investigated the best management practices for sustaining a high quality ‘Champion’ bermudagrass (Cynodon dactylon (L.) Pers. X C. transvaalensis Burtt‐Davy) putting green maintained at a 3.2‐mm mowing height under reduced sunlight. Treatments included full‐sunlight, 55% full‐day shade, TE (0.02 kg a.i. ha−1 2 wk−1), Fe (2.7 kg ha−1 2 wk−1), and N as liquid urea at 147, 293, and 440 kg ha−1 yr−1. Data collection included visual turfgrass quality (TQ), total clipping yield, clipping chlorophyll concentration, root total nonstructural carbohydrates (TNC), thatch accumulation, and thatch depth. Overall, Fe applications minimally impacted parameters measured. Increasing N rates linearly increased TQ when grown under full sunlight. Applying N at ∼40% lower (147 kg ha−1 yr−1) than the typical recommended rates for ultradwarf bermudagrass putting greens improved Champion TQ under reduced light compared to higher N rates. Applying TE resulted in a linear TQ increase for full sunlight and shade‐grown Champion bermudagrass. Under reduced sunlight, a 15% chlorophyll concentration increase was noted for TE‐treated plots compared to nonTE‐treated plots. Shade reduced thatch accumulation 40% compared to sun‐grown Champion, which suggests less aggressive cultivation practices are required for thatch control under reduced light. Champion bermudagrass did not provide an acceptable putting green quality when grown under 55% full‐day shade, however, adjusting management practices enhanced Champion bermudagrass quality under reduced light.
Analysis of High Yielding, Early‐Planted Soybean in Indiana
Authors: Robinson Andrew P. , Conley Shawn P. , Volenec Jeffrey J. , Santini Judith B.
Published: January 2009

A trend toward early planting of soybean [Glycine max (L.) Merr.] in Indiana results in higher yield, but the limit to which a positive response to early planting occurs has not been evaluated. Our objective was to determine how early planting affects yield components and seed composition of indeterminate soybean planted in late March through early June in Indiana. Three cultivars (Pioneer brand 92M61, Becks brand 321NRR, and Becks brand 367NRR) were sown at six planting dates (late March through early June) in West Lafayette, IN, in 2006 and 2007. Across cultivars, yield in 2006 ranged between 4.24 to 4.43 Mg ha−1 at the planting dates from late March to mid‐May, and decreased to 3.36 and 3.56 Mg ha−1 at later planting dates. In 2007, yield ranged from 4.21 to 4.44 Mg ha−1 for the 10 April, 30 April, and 9 May planting dates. Yield was reduced at the late March and early June plantings and ranged from 3.85 to 3.99 Mg ha−1. Path analysis revealed that pods m−2 had the greatest impact on yield, but seed mass was also an important constituent. Mean oil concentration decreased approximately 12 g kg−1 as planting was delayed in both years. In 2006, average seed protein concentration varied by planting date. In 2007, mean protein concentration increased 14 g kg−1 as planting was delayed. Delaying planting until late May or early June altered seed composition slightly, but significantly reduced yield. Planting in April or early May is an effective management strategy to increase soybean yield in Indiana.
Nitrogen Supply for Cover Crops and Effects on Peanut Grown in Succession under a No‐Till System
Authors: Crusciol Carlos A. C. , Soratto Rogério P.
Published: January 2009

In Brazil, as no‐till (NT) crop management expands, there is an increased interest in growing peanut (Arachis hypogaea L.) with this system. However, it is not known if the preceding cover crop species, the amount of straw on the soil surface, or the N supplied to the cover crop will affect peanut grown in a NT system. An experiment was conducted on a Typic Haplorthox in Botucatu, São Paulo State, Brazil, during two agricultural years, to evaluate the cover crop dry matter (DM) and nutrient accumulation as affected by N fertilization and peanut nutrition and yield when grown in succession, under a NT system. Treatments included three cover crops {palisadegrass [Brachiaria brizantha (Hochst. ex A. Rich) Stapf], pearl millet [Pennisetum glaucum (L.) R. Brown], and guineagrass [Panicum maximum Jacq.]} and two N rates (0 and 60 kg ha−1) supplied to the cover crops 50 d after emergence (DAE). Pearl millet showed lower nutrient concentrations in aboveground biomass compared with palisadegrass and guineagrass, but accumulated the largest quantities of DM (14.8 Mg ha−1) and macronutrients. Nitrogen application increased N and P concentration in all cover crops, as well as the accumulation of N, Ca, and Mg in pearl millet. Nitrogen‐fertilized pearl millet resulted in higher P, Ca, Mg, and S concentrations in peanut leaves grown after. Previous cover crops, even with large straw mulch production (6.0–14.8 Mg ha−1 of DM), did not influence peanut pod yield (mean 2.3 Mg ha−1) in the NT system, nor did N fertilization of the cover crop.
Nitrogen Increases Evapotranspiration and Growth of a Warm‐Season Turfgrass
Authors: Barton L. , Wan G. G. Y. , Buck R. P. , Colmer T. D.
Published: January 2009

The effect of N fertilizer rate on Kikuyu turfgrass [Pennisetum clandestinum (Hochst. ex Chiov)] evapotranspiration was evaluated during two summers. Evapotranspiration was measured using weighing lysimeters (205 mm in diameter by 625 mm in length) inserted in turfgrass field plots (10 m2). The experiment was a randomized plot design with three replicates. Treatments included two turfgrass ages (established from 20 wk or 20‐yr‐old turfgrass) and three N application rates (0, 50, or 150 kg N ha−1 yr−1). Evapotranspiration ranged from 2.8 to 7.5 mm d−1 (or 56–81% of evaporative demand), and varied with daily evaporative demand, turfgrass age, and N fertilizer rate. The older turfgrass used more water than the younger turfgrass during both summers; while increasing the N application rate also increased evapotranspiration for both turfgrass types (younger turfgrass only in the second summer). Evapotranspiration was positively correlated with turfgrass growth (r2 = 0.74–0.80) and transpiring leaf area (r2 = 0.78). Older turfgrass at all N treatments, and the younger turfgrass receiving 150 kg N ha−1 yr−1, had adequate growth, color, and leaf N concentrations. Optimizing fertilizer applications such that the minimum N required to maintain turfgrass quality is applied, is an approach for decreasing water consumption by turfgrass.
Dairy Cattle Manure Improves Soil Productivity in Low Residue Rotation Systems
Authors: Nyiraneza Judith , Chantigny Martin H. , N'Dayegamiye Adrien , Laverdière Marc R.
Published: January 2009

Mineral fertilizer alone may not sustain soil productivity in cropping systems that return little crop residues to the soil, unless additional organic residues and/or manure is applied regularly to the soil. The objective of the present study was to assess the long‐term effects of mineral fertilization (No fertilizer, PK, and NPK) and manure addition (0 and 20 Mg ha−1yr−1) on soil physical and chemical properties and crop yields in a cereal rotation with removal of crop residues. After 28 yr, soil organic carbon (SOC) declined by −0.25 g C kg−1yr−1and total nitrogen (TN) by −0.025 g N kg−1yr−1with balanced mineral fertilization (NPK, no manure), comparable to the control (no manure, no fertilizer). In addition, mean weight diameter (MWD) of water‐stable aggregates was lower with balanced mineral fertilization than in the control. In contrast, long‐term application of manure significantly increased water‐stable macroaggregates, potentially mineralizable nitrogen (PMN), and soil preseeding NO3–N levels. Corn yield and N uptake were increased by mineral fertilization compared to the control, and manure application increased corn yield by 89 and 87% and corn N uptake by 110 and 79% in 2005 and 2006, respectively. Increased corn yield in manured plots was attributed to the residual manure‐derived nutrients and to improved soil properties. Mineral fertilizer alone could not sustain soil productivity in intensive low‐residues cropping systems.
Effectiveness of Cultural Thatch‐Mat Controls for Young and Mature Kikuyu Turfgrass
Authors: Barton L. , Wan G. G. Y. , Buck R. P. , Colmer T. D.
Published: January 2009

Excessive thatch and mat can be detrimental to turfgrass health and management. Mechanical and topdressing techniques to reduce accumulation of thatch and mat were evaluated in a 24‐mo field study of kikuyu [Pennisetum clandestinum (Hochst. ex Chiov.)] turfgrass of two contrasting organic matter (OM) contents in the surface 50 mm of soil. Treatments included two kikuyugrass ages (established from 20 wk or 20‐yr‐old kikuyugrass) and five renovation techniques (none, verticutting, coring, topdressing with sand, coring + topdressing). The renovation techniques varied in effectiveness depending on the initial OM content of the soil immediately underlying the kikuyugrass. Annual verticutting, or twice annual topdressing with or without annual coring a young kikuyugrass were most successful at restricting the accumulation of soil OM (P < 0.05), with OM content <3.5% by 24 mo. Twice annual topdressing with or without annual coring, most rapidly decreased soil OM in the mature kikuyugrass (P < 0.05), with OM content averaging 6.2% by 24 mo. Combining coring with topdressing did not necessarily further decrease OM contents. Topdressing was up to three times more effective at reducing soil OM content than coring alone (P < 0.05). The color and N concentration of both kikuyugrass ages was maintained to local standards by all mechanical and topdressing techniques, although verticutting decreased the incidence of mower scalping in the second year. Verticutting was the most effective approach for restricting the progressive softening of young kikuyugrass with time (P < 0.05), whereas the mature kikuyugrass softened by the same amount irrespective of the renovation treatment.
Effect of Loblolly Pine Root Pruning on Alley Cropped Herbage Production and Tree Growth
Authors: Burner D. M. , Pote D. H. , Belesky D. P.
Published: January 2009

Tillage to disrupt (prune) tree roots is an intensive practice which could improve herbage productivity at the crop–tree interface by reducing competition for water. We compared tillage effects on 9‐ to 11‐yr‐old loblolly pine (Pinus taeda L.) growth and herbage yields of annual ryegrass (Lolium multiflorum Lam.) and pearl millet [Pennisetum glaucum (L.) R. Br.] on a fragipan soil in Arkansas. Alley crops were rotationally grown in a 9.7‐m wide alley (main plot) between bordering trees on one of three tillage treatments: control (surface tillage), rip followed by surface tillage, and trench plus root barrier followed by surface tillage. Topsoil water in May through September, herbage mass, and nutritive value were measured for each crop for 2 or 3 yr in three subplots systematically arrayed (north, middle, and south) across the alley. Diameter at breast height (DBH, measured 1.3 m above soil surface) and height of border trees were measured annually. Trenching resulted in a more uniform distribution of topsoil water among subplots compared to the other tillage treatments. Annual ryegrass yield did not show a tillage response, but pearl millet yielded more herbage in the rip (6760 kg ha−1 in 2003) and trench (3300 kg ha−1 in 2005) than the control treatment (4990 and 1260 kg ha−1 for 2003 and 2005, respectively). Ripping and trenching significantly reduced loblolly pine DBH and height compared to the control. Similarly configured alley cropping practices probably have little potential for annual herbage production even with root pruning.
Classifying Maize Inbred Lines into Heterotic Groups using a Factorial Mating Design
Authors: Fan X. M. , Zhang Y. M. , Yao W. H. , Chen H. M. , Tan J. , Xu C. X. , Han X. L. , Luo L. M. , Kang M. S.
Published: January 2009

A novel method of using a heterotic group's specific and general combining ability (HSGCA) to assign maize (Zea mays L.) inbred lines into heterotic groups has been proposed recently. The objectives of this study were to (i) assign maize inbred lines to known heterotic groups using this method and (ii) compare efficiency of this method to traditional and molecular methods relative to the percentage of high‐yielding hybrids obtained across the total number of the crosses made between testers and lines. An experiment with 23 maize inbred lines crossed to four testers with known heterotic groups was conducted in 2003 and 2004. This study successfully established a clear procedure to classify maize inbred lines into heterotic groups. The HSGCA method increased maize breeding efficiency by 16.7 to 23.6% compared with simple sequence repeat (SSR) and specific combining ability combined line pedigree and hybrid yield information (SCA_PY) methods, respectively. An analysis of variance showed that crosses classified by HSGCA method could explain more variation in maize hybrid yield and produce more predictable yield than the other two methods. The superiority of HSGCA relative to the other two methods is that HSGCA includes both GCA and SCA effect in assigning an unknown maize line to a known maize heterotic group.
Enriched MU-Calculi Module Checking
Authors: Ferrante Alessandro , Murano Aniello , Parente Mimmo
Published: January 2009

The model checking problem for open systems has been intensively studied in
the literature, for both finite-state (module checking) and infinite-state
(pushdown module checking) systems, with respect to Ctl and Ctl*. In this
paper, we further investigate this problem with respect to the \mu-calculus
enriched with nominals and graded modalities (hybrid graded Mu-calculus), in
both the finite-state and infinite-state settings. Using an automata-theoretic
approach, we show that hybrid graded \mu-calculus module checking is solvable
in exponential time, while hybrid graded \mu-calculus pushdown module checking
is solvable in double-exponential time. These results are also tight since they
match the known lower bounds for Ctl. We also investigate the module checking
problem with respect to the hybrid graded \mu-calculus enriched with inverse
programs (Fully enriched \mu-calculus): by showing a reduction from the domino
problem, we show its undecidability. We conclude with a short overview of the
model checking problem for the Fully enriched Mu-calculus and the fragments
obtained by dropping at least one of the additional constructs.
Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus
Authors: Shikuma Naokata , Igarashi Atsushi
Published: January 2009

Tse and Zdancewic have formalized the notion of noninterference for Abadi et
al.'s DCC in terms of logical relations and given a proof of noninterference by
reduction to parametricity of System F. Unfortunately, their proof contains
errors in a key lemma that their translation from DCC to System F preserves the
logical relations defined for both calculi. In fact, we have found a
counterexample for it. In this article, instead of DCC, we prove
noninterference for sealing calculus, a new variant of DCC, by reduction to the
basic lemma of a logical relation for the simply typed lambda-calculus, using a
fully complete translation to the simply typed lambda-calculus. Full
completeness plays an important role in showing preservation of the two logical
relations through the translation. Also, we investigate relationship among
sealing calculus, DCC, and an extension of DCC by Tse and Zdancewic and show
that the first and the last of the three are equivalent.
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics
Authors: Constable Robert , Moczydlowski Wojciech
Published: January 2009

Church's Higher Order Logic is a basis for influential proof assistants --
HOL and PVS. Church's logic has a simple set-theoretic semantics, making it
trustworthy and extensible. We factor HOL into a constructive core plus axioms
of excluded middle and choice. We similarly factor standard set theory, ZFC,
into a constructive core, IZF, and axioms of excluded middle and choice. Then
we provide the standard set-theoretic semantics in such a way that the
constructive core of HOL is mapped into IZF. We use the disjunction, numerical
existence and term existence properties of IZF to provide a program extraction
capability from proofs in the constructive core.
We can implement the disjunction and numerical existence properties in two
different ways: one using Rathjen's realizability for IZF and the other using a
new direct weak normalization result for IZF by Moczydlowski. The latter can
also be used for the term existence property.
Coinductive Formal Reasoning in Exact Real Arithmetic
Authors: Niqui Milad
Published: January 2009

In this article we present a method for formally proving the correctness of
the lazy algorithms for computing homographic and quadratic transformations --
of which field operations are special cases-- on a representation of real
numbers by coinductive streams. The algorithms work on coinductive stream of
M\"{o}bius maps and form the basis of the Edalat--Potts exact real arithmetic.
We use the machinery of the Coq proof assistant for the coinductive types to
present the formalisation. The formalised algorithms are only partially
productive, i.e., they do not output provably infinite streams for all possible
inputs. We show how to deal with this partiality in the presence of syntactic
restrictions posed by the constructive type theory of Coq. Furthermore we show
that the type theoretic techniques that we develop are compatible with the
semantics of the algorithms as continuous maps on real numbers. The resulting
Coq formalisation is available for public download.
Interpolation in local theory extensions
Authors: Sofronie-Stokkermans Viorica
Published: January 2009

In this paper we study interpolation in local extensions of a base theory. We
identify situations in which it is possible to obtain interpolants in a
hierarchical manner, by using a prover and a procedure for generating
interpolants in the base theory as black-boxes. We present several examples of
theory extensions in which interpolants can be computed this way, and discuss
applications in verification, knowledge representation, and modular reasoning
in combinations of local theories.
Coalgebraic Automata Theory: Basic Results
Authors: Kupke C. , Venema Y.
Published: January 2009

We generalize some of the central results in automata theory to the
abstraction level of coalgebras and thus lay out the foundations of a universal
theory of automata operating on infinite objects.
Let F be any set functor that preserves weak pullbacks. We show that the
class of recognizable languages of F-coalgebras is closed under taking unions,
intersections, and projections. We also prove that if a nondeterministic
F-automaton accepts some coalgebra it accepts a finite one of the size of the
automaton. Our main technical result concerns an explicit construction which
transforms a given alternating F-automaton into an equivalent nondeterministic
one, whose size is exponentially bound by the size of the original automaton.
A Rational Deconstruction of Landin's SECD Machine with the J Operator
Authors: Danvy Olivier , Millikin Kevin
Published: January 2009

Landin's SECD machine was the first abstract machine for applicative
expressions, i.e., functional programs. Landin's J operator was the first
control operator for functional languages, and was specified by an extension of
the SECD machine. We present a family of evaluation functions corresponding to
this extension of the SECD machine, using a series of elementary
transformations (transformation into continu-ation-passing style (CPS) and
defunctionalization, chiefly) and their left inverses (transformation into
direct style and refunctionalization). To this end, we modernize the SECD
machine into a bisimilar one that operates in lockstep with the original one
but that (1) does not use a data stack and (2) uses the caller-save rather than
the callee-save convention for environments. We also identify that the dump
component of the SECD machine is managed in a callee-save way. The caller-save
counterpart of the modernized SECD machine precisely corresponds to Thielecke's
double-barrelled continuations and to Felleisen's encoding of J in terms of
call/cc. We then variously characterize the J operator in terms of CPS and in
terms of delimited-control operators in the CPS hierarchy. As a byproduct, we
also present several reduction semantics for applicative expressions with the J
operator, based on Curien's original calculus of explicit substitutions. These
reduction semantics mechanically correspond to the modernized versions of the
SECD machine and to the best of our knowledge, they provide the first syntactic
theories of applicative expressions with the J operator.
Bisimilarity and Behaviour-Preserving Reconfigurations of Open Petri Nets
Authors: Baldan Paolo , Corradini Andrea , Ehrig Hartmut , Heckel Reiko , König Barbara
Published: January 2009

We propose a framework for the specification of behaviour-preserving
reconfigurations of systems modelled as Petri nets. The framework is based on
open nets, a mild generalisation of ordinary Place/Transition nets suited to
model open systems which might interact with the surrounding environment and
endowed with a colimit-based composition operation. We show that natural
notions of bisimilarity over open nets are congruences with respect to the
composition operation. The considered behavioural equivalences differ for the
choice of the observations, which can be single firings or parallel steps.
Additionally, we consider weak forms of such equivalences, arising in the
presence of unobservable actions. We also provide an up-to technique for
facilitating bisimilarity proofs. The theory is used to identify suitable
classes of reconfiguration rules (in the double-pushout approach to rewriting)
whose application preserves the observational semantics of the net.
Recursive Concurrent Stochastic Games
Authors: Etessami Kousha , Yannakakis Mihalis
Published: January 2009

We study Recursive Concurrent Stochastic Games (RCSGs), extending our recent
analysis of recursive simple stochastic games to a concurrent setting where the
two players choose moves simultaneously and independently at each state. For
multi-exit games, our earlier work already showed undecidability for basic
questions like termination, thus we focus on the important case of single-exit
RCSGs (1-RCSGs).
We first characterize the value of a 1-RCSG termination game as the least
fixed point solution of a system of nonlinear minimax functional equations, and
use it to show PSPACE decidability for the quantitative termination problem. We
then give a strategy improvement technique, which we use to show that player 1
(maximizer) has \epsilon-optimal randomized Stackless & Memoryless (r-SM)
strategies for all \epsilon > 0, while player 2 (minimizer) has optimal r-SM
strategies. Thus, such games are r-SM-determined. These results mirror and
generalize in a strong sense the randomized memoryless determinacy results for
finite stochastic games, and extend the classic Hoffman-Karp strategy
improvement approach from the finite to an infinite state setting. The proofs
in our infinite-state setting are very different however, relying on subtle
analytic properties of certain power series that arise from studying 1-RCSGs.
We show that our upper bounds, even for qualitative (probability 1)
termination, can not be improved, even to NP, without a major breakthrough, by
giving two reductions: first a P-time reduction from the long-standing
square-root sum problem to the quantitative termination decision problem for
finite concurrent stochastic games, and then a P-time reduction from the latter
problem to the qualitative termination problem for 1-RCSGs.
Multi-Objective Model Checking of Markov Decision Processes
Authors: Etessami Kousha , Kwiatkowska Marta , Vardi Moshe Y. , Yannakakis Mihalis
Published: January 2009

We study and provide efficient algorithms for multi-objective model checking
problems for Markov Decision Processes (MDPs). Given an MDP, M, and given
multiple linear-time (\omega -regular or LTL) properties \varphi\_i, and
probabilities r\_i \epsilon [0,1], i=1,...,k, we ask whether there exists a
strategy \sigma for the controller such that, for all i, the probability that a
trajectory of M controlled by \sigma satisfies \varphi\_i is at least r\_i. We
provide an algorithm that decides whether there exists such a strategy and if
so produces it, and which runs in time polynomial in the size of the MDP. Such
a strategy may require the use of both randomization and memory. We also
consider more general multi-objective \omega -regular queries, which we
motivate with an application to assume-guarantee compositional reasoning for
probabilistic systems.
Note that there can be trade-offs between different properties: satisfying
property \varphi\_1 with high probability may necessitate satisfying \varphi\_2
with low probability. Viewing this as a multi-objective optimization problem,
we want information about the "trade-off curve" or Pareto curve for maximizing
the probabilities of different properties. We show that one can compute an
approximate Pareto curve with respect to a set of \omega -regular properties in
time polynomial in the size of the MDP.
Our quantitative upper bounds use LP methods. We also study qualitative
multi-objective model checking problems, and we show that these can be analysed
by purely graph-theoretic methods, even though the strategies may still require
both randomization and memory.
Incremental Value of the Pancreas Allograft to the Survival of Simultaneous Pancreas-Kidney Transplant Recipients
Authors: Salvalaggio Paolo R. , Dzebisashvili Nino , Pinsky Brett , Schnitzler Mark A. , Burroughs Thomas E. , Graff Ralph , Axelrod David A. , Brennan Daniel C. , Lentine Krista L.
Published: January 2009

OBJECTIVE

To quantify the incremental survival benefit of the pancreas allograft in simultaneous pancreas-kidney (SPK) transplant recipients.

RESEARCH DESIGN AND METHODS

Data from the national transplant database from 2000 to 2007 were analyzed. SPK recipients who had functioning allografts to 1-year post transplant (n = 3,304) were compared with those who had failure of the renal (n = 233) or pancreatic (n = 112) graft. The main outcome was a projection of 10 life-years of patient survival beyond the first transplant anniversary.

RESULTS

Recipients with function of both organs accrued 9.4 life-years following transplantation. Projected survival in patients with kidney failure was reduced to 2.5 life-years. Pancreas failure reduced predicted survival to 8 life-years. Renal allograft failure impacts life expectancy significantly (adjusted hazard ratio [aHR] 12.13). However, pancreas allograft failure was also associated with reduced survival (aHR 2.62).

CONCLUSIONS

Although the majority of the survival benefit of SPK transplant is due to the renal transplant, pancreas allograft function does contribute to patient survival.
Synergy Between Adiposity, Insulin Resistance, Metabolic Risk Factors, and Inflammation in Adolescents
Authors: Huang Rae-Chi , Mori Trevor A. , Burke Valerie , Newnham John , Stanley Fiona J. , Landau Louis I. , Kendall Garth E. , Oddy Wendy H. , Beilin Lawrence J.
Published: January 2009

OBJECTIVE

The purpose of this study was to investigate relationships between inflammatory markers and components of a metabolic syndrome cluster in adolescents.

RESEARCH DESIGN AND METHODS

This was a cross-sectional analysis of an Australian childhood cohort (n = 1,377) aged 14 years. Cluster analysis defined a “high-risk” group similar to adults with metabolic syndrome. Relevant measures were anthropometry, fasting insulin, glucose, lipids, inflammatory markers, liver function, and blood pressure.

RESULTS

Of the children, 29% fell into a high-risk metabolic cluster group compared with 2% by a pediatric metabolic syndrome definition. Relative to the “low-risk” cluster, they had higher BMI (95% CI 19.5–19.8 vs. 24.5–25.4), waist circumference (centimeters) (95% CI 71.0–71.8 vs. 83.4–85.8), insulin (units per liter) (95% CI 1.7–1.8 vs. 3.5–3.9), homeostasis model assessment (95% CI 1.7–1.8 vs. 3.5–3.9), systolic blood pressure (millimeters of mercury) (95% CI 110.8–112.1 vs. 116.7–118.9), and triglycerides (millimoles per liter) (95% CI 0.78–0.80 vs. 1.25–1.35) and lower HDL cholesterol (millimoles per liter) (95% CI 1.44–1.48 vs. 1.20–1.26). Inflammatory and liver function markers were higher in the high-risk group: C-reactive protein (CRP) (P < 0.001), uric acid (P < 0.001), alanine aminotransferase (ALT) (P < 0.001), and γ-glutamyl transferase (GGT) (P < 0.001). The highest CRP, GGT, and ALT levels were restricted to overweight children in the high-risk group.

CONCLUSIONS

Cluster analysis revealed a strikingly high proportion of 14 year olds at risk of cardiovascular disease–related metabolic disorders. Adiposity and the metabolic syndrome cluster are synergistic in the pathogenesis of inflammation. Systemic and liver inflammation in the high-risk cluster is likely to predict diabetes, cardiovascular disease, and nonalcoholic fatty liver disease.
Affine compact almost-homogeneous manifolds of cohomogeneity one
Authors: Guan Daniel
Published: January 2009

This paper is one in a series generalizing our results in [12, 14, 15, 20] on the existence of extremal metrics to the general almost-homogeneous manifolds of cohomogeneity one. In this paper, we consider the affine cases with hypersurface ends. In particular, we study the existence of Kähler-Einstein metrics on these manifolds and obtain new Kähler-Einstein manifolds as well as Fano manifolds without Kähler-Einstein metrics. As a consequence of our study, we also give a solution to the problem posted by Ahiezer on the nonhomogeneity of compact almost-homogeneous manifolds of cohomogeneity one; this clarifies the classification of these manifolds as complex manifolds. We also consider Fano properties of the affine compact manifolds.
Stable outer conjugacy and strong Morita equivalence of group actions on pro-C *-algebras
Authors: Joiţa Maria
Published: January 2009

We show that two continuous inverse limit actions α and β of a locally compact group G on two pro-C *-algebras A and B are stably outer conjugate if and only if there is a full Hilbert A-module E and a continuous action u of G on E such that E and E *(the dual module of E) are countably generated in M(E)(the multiplier module of E), respectively M(E *) and the pair (E, u) implements a strong Morita equivalence between α and β. This is a generalization of a result of F. Combes [Proc. London Math. Soc. 49(1984), 289–306].
On an inequality of Oprea for Lagrangian submanifolds
Authors: Dillen Franki , Fastenakels Johan
Published: January 2009

We show that a Lagrangian submanifold of a complex space form attaining equality in the inequality obtained by Oprea in [8], must be totally geodesic.
Gastrocnemius-Soleus Muscle Tendon Unit Changes Over the First 12 Weeks of Adjusted Age in Infants Born Preterm
Authors: Grant-Beuttler Marybeth , Palisano Robert J , Miller Debra P , Reddien Wagner Barbara , Heriza Carolyn B , Shewokis Patricia A
Published: January 2009

Background and Purpose

Differences in the gastrocnemius-soleus muscle and tendon have been documented shortly after birth in infants born preterm compared with infants born at term. Knowledge of muscle tendon unit lengths at term age to 12 weeks of age in infants born preterm may be useful in understanding motor development.

Participants and Method

Gastrocnemius-soleus muscle tendon unit lengths were compared at term age, at 6 weeks of age, and at 12 weeks of age (preterm adjusted age) in 20 infants born full term and 22 infants born preterm.

Results

Significant differences were found between the 2 groups on taut tendon, relaxed muscle length (AO); taut tendon, stretched muscle length (AMax); and muscle stretch (AO to AMax). Infants born preterm demonstrated measures of AO and AMax in positions of greater plantar flexion compared with infants born full term. Significant differences in measurements of AO were found between term age and 12 weeks of age, indicating that the tendon lengthens during this period for both groups.

Discussion and Conclusion

These results provide knowledge of musculoskeletal development of the gastrocnemius-soleus muscle and tendon. Differences in musculoskeletal measurements are consistent with uterine confinement in the last weeks of full-term gestation. These findings have implications when examining the musculoskeletal system in infants born preterm who are demonstrating functional changes.
Physical Therapy Health Human Resource Ratios: A Comparative Analysis of the United States and Canada
Authors: Landry Michel D , Ricketts Thomas C , Fraher Erin , Verrier Molly C
Published: January 2009

Background and Purpose

Health human resource (HHR) ratios are a measure of workforce supply and are expressed as a ratio of the number of health care practitioners to a subset of the population. Health human resource ratios for physical therapists have been described for Canada but have not been fully described for the United States. In this study, HHR ratios for physical therapists across the United States were estimated in order to conduct a comparative analysis of the United States and Canada.

Methods

National US Census Bureau data were linked to jurisdictional estimates of registered physical therapists to create HHR ratios at 3 time points: 1995, 1999, and 2005. These results then were compared with the results of a similar study conducted by the same authors in Canada.

Results

The national HHR ratio across the United States in 1995 was 3.8 per 10,000 people; the ratio increased to 4.3 in 1999 and then to 6.2 in 2005. The aggregated results indicated that HHR ratios across the United States increased by 61.3% between 1995 and 2005. In contrast, the rate of evolution of HHR ratios in Canada was lower, with an estimated growth of 11.6% between 1991 and 2005. Although there were wide variations across jurisdictions, the data indicated that HHR ratios across the United States increased more rapidly than overall population growth in 49 of 51 jurisdictions (96.1%). In contrast, in Canada, the increase in HHR ratios surpassed population growth in only 7 of 10 jurisdictions (70.0%).

Discussion and Conclusion

Despite their close proximity, there are differences between the United States and Canada in overall population and HHR ratio growth rates. Possible reasons for these differences and the policy implications of the findings of this study are explored in the context of forecasted growth in demand for health care and rehabilitation services.
Harris Infant Neuromotor Test: Comparison of US and Canadian Normative Data and Examination of Concurrent Validity With the Ages and Stages Questionnaire
Authors: Westcott McCoy Sarah , Bowman Alicia , Smith-Blockley Jessica , Sanders Katie , Megens Antoinette M , Harris Susan R
Published: January 2009

Background

The Harris Infant Neuromotor Test (HINT) was developed as a screening tool for potential motor and cognitive developmental disorders in infants. Scoring on the HINT has been shown to be reliable, and several studies have supported the validity of the HINT. Normative values for the tool have been developed using Canadian infants.

Objective

The aims of this study were (1) to further evaluate the validity of the HINT by comparing data obtained on US infants who were developing typically with data previously acquired on Canadian infants and (2) to determine the concurrent validity of the HINT with the Ages and Stages Questionnaire (ASQ). Secondary analyses of HINT scores for US white and nonwhite infants and for US infants who had parents with lower levels of education and US infants who had parents with higher levels of education (as a proxy for socioeconomic status [SES]) were conducted.

Design

Cross-sectional exploratory and quasi-experimental comparative research designs were used to evaluate the validity of the HINT.

Methods

Sixty-seven infants from the United States who were developing typically and who were aged 2.5 to 12.5 months were recruited via convenience sampling. Sixty-four of these infants were compared with Canadian infants matched for age, sex, ethnicity or race, and parental education. The HINT was administered by raters who had been trained to attain acceptable levels of interrater reliability, and parents completed the ASQ. The HINT scores for US white versus nonwhite infants (n=46) and infants who had parents with lower SES versus a higher SES (n=52) were compared.

Results

There were no significant differences between HINT total scores for US and Canadian infants or for US racial or ethnic groups and SES groups. There were high correlations (r=−.82 to −.84) between HINT and ASQ scores.

Limitations

The study used a small US sample with limited geographical diversity. Small sample numbers also did not allow for comparisons of specific racial or ethnic groups. The SES groups were created primarily using parental education as a proxy for SES.

Conclusions

The results suggest that HINT screening in the United States is supported on the basis of Canadian norms and the validity of the HINT in screening for motor and cognitive delays. Although there is preliminary support for the HINT as an appropriate screening tool for US infants who are nonwhite or who have parents with a lower SES, more research is warranted.
Applications of Micro-Raman Spectroscopy in Cultural Heritage – Examples from the Laboratory for Conservation Research of the Collections Centre of the Swiss National Museums
Authors: Berger Olivier , Yersin Pascale Bonnard , Yersin Jean-Marc Bonnard , Hartmann Chantal , Hildbrand Erwin , Hubert Vera , Hunger Katja , Ramstein Marianne , Wörle Marie
Published: January 2009

The paper reports on three applications of micro-Raman spectroscopy which were carried out in the Laboratory for Conservation Research of the Collections Centre of the Swiss National Museums. The first application addresses archaeological questions about three early mediaeval fibulae
which were decorated with gemstones. The determination of different corrosion products on pigeon cameras by micro-Raman spectroscopy is described in the second part of this article. The last case study discusses an example from the field of preventive conservation where changes on metal coupons
from the so-called Oddy test were analysed.