NoSQL databases do not enforce a fixed and explicit schema, and thus offer a high level of flexibility in designing a database schema. However, how data is structured has a significant impact on the query and update performance. Selecting an appropriate schema depends not only on the application's conceptual data model but also on data characteristics and workload information. The challenge is to determine the most effective data modeling strategy —referencingordenormalization— to improve the overall workload performance. To this end, we provide an automated temporal schema optimization for NoSQL wide-column stores that improves workload performance by making a good trade-off between denormalization and referencing. Using data characteristics and workload information, we propose a two-step transformation from a temporal conceptual model into a model for the Cassandra wide-column store: (i) mapping a temporal UML class model to a schema design graph (SDG) and (ii) mapping the SDG to a Cassandra schema. In the two mappings, we adopt a cost model to optimize schema design via a trade-off between read and write costs. An experimental evaluation demonstrates that our approach generates schemas that lead to significant performance improvements while remaining workload sensitive. For the most expensive cases, our schema reduces the workload latency by up to three orders of magnitude.

The Variant Call Format (VCF) and its binary counterpart (BCF) are commonly used in bioinformatics for storing gene sequence data. While VCF files provide compact storage, they require specific tools and scripts for querying, thereby missing the rich functionality arsenal of database management systems and their potential for integration in multiomics pipelines. In this paper, we leverage Relational Database Management Systems (RDBMS) to enhance efficiency and flexibility in storing and querying large-scale genetic datasets. We map the VCF file structure to narrow, wide, and array-based data models that are further refined using JSON data structures, resulting in eight data models. Our experimental evaluation shows that RDBMS provide competitive performance in comparison with specialized state-of-the-art tools while making full-fledged database capabilities available for genetic data analysis.

Deep inference is a proof theoretical formalism that generalises the “shallow inference” of sequent calculus by permitting the application of inference rules on subformulae like term rewriting rules. Deep inference makes it possible to build shorter proofs than sequent calculus proofs. However, deep inference in proof search introduces higher nondeterminism, an obstacle in front of applications. Deep inference is essential for designing system BV, an extension of multiplicative linear logic (MLL) with a self-dual non-commutative operator. MLL has shallow inference systems, whereas BV is impossible with a shallow-only system. As Tiu showed, any restriction on rule depth makes a system incomplete for BV. This paper shows that any restriction that rules out shallow rules makes the system incomplete, too. Our results indicate that for system BV, shallow and deep rules must coexist for completeness. We provide extensive empirical evidence that deep inference can still be faster than shallow inference when used strategically with a proof theoretical technique for reducing nondeterminism. We show that prioritising deeper rule instances, in general, reduces the cost of proof search by reducing the size of the managed contexts, consequently providing more immediate access to shorter proofs. Moreover, we identify a class of MLL formulae with deep inference proof search times that grow linearly in the number of atoms in contrast to an exponential growth pattern with shallow inference. We introduce a large and exhaustive benchmark for MLL, with and without mix, and a proof search framework to apply various search strategies, which should be of independent interest.

The deep inference presentation of multiplicative exponential linear logic (MELL) benefits from a rich combinatoric analysis with many more proofs in comparison to its sequent calculus presentation. In the deep inference setting, all the sequent calculus proofs are preserved. Moreover, many other proofs become available, and some of these proofs are much shorter. However, proof search in deep inference is subject to a greater nondeterminism, and this nondeterminism constitutes a bottleneck for applications. To this end, we address the problem of reducing nondeterminism in MELL by refining and extending our technique that has been previously applied to multiplicative linear logic and classical logic. We show that, besides the nondeterminism in commutative contexts, the nondeterminism in exponential contexts can be reduced in a proof theoretically clean manner. The method conserves the exponential speed-up in proof construction due to deep inference, exemplified by Statman tautologies. We validate the improvement in accessing the shorter proofs by experiments with our implementations.

UNLABELLED: : Gener is a development module for programming chemical controllers based on DNA strand displacement. Gener is developed with the aim of providing a simple interface that minimizes the opportunities for programming errors: Gener allows the user to test the computations of the DNA programs based on a simple two-domain strand displacement algebra, the minimal available so far. The tool allows the user to perform stepwise computations with respect to the rules of the algebra as well as exhaustive search of the computation space with different options for exploration and visualization. Gener can be used in combination with existing tools, and in particular, its programs can be exported to Microsoft Research's DSD tool as well as to LaTeX. AVAILABILITY AND IMPLEMENTATION: Gener is available for download at the Cosbi website at http://www.cosbi.eu/research/prototypes/gener as a windows executable that can be run on Mac OS X and Linux by using Mono. CONTACT: [email protected].

Rho GTP-binding proteins play a key role as molecular switches in many cellular activities. In response to extracellular stimuli and with the help of regulators (GEF, GAP, Effector, GDI), these proteins serve as switches that interact with their environment in a complex manner. Based on the structure of a published ordinary differential equations (ODE) model, we first present a generic process model for the Rho GTP-binding proteins, and compare it with the ODE model. We then extend the basic model to include the behaviour of the GDI regulators and explore the parameter space for the extended model with respect to biological data from the literature. We discuss the challenges this extension brings and the directions of further research. In particular, we present techniques for modular representation and refinement of process models, where, for example, different Rho proteins with different rates for regulator interactions can be given as instances of the same parametric model.