BACKGROUND: Microbiomes consist of bacteria, viruses, and other microorganisms, and are responsible for many different functions in both organisms and the environment. Past analyses of microbiomes focused on using correlation to determine linear relationships between microbes and diseases. Weak correlations due to nonlinearity between microbe pairs may cause researchers to overlook critical components of the data. With the abundance of available microbiome, we need a method that comprehensively studies microbiomes and how they are related to each other. RESULTS: We collected publicly available datasets from human, environment, and animal samples to determine both symmetric and asymmetric Boolean implication relationships between a pair of microbes. We then found relationships that are potentially invariants, meaning they will hold in any microbe community. In other words, if we determine there is a relationship between two microbes, we expect the relationship to hold in almost all contexts. We discovered that around 330,000 pairs of microbes universally exhibit the same relationship in almost all the datasets we studied, thus making them good candidates for invariants. Our results also confirm known biological properties and seem promising in terms of disease diagnosis. CONCLUSIONS: Since the relationships are likely universal, we expect them to hold in clinical settings, as well as general populations. If these strong invariants are present in disease settings, it may provide insight into prognostic, predictive, or therapeutic properties of clinically relevant diseases. For example, our results indicate that there is a difference in the microbe distributions between patients who have or do not have IBD, eczema and psoriasis. These new analyses may improve disease diagnosis and drug development in terms of accuracy and efficiency.

Biological systems are often modeled as a system of ordinary differential equations (ODEs) with time-invariant parameters. However, cell signaling events or pharmacological interventions may alter the cellular state and induce multimode dynamics of the system. Such systems are naturally modeled as hybrid automata, which possess multiple operational modes with specific nonlinear dynamics in each mode. In this paper we introduce a model checking-enabled framework than can model and analyze both single- and multi-mode biological systems. We tackle the central problem in systems biology- identify parameter values such that a model satisfies desired behaviors-using bounded model checking. We resort to the delta- decision procedures to solve satisfiability modulo theories (SMT) problems and sidestep undecidability of reachability problems. Our framework enables several analysis tasks including model calibration and falsification, therapeutic strategy identification, and Lyapunov stability analysis. We demonstrate the applica- blitliy of these methods using case studies of prostate cancer progression, cardiac cell action potential and radiation diseases.