Evidence for social anxiety and impaired social cognition in a mouse model of fragile X syndrome.

This study assessed social behavior in a mouse model of Fragile X syndrome (FXS), the Fmr1 tm1Cgr or Fmr1 "knockout" (KO) mouse. Both the KO and wild-type (WT) mice preferred to be near a novel conspecific than to be alone. However, during the initial interaction with a novel conspecific, (1) a greater proportion of the KO mice exhibited high levels of grooming; and (2) the average duration of nose contact with the stimulus mouse was significantly shorter for the KO mice, both indicative of increased arousal and/or anxiety. Both groups exhibited a robust novelty preference when the novel animal was a "preferred" mouse. However, when the novel mouse was a "nonpreferred" animal, both groups showed a diminished novelty preference but this effect was more pronounced for the WT mice. This blunted negative reaction of the KO mice to a nonpreferred animal may indicate that they were less proficient than controls in distinguishing between positive and negative social interactions. These findings provide support for the use of this animal model to study the autistic features of FXS and autism spectrum disorders. (PsycINFO Database Record (c) 2010 APA, all rights reserved)     

Specifying and proving properties of timed I/O automata using Tempo

Timed I/O automata (TIOA) is a mathematical framework for modeling and verification of distributed systems that involve discrete and continuous dynamics. TIOA can be used for example, to model a real-time software component controlling a physical process. The TIOA model is sufficiently general to subsume other models in use for timed systems. The Tempo Toolset, currently under development, is aimed at supporting system development based on TIOA specifications. The Tempo Toolset is an extension of the IOA toolkit, which provides a specification simulator, a code generator, and both model checking and theorem proving support for analyzing specifications. This paper focuses on the modeling of timed systems and their properties with TIOA and on the use of TAME4TIOA, the TAME (Timed Automata Modeling Environment) based theorem proving support provided in Tempo, for proving system properties, including timing properties. Several examples are provided by way of illustration.     

Triacylglycerols and regiospecific fatty acid analyses of philippine seed oils

Three Philippine seed oils, namely coconut (Cocos nucifera Linn.), pilinut (Canarium ovatum Engl.), and cashew (Anacardium occidentale Linn.), which were selected for their local abundance and availability, were examined for their triacylglycerol profiles and fatty acid compositions. Triacylglycerol molecular species in terms of carbon number and partition number were determined by gas chromatography and liquid chromatography, respectively. The distribution of fatty acids in the primary and secondary positions of the glycerol backbones for the three oils were examined by regiospecific analysis by using pancreatic lipase. Coconut oil had high concentrations of lauric and myristic acids, while the other two oils did not have such fatty acids. Lauric acid in coconut oil and linoleic acid in pilinut oil were distributed mainly in the primary positions (sn-1,3) of the glycerol backbone. Trilaurin and dioleylpalmitoylglycerol were the major triglycerides in coconut and pilinut oils, respectively.     

Discovery of Halogenated Benzothiadiazine Derivatives with Anticancer Activity**

Mitochondrial respiratory complex II (CII), also known as succinate dehydrogenase, plays a critical role in mitochondrial metabolism. Known but low potency CII inhibitors are selectively cytotoxic to cancer cells including the benzothiadiazine-based anti-hypoglycemic diazoxide. Herein, we study the structure-activity relationship of benzothiadiazine derivatives for CII inhibition and their effect on cancer cells for the first time. A 15-fold increase in CII inhibition was achieved over diazoxide, albeit with micromolar IC₅₀ values. Cytotoxicity evaluation of the novel derivatives resulted in the identification of compounds with much greater antineoplastic effect than diazoxide, the most potent of which possesses an IC₅₀ of 2.93±0.07 μM in a cellular model of triple-negative breast cancer, with high selectivity over nonmalignant cells and more than double the potency of the clinical agent 5-fluorouracil. No correlation between cytotoxicity and CII inhibition was found, thus indicating an as-yet-undefined mechanism of action of this scaffold. The derivatives described herein represent valuable hit compounds for therapeutic discovery in triple-negative breast cancer.     

Perinatal choline supplementation improves cognitive functioning and emotion regulation in the Ts65Dn mouse model of Down syndrome.

In addition to mental retardation, individuals with Down syndrome (DS) also develop the neuropathological changes typical of Alzheimer's disease (AD) and the majority of these individuals exhibit dementia. The Ts65Dn mouse model of DS exhibits key features of these disorders, including early degeneration of cholinergic basal forebrain (CBF) neurons and impairments in functions dependent on the two CBF projection systems; namely, attention and explicit memory. Herein, we demonstrate that supplementing the maternal diet with excess choline during pregnancy and lactation dramatically improved attentional function of the adult trisomic offspring. Specifically, the adult offspring of choline-supplemented Ts65Dn dams performed significantly better than unsupplemented Ts65Dn mice on a series of 5 visual attention tasks, and in fact, on some tasks did not differ from the normosomic (2N) controls. A second area of dysfunction in the trisomic animals, heightened reactivity to committing an error, was partially normalized by the early choline supplementation. The 2N littermates also benefited from increased maternal choline intake on 1 attention task. These findings collectively suggest that perinatal choline supplementation might significantly lessen cognitive dysfunction in DS and reduce cognitive decline in related neurodegenerative disorders such as AD. (PsycINFO Database Record (c) 2010 APA, all rights reserved)     

PVS Strategies for Proving Abstraction Properties of Automata

Abstractions are important in specifying and proving properties of complex systems. To prove that a given automaton implements an abstract specification automaton, one must first find the correct abstraction relation between the states of the automata, and then show that this relation is preserved by all corresponding action sequences of the two automata. This paper describes tool support based on the PVS theorem prover that can help users accomplish the second task, in other words, in proving a candidate abstraction relation correct. This tool support relies on a clean and uniform technique for defining abstraction properties relating automata that uses library theories for defining abstraction relations and templates for specifying automata and abstraction theorems. The paper then describes how the templates and theories allow development of generic, high level PVS strategies that aid in the mechanization of abstraction proofs. These strategies first set up the standard subgoals for the abstraction proofs and then execute the standard initial proof steps for these subgoals, thus making the process of proving abstraction properties in PVS more automated. With suitable supplementary strategies to implement the “natural” proof steps needed to complete the proofs of any of the standard subgoals remaining to be proved, the abstraction proof strategies can form part of a set of mechanized proof steps that can be used interactively to translate high level proof sketches into PVS proofs. Using timed I/O automata examples taken from the literature, this paper illustrates use of the templates, theories, and strategies described to specify and prove two types of abstraction property: refinement and forward simulation.     

Proving Invariants of I/O Automata with TAME

This paper describes a specialized interface to PVS called TAME (Timed Automata Modeling Environment) which provides automated support for proving properties of I/O automata. A major goal of TAME is to allow a software developer to use PVS to specify and prove properties of an I/O automaton efficiently and without first becoming a PVS expert. To accomplish this goal, TAME provides a template that the user completes to specify an I/O automaton and a set of proof steps natural for humans to use for proving properties of automata. Each proof step is implemented by a PVS strategy and possibly some auxiliary theories that support that strategy. We have used the results of two recent formal methods studies as a basis for two case studies to evaluate TAME. In the first formal methods study, Romijn used I/O automata to specify and verify memory and remote procedure call components of a concurrent system. In the second formal methods study, Devillers et al. specified a tree identify protocol (TIP), part of the IEEE 1394 bus protocol, and provided hand proofs of TIP properties. Devillers also used PVS to specify TIP and to check proofs of TIP properties. In our first case study, the third author, a new TAME user with no previous PVS experience, used TAME to create PVS specifications of the I/O automata formulated by Romijn and Devillers et al. and to check their hand proofs. In our second case study, the TAME approach to verification was compared with an alternate approach by Devillers which uses PVS directly.     

Translation Templates to Support Strategy Development in PVS

In presenting specifications and specification properties to a theorem prover, there is a tension between convenience for the user and convenience for the theorem prover. A choice of specification formulation that is most natural to a user may not be the ideal formulation for reasoning about that specification in a theorem prover. However, when the theorem prover is being integrated into a system development framework, a desirable goal of the integration is to make use of the theorem prover as easy as possible for the user. In such a context, it is possible to have the best of both worlds: specifications that are natural for a system developer to write in the language of the development framework, and representations of these specifications that are well matched to the reasoning techniques provided in the prover. In a tactic-based prover, these reasoning techniques include the use of tactics (or strategies) that can rely on certain structural elements in the theorem prover's representation of specifications. This paper illustrates how translation techniques used in integrating PVS into the TIOA (Timed Input/Output Automata) system development framework produce PVS specifications structured to support development of PVS strategies that implement reasoning steps appropriate for proving TIOA specification properties.