Search

The existing techniques for reachability analysis of linear hybrid automata do not scale well to problem sizes of practical interest. Instead of developing a tool to perform reachability check on all the paths of a linear hybrid automaton, a complementary approach is to develop an efficient path-oriented tool to check one path at a time where the length of the path being checked can be made very large and the size of the automaton can be made large enough to handle problems of practical interest. This approach of symbolic execution of paths can be used by design engineers to check important paths and thereby, increase the faith in the correctness of the system. Unlike simple testing, each path in our framework represents a dense set of possible trajectories of the system being analyzed. In this paper, we develop the linear programming based techniques towards an efficient path-oriented tool for the bounded reachability analysis of linear hybrid systems.

Identifying a bona fide population of cardiac stem cells (CSCs) is a critical step for developing cell-based therapies for heart failure patients. Previously, cardiac c-kit+ cells were reported to be CSCs with a potential to become myocardial, endothelial and smooth muscle cells in vitro and after cardiac injury. Here we provide further insights into the nature of cardiac c-kit+ cells. By targeting the c-kit locus with multiple reporter genes in mice, we find that c-kit expression rarely co-localizes with the expression of the cardiac progenitor and myogenic marker Nkx2.5, or that of the myocardial marker, cardiac troponin T (cTnT). Instead, c-kit predominantly labels a cardiac endothelial cell population in developing and adult hearts. After acute cardiac injury, c-kit+ cells retain their endothelial identity and do not become myogenic progenitors or cardiomyocytes. Thus, our work strongly suggests that c-kit+ cells in the murine heart are endothelial cells and not CSCs., The issue whether the cell surface protein c-kit identifies resident cardiac stem cells (CSC) is controversial. By using novel reporter mouse models, Sultana et al. show that c-kit+ cells represent a subpopulation of endothelial cells in the developing and adult heart and do not exhibit CSC traits in health or disease.

Cardiac progenitor cells (CPCs) have the capacity to differentiate into cardiomyocytes, smooth muscle cells (SMC), and endothelial cells and hold great promise in cell therapy against heart disease. Among various methods to isolate CPCs, differentiation of embryonic stem cell (ESC) into CPCs attracts great attention in the field since ESCs can provide unlimited cell source. As a result, numerous strategies have been developed to derive CPCs from ESCs. In this protocol, differentiation and purification of embryonic CPCs from both mouse and human ESCs is described. Due to the difficulty of using cell surface markers to isolate embryonic CPCs, ESCs are engineered with fluorescent reporters activated by CPC-specific cre recombinase expression. Thus, CPCs can be enriched by fluorescence-activated cell sorting (FACS). This protocol illustrates procedures to form embryoid bodies (EBs) from ESCs for CPC specification and enrichment. The isolated CPCs can be subsequently cultured for cardiac lineage differentiation and other biological assays. This protocol is optimized for robust and efficient derivation of CPCs from both mouse and human ESCs.

Terminal capacity and performance have become a major concern for rail transit agencies in China due to the ever increasing passenger demand. This paper develops a mixed integer programming (MIP) optimization model to estimate the turnback capacity and performance of a rail transit terminal with two-tail tracks. The capacity evaluation and delay propagation are described and assessed as anN-track integrated model with minimal time span and train delay. Operations and design parameters such as tail track allocation strategies, maximum layover time, headway pattern, buffer time distribution scheme, and primary delay are also considered in this model. The effectiveness of the model is tested by a case study with computation results drawn from one terminal station in Shanghai, China. The case study results show that unfixed platform time and flexible tail track allocation strategies can improve the capacity of turnback operation, and the strategy of allowing swapping of the tail tracks has a significantly positive impact on delay absorption.

Cardiogenesis requires the generation of endothelial, cardiac, and smooth muscle cells, thought to arise from distinct embryonic precursors. We use genetic fate-mapping studies to document that isl1(+) precursors from the second heart field can generate each of these diverse cardiovascular cell types in vivo. Utilizing embryonic stem (ES) cells, we clonally amplified a cellular hierarchy of isl1(+) cardiovascular progenitors, which resemble the developmental precursors in the embryonic heart. The transcriptional signature of isl1(+)/Nkx2.5(+)/flk1(+) defines a multipotent cardiovascular progenitor, which can give rise to cells of all three lineages. These studies document a developmental paradigm for cardiogenesis, where muscle and endothelial lineage diversification arises from a single cell-level decision of a multipotent isl1(+) cardiovascular progenitor cell (MICP). The discovery of ES cell-derived MICPs suggests a strategy for cardiovascular tissue regeneration via their isolation, renewal, and directed differentiation into specific mature cardiac, pacemaker, smooth muscle, and endothelial cell types.

The LIM homeodomain transcription factor Islet1 (Isl1) is expressed in both foregut endoderm and cardiogenic mesoderm and is required for earliest stages of heart development. Here, we report that isl1 is also required upstream of Shh. We find that, in isl1 null mice, Sonic hedgehog (Shh) is downregulated in foregut endoderm. Shh signals through the unique activating receptor smoothened (Smo). To investigate the role of hedgehog signaling in the isl1 domain, we ablated smo utilizing isl1-cre. Isl1-cre;smo mutants exhibit cardiovascular defects similar to those observed in Shh null mice, defining a spatial requirement for hedgehog signaling within isl1 expression domains for aortic arch and outflow tract formation. Semaphorin signaling through neuropilin receptors npn1 and npn2 is required for aortic arch and outflow tract formation. We find that expression of npn2 is downregulated in isl1-cre;smo mutants, suggesting an isl1/Shh/npn pathway required to affect morphogenesis at the anterior pole of the heart.

Chromosome 5p, especially 5p15, involves in several cancers. To investigate its role in gastric cancer, we analyzed 46 intestinal-type and 34 diffuse-type gastric cancers by Loss of heterozygosity (LOH). We found a high frequent LOH at 5p15.33, and identified a minimal 2.7 cM candidate region of tumor suppressor gene, encompassing four loci (D5S417, D5S2849, D5S1492 and D5S2088). In total 80 cases, the highest LOH occurs at D5S2849 (35.19%). In intestinal-type cases, the highest LOH frequency is 50%, whereas in diffuse-type cases, the highest is only 16.67%. By statistical analysis we also observed an obvious genotype–phenotype correlation on 5p15.3 ( P

Mutations in T-box genes are the cause of several congenital diseases and are implicated in cancer. Tbx20-null mice exhibit severely hypoplastic hearts and express Tbx2, which is normally restricted to outflow tract and atrioventricular canal, throughout the heart. Tbx20 mutant hearts closely resemble those seen in mice overexpressing Tbx2 in myocardium,suggesting that upregulation of Tbx2 can largely account for the cardiac phenotype in Tbx20-null mice. We provide evidence that Tbx2 is a direct target for repression by Tbx20 in developing heart. We have also found that Tbx2 directly binds to the Nmyc1 promoter in developing heart, and can repress expression of the Nmyc1 promoter in transient transfection studies. Repression of Nmyc1 (N-myc) by aberrantly regulated Tbx2 can account in part for the observed cardiac hypoplasia in Tbx20 mutants. Nmyc1 is required for growth and development of multiple organs, including the heart, and overexpression of Nmyc1 is associated with childhood tumors. Despite its clinical relevance, the factors that regulate Nmyc1 expression during development are unknown. Our data present a paradigm by which T-box proteins regulate regional differences in Nmyc1 expression and proliferation to effect organ morphogenesis. We present a model whereby Tbx2 directly represses Nmyc1 in outflow tract and atrioventricular canal of the developing heart, resulting in relatively low proliferation. In chamber myocardium, Tbx20 represses Tbx2,preventing repression of Nmyc1 and resulting in relatively high proliferation. In addition to its role in regulating regional proliferation, we have found that Tbx20 regulates expression of a number of genes that specify regional identity within the heart, thereby coordinating these two important aspects of organ development.

Slot bottom size has directly effect on conductor abrasion,Chinese Technical Regulation of design for Stringing blocks of overhead transmission lines (DL/T371-2010) clearly states that slot bottom size should be no less than 20 times of the size of conductor to be extended. In this paper, based on effect of slot bottom size on conductor abrasion,the size of slot bottom of stringing pulley is analyzed. Some useful suggestions are given.

Conductor scheme is one of key issues in the design of the UHVDC transmission project, and it is significant for the construction cost and safe operation of transmission line. It can be concluded from analysis on application of existing conductor that the appropriate decrease in number of bundle conductor and increase of the conductor cross-section will reduce line loss, which has remarkable social-economic benefits. In this paper, the economic analysis of large cross-section conductor is conducted based on UHVDC Project. Some useful suggestions are given.

Disseminated superficial porokeratosis (DSP) is a rare autosomal dominant epidermal keratinization disorder of lesions characterized by cornoid lamella with parakeratosis, hyperkeratosis, and loss of granular layers. The genetic basis for this disease is unknown. Through a proband with a diagnosis of DSP, we identified a large four-generation Chinese family with multiple DSP-affected members from Anhui province in China. After excluding the linkage of the disease phenotype to two known loci for disseminated superficial actinic porokeratosis in this family, we performed a genome-wide linkage analysis using 387 microsatellite markers and identified a novel disease locus for DSP at 18p11.3. Our subsequent fine mapping and haplotype analyses further narrowed down the disease locus into an 18.7 cM region between the telomere and D18S391 with a maximum two-point LOD (logarithm of the odds) score of 4.82 (theta =0.00) at D18S1138. Therefore, this study provides strong linkage evidence for a DSP locus at 18p11.3.

Background Porokeratosis palmaris et plantaris disseminata (PPPD) is a rare autosomal dominant dyskeratotic disorder characterized by a cornoid lamella with parakeratosis, hyperkeratosis and loss of granular layers. The genetic basis of this disease is still unknown. Two loci for disseminated superficial actinic porokeratosis (DSAP) were found to be located on 12q23.2-24.1 and 15q25.1-26.1. Both PPPD and DSAP are disseminated types of porokeratosis. Objectives To locate the locus for PPPD, thereby facilitating the identification of this disease gene and leading to an understanding of the pathogenesis of porokeratosis. Methods Genotyping was performed in a Chinese family with PPPD using polymorphic microsatellite markers on 12q and 15q. Results The locus for PPPD is located within a 6.9-cM region between markers D12S1613 and D12S1341, with a maximum two-point LOD score of 8.14 (theta = 0.00) at D12S1335. Conclusions This study provides a map location for isolation of a gene causing PPPD.

Tnnt2, encoding thin-filament sarcomeric protein cardiac troponin T, plays critical roles in heart development and function in mammals. To develop an inducible genetic deletion strategy in myocardial cells, we generated a new Tnnt2:MerCreMer (Tnnt2(MerCreMer/+)) knock-in mouse. Rosa26 reporter lines were used to examine the specificity and efficiency of the inducible Cre recombinase. We found that Cre was specifically and robustly expressed in the cardiomyocytes at embryonic and adult stages following tamoxifen induction. The knock-in allele on Tnnt2 locus does not impact cardiac function. These results suggest that this new Tnnt2(MerCreMer/+) mouse could be applied towards the temporal genetic deletion of genes of interests in cardiomyocytes with Cre-LoxP technology. The Tnnt2(MerCreMer/+) mouse model also provides a useful tool to trace myocardial lineage during development and repair after cardiac injury.

Control Cyber-Physical Systems (CPS) is a major category of CPS. In control CPS, besides the well-studied noises within the physical control subsystem, we are particularly interested in better understanding cross-domain noises: those come from the “physical” control subsystem, propagate through the “cyber” computing subsystem, and go back to the physical subsystem. The focus of this paper is to propose a framework to profile the propagation of cross-domain noises.

Rosa26 -targeted swine models for stable gene over-expression and Cre-mediated lineage tracing

Gingival fibromatosis ( GINGF ) is an oral disorder characterized by enlargement of the gingiva. It occurs either as the sole phenotype or combined with other symptoms. Thus far, one GINGF locus has been mapped on chromosome 2, at 2p21, and a second possible locus has been mapped to 2p13. However, the genes responsible for this disorder have not been elucidated. We identified a four-generation Chinese GINGF family in which the disease manifests within 1 year after birth. After exclusion of the two known GINGF loci in this family, we performed a genome-wide search to map the chromosome location of the responsible gene. We identified a new locus, GINGF2, on chromosome 5q13–q22 with a maximum two-point lod score of 4.31 at D5S1721 (θ = 0.00). Haplotype analysis placed the critical region in the interval defined by D5S1491 and D5S1453. Within this region, calcium/calmodulin-dependent protein kinase IV ( CAMK4 ) is a strong candidate.

Dentinogenesis imperfecta 1 (DGI1, MIM 125490) is an autosomal dominant dental disease characterized by abnormal dentin production and mineralization. The DGI1 locus was recently refined to a 2-Mb interval on 4q21 (ref. 1). Here we study three Chinese families carrying DGI1. We find that the affected individuals of two families also presented with progressive sensorineural high-frequency hearing loss (gene DFNA39). We identified three disease-specific mutations within the dentin sialophosphoprotein gene (DSPP) in these three families. We detected a G→A transition at the donor-splicing site of intron 3 in one family without DFNA39, a mutation predicted to result in the skipping of exon 3. In two other families affected with both DGI1 and DFNA39, however, we identified two independent nucleotide transversions in exons 2 and 3 of DSPP, respectively, that cause missense mutations of two adjacent amino-acid residues in the predicted transmembrane region of the protein. Moreover, transcripts of DSPP previously reported to be expressed specifically in teeth2 are also detected in the inner ear of mice. We have thus demonstrated for the first time that distinct mutations in DSPP are responsible for the clinical manifestations of DGI1 with or without DFNA39.

Cyber-Physical Systems (CPS) integrate discrete-time computing and continuous-time physical-world entities, which are often wirelessly interlinked. The use of wireless safety critical CPS (control, healthcare etc.) requires safety guarantees despite communication faults. This paper focuses on one important set of such safety rules: Proper-Temporal-Embedding (PTE). Our solution introduces hybrid automata to formally describe and analyze CPS design patterns. We propose a novel lease based design pattern, along with closed-form configuration constraints, to guarantee PTE safety rules under arbitrary wireless communication faults. We propose a formal methodology to transform the design pattern hybrid automata into specific wireless CPS designs. This methodology can effectively isolate physical world parameters from affecting the PTE safety of the resultant specific designs. We conduct a case study on laser tracheotomy wireless CPS to show that the resulting system is safe and can withstand communication disruptions.

Ichthyosis vulgaris (IV) is an inherited scaling skin disorder with a prevalence estimated at 2.29% in China. The gene responsible for this disorder has not been elucidated. To find the disease gene, we ascertained two Chinese IV families. Linkage analysis identified an IV locus on chromosome 1q22 with a maximum two-point Lod score of 2.47 at D1S1653 (theta=0.00). Haplotype analysis placed the critical region in a 7-cM interval defined by D1S1653 and D1S2675. These results provide the basis for further identifying the gene responsible for IV disorder.

Automatically generating test data to cover a given path is a challenging problem. This paper present a program execution based approach driven by component linear fitting functions. Here, component linear fitting functions built on inputs and values at decision points, are used to approximate constraints. They drive the search to reach constraints' solutions by calculating feasible intervals. Experiments show that the approach is effective and has good potentiality in treating nonlinear constraints and constraints with many local optimal points.

As most of the CPS systems are working in open environment, many control parameters used in the systems are generated online. The exact values of these parameters are unpredictable offline in advance. This causes the behavior of the CPS model has high nondeterminism and can not be verified by model checking in the design phase. To overcome this problem, we proposed that the modeling and verification of CPS system should be conducted online and focus on the system's time-bounded behavior in short-run future. In this demo, we present a tool BACHOL which can handle the online modeling and verification of parametric linear hybrid automata. We use a simulation of a state-of-the-art train control system to show how BACHOL can be deployed online to predict error before it happen, and strengthen the reliability of the system.

Timing-sync Protocol for Sensor Networks (TPSN) is a widely used protocol which provides network-wide time synchronization in a sensor network. We use formal methods to study it thoroughly in this poster. First of all, we model the protocol with timed automata which can describe the workflow of TPSN in an ideal environment. However, in realistic circumstances, there are many uncertainties, for example, message loss and node dynamics. Thus, we extend our model with probabilities to describe these uncertainties. Besides verifying the system against several critical functional properties, we also show that it is also possible to evaluate the performance of TPSN by statistical model checking to estimate how it works in realistic environments.

Heart diseases such as myocardial infarction cause massive loss of cardiomyocytes, but the human heart lacks the innate ability to regenerate. In the adult mammalian heart, a resident progenitor cell population, termed epicardial progenitors, has been identified and reported to stay quiescent under uninjured conditions; however, myocardial infarction induces their proliferation and de novo differentiation into cardiac cells. It is conceivable to develop novel therapeutic approaches for myocardial repair by targeting such expandable sources of cardiac progenitors, thereby giving rise to new muscle and vasculatures. Human pluripotent stem cells such as embryonic stem cells and induced pluripotent stem cells can self-renew and differentiate into the three major cell types of the heart, namely cardiomyocytes, smooth muscle, and endothelial cells. In this review, we describe our current knowledge of the therapeutic potential and challenges associated with the use of pluripotent stem cell and progenitor biology in cell therapy. An emphasis is placed on the contribution of paracrine factors in the growth of myocardium and neovascularization as well as the role of immunogenicity in cell survival and engraftment.

In this work we investigated the possibility to use CNT film strain gauge on the metallic surface. Brass cantilever was used to investigate the tensile and compressive strain sensing property of MWCNT films. Two types of isolation layer were used between MWCNT film and brass cantilever, ink jet film and aerosol varnish. From the measurements we found higher gauge factor can be obtained by using aerosol varnish as isolation layer due to a better transfer of loading. CNT films produced by two types of MWCNTs have different conductivity and gauge factor. By choosing the suitable CNTs, compromise should thus be made between conductivity and reproducibility as well as the sensitivity depending on the different applications. MWCNT-polymer (Polyethylene oxide, PEO) composites with different MWCNT weight fractions were also produced to obtain higher and tailored gauge factor. Higher gauge factor of 10 can be achieved for MWCNT-PEO composite film with 2.5wt% MWCNTs. Tailored gauge factor can be achieved by changing the MWCNT concentration.

In the authors' previous work, we proposed a linear programming (LP) based approach to check the reachability specification along one abstract path in a linear hybrid automaton (LHA) at a time by translating the reachability problem into the satisfiability problem of a linear constraint set. Then a depth-first-search (DFS) is deployed on the graph structure of the LHA to check all the paths with length in the threshold to answer the question of bounded reachability. In this DFS-style bounded model checking (BMC) algorithm, once a path is found to be infeasible by the underlying LP solver, a backtracking on the graph structure will be conducted. Clearly, the efficiency of the algorithm depends on the accuracy of the backtracking. If the DFS can backtrack to the most reasonable location, the state space need to search and verify can be reduced significantly. Fortunately, once a linear constraint set is judged to be unsatisfiable, the irreducible infeasible set (IIS) technique can be deployed on the unsatisfiable constraint set to give a quick analysis and find a small set of constraints which makes the whole program unsatisfiable. In this paper, we adopt this technique into our DFS-style BMC of LHA to locate the nodes and transitions which make the path under verification infeasible to guide the backtracking and answer the bounded reachability of LHA more efficiently.

Congenital cataracts cause 10–30% of all blindness in children, with one-third of cases estimated to have a genetic cause1. Lamellar cataract is the most common type of infantile cataract2. We carried out whole-genome linkage analysis of Chinese individuals with lamellar cataract, and found that the disorder is associated with inheritance of a 5.11-cM locus on chromosome 16. This locus coincides with one previously described for Marner cataract3. We screened individuals of three Chinese families for mutations in HSF4 (a gene at this locus that encodes heat-shock transcription factor 4) and discovered that in each family, a distinct missense mutation, predicted to affect the DNA-binding domain of the protein, segregates with the disorder. We also discovered an association between a missense mutation and Marner cataract in an extensive Danish family. We suggest that HSF4 is critical to lens development.

Transshipment work of multimodal freight at the railway container center station is a very complex process, as it is restricted by time, space and its own features. In order to optimize the transshipment operation, we need firstly to manage all the key information of multimodal freight. This paper studies the design of the MIS of container freight transshipment at railway container center stations on the basis of the key spatio-temporal data of the railway container center stations and the multimodal container freight coming from the original sea ports to the destination sea port. The function and module of this system is described.

Being nodes of intermodal transport network, the railway container terminals need to make efficient plans over transshipment operation to guarantee punctuality of the whole transport network. This paper takes multimodal freight that needs to be repacked as the object of study. It looks into the main factors that cause freight delay through investigation of multimodal freight delay phenomenon during transshipment operation in railway container terminals. Combining the practical requirement of transshipment operation of multimodal freight, an evaluation index system of transshipment and repacking solutions in railway container terminals is proposed. This evaluation index system can be used to range the work of loading and reloading containers for further improvement.

Since Wireless Sensor Networks (WSNs) are increasingly used in many industrial and civilian application areas, the correctness of their low level protocol such as the Flooding Time Synchronization Protocol (FTSP) is critical. However ensuring such correctness is difficult because of the complexity of the runtime environment. Model checking is an effective method for this problem, since it is a formal verification approach which has an advantage in exploring all behaviors of the system and discovering subtle errors. In this paper, we present a novel timed automaton model for FTSP. The main insight of our method is that by using timed automata, we can introduce the transmission delay and node failures that exist in real WSNs into our model and check whether FTSP is robust to node failures under a more realistic environment. We generate the timed automata models of FTSP and verify them by the model checking tool UPPAAL. Our evaluation result depicts an error of FTSP when the algorithm runs in the scenario that two root nodes fail continuously.

Carbon nanotube (CNT) films made from sing-wall and multi-wall nanotubes (SWCNTs and MWCNTs) were investigated recently as strain gauge for strain sensing. The quality of CNT films is important thereby as well as for many related applications. In this paper relevant processing factors such as the sonication time and concentration of sodium dodecyl sulfate (SDS) are investigated to characterize their influences on electrical properties of the produced CNT films. The results show that sonication time plays an important role for the quality of CNT films. A longer sonication time realizes better homogeneity of the CNT films, lower resistance values and higher reproducibility of the specimens. SWCNT and MWCNT specimens were manufactured and measured for strain sensing. MWCNT specimens show a better sensing property than SWCNT specimens with an applied strain up to 1%. Two strain sensing regions for MWCNT films can be clearly recognized possibly due to the different response characteristics of contact resistance and tube resistance to external loading. As the strain is smaller than 0.1% the sensitivity of the MWCNT films is low, about 2.5. For the strain from 0.1% to 1% the sensitivity is about 5 and the sensing property is reproducibility. Results of SWCNT films are much complex compared to MWCNT films. For the strain smaller than 0.2% the resistance variation curves and the sensitivities of SWCNT films are similar to those of MWCNT films. The sensitivities decrease however for the strain from 0.2% to 0.3% and change dramatically and irreproducibility for the strain from 0.5% to 1%.

Hybrid automata are well-studied formal models for dynamical systems. However, the analysis of hybrid automata is extremely difficult, and even state-of-the-art tools can only analyze systems with few continuous variables and simple dynamics. Because the reachability problem for general hybrid automata is undecidable, we give a path-oriented reachability analysis procedure for a class of nonlinear hybrid automata called convex hybrid automata. Our approach encodes the reachability problem along a path of a convex hybrid automaton as a convex feasibility problem, which can be efficiently solved by off-the-shelf convex solvers, such as CVX. Our path-oriented reachability verification approach can be applied in the frameworks of bounded model checking and counterexample-guided abstraction refinement with the goal of achieving significant performance improvement for this subclass of hybrid automata.

In this paper, we present TASS which is a timing analyzer of scenario-based specifications. TASS accepts UML2.0 interaction models with general and expressive timing constraints and can be used for three kinds of timing analysis problems: the reachability analysis, the constraint conformance analysis, and the bounded delay analysis. The underlying technique of TASS is to reduce the timing analysis problems into linear programming problems.

In this paper, the three-dimensional bin packing optimization for freight transshipment in multimodal transportation is considered. The problem is to load a set of different size regular goods with given quantities in containers at the container transfer station, and the objective is to minimize the number of containers needed. The authors set up the mathematic model considering the general characteristic of container multi-modal transportation. The authors put out an immune algorithm for problem to enforce constringency. In this algorithm, effective antibody coding is designed in view of constraints of load capacity, loading mass, direction and sequence of placement, and affinity function is designed in view of constraints of loading stability and freight transportation time window. Computer simulation shows

Recent studies have demonstrated that the LIM homeodomain transcription factor Islet1 (Isl1) marks pluripotent cardiovascular progenitor cells and is required for proliferation, survival, and migration of recently defined second heart field progenitors. Factors that are upstream of Isl1 in cardiovascular progenitors have not yet been defined. Here we demonstrate that β-catenin is required for Isl1 expression in cardiac progenitors, directly regulating the Isl1 promoter. Ablation of β-catenin in Isl1-expressing progenitors disrupts multiple aspects of cardiogenesis, resulting in embryonic lethality at E13. β-Catenin is also required upstream of a number of genes required for pharyngeal arch, outflow tract, and/or atrial septal morphogenesis, including Tbx2, Tbx3, Wnt11, Shh, and Pitx2. Our findings demonstrate that β-catenin signaling regulates proliferation and survival of cardiac progenitors. © 2007 by The National Academy of Sciences of the USA., link_to_subscribed_fulltext

A mouse model that mediates temporal, specific, and efficient myocardial deletion with Cre-LoxP technology will be a valuable tool to determine the function of genes during heart formation. Mhy6 encodes a cardiac muscle specific protein: alpha-myosin heavy chain. Here, we generated a new Myh6-MerCreMer (Myh6(MerCreMer/+)) inducible Cre knock-in mouse by inserting a MerCreMer cassette into the Myh6 start codon. By crossing knock-in mice with Rosa26 reporter lines, we found the Myh6(MerCreMer/+) mice mediate complete Cre-LoxP recombination in cardiomyocytes after tamoxifen induction. X-gal staining and immunohistochemistry analysis revealed that Myh6-driven Cre recombinase was specifically activated in cardiomyocytes at embryonic and adult stages. Furthermore, echocardiography showed that Myh6(MerCreMer/+) mice maintained normal cardiac structure and function before and after tamoxifen administration. These results suggest that the new Myh6(MerCreMer/+) mouse can serve as a robust tool to dissect the roles of genes in heart development and function. Additionally, myocardial progeny during heart development and after cardiac injury can be traced using this mouse line.

To explore the relationship between loss of heterozygosity (LOH) of 5p with the histological phenotype in gastric cancer.Eighty pairs of tumor and adjacent normal mucosa samples were collected and genomic DNA was extracted. Total of 17 polymorphic microsatellite markers for 5p were used for LOH analysis. A part of samples were fixed in 10% buffered formalin and stained with HE. Histological type of gastric cancer was defined according to Lauren's classification.The average informative rate of all seventeen markers was 60.0%. The LOH at least in one locus was detected in 28 of the 80 (35.0%) cases. The highest LOH frequency occurring at D5S2849 (7.77 cM), with LOH frequency of 35.2% (19/54). The minimal LOH region was spanned from 6.67 to 9.41 cM (1.18 Mb, covering 2.7 cM), including D5S417, D5S2849, D5S1492 and D5S2088. In 28 with LOH, 24 (85.7%) cases were of intestinal type, and only 4 cases (14.3%) were of diffuse type. There is significant difference between LOH frequency in intestinal-type and diffuse-type gastric cancers (P0.01). Searching the NCBI database disclosed that this minimal deletion region at 5p15.33 covered 3 candidate genes, IRX1, IRX2, and CEI.The molecular events in 5p 15.33 may be related with the morphological differentiation and development of gastric cancer. Gastric cancer with LOH of 5p15.33 locus tends to develop in to intestinal type. The cluster of candidate genes in 5p15.33 may be closely implicated in carcinogenesis of intestinal type gastric carcinoma.

Scenario-based specifications such as message sequence charts (MSCs) offer an intuitive and visual way of describing design requirements. As one powerful formalism, Petri nets can model concurrency constraints in a natural way, and are often used in modelling system specifications and designs. Since there are gaps between MSC models and Petri net models, keeping consistency between these two kinds of models is important for the success of software development. In this paper, we use Petri nets to model concurrent systems, and consider the problem of checking Petri nets for scenario-based specifications expressed by message sequence charts. We develop the algorithms to solve the following two verification problems: the existential consistency checking problem, which means that a scenario described by a given MSC must happen during a Petri net runs, or any forbidden scenario described by a given MSC never happens during a Petri net run; and the mandatory consistency checking problem, which means that if a reference scenario described by the given MSCs occurs during a Petri net run, it must adhere to a scenario described by the other given MSC.

Aims . Hereditary non-polyposis colorectal cancer, thyroid medullary carcinoma, breast/ovarian cancer and gastric cancer/breast cancer syndrome are encountered in surgery. Some gastric cancer/breast cancer syndrome may be the result of a CDH1 germline mutation. This is the first report of CDH1 germline mutations gastric cancer/breast cancer syndrome in Chinese patients. Methods . Peripheral blood from the proband, as well as, her first and second degree relatives was collected and CDH1 gene exon 1–16 mutations were screened. E-cadherin/β-catenin proteins expression and histopathologic features were examined on gastric cancer/breast cancer tissues from the proband. Results . A C→T nucleotide substitution at exon 13 (mRNA 2200 locus, Accession number NM-004360) was found. This was a transition from GCC→GCT in DNA sequence (Ala154Ala). Diffuse-type gastric cancer and infiltrating ductal breast carcinoma were present. Both tumours preserved E-cadherin/β-catenin expression immunohistochemically. Conclusions . Familial cancer syndrome with diffuse-type gastric cancer/breast cancer proband in Chinese has a propensity of early onset during lifespan. No truncating or splice-site CDH1 mutations had been identified in this family. A silent nucleotide variation in exon 13 of the CDH1 gene may contribute to some forms of cancer susceptibility.

Autosomal dominant congenital cataract (ADCC) is a clinically and genetically heterogeneous lens disorder that usually presents as a sight-threatening trait in childhood. Here, we described a six-generation Chinese family presenting with morphologically homogeneous "nuclear pulverulent" cataracts.A whole genome scan was performed with polymorphic microsatellites in the Human MapPairs marker set, with special attention paid to known ADCC loci. Then we screened for mutations by direct sequencing.A significantly positive two-point LOD score was obtained at marker D13S175(Zmax=7.83, theta=0). Haplotype analysis indicated this disease was located at 13q11, close to GJA3. Upon screening for mutations in GJA3 in this family, we found a novel transition mutation (TTC-TTA) resulting in a Phenylalanine-Leucine substitution at the highly conserved codon 32 of the GJA3 protein. This mutation segregated with the affected members of the family.This finding is the first report of a mutation in the first transmembrane region of GJA3. Our study further confirmed that GJA3 plays a vital role in the maintenance of human lens transparency.

Hereditary gingival fibromatosis (HGF, MIM 135300; approved gene symbol GINGF) is an oral disease characterized by enlargement of gingiva. Recently, a locus for autosomal dominant HGF has been mapped to an 11-cM region on chromosome 2p21. In the current investigation, we genotyped four Chinese HGF families using polymorphic microsatellite markers on 2p21. The HOMOG test provided evidence for genetic homogeneity, with evidence for linkage in four families (heterogeneity versus homogeneity test HOMOG, χ2 = 0.00). A cumulative maximum two-point lod score of 5.04 was produced with marker D2S390 at a recombination frequency of θ = 0 in the four linked families. Haplotype analysis localized the hereditary gingival fibromatosis locus within the region defined by D2S352 and D2S2163. This region overlaps by 3.8 cM with the previously reported HGF region. Single-strand conformation polymorphism and sequence analysis of the coding region of cytochrome P450 1B1 (CYP1B1) excluded it as a likely candidate gene.

Replying to: V. M. Christoffels et al. , 10.1038/nature07916 (2009) We recognized the importance of confirming data from Cre lineage studies with an alternative approach, and thus used a fluorescent dye to lineage-label epicardial cells. This approach confirmed that epicardial cells contributed to myocytes within the heart1. In our experiments, we never observed Tbx18 mRNA within ventricles at embryonic day E10.5 to E11.5, although our RNA signal in epicardium at these stages is at least as strong as that observed by Christoffels et al.2. We note a discrepancy between amount of RNA staining (broadly throughout the middle of the ventricle) and protein staining (much more restricted) that Christoffels et al.2 observe at early stages. Reasons for discrepancies between our RNA in situ data and that of Christoffels et al. are unclear. Christoffels et al.2 detect Tbx18 intronic sequences by RT–PCR of E11.5 IVS, but do not provide data to demonstrate mature Tbx18 mRNA. Notably, we did observe active expression of Tbx18 in non-myocytes after E11.5 (ref. 1).

Objective The therapeutic effect of acupuncture in treating the patients with urine retention after spinal and craniocerebral injuries was observed.