Armstrong databases for functional and inclusion dependencies

An Armstrong database is a database that obeys precisely a given set of sentences (and their logical consequences) and no other sentences of a given type. It is shown that if the sentences of interest are inclusion dependencies and standard functional dependencies (functional dependencies for which the left-hand side is nonempty), then there is always an Armstrong database for each set of sentences. (An example of an inclusion dependency is the sentence that says that every $\text{MANAGER}$ is an $\text{EMPLOYEE}$.) If, however, the sentences of interest are inclusion dependencies and unrestricted functional dependencies, then there need not exist an Armstrong database. This result holds even if we allow only ‘full’ inclusion dependencies. Thus, a fairly sharp line is drawn, in a case of interest, as to when an Armstrong database must exist. These results hold whether we restrict our attention to finite databases (databases with a finite number of tuples), or whether we allow unrestricted databases.     

View-based query processing: On the relationship between rewriting,answering and losslessness

As a result of the extensive research in view-based query processing, three notions have been identified as fundamental, namely rewriting, answering, and losslessness. Answering amounts to computing the tuples satisfying the query in all databases consistent with the views. Rewriting consists in first reformulating the query in terms of the views and then evaluating the rewriting over the view extensions. Losslessness holds if we can answer the query by solely relying on the content of the views. While the mutual relationship between these three notions is easy to identify in the case of conjunctive queries, the terrain of notions gets considerably more complicated going beyond such a query class. In this paper, we revisit the notions of answering, rewriting, and losslessness and clarify their relationship in the setting of semistructured databases, and in particular for the basic query class in this setting, i.e., two-way regular path queries. Our first result is a clean explanation of the relationship between answering and rewriting, in which we characterize rewriting as a “linear approximation” of query answering. We show that applying this linear approximation to the constraint-satisfaction framework yields an elegant automata-theoretic approach to query rewriting. As for losslessness, we show that there are indeed two distinct interpretations for this notion, namely with respect to answering, and with respect to rewriting. We also show that the constraint-theoretic approach and the automata-theoretic approach can be combined to give algorithmic characterization of the various facets of losslessness. Finally, we deal with the problem of coping with loss, by considering mechanisms aimed at explaining lossiness to the user.     

GSTE is partitioned model checking

Verifying whether an ω-regular property is satisfied by a finite-state system is a core problem in model checking. Standard techniques build an automaton with the complementary language, compute its product with the system, and then check for emptiness. Generalized symbolic trajectory evaluation (GSTE) has been recently proposed as an alternative approach, extending the computationally efficient symbolic trajectory evaluation (STE) to general ω-regular properties. In this paper, we show that the GSTE algorithms are essentially a partitioned version of standard symbolic model-checking (SMC) algorithms, where the partitioning is driven by the property under verification. We export this technique of property-driven partitioning to SMC and show that it typically does speed up SMC algorithms. A shorter version of this paper has been presented at CAV’04 (R. Sebastiani et al., Lecture Notes in Comput. Sci., vol. 3114, pp. 143–160, 2004). R. Sebastiani supported in part by the CALCULEMUS! IHP-RTN EC project, code HPRN-CT-2000-00102, by a MIUR COFIN02 project, code 2002097822_003, and by a grant from the Intel Corporation. M.Y. Vardi supported in part by NSF grants CCR-9988322, CCR-0124077, CCR-0311326, IIS-9908435, IIS-9978135, EIA-0086264, and ANI-0216467 by BSF grant 9800096, and by a grant from the Intel Corporation.     

On computing minimal independent support and its applications to sampling and counting

Constrained sampling and counting are two fundamental problems arising in domains ranging from artificial intelligence and security, to hardware and software testing. Recent approaches to approximate solutions for these problems rely on employing SAT solvers and universal hash functions that are typically encoded as XOR constraints of length n/2 for an input formula with n variables. As the runtime performance of SAT solvers heavily depends on the length of XOR constraints, recent research effort has been focused on reduction of length of XOR constraints. Consequently, a notion of Independent Support was proposed, and it was shown that constructing XORs over independent support (if known) can lead to a significant reduction in the length of XOR constraints without losing the theoretical guarantees of sampling and counting algorithms. In this paper, we present the first algorithmic procedure (and a corresponding tool, called MIS) to determine minimal independent support for a given CNF formula by employing a reduction to group minimal unsatisfiable subsets (GMUS). By utilizing minimal independent supports computed by MIS, we provide new tighter bounds on the length of XOR constraints for constrained counting and sampling. Furthermore, the universal hash functions constructed from independent supports computed by MIS provide two to three orders of magnitude performance improvement in state-of-the-art constrained sampling and counting tools, while still retaining theoretical guarantees.     

From liveness to promptness

Liveness temporal properties state that something “good” eventually happens, e.g., every request is eventually granted. In Linear Temporal Logic (LTL), there is no a priori bound on the “wait time” for an eventuality to be fulfilled. That is, F θ asserts that θ holds eventually, but there is no bound on the time when θ will hold. This is troubling, as designers tend to interpret an eventuality F θ as an abstraction of a bounded eventuality F ^≤k θ, for an unknown k, and satisfaction of a liveness property is often not acceptable unless we can bound its wait time. We introduce here prompt-LTL, an extension of LTL with the prompt-eventually operator F _p . A system S satisfies a prompt-LTL formula φ if there is some bound k on the wait time for all prompt-eventually subformulas of φ in all computations of S. We study various problems related to prompt-LTL, including realizability, model checking, and assume-guarantee model checking, and show that they can be solved by techniques that are quite close to the standard techniques for LTL.     

A heuristic clustering approach to use case-aware application-specific network-on-chip synthesis

Network-on-chip (NoC) is a promising paradigm for efficient communication between the processing elements inside multi-core system-on-chip (SoC) and general purpose chip-multi-processor. Choosing appropriate topology for NoCs with predefined application characteristics plays a pivotal role in improving power and area metrics. Until now, different irregular topologies with varying objective optimization parameters have been offered. In this paper, a novel heuristic topology synthesis method for creating application-specific NoCs consisting of some use cases which are described the applications characteristics has been proposed. This approach is composed of application clustering for assigning cores to specific routers, topology construction for finding a routing path for all flows, and also link insertion for producing final topology by interconnecting the routers. To confirm the proposed method, results of an industrial smartphone SoC and some generic benchmarks have been used as case studies. Experimental results demonstrate the benefits of the proposed method compared to state-of-the-art approaches.     

Symbolic Techniques in Satisfiability Solving

Recent work has shown how to use binary decision diagrams for satisfiability solving. The idea of this approach, which we call symbolic quantifier elimination, is to view an instance of propositional satisfiability as an existentially quantified proposition formula. Satisfiability solving then amounts to quantifier elimination; once all quantifiers have been eliminated, we are left with either 1 or 0. Our goal in this work is to study the effectiveness of symbolic quantifier elimination as an approach to satisfiability solving. To that end, we conduct a direct comparison with the DPLL-based ZChaff, as well as evaluate a variety of optimization techniques for the symbolic approach. In comparing the symbolic approach to ZChaff, we evaluate scalability across a variety of classes of formulas. We find that no approach dominates across all classes. While ZChaff dominates for many classes of formulas, the symbolic approach is superior for other classes of formulas. Once we have demonstrated the viability of the symbolic approach, we focus on optimization techniques for this approach. We study techniques from constraint satisfaction for finding a good plan for performing the symbolic operations of conjunction and of existential quantification. We also study various variable-ordering heuristics, finding that while no heuristic seems to dominate across all classes of formulas, the maximum-cardinality search heuristic seems to offer the best overall performance. ★A preliminary version of the paper was presented in SAT'04. Supported in part by NSF grants CCR-9988322, CCR-0124077, CCR-0311326, IIS-9908435, IIS-9978135, EIA-0086264, ANI-0216467, and by BSF grant 9800096.     

Once and for all

It has long been known that past-time operators add no expressive power to linear temporal logics. In this paper, we consider the extension of branching temporal logics with past-time operators. Two possible views regarding the nature of past in a branching-time model induce two different such extensions. In the first view, past is branching and each moment in time may have several possible futures and several possible pasts. In the second view, past is linear and each moment in time may have several possible futures and a unique past. Both views assume that past is finite. We discuss the practice of these extensions as specification languages, characterize their expressive power, and examine the complexity of their model-checking and satisfiability problems.     

Cryostructuring of polymer systems. XXIX. Preparation and characterization of supermacroporous (spongy) agarose-based cryogels used as three-dimensional scaffolds for culturing insulin-producing cell aggregates

Supermacroporous (spongy) agarose-based cryogels were prepared by a two-step freezing procedure (freezing at −30°C followed by incubation at a warmer subzero temperature) and subsequent thawing. The cryogels were formed as cylinders in plastic syringes and as platelike samples in flat metal molds. The characteristic feature of the gel matrices thus obtained was their heterogeneous spongelike morphology with a system of interconnected gross (50–250-μm and larger) pores. The influence of the cryogenic processing regimes on the properties and porous morphology of such agarose cryogels was explored by flow-through analysis, optical microscopy, thermometry, and high-sensitivity differential scanning calorimetry. These biocompatible, spongelike matrices were used as three-dimensional scaffolds for culturing insulin-producing rat insulinoma cells self-assembled in multicellular spherical aggregates (pseudoislets). The cell morphology and functional activity of such pseudoislets indicate that supermacroporous agarose-based cryogels can be useful as a tool for engineering biohybrid insulin-producing tissue. © 2008 Wiley Periodicals, Inc. J Appl Polym Sci, 2008     

Symbolic systems,explicit properties: on hybrid approaches for LTL symbolic model checking

In this work we study hybrid approaches to LTL symbolic model checking; that is, approaches that use explicit representations of the property automaton, whose state space is often quite manageable, and symbolic representations of the system, whose state space is typically exceedingly large. We compare the effects of using, respectively, (i) a purely symbolic representation of the property automaton, (ii) a symbolic representation, using logarithmic encoding, of explicitly compiled property automaton, and (iii) a partitioning of the symbolic state space according to an explicitly compiled property automaton. We apply this comparison to three model-checking algorithms: the doubly-nested fixpoint algorithm of Emerson and Lei, the reduction of emptiness to reachability of Biere et al., and the singly-nested fixpoint algorithm of Bloem et al. for weak automata. The emerging picture from our study is quite clear, hybrid approaches outperform pure symbolic model checking, while partitioning generally performs better than logarithmic encoding. The conclusion is that the hybrid approaches benefit from state-of-the-art techniques in semantic compilation of LTL properties. Partitioning gains further from the fact that the image computation is applied to smaller sets of states.