bluuebunny/crossref_metadata_2025 huggingface dataset:
Resilient Tree-Based Video Streaming with a Guaranteed Latency
Authors: FUJITA SATOSHI
Published: December 2019

In this paper, we propose a method to organize a tree-based Peer-to-Peer (P2P) overlay for video streaming which is resilient to the temporal reduction of the upload capacity of a node. The basic idea of the proposed method is: (1) to introduce the redundancy to a given tree-structured overlay, in such a way that a part of the upload capacity of each node is proactively used for connecting to a sibling node, and (2) to use those links connecting to the siblings to forward video stream to the siblings. More specifically, we prove that even if the maximum number of children of a node temporally reduces from m to m − k for some 1 ≤ k ≤ m − 1, the proposed method continues the forwarding of video stream to all of m children in at most 2x hops, where x is the smallest integer satisfying m − k ≥ m/2x. We also derive a sufficient condition to bound the increase of the latency by an additive constant. The derived sufficient condition indicates that if each node can have at least six children in the overlay, the proposed method increases the latency by at most one, provided that the number of nodes in the overlay is at most 9331; namely the proposed method guarantees the delivery of video stream with a nearly optimal latency.
GLOBALIZATION, GENDER AND ENTREPRENEURIAL ACTIVITIES IN LATIN AMERICA
Authors: SAADATMAND YASSAMAN , BARBER DENNIS
Published: December 2019

Although a large body of literature deals with the concept of globalization, the study of the relationship between globalization and entrepreneurship is an unchartered territory. We look at data from eighteen Latin American and Caribbean countries over a fifteen-year time span. Our findings indicate that de facto economic, social, trade and interpersonal globalization are negatively related to female and male entrepreneurial activities. De facto political globalization is the only category of globalization this study finds to be related positively to entrepreneurial activity (male and female), which implies policymaking may be a viable manner to encourage entrepreneurial activities. Political shifts to encourage females to undertake entrepreneurial activities can be seen across the globe.
Dependability in edge computing
Authors: Bagchi Saurabh , Siddiqui Muhammad-Bilal , Wood Paul , Zhang Heng
Published: December 2019

Edge computing holds great promise, and almost as many challenges in deployment.
Mastering concurrent computing through sequential thinking
Authors: Rajsbaum Sergio , Raynal Michel
Published: December 2019

A 50-year history of concurrency.
Space time discontinuum
Authors: Helland Pat
Published: December 2019

Combining data from many sources may cause painful delays.
Taylor subsumes Scott, Berry, Kahn and Plotkin
Authors: Barbarossa Davide , Manzonetto Giulio
Published: December 2019

The speculative ambition of replacing the old theory of program approximation based on syntactic continuity with the theory of resource consumption based on Taylor expansion and originating from the differential λ-calculus is nowadays at hand. Using this resource sensitive theory, we provide simple proofs of important results in λ-calculus that are usually demonstrated by exploiting Scott’s continuity, Berry’s stability or Kahn and Plotkin’s sequentiality theory. A paradigmatic example is given by the Perpendicular Lines Lemma for the Böhm tree semantics, which is proved here simply by induction, but relying on the main properties of resource approximants: strong normalization, confluence and linearity.
Dependent type systems as macros
Authors: Chang Stephen , Ballantyne Michael , Turner Milo , Bowman William J.
Published: December 2019

We present Turnstile+, a high-level, macros-based metaDSL for building dependently typed languages.

With it, programmers may rapidly prototype and iterate on the design of new dependently typed features and extensions.

Or they may create entirely new DSLs whose dependent type ``power'' is tailored to a specific domain.

Our framework's support of language-oriented programming also makes it suitable for experimenting with systems of interacting components, e.g., a proof assistant and its companion DSLs.

This paper explains the implementation details of Turnstile+, as well as how it may be used to create a wide-variety of dependently typed languages, from a lightweight one with indexed types, to a full spectrum proof assistant, complete with a tactic system and extensions for features like sized types and SMT interaction.
Complexity and information in invariant inference
Authors: Feldman Yotam M. Y. , Immerman Neil , Sagiv Mooly , Shoham Sharon
Published: December 2019

This paper addresses the complexity of SAT-based invariant inference, a prominent approach to safety verification. We consider the problem of inferring an inductive invariant of polynomial length given a transition system and a safety property. We analyze the complexity of this problem in a black-box model, called the Hoare-query model, which is general enough to capture algorithms such as IC3/PDR and its variants. An algorithm in this model learns about the system's reachable states by querying the validity of Hoare triples.

We show that in general an algorithm in the Hoare-query model requires an exponential number of queries. Our lower bound is information-theoretic and applies even to computationally unrestricted algorithms, showing that no choice of generalization from the partial information obtained in a polynomial number of Hoare queries can lead to an efficient invariant inference procedure in this class.

We then show, for the first time, that by utilizing rich Hoare queries, as done in PDR, inference can be exponentially more efficient than approaches such as ICE learning, which only utilize inductiveness checks of candidates. We do so by constructing a class of transition systems for which a simple version of PDR with a single frame infers invariants in a polynomial number of queries, whereas every algorithm using only inductiveness checks and counterexamples requires an exponential number of queries.

Our results also shed light on connections and differences with the classical theory of exact concept learning with queries, and imply that learning from counterexamples to induction is harder than classical exact learning from labeled examples. This demonstrates that the convergence rate of Counterexample-Guided Inductive Synthesis depends on the form of counterexamples.
Incorrectness logic
Authors: O'Hearn Peter W.
Published: December 2019

Program correctness and incorrectness are two sides of the same coin. As a programmer, even if you would like to have correctness, you might find yourself spending most of your time reasoning about incorrectness. This includes informal reasoning that people do while looking at or thinking about their code, as well as that supported by automated testing and static analysis tools. This paper describes a simple logic for program incorrectness which is, in a sense, the other side of the coin to Hoare's logic of correctness.
Recurrence extraction for functional programs through call-by-push-value
Authors: Kavvos G. A. , Morehouse Edward , Licata Daniel R. , Danner Norman
Published: December 2019

The main way of analysing the complexity of a program is that of extracting and solving a recurrence that expresses its running time in terms of the size of its input. We develop a method that automatically extracts such recurrences from the syntax of higher-order recursive functional programs. The resulting recurrences, which are programs in a call-by-name language with recursion, explicitly compute the running time in terms of the size of the input. In order to achieve this in a uniform way that covers both call-by-name and call-by-value evaluation strategies, we use Call-by-Push-Value (CBPV) as an intermediate language. Finally, we use domain theory to develop a denotational cost semantics for the resulting recurrences.
Towards verified stochastic variational inference for probabilistic programs
Authors: Lee Wonyeol , Yu Hangyeol , Rival Xavier , Yang Hongseok
Published: December 2019

Probabilistic programming is the idea of writing models from statistics and machine learning using program notations and reasoning about these models using generic inference engines. Recently its combination with deep learning has been explored intensely, which led to the development of so called deep probabilistic programming languages, such as Pyro, Edward and ProbTorch. At the core of this development lie inference engines based on stochastic variational inference algorithms. When asked to find information about the posterior distribution of a model written in such a language, these algorithms convert this posterior-inference query into an optimisation problem and solve it approximately by a form of gradient ascent or descent. In this paper, we analyse one of the most fundamental and versatile variational inference algorithms, called score estimator or REINFORCE, using tools from denotational semantics and program analysis. We formally express what this algorithm does on models denoted by programs, and expose implicit assumptions made by the algorithm on the models. The violation of these assumptions may lead to an undefined optimisation objective or the loss of convergence guarantee of the optimisation process. We then describe rules for proving these assumptions, which can be automated by static program analyses. Some of our rules use nontrivial facts from continuous mathematics, and let us replace requirements about integrals in the assumptions, such as integrability of functions defined in terms of programs' denotations, by conditions involving differentiation or boundedness, which are much easier to prove automatically (and manually). Following our general methodology, we have developed a static program analysis for the Pyro programming language that aims at discharging the assumption about what we call model-guide support match. Our analysis is applied to the eight representative model-guide pairs from the Pyro webpage, which include sophisticated neural network models such as AIR. It finds a bug in one of these cases, reveals a non-standard use of an inference engine in another, and shows that the assumptions are met in the remaining six cases.
Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time
Authors: Wang Peixin , Fu Hongfei , Chatterjee Krishnendu , Deng Yuxin , Xu Ming
Published: December 2019

The notion of program sensitivity (aka Lipschitz continuity) specifies that changes in the program input result in proportional changes to the program output. For probabilistic programs the notion is naturally extended to expected sensitivity. A previous approach develops a relational program logic framework for proving expected sensitivity of probabilistic while loops, where the number of iterations is fixed and bounded. In this work, we consider probabilistic while loops where the number of iterations is not fixed, but randomized and depends on the initial input values. We present a sound approach for proving expected sensitivity of such programs. Our sound approach is martingale-based and can be automated through existing martingale-synthesis algorithms. Furthermore, our approach is compositional for sequential composition of while loops under a mild side condition. We demonstrate the effectiveness of our approach on several classical examples from Gambler's Ruin, stochastic hybrid systems and stochastic gradient descent. We also present experimental results showing that our automated approach can handle various probabilistic programs in the literature.
The weak call-by-value λ-calculus is reasonable for both time and space
Authors: Forster Yannick , Kunze Fabian , Roth Marc
Published: December 2019

We study the weak call-by-value λ-calculus as a model for computational complexity theory and establish the natural measures for time and space — the number of beta-reduction steps and the size of the largest term in a computation — as reasonable measures with respect to the invariance thesis of Slot and van Emde Boas from 1984. More precisely, we show that, using those measures, Turing machines and the weak call-by-value λ-calculus can simulate each other within a polynomial overhead in time and a constant factor overhead in space for all computations terminating in (encodings of) ”true” or ”false”. The simulation yields that standard complexity classes like
P
,
NP
,
PSPACE
, or
EXP
can be defined solely in terms of the λ-calculus, but does not cover sublinear time or space.

Note that our measures still have the well-known size explosion property, where the space measure of a computation can be exponentially bigger than its time measure. However, our result implies that this exponential gap disappears once complexity classes are considered instead of concrete computations.

We consider this result a first step towards a solution for the long-standing open problem of whether the natural measures for time and space of the λ-calculus are reasonable. Our proof for the weak call-by-value λ-calculus is the first proof of reasonability (including both time and space) for a functional language based on natural measures and enables the formal verification of complexity-theoretic proofs concerning complexity classes, both on paper and in proof assistants.

The proof idea relies on a hybrid of two simulation strategies of reductions in the weak call-by-value λ-calculus by Turing machines, both of which are insufficient if taken alone. The first strategy is the most naive one in the sense that a reduction sequence is simulated precisely as given by the reduction rules; in particular, all substitutions are executed immediately. This simulation runs within a constant overhead in space, but the overhead in time might be exponential. The second strategy is heap-based and relies on structure sharing, similar to existing compilers of eager functional languages. This strategy only has a polynomial overhead in time, but the space consumption might require an additional factor of log
n
, which is essentially due to the size of the pointers required for this strategy. Our main contribution is the construction and verification of a space-aware interleaving of the two strategies, which is shown to yield both a constant overhead in space
and
a polynomial overhead in time.
Decomposition diversity with symmetric data and codata
Authors: Binder David , Jabs Julian , Skupin Ingo , Ostermann Klaus
Published: December 2019

The expression problem describes a fundamental trade-off in program design: Should a program's primary decomposition be determined by the way its domain objects are constructed ("functional" decomposition), or by the way they are destructed ("object-oriented" decomposition)? We argue that programming languages should not force one of these decompositions on the programmer; rather, a programming language should support both ways of decomposing a program in a symmetric way, with an easy translation between these decompositions. However, current programming languages are usually not symmetric and hence make it unnecessarily hard to switch the decomposition.

We propose a language that is symmetric in this regard and allows a fully automatic translation between "functional" and "object-oriented" decomposition. We present a language with algebraic data types and pattern matching for "functional" decomposition and codata types and copattern matching for "object-oriented" decomposition, together with a bijective translation that turns a data type into a codata type ("destructorization") or vice versa ("constructorization"). We present the first symmetric programming language with support for local (co)pattern matching, which includes local anonymous function or object definitions, that allows an automatic translation as described above. We also present the first mechanical formalization of such a language and prove i) that the type system is sound, that the translations between data and codata types are ii) type-preserving, iii) behavior-preserving and iv) inverses of each other. We also extract a mechanically verified implementation from our formalization and have implemented an IDE with direct support for these translations.
PλωNK: functional probabilistic NetKAT
Authors: Vandenbroucke Alexander , Schrijvers Tom
Published: December 2019

This work presents PλωNK, a functional probabilistic network programming language that extends Probabilistic NetKAT (PNK). Like PNK, it enables probabilistic modelling of network behaviour, by providing probabilistic choice and infinite iteration (to simulate looping network packets). Yet, unlike PNK, it also offers abstraction and higher-order functions to make programming much more convenient.

The formalisation of PλωNK is challenging for two reasons: Firstly, network programming induces multiple side effects (in particular, parallelism and probabilistic choice) which need to be carefully controlled in a functional setting. Our system uses an explicit syntax for thunks and sequencing which makes the interplay of these effects explicit. Secondly, measure theory, the standard domain for formalisations of (continuous) probablistic languages, does not admit higher-order functions. We address this by leveraging ω-Quasi Borel Spaces (ωQBSes), a recent advancement in the domain theory of probabilistic programming languages.

We believe that our work is not only useful for bringing abstraction to PNK, but that—as part of our contribution—we have developed the meta-theory for a probabilistic language that combines advanced features like higher-order functions, iteration and parallelism, which may inform similar meta-theoretic efforts.
Partial type constructors: or, making ad hoc datatypes less ad hoc
Authors: Jones Mark P. , Morris J. Garrett , Eisenberg Richard A.
Published: December 2019

Functional programming languages assume that type constructors are total. Yet functional programmers know better: counterexamples range from container types that make limiting assumptions about their contents (e.g., requiring computable equality or ordering functions) to type families with defining equations only over certain choices of arguments. We present a language design and formal theory of partial type constructors, capturing the domains of type constructors using qualified types. Our design is both simple and expressive: we support partial datatypes as first-class citizens (including as instances of parametric abstractions, such as the Haskell Functor and Monad classes), and show a simple type elaboration algorithm that avoids placing undue annotation burden on programmers. We show that our type system rejects ill-defined types and can be compiled to a semantic model based on System F. Finally, we have conducted an experimental analysis of a body of Haskell code, using a proof-of-concept implementation of our system; while there are cases where our system requires additional annotations, these cases are rarely encountered in practical Haskell code.
Mechanized semantics and verified compilation for a dataflow synchronous language with reset
Authors: Bourke Timothy , Brun Lélio , Pouzet Marc
Published: December 2019

Specifications based on block diagrams and state machines are used to design control software, especially in the certified development of safety-critical applications. Tools like SCADE Suite and Simulink/Stateflow are equipped with compilers that translate such specifications into executable code. They provide programming languages for composing functions over streams as typified by Dataflow Synchronous Languages like Lustre.

Recent work builds on CompCert to specify and verify a compiler for the core of Lustre in the Coq Interactive Theorem Prover. It formally links the stream-based semantics of the source language to the sequential memory manipulations of generated assembly code. We extend this work to treat a primitive for resetting subsystems. Our contributions include new semantic rules that are suitable for mechanized reasoning, a novel intermediate language for generating optimized code, and proofs of correctness for the associated compilation passes.
Graduality and parametricity: together again for the first time
Authors: New Max S. , Jamner Dustin , Ahmed Amal
Published: December 2019

Parametric polymorphism and gradual typing have proven to be a difficult combination, with no language yet produced that satisfies the fundamental theorems of each: parametricity and graduality. Notably, Toro, Labrada, and Tanter (POPL 2019) conjecture that for any gradual extension of System F that uses dynamic type generation, graduality and parametricity are ``simply incompatible''. However, we argue that it is not graduality and parametricity that are incompatible per se, but instead that combining the syntax of System F with dynamic type generation as in previous work necessitates type-directed computation, which we show has been a common source of graduality and parametricity violations in previous work.

We then show that by modifying the syntax of universal and existential types to make the type name generation explicit, we remove the need for type-directed computation, and get a language that satisfies both graduality and parametricity theorems. The language has a simple runtime semantics, which can be explained by translation to a statically typed language where the dynamic type is interpreted as a dynamically extensible sum type. Far from being in conflict, we show that the parametricity theorem follows as a direct corollary of a relational interpretation of the graduality property.
Synthesis of coordination programs from linear temporal specifications
Authors: Bansal Suguman , Namjoshi Kedar S. , Sa'ar Yaniv
Published: December 2019

This paper presents a method for synthesizing a reactive program to coordinate the actions of a group of other reactive programs so that the combined system satisfies a temporal specification of its desired long-term behavior. Traditionally, reactive synthesis has been applied to the construction of a stateful hardware circuit. This work is motivated by applications to other domains, such as the IoT (the Internet of Things) and robotics, where it is necessary to coordinate the actions of multiple sensors, devices, and robots to carry out a task. The mathematical model represents each agent as a process in Hoare’s CSP model. Given a network of interacting agents, called an
environment
, and a temporal specification of long-term behavior, the synthesis method constructs a
coordinator
process (if one exists) that guides the actions of the environment agents so that the combined system is deadlock-free and satisfies the given specification. The main technical challenge is that a coordinator may have only
partial information
of the environment state, due to non-determinism within the environment and internal environment actions that are hidden from the coordinator. This is the first method to handle both sources of partial information and to do so for arbitrary linear temporal logic specifications. It is established that the coordination synthesis problem is
PSPACE
-hard in the size of the environment. A prototype implementation is able to synthesize compact solutions for a number of coordination problems.
Augmented example-based synthesis using relational perturbation properties
Authors: An Shengwei , Singh Rishabh , Misailovic Sasa , Samanta Roopsha
Published: December 2019

Example-based specifications for program synthesis are inherently ambiguous and may cause synthesizers to generate programs that do not exhibit intended behavior on unseen inputs. Existing synthesis techniques attempt to address this problem by either placing a domain-specific syntactic bias on the hypothesis space or heavily relying on user feedback to help resolve ambiguity.

We present a new framework to address the ambiguity/generalizability problem in example-based synthesis. The key feature of our framework is that it places a semantic bias on the hypothesis space using "relational perturbation properties" that relate the perturbation/change in a program output to the perturbation/change in a program input. An example of such a property is permutation invariance: the program output does not change when the elements of the program input (array) are permuted. The framework is portable across multiple domains and synthesizers and is based on two core steps: (1) automatically augment the set of user-provided examples by "applying" relational perturbation properties and (2) use a generic example-based synthesizer to generate a program consistent with the augmented set of examples. Our framework can be instantiated with three different user interfaces, with varying degrees of user engagement to help infer relevant relational perturbation properties. This includes an interface in which the user only provides examples and our framework automatically infers relevant properties. We implement our framework in a tool SKETCHAX specialized to the SKETCH synthesizer and demonstrate that SKETCHAX is effective in significantly boosting the performance of SKETCH for all three user interfaces.
SyTeCi: automating contextual equivalence for higher-order programs with references
Authors: Jaber Guilhem
Published: December 2019

We propose a framework to study contextual equivalence of programs written in a call-by-value functional language with local integer references. It reduces the problem of contextual equivalence to the problem of non-reachability in a transition system of memory configurations. This reduction is complete for recursion-free programs.

Restricting to programs that do not allocate references inside the body of functions, we encode this non-reachability problem as a set of constrained Horn clause that can then be checked for satisfiability automatically. Restricting furthermore to a language with finite data-types, we also get a new decidability result for contextual equivalence at any type.
Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time
Authors: Smolka Steffen , Foster Nate , Hsu Justin , Kappé Tobias , Kozen Dexter , Silva Alexandra
Published: December 2019

Guarded Kleene Algebra with Tests (GKAT) is a variation on Kleene Algebra with Tests (KAT) that arises by restricting the union (+) and iteration (*) operations from KAT to predicate-guarded versions. We develop the (co)algebraic theory of GKAT and show how it can be efficiently used to reason about imperative programs. In contrast to KAT, whose equational theory is PSPACE-complete, we show that the equational theory of GKAT is (almost) linear time. We also provide a full Kleene theorem and prove completeness for an analogue of Salomaa’s axiomatization of Kleene Algebra.
MTL and TPTL for One-Counter Machines
Authors: Feng Shiguang , Carapelle Claudia , Gil Oliver Fernández , Quaas Karin
Published: December 2019

Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) are quantitative extensions of Linear Temporal Logic (LTL) that are prominent and widely used in the verification of real-timed systems. We study MTL and TPTL as specification languages for one-counter machines. It is known that model checking one-counter machines against formulas of Freeze LTL (FLTL), a strict fragment of TPTL, is undecidable. We prove that in our setting, MTL is strictly less expressive than TPTL, and incomparable in expressiveness to FLTL, so undecidability for MTL is not implied by the result for FLTL. We show, however, that the model-checking problem for MTL is undecidable. We further prove that the satisfiability problem for the unary fragments of TPTL and MTL are undecidable; for TPTL, this even holds for the fragment in which only one register and the finally modality is used. This is opposed to a known decidability result for the satisfiability problem for the same fragment of FLTL.
Increasing automation in policing
Authors: Joh Elizabeth E.
Published: December 2019

Seeking the delicate balance between civil liberties and policing public safety.
von Neumann thought Turing's universal machine was 'simple and neat.'
Authors: Haigh Thomas , Priestley Mark
Published: December 2019

New discoveries answer an old question.
Build your own SQL-on-Hadoop Query Engine
Authors: Scherzinger Stefanie
Published: December 2019

This is a report on a course taught at OTH Regensburg in the summer term of 2018. The students in this course built their own SQL-on-Hadoop engine as a term project in just 8 weeks. miniHive is written in Python and compiles SQL queries into MapReduce workflows. These are then executed on Hadoop. miniHive performs generic query optimizations (selection and projection pushdown, or cost-based join reordering), as well as Map- Reduce-specific optimizations.

The course was taught in English, using a flipped classroom model. The course material was mainly compiled from third-party teaching videos. This report describes the course setup, the miniHive milestones, and gives a short review of the most successful student projects.
Novel measures of left ventricular electromechanical discoordination predict clinical outcomes in children with pulmonary arterial hypertension
Authors: Frank Benjamin S. , Schäfer Michal , Douwes Johannes M. , Ivy D. Dunbar , Abman Steven H. , Davidson Jesse A. , Burzlaff Sandra , Mitchell Max B. , Morgan Gareth J. , Browne Lorna P. , Barker Alex J. , Truong Uyen , von Alvensleben Johannes C.
Published: December 2019

Adverse ventricle-ventricle interaction and resultant left ventricular (LV) dysfunction are a recognized pathophysiological component of disease progression in pulmonary arterial hypertension (PAH) and can be associated with electrical and mechanical dyssynchrony. The purpose of this study was to investigate the clinical and mechanistic implications of LV electromechanical dyssynchrony in children with PAH by using novel systolic stretch and diastolic relaxation discoordination indexes derived noninvasively from cardiac MRI (CMR). In children with PAH referred for CMR ( n = 64) and healthy controls ( n = 20), we calculated two novel markers of ventricular discoordination, systolic stretch fraction (SSF) and diastolic relaxation fraction (DRF). SSF and DRF were evaluated with respect to 1) electrical dyssynchrony, 2) functional status, and 3) composite clinical outcomes. SSF was increased in patients with PAH compared with controls ( P = 0.004). There was no difference in DRF between PAH and control groups. There were no differences between groups in standard mechanical dyssynchrony and LV global circumferential strain. Increased SSF was associated with greater electrical dyssynchrony (QRS duration) as well as worse WHO functional class. SSF, DRF, mechanical dyssynchrony, and right ventricular (RV) volumes were prognostic for worse clinical outcomes. LV dyssynchrony indexes are altered in pediatric patients with PAH compared with controls in proportion with greater degrees of RV dilation. Patients with PAH with greater dyssynchrony have worse clinical outcomes. RV-induced increased LV electromechanical dyssynchrony therefore may be an important link in the causal pathway from PAH to clinically significant LV dysfunction. Since dyssynchrony could precede overt LV dysfunction, addition of ventricular synchrony analysis to CMR postprocessing protocols may be of clinical benefit.

NEW & NOTEWORTHY We demonstrate that left ventricular discoordination indexes are altered in pediatric patients with pulmonary arterial hypertension compared with controls and pediatric patients with pulmonary arterial hypertension with greater dyssynchrony have worse clinical outcomes. Furthermore, there is evidence for the mechanism of right ventricular-induced left ventricular discoordination to include a combination of delayed early systolic electromechanical activation, late-systolic septal shift, and prolonged, postsystolic septal thickening.
Effects of Ethyl Pyruvate on Bile Duct Ligation-Induced Liver Fibrosis by Regulating Nrf2 Pathway and Proinflammatory Cytokines in Rats
Authors: Zong Yonghua , Zhang Mingxiao , Li Shuai , Qi Wenqian , Li Juan , Liu Tonghua , Yang Huijun , Lu Chen , Hu Xiaosong
Published: December 2019

Aim. The aim of this paper is to investigate the effects of ethyl pyruvate (EP) on experimental liver fibrosis induced by bile duct ligation (BDL) and explore the underlying molecular mechanisms. Material and Method. Rats were randomly divided into three groups: the sham group, the BDL group, and the BDL+EP group. Liver fibrosis was induced by common bile duct ligation and was evaluated by serum biochemical parameter levels, Masson’s trichrome staining, α-SMA expression, and collagen I deposition. The levels of Nrf2 signaling pathway-related antioxidant genes (Nrf2, SOD2, NQO1, and GSH-Px) in liver tissues were also measured. Meanwhile, the mRNA expression levels of HMGB1, IL-1β, TNF-α, and HSP27 were analyzed. In BDL-induced liver fibrosis rats, the successfully established model was confirmed by the significant increase of serum ALT and AST levels, the high liver fibrosis score, α-SMA expression, and collagen deposition. Results. Compared with the BDL group, EP administration could diminish fibrosis level and substantially increase the expression of Nrf2 signaling pathway-related antioxidant genes. Furthermore, EP significantly suppressed the mRNA expression levels of HMGB1, IL-1β, TNF-α, and HSP27. Conclusions. The results suggested that EP administration could effectively inhibit the liver fibrosis induced by BDL in rat, which may be associated with the enhanced activity of Nrf2 to mediate antioxidant enzyme system and downregulate the inflammatory genes.
tert-Butylhydroquinone Treatment Alleviates Contrast-Induced Nephropathy in Rats by Activating the Nrf2/Sirt3/SOD2 Signaling Pathway
Authors: Zhou Qin , Wang Xin , Shao Xiaofei , Wang Honglei , Liu Xiaobo , Ke Xiaosu , Xiong Chongxiang , Wei Lixin , Zou Hequn
Published: December 2019

Oxidative stress plays a critical role in the pathophysiology of contrast-induced nephropathy (CIN). Since the specific treatment of CIN remains an unmet medical need, it is imperative to find an effective strategy against the clinical management of CIN. The transcription factor Nrf2 is known to regulate antioxidative stress response. The aim of the present study was to assess the effects oftert-butylhydroquinone (t-BHQ), an activator of Nrf2, in the prevention of CIN and elucidate the underlying mechanism of its actionin vitroandin vivo. We established a rat model of CIN and treated the animals with t-BHQ (25 mg/kg). The effects of t-BHQ treatment on CIN rats were elucidated by assessing renal function, HE staining, immunohistochemistry, and western blotting. We also studied the activity of oxidative stress-related markers, such as intracellular ROS level, MDA level, SOD2 activity, and GSH/GSSG ratio. We validated our results by siRNA-mediated silencing of Nrf2 in HK-2 cells exposed to the radiocontrast agent. Treatment with t-BHQ significantly ameliorated the renal function and the histopathological lesions in CIN rats. Further, pretreatment with t-BHQ significantly increased the SOD2 activity and GSH/GSSG ratio and decreased the levels of ROS and MDA in animals subjected to ioversol exposure. In addition, t-BHQ treatment increased the expression of Nrf2, Sirt3, and SOD2 and concomitantly decreased the expression of acetylated-SOD2. When Nrf2-silenced HK-2 cells were exposed to radiocontrast agent, they suffered severe cell oxidative stress, exhibited lower expression of Sirt3 and SOD2, and expressed higher levels of acetylated-SOD2; however, t-BHQ treatment did not affect the protein expression of these indicators in si-Nrf2 HK-2 cells. Our findings suggested that Nrf2 plays an important role in the regulation of the Sirt3/SOD2 antioxidative pathway, and t-BHQ may be a potential agent to ameliorate radiocontrast-induced nephropathy via activating the Nrf2/Sirt3/SOD2 signaling pathway in vitro and in vivo.
New Contour Design Method for Rocket Nozzle of Large Area Ratio
Authors: Sun Dechuan , Luo Tianyou , Feng Qiang
Published: December 2019

A rocket engine for space propulsion usually has a nozzle of a large exit area ratio. The nozzle efficiency is greatly affected by the nozzle contour. This paper analysed the effect of the constant capacity ratio in Rao’s method through the design process of an apogee engine. The calculation results show that increasing the heat capacity ratio can produce an expansion contour of smaller expansion angle and exit area ratio. A simple modification of Rao’s method based on thermally perfect gas assumption was made and verified to be more effective. The expansion contour designed by this method has much thinner expansion section and higher performance. For the space engine, a new extension contour type for the end section of the nozzle is proposed. The extension curve bent outward with increasing expansion angle increases the vacuum specific impulse obviously.
Master‐Slave Composite Vibration Control of a Mobile Flexible Manipulator via Synchronization Optimization of Observation and Feedback
Authors: Ju Jin-yong , Liu Yufei , Kan Honglin , Zhang Chunrui
Published: December 2019

The elastic vibration of the flexible manipulator is the key problem to be solved before its effective application. The mobile flexible manipulator system (MFMS), under variable load conditions, is taken as the research object. Based on Lagrange’s principle and the singular perturbation theory, the two‐timescale subsystems dynamic models of the MFMS are constructed to set up the system payment function and the Hamiltonian function which correspond to the subsystems states and errors. Then, with the minimization of the system Hamiltonian function, the synchronization optimization of the designed two‐timescale optimal observer (TSOO) and the designed optimal state feedback controller is realized, under the premise of the system stability which is verified by the Lyapunov stability criterion. Furthermore, with the contradiction between the control rapidity and the accuracy of the optimal state feedback controller considered, by combining the input shaping technology, the master‐slave composite controller for the elastic vibration of the MFMS is constructed. Finally, simulation results verify the validity of the designed TSOO and the master‐slave composite controller.
Population Structure of the Freshwater CrabPotamon algeriense(Bott, 1967) Inhabiting Oued Zegzel, (Northeast of Morocco)
Authors: Fadlaoui Soufiane , Melhaoui Mohammed
Published: December 2019

This is the first study to determine the population structure of the freshwater crabPotamon algeriensein Oued Zegzel, a mountain stream in the northeast of Morocco. Monthly collections were carried out by hand, from October 2017 to September 2018. A total of 669 individuals, 378 males and 291 females, were captured, measured, marked, and released. Due to their extremely cryptic behavior during egg incubation, few ovigerous females were caught during the entire sampling period. The average size of males (28.98 ± 10.78 mm CW) is significantly larger than that of the females (28.62 ± 8.48 mm CW). Significant deviation from 1 : 1 sex ratio during the study period was recorded, and the size distribution of the sampled population presented an abnormal distribution where specimens over 31 and under 25 mm CW were often males, whereas females were represented more in the 26–30 mm CW range.
The Oxidative Stress-Induced miR-200c Is Upregulated in Psoriasis and Correlates with Disease Severity and Determinants of Cardiovascular Risk
Authors: Magenta A. , D’Agostino M. , Sileno S. , Di Vito L. , Uras C. , Abeni D. , Martino F. , Barillà F. , Madonna S. , Albanesi C. , Napolitano M. , Capogrossi M. C. , Melillo G.
Published: December 2019

Psoriasis is a chronic inflammatory skin disease associated with reactive oxygen species (ROS) increase and a higher risk of cardiovascular (CV) events. We previously showed that the miR-200 family (miR-200s) is induced by ROS, miR-200c being the most upregulated member responsible for apoptosis, senescence, ROS increase, and nitric oxide decrease, finally causing endothelial dysfunction. Moreover, circulating miR-200c increases in familial hypercholesterolemic children and in plaques and plasma of atherosclerotic patients, two pathologies associated with increased ROS. Given miR-200s’ role in endothelial dysfunction, ROS, and inflammation, we hypothesized that miR-200s were modulated in lesional skin (LS) and plasma of psoriatic patients (Pso) and that their levels correlated with some CV risk determinants at a subclinical level. All Pso had severe psoriasis, i.e., Psoriasis Area and Severity Index PASI>10, and one of the following: at least two systemic psoriasis treatments, age at onset<40 years, and disease duration>10 years. RNA was extracted from plasma (Pso, N=29; Ctrl, N=29) and from nonlesional skin (NLS) and LS of 6 Pso and 6 healthy subject skin (HS) biopsies. miR-200 levels were assayed by quantitative RT-PCR. We found that all miR-200s were increased in LS vs. NLS and miR-200c was the most expressed and upregulated in LS vs. HS. In addition, circulating miR-200c and miR-200a were upregulated in Pso vs. Ctrl. Further, miR-200c positively correlated with PASI, disease duration, left ventricular (LV) mass, LV relative wall thickness (RWT), and E/e′, a marker of diastolic dysfunction. Multiple regression analysis indicates a direct association between miR-200c and both RWT and LV mass. Circulating miR-200a correlated positively only with LV mass and arterial pressure augmentation index, a measure of stiffness, although the correlations were nearly significant (P=0.06). In conclusion, miR-200c is upregulated in LS and plasma of Pso, suggesting its role in ROS increase and inflammation associated with CV risk in psoriasis.
The Impact of Preoperative Opioid Use Disorder on Complications and Costs following Primary Total Hip and Knee Arthroplasty
Authors: Wilson Jacob M. , Farley Kevin X. , Aizpuru Matthew , Wagner Eric R. , Bradbury Thomas L. , Guild George N.
Published: December 2019

Introduction. Multiple studies have demonstrated that patients taking opioids in the preoperative period are at elevated risk for complications following total hip (THA) and knee (TKA) arthroplasty. However, the incidence and impact of opioid use disorder (OUD) among these patients—both clinically and fiscally—remain unknown. The purpose of this study was to investigate this relationship. Methods. The Nationwide Readmission Database (NRD) was used to identify patients undergoing THA and TKA from 2011 to 2015. Coarsened exact matching was used to statistically match the OUD and non-OUD cohorts. Further analysis was then conducted on matched cohorts with multivariate analysis. The incidence of OUD was also determined, and the costs associated with this comorbidity were calculated. Results. The incidence of OUD in arthroplasty patients increased 80% over the study period. OUD patients had higher odds of prosthetic joint infection (OR 1.55, 95% CI 1.23–1.94), wound complication (OR 1.40, 95% CI 1.12–1.76), prosthetic complication (OR 1.37, 95% CI 1.10–1.70), and revision surgery (OR 1.47, 95% CI 1.19–1.81). OUD patients also had longer length of stays (TKA: +0.67 days; THA: +1.09 days), higher readmission (OR 1.60, 95% CI 1.43–1.79), and increased 90-day costs (TKA: +$3,602 [95% CI $3,138–4,065]; THA: +4,527 [95% CI $3,593–4,920). Conclusion. Opioid use disorder is becoming a more common comorbidity among THA and TKA patients. This is concerning as it represents a significant risk factor for postoperative complication. It additionally confers increased perioperative costs. Patients with OUD should be counseled on their elevated risk, and future work will be needed to determine if this is a modifiable risk factor.
Finite‐Time Synchronization of Uncertain Complex Dynamic Networks with Nonlinear Coupling
Authors: Luo Yiping , Yao Yuejie
Published: December 2019

The finite‐time synchronization control is studied in this paper for a class of nonlinear uncertain complex dynamic networks. The uncertainties in the network are unknown but bounded and satisfy some matching conditions. The coupling relationship between network nodes is described by a nonlinear function satisfying the Lipchitz condition. By introducing a simple Lyapunov function, two main results regarding finite‐time synchronization of a class of complex dynamic networks with parameter uncertainties are derived. By employing some analysis techniques like matrix inequalities, suitable controllers can be designed based on the obtained synchronization criteria. Moreover, with the obtained control input, the time instant required for the system to achieve finite‐time synchronization can be estimated if a set of LMIs are feasible or an assumption on the eigenvalues of some matrices can be satisfied. Finally, the effectiveness of the proposed results is verified by numerical simulation.
Quantitative and Qualitative Analyses of the Clock Drawing Test in Fall and Non-Fall Patients with Alzheimer’s Disease
Authors: Suzuki Yukiko , Mochizuki Hideki , Oki Mayuka , Matsumoto Miyuki , Fukushima Mitsuko , Yoshikawa Yukiko , Nagasawa Akira , Takakura Tomokazu , Shimoda Nobuaki
Published: December 2019

Aim: The clock drawing test (CDT) is widely used as a visual spatial ability test and screening test for dementia patients. The appearance frequency of qualitative errors obtained through the qualitative analysis of CDT may be related to the participant’s falls. The aim of this study was to clarify the difference in the number of people who presented with qualitative errors in the CDT between a fall and non-fall group of patients with Alzheimer’s disease (AD). Methods: The CDT was implemented for 47 patients with AD. A quantitative analysis was conducted, and a qualitative analysis was performed for errors. The patients were divided into two groups based on their history of falls over the past year. The results of the CDT quantitative analysis were tested using the Mann-Whitney U test, and Fisher’s exact test was employed to determine the difference in the number of people who presented with error types between the two groups (fall group, non-fall group) in the CDT qualitative analysis. Results: In the quantitative analysis, a significant difference was found for the total scores, with the total CDT score of the fall group (n = 22) significantly lower than that of the non-fall group (n = 25) (p = 0.006, effect size: φ = 0.40). In the qualitative analysis, a significantly higher number of patients in the fall group than in the non-fall group presented with a conceptual deficit (p =0.001, φ = 0.51). No differences were found in the number of patients in the two groups who presented with the other five error types. Conclusions: These results showed that a lower score in the CDT quantitative analysis might suggest an increased risk of falls. It was also clarified that a larger number of patients in the fall group than in the non-fall group presented with a conceptual deficit of the qualitative error types in the CDT. Therefore, these results suggest that the appearance of a conceptual deficit may be an index for the selection of patients with AD prone to falling when implementing fall prevention measures.