Search

The class UMU consists of propositional formulas which are a union of minimal unsatisfiable formulas (MU formulas). The structural complexity of UMU formulas depends essentially on the type and degree of intertwining of the MU subformulas. Starting from class of formulas that consist only of clause (or variable) disjoint minimal unsatisfiable subformulas, we study various UMU subclasses given by weakening and these conditions. Generalizing an idea from [6] , we investigate a characterization of UMU formulas by whether they allow transformation into a MU formula by adding literals and/or clauses. It can be shown that simplicity in constructing of such extensions correlates with the degree of intertwining of the MU subformulas. For UMU formulas, however, we can give only extensions that have an exponential size in the worst case. The question of the existence of short MU combinations of MU-formulas by adding literals and clauses remains open. [ABSTRACT FROM AUTHOR]

A dominating set S of graph G is called an r-grouped dominating set if S can be partitioned into S 1 , S 2 , ... , S k such that the size of each unit S i is r and the subgraph of G induced by S i is connected. The concept of r -grouped dominating sets generalizes several well-studied variants of dominating sets with requirements for connected component sizes, such as the ordinary dominating sets (r = 1), paired dominating sets (r = 2), and connected dominating sets (r is arbitrary and k = 1). In this paper, we investigate the computational complexity of r -Grouped Dominating Set , which is the problem of deciding whether a given graph has an r -grouped dominating set with at most k units. For general r , r -Grouped Dominating Set is hard to solve in various senses because the hardness of the connected dominating set is inherited. We thus focus on the case in which r is a constant or a parameter, but we see that r -Grouped Dominating Set for every fixed r > 0 is still hard to solve. From the observations about the hardness, we consider the parameterized complexity concerning well-studied graph structural parameters. We first see that r -Grouped Dominating Set is fixed-parameter tractable for r and treewidth, which is derived from the fact that the condition of r -grouped domination for a constant r can be represented as monadic second-order logic (MSO 2). This fixed-parameter tractability is good news, but the running time is not practical. We then design an O ⁎ (min ⁡ { (2 τ (r + 1)) τ , (2 τ) 2 τ }) -time algorithm for general r ≥ 2 , where τ is the twin cover number, which is a parameter between vertex cover number and clique-width. For paired dominating set and trio dominating set, i.e., r ∈ { 2 , 3 } , we can speed up the algorithm, whose running time becomes O ⁎ ((r + 1) τ). We further argue the relationship between FPT results and graph parameters, which draws the parameterized complexity landscape of r -Grouped Dominating Set. [ABSTRACT FROM AUTHOR]

We introduce a method for translating an alternating weak Büchi automaton (AWA), which corresponds to a Linear Dynamic Logic (LDL) formula, to an unambiguous Büchi automaton (UBA). Our translations generalize constructions for Linear Temporal Logic (LTL), a less expressive specification language than LDL. In classical constructions, LTL formulas are first translated to alternating very weak Büchi automata (AVAs)—automata that have only singleton strongly connected components (SCCs); these AVAs are then handled by efficient disambiguation procedures. However, general AWAs can have larger SCCs, which complicates disambiguation. Currently, the only available disambiguation procedure has to go through an intermediate construction of nondeterministic Büchi automata (NBAs), which would incur an exponential blow-up of its own. We introduce a translation from general AWAs to UBAs with a singly exponential blow-up, which also immediately provides a singly exponential translation from LDL to UBAs. Interestingly, the complexity of our translation is smaller than the best known disambiguation algorithm for NBAs (broadly (0.53 n) n vs. (0.76 n) n), while the input of our construction can be exponentially more succinct. • We have presented the first singly exponential translation of AWAs to UBAs. • The translation complexity to UBAs from AWAs is lower than from NBAs while AWAs can be exponentially smaller than NBAs. • We have established an exponential lower bound for the translation from AWAs to UBAs. [ABSTRACT FROM AUTHOR]

The skin microbiome plays an important role in the maintenance of a healthy skin. It is an ecosystem, composed of several species, competing for resources and interacting with the skin cells. Imbalance in the cutaneous microbiome, also called dysbiosis, has been correlated with several skin conditions, including acne and atopic dermatitis. Generally, dysbiosis is linked to colonization of the skin by a population of opportunistic pathogenic bacteria. Treatments consisting in non-specific elimination of cutaneous microflora have shown conflicting results. In this article, we introduce a mathematical model based on ordinary differential equations, with 2 types of bacteria populations (skin commensals and opportunistic pathogens) and including the production of antimicrobial peptides to study the mechanisms driving the dominance of one population over the other. By using published experimental data, assumed to correspond to the observation of stable states in our model, we reduce the number of parameters of the model from 13 to 5. We then use a formal specification in quantitative temporal logic to calibrate our model by global parameter optimization and perform sensitivity analyses. On the time scale of 2 days of the experiments, the model predicts that certain changes of the environment, like the elevation of skin surface pH, create favorable conditions for the emergence and colonization of the skin by the opportunistic pathogen population, while the production of human AMPs has non-linear effect on the balance between pathogens and commensals. Surprisingly, simulations on longer time scales reveal that the equilibrium reached around 2 days can in fact be a quasi-stable state followed by the reaching of a reversed stable state after 12 days or more. We analyze the conditions of quasi-stability observed in this model using tropical algebraic methods, and show their non-generic character in contrast to slow-fast systems. These conditions are then generalized to a large class of population dynamics models over any number of species. • A first ODE model of skin microbiome with anti-microbial peptide interactions. • Reduced model by steady-state reasoning. • Parameterized using quantitative temporal logic methods. • Quasi-stability phenomenon analyzed by tropical algebra methods. • Generalized to a large class of population dynamics. [ABSTRACT FROM AUTHOR]

When modelling a complex biological system, the bottleneck of the process is the determination of parameter values that lead to model dynamics that are compatible with observations. Even for discrete modelling frameworks, this step can be limiting. Here we introduce a representation of the whole family of discrete models that can be associated to a biological system, where states are shared by all models and transitions are labelled by constraints on dynamical parameters. A model checking procedure is defined to handle this new representation. This procedure extracts the conditions on parameter settings that are compatible with a given dynamical property expressed in a temporal logic. We prove the correctness of our model checking procedure and illustrate the advantage of such an approach on some different systems of biological interest. • Identifying the parameters that control the dynamics of biological systems is one of the major problems in the modelling process. • The brute-force approach considers each parameter setting, builds the associated dynamics and confronts it with the known temporal properties. • The brute-force approach faces the combinatorial explosion of the number of parameter settings (a product of double exponentials). • We introduce a parametric model representing the set of possible transitions (constrained Kripke structure). • An ad hoc model checking algorithm decides for each state under which conditions on the parameters the temporal properties in that state are true. [ABSTRACT FROM AUTHOR]

GF(2)-operations on formal languages (Bakinova et al., "Formal languages over GF(2)", Inf. Comput., 2022) are variants of the classical concatenation and Kleene star obtained by replacing Boolean logic in their definitions with the GF(2) field. This paper investigates closure and non-closure of basic families of languages under these operations. First, it is proved that the group languages (those defined by permutation automata) are closed under GF(2)-concatenation and not closed under GF(2)-star; furthermore, the state complexity of GF(2)-concatenation for m -state and n -state permutation automata is determined as m ⋅ 2 n. Next, it is shown that the languages defined by trellis automata (one-way real-time cellular automata) are not closed under either operation, but are closed under GF(2)-concatenation with regular languages; the context-free languages and their linear and unambiguous variants are not closed under GF(2)-concatenation with a two-element set, nor under GF(2)-star; the LR(k) languages are closed under GF(2)-concatenation with a regular set on the right, but not on the left. • Two operations on formal languages, GF(2)-concatenation and GF(2)-star, are investigated. • The language family recognized by permutation automata is closed under GF(2)-concatenation, but not under GF(2)-star. • The language families defined by context-free grammars and their main subclasses are not closed under either operation. • The family recognized by trellis automata is closed under GF(2)-concatenation with regular sets. • The family defined by LR(k) grammars is closed under GF(2) concatenation with regular sets on the right, but not on the left. [ABSTRACT FROM AUTHOR]