We introduce RexBDDs, binary decision diagrams (BDDs) that exploit reduction opportunities well beyond those of reduced ordered BDDs, zero-suppressed BDDs, and recent proposals integrating multiple reduction rules. RexBDDs also leverage (output) complement flags and (input) swap flags to potentially decrease the number of nodes by a factor of four. We define a reduced form of RexBDDs that ensures canonicity, and use a set of benchmarks to demonstrate their superior storage and runtime requirements compared to previous alternatives.

Chess endgame tables encode unapproximated game-theoretic values of endgame positions. The speed at which information is retrieved from these tables and their representation size are major limiting factors in their effective use. We explore and make novel extensions to three alternatives (decision trees, decision diagrams, and logic minimization) to the currently preferred implementation (Syzygy) for representing such tables. Syzygy is most compact, but also slowest at handling queries. Two-level logic minimization works well, though performing the compression takes significant time. Decision DAGs and multiterminal binary decision diagrams are both comparable and offer the best querying times, with decision diagrams providing better compression.

The Model Checking Contest (MCC) is an annual competition of software tools for model checking. Tools must process an increasing benchmark gathered from the whole community and may participate in various examinations: state space generation, computation of global properties, computation of some upper bounds in the model, evaluation of reachability formulas, evaluation of CTL formulas, and evaluation of LTL formulas. For each examination and each model instance, participating tools are provided with up to 3600 s and 16 gigabyte of memory. Then, tool answers are analyzed and confronted to the results produced by other competing tools to detect diverging answers (which are quite rare at this stage of the competition, and lead to penalties). For each examination, golden, silver, and bronze medals are attributed to the three best tools. CPU usage and memory consumption are reported, which is also valuable information for tool developers.

Finding good variable orders for decision diagrams is essential for their effective use. We consider Multiway Decision Diagrams (MDDs) encoding a set of fixed-size vectors satisfying a set of linear invariants. Two critical applications of this problem are encoding the state space of a discrete-event discrete state system (DEDS) and encoding all solutions to a set of integer constraints. After studying the relations between the MDD structure and the constraints imposed by the linear invariants, we define i $$_\mathrm {Rank}$$ , a new variable order metric that exploits the knowledge embedded in these invariants. We evaluate i $$_\mathrm {Rank}$$ against other previously proposed metrics on a benchmark of 40 different DEDS and show that it is a better predictor of the MDD size and it is better at driving heuristics for the generation of good variable orders.

Various versions of binary decision diagrams (BDDs) have been proposed in the past, differing in the reduction rule needed to give meaning to edges skipping levels. The most widely adopted, fully-reduced BDDs and zero-suppressed BDDs, excel at encoding different types of boolean functions (if the function contains subfunctions independent of one or more underlying variables, or it tends to have value zero when one of its arguments is nonzero, respectively). Recently, new classes of BDDs have been proposed that, at the cost of some additional complexity and larger memory requirements per node, exploit both cases. We introduce a new type of BDD that we believe is conceptually simpler, has small memory requirements in terms of node size, tends to result in fewer nodes, and can easily be further extended with additional reduction rules. We present a formal definition, prove canonicity, and provide experimental results to support our efficiency claims.

A complementary technique to decision-diagram-based model checking is SAT-based bounded model checking (BMC), which reduces the model checking problem to a propositional satisfiability problem so that the corresponding formula is satisfiable iff a counterexample or witness exists. Due to the branching time nature of computation tree logic (CTL), BMC for the universal fragment of CTL (ACTL) considers a counterexample in a bounded model as a set of bounded paths. Since the existential fragment of CTL (ECTL) is dual to ACTL, and ACTL formulas are often negated to obtain ECTL ones in practice, we focus on BMC for ECTL and propose an improved translation that generates a possibly smaller propositional formula by reducing the number of bounded paths to be considered in a witness. Experimental results show that the formulas generated by our approach are often easier for a SAT solver to answer. In addition, we propose a simple modification to the translation so that it is also defined for models with deadlock states.

MOTIVATION: As the invention of DNA sequencing in the 70s, computational biologists have had to deal with the problem of de novo genome assembly with limited (or insufficient) depth of sequencing. In this work, we investigate the opposite problem, that is, the challenge of dealing with excessive depth of sequencing. RESULTS: We explore the effect of ultra-deep sequencing data in two domains: (i) the problem of decoding reads to bacterial artificial chromosome (BAC) clones (in the context of the combinatorial pooling design we have recently proposed), and (ii) the problem of de novo assembly of BAC clones. Using real ultra-deep sequencing data, we show that when the depth of sequencing increases over a certain threshold, sequencing errors make these two problems harder and harder (instead of easier, as one would expect with error-free data), and as a consequence the quality of the solution degrades with more and more data. For the first problem, we propose an effective solution based on 'divide and conquer': we 'slice' a large dataset into smaller samples of optimal size, decode each slice independently, and then merge the results. Experimental results on over 15 000 barley BACs and over 4000 cowpea BACs demonstrate a significant improvement in the quality of the decoding and the final assembly. For the second problem, we show for the first time that modern de novo assemblers cannot take advantage of ultra-deep sequencing data. AVAILABILITY AND IMPLEMENTATION: Python scripts to process slices and resolve decoding conflicts are available from http://goo.gl/YXgdHT; software Hashfilter can be downloaded from http://goo.gl/MIyZHs CONTACT: [email protected] or [email protected] SUPPLEMENTARY INFORMATION: Supplementary data are available at Bioinformatics online.

A continuous-time Markov process (CTMP) is a collection of variables indexed by a continuous quantity, time. It obeys the Markov property that the distribution over a future variable is independent of past variables given the state at the present time. We introduce continuous-time Markov process representations and algorithms for filtering, smoothing, expected sufficient statistics calculations, and model estimation, assuming no prior knowledge of continuous-time processes but some basic knowledge of probability and statistics. We begin by describing "flat" or unstructured Markov processes and then move to structured Markov processes (those arising from state spaces consisting of assignments to variables) including Kronecker, decision-diagram, and continuous-time Bayesian network representations. We provide the first connection between decision-diagrams and continuous-time Bayesian networks.

For the vast majority of species - including many economically or ecologically important organisms, progress in biological research is hampered due to the lack of a reference genome sequence. Despite recent advances in sequencing technologies, several factors still limit the availability of such a critical resource. At the same time, many research groups and international consortia have already produced BAC libraries and physical maps and now are in a position to proceed with the development of whole-genome sequences organized around a physical map anchored to a genetic map. We propose a BAC-by-BAC sequencing protocol that combines combinatorial pooling design and second-generation sequencing technology to efficiently approach denovo selective genome sequencing. We show that combinatorial pooling is a cost-effective and practical alternative to exhaustive DNA barcoding when preparing sequencing libraries for hundreds or thousands of DNA samples, such as in this case gene-bearing minimum-tiling-path BAC clones. The novelty of the protocol hinges on the computational ability to efficiently compare hundred millions of short reads and assign them to the correct BAC clones (deconvolution) so that the assembly can be carried out clone-by-clone. Experimental results on simulated data for the rice genome show that the deconvolution is very accurate, and the resulting BAC assemblies have high quality. Results on real data for a gene-rich subset of the barley genome confirm that the deconvolution is accurate and the BAC assemblies have good quality. While our method cannot provide the level of completeness that one would achieve with a comprehensive whole-genome sequencing project, we show that it is quite successful in reconstructing the gene sequences within BACs. In the case of plants such as barley, this level of sequence knowledge is sufficient to support critical end-point objectives such as map-based cloning and marker-assisted breeding.

Witness generation is a fundamental model checker feature, but generating shortest witnesses for an EG CTL formula has long been a difficult problem of both theoretical and practical relevance. We propose a symbolic approach to shortest EG witness generation based on edge-valued multi-way decision diagrams. We employ a fix point symbolic iteration to compute the transitive closure enhanced with distance information, using the saturation algorithm to cope with the high computational complexity of this approach. We also extend this approach to tackling the shortest witness generation for other properties and the shortest fair witness generation. Experimental results show that our approach can generate a shortest witness which could not be found within acceptable time using previous algorithms.

The Saturation-style fixpoint iteration strategy for symbolic reachability analysis is particularly effective for globally-asynchronous locally-synchronous discrete-state systems. However, its inherently sequential nature makes it difficult to parallelize Saturation on a NOW. We then propose the idea of using idle workstation time to perform speculative image computations. Since an unrestrained prediction may make excessive use of computational resources, we introduce a history-based approach to dynamically recognize image computation (event firing) patterns and explore only firings that conform to these patterns. In addition, we employ an implicit encoding for the patterns, so that the actual image computation history can be efficiently preserved. Experiments not only show that image speculation works on a realistic model, but also indicate that the use of an implicit encoding together with two heuristics results in a better informed speculation.

We discuss availability aspects of large software- based systems. We classify faults into Bohrbugs, Mandelbugs and aging-related bugs, then examine mitigation methods for the last two bug types. We also consider quantitative approaches to availability assurance.

The saturation strategy for symbolic state-space generation is very effective for globally-asynchronous locally-synchronous discrete-state systems. Its inherently sequential nature, however, makes it difficult to parallelize on a NOW. An initial attempt that utilizes idle workstations to recognize event firing patterns and then speculatively compute firings conforming to these patterns is at times effective but can introduce large memory overheads. We suggest an implicit method to encode the firing history of decision diagram nodes, where patterns can be shared by nodes. By preserving the actual firing history efficiently and effectively, the speculation is more informed. Experiments show that our implicit encoding method not only reduces the memory requirements but also enables dynamic speculation schemes that further improve runtime.

We focus on load balancing policies for homogeneous clustered Web servers that tune their parameters on-the-fly to adapt to changes in the arrival rates and service times of incoming requests. The proposed scheduling policy, ADAPTLOAD, monitors the incoming workload and self-adjusts its balancing parameters according to changes in the operational environment such as rapid fluctuations in the arrival rates or document popularity. Using actual traces from the 1998 World Cup Web site, we conduct a detailed characterization of the workload demands and demonstrate how online workload monitoring can play a significant part in meeting the performance challenges of robust policy design. We show that the proposed load, balancing policy based on statistical information derived from recent workload history provides similar performance benefits as locality-aware allocation schemes, without requiring locality data. Extensive experimentation indicates that ADAPTLOAD results in an effective scheme, even when servers must support both static and dynamic Web pages.

We present an exact decomposition algorithm for the analysis of Markov chains with a GI/G/1-type repetitive structure. Such processes exhibit both M/G/1-type & GI/M/1-type patterns, and cannot be solved using existing techniques. Markov chains with a GI/G/1 pattern result when modeling open systems which accept jobs from multiple exogenous sources, and are subject to failures & repairs; a single failure can empty the system of jobs, while a single batch arrival can add many jobs to the system. Our method provides exact computation of the stationary probabilities, which can then be used to obtain performance measures such as the average queue length or any of its higher moments, as well as the probability of the system being in various failure states, thus performability measures. We formulate the conditions under which our approach is applicable, and illustrate it via the performability analysis of a parallel computer system.

SMART is a software package integrating logic and stochastic modeling formalisms into a single environment. Models expressed in different formalisms can be combined in the same study. To study logical behavior, both explicit and symbolic state-space generation techniques, as well as CTL model-checking algorithms, are available. To study stochastic and timing behavior, both explicit and Kronecker-based numerical solution approaches are available. Since SMART is intended as an industry and research tool, it is written in a modular way that allows for easy integration of new formalisms and solution algorithms.

We focus on adaptive policies for load balancing in clustered web servers, based on the size distribution of the requested documents. The proposed scheduling policy, ADAPTLOAD, adapts its balancing parameters on-the-fly, according to changes in the behavior of the customer population such as fluctuations in the intensity of arrivals or document popularity. Detailed performance comparisons via simulation using traces from the 1998 World Cup show that ADAPTLOAD is robust as it consistently outperforms traditional load balancing policies, especially under conditions of transient overload.

The presence of temporal locality in web traces has long been recognized. However, the close proximity of requests for the same file in a trace can be attributed to two orthogonal reasons: long-term popularity and short-term correlation. The former reflects the fact that requests for a popular document appear "frequently" thus they are likely to be "close" in an absolute sense. The latter reflects the fact that requests for a given document might concentrate around particular points in the trace due to a variety of reasons, such as deadlines or surges in user interests, hence it focuses on "relative" closeness. We introduce a new measure of temporal locality, the scaled stack distance, which is insensitive to popularity and captures instead the impact of short-term correlation, and use it to parameterize a synthetic trace generator. Then, we validate the appropriateness of this quantity by comparing the file and byte miss ratios corresponding to either the original or the synthetic traces.

We present a new approximation algorithm based on an exact representation of the state space S, using decision diagrams, and of the transition rate matrix R, using Kronecker algebra, for a Markov model with K submodels. Our algorithm builds and solves K Markov chains, each corresponding to a different aggregation of the exact process, guided by the structure of the decision diagram, and iterates on their solution until their entries are stable. We prove that exact results are obtained if the overall model has a product-form solution. Advantages of our method include good accuracy, low memory requirements, fast execution times, and a high degree of automation, since the only additional information required to apply it is a partition of the model into the K submodels. As far as we know, this is the first time an approximation algorithm has been proposed where knowledge of the exact state space is explicitly used.

We present new algorithms for the solution of large structured Markov models whose infinitesimal generator can be expressed as a Kronecker expression of sparse matrices. We then compare them with the shuffle-based method commonly used in this context and show how our new algorithms can be advantageous in dealing with very sparse matrices and in supporting both Jacobi-style and Gauss-Seidel-style methods with appropriate multiplication algorithms. Our main contribution is to show how solution algorithms based on Kronecker expression can be modified to consider probability vectors of size equal to the “actual” state space instead of the “potential” state space, thus providing space and time savings. The complexity of our algorithms is compared under different sparsity assumptions. A nontrivial example is studied to illustrate the complexity of the implemented algorithms.

The purpose of this paper is to describe a method for the simulation of the recently introduced fluid stochastic Petri nets. Since such nets result in rather complex system of partial differential equations, numerical solution becomes a formidable task. Because of a mixed (discrete and continuous) state space, simulative solution also poses some interesting challenges, which are addressed in the paper.

High-level formalisms such as stochastic Petri nets can be used to model complex systems. Analysis of logical and numerical properties of these models often requires the generation and storage of the entire underlying state space. This imposes practical limitations on the types of systems that can be modeled. Because of the vast amount of memory consumed, we investigate distributed algorithms for the generation of state space graphs. The distributed construction allows us to take advantage of the combined memory readily available on a network of workstations. The key technical problem is to find effective methods for on-the-fly partitioning, so that the state space is evenly distributed among processors. In this article we report on the implementation of a distributed state space generator that may be linked to a number of existing system modeling tools. We discuss partitioning strategies in the context of Petri net models, and report on performance observed on a network of workstations, as well as on a distributed memory multicomputer.

We consider the problem of generating a large state-space in a distributed fashion. Unlike previously proposed solutions that partition the set of reachable states according to a hashing function provided by the user, we explore heuristic methods that completely automate the process. The first step is an initial random walk through the state space to initialize a search tree, duplicated in each processor. Then, the reachability graph is built in a distributed way, using the search tree to assign each newly found state to classes assigned to the available processors. Furthermore, we explore two remapping criteria that attempt to balance memory usage or future workload, respectively. We show how the cost of computing the global snapshot required for remapping will scale up for system sizes in the foreseeable future. An extensive set of results is presented to support our conclusions that remapping is extremely beneficial.

No abstract available.

Non-Markovian models allow us to capture a very wide range of circumstances in which it is necessary to model phenomena whose times to occurrence is not exponentially distributed. Events such as timeouts in a protocol, service times at a machine performing the same task on each part, and memory access or instruction execution in a low-level h/w or s/w model, have durations which are constant or with a very low variance. Phase-type distributions can be used to approximate a non-exponential, but they increase the size of the state space.The analysis of stochastic systems with non-exponential timing is of increasing interest in the literature and requires the development of suitable modeling tools. Recently, some effort has been devoted to generalize the concept of Stochastic Petri Nets (SPN), by allowing the firing times to be generally distributed.A particular case of non-Markovian SPN, is the class of Deterministic and SPN (DSPN) [1]. A DSPN is a non-Markovian SPN where, in each marking, at most one transition is allowed to have a deterministic firing time with enabling memory policy.A new class of stochastic Petri nets has recently been defined [2, 3] by generalizing the deterministic firing times of the DSPN to generally distributed firing times. The underlying stochastic process for these classes of Petri nets is a Markov Regenerative Process (MRGP). This observation has opened a very fertile line of research aimed at the definition of solvable classes of models whose underlying marking process is an MRGP, and therefore referred to as Markov Regenerative Stochastic Petri Nets (MRSPN).Some of the results in this filed will be described in the session. In particular, Ciardo investigates stochastic confusion by defining the selection probability for transitions attempting to fire at the same time. German introduces the "method of supplementary variables" for the derivation of state equations describing the transient behavior of the marking process. Puliafito describes how, under some constraints, concurrent enabling of several generally distributed timed transitions is allowed. Bobbio and Telek discuss how age memory policy can be included to capture preemptive mechanisms of the resume (prs) type.

We point out some errors in the combinatorial approach for the steady-state analysis of a deterministic and stochastic Petri net (DSPN) presented by M. Lu, D. Zhang, and T. Murata (1990). However, the methodology for analyzing the self-stability of fault-tolerant clock synchronisation (FCS) systems introduced in that paper is applicable for FCS systems with many clocking modules, even if the combinatorial approach is not valid. This is due to the progress in improving the efficiency of the DSPN solution algorithm made in recent years. We show that the explicit computation of the steady-state solution of the DSPN can be performed with reasonable computational effort on a modern workstation by the software package DSPNexpress.>

Stochastic Petri nets (SPN's) with generally distributed firing times can model a large class of systems, but simulation is the only feasible approach for their solution. We explore a hierarchy of SPN classes where modeling power is reduced in exchange for an increasingly efficient solution. Generalized stochastic Petri nets (GSPN's), deterministic and stochastic Petri nets (DSPN's), semi-Markovian stochastic Petri nets (SM-SPN's), timed Petri nets (TPN's), and generalized timed Petri nets (GTPN's) are particular entries in our hierarchy. Additional classes of SPN's for which we show how to compute an analytical solution are obtained by the method of the embedded Markov chain (DSPN's are just one example in this class) and state discretization, which we apply not only to the continuous-time case (PH-type distributions), but also to the discrete case.>

M.D. Beaudry (1978) proposed a simple method of computing the distribution of performability in a Markov reward process. Two extensions of Beaudry's approach are presented. The authors generalize the method to a semi-Markov reward process by removing the restriction requiring the association of zero reward to absorbing states only. The algorithm proceeds by replacing zero reward nonabsorbing states by a probabilistic switch; it is therefore related to the elimination of vanishing states from the reachability graph of a generalized stochastic Petri net and to the elimination of fast transient states in a decomposition approach to stiff Markov chains. The use of the approach is illustrated with three applications.>

Continuous-time Markov chains (CTMC) are widely used mathematical models. Reliability models, queueing networks, and inventory models all require transient solutions of CTMC. The cost of CTMC transient solution increases with size, stiffness, and mission time. To eliminate stiffness and reduce the cost of solution, approximation techniques have been proposed. In this paper, we describe a software package for the specification and solution of stiff CTMC. As an interface, we use a language for the description of Markov chains. The language also provides facilities for controlling the solution procedure. Both exact and approximate solution techniques are provided. To conclude the paper, we use several examples to show the use of our specification language and the utility of our approximation technique. INFORMS Journal on Computing, ISSN 1091-9856, was published as ORSA Journal on Computing from 1989 to 1995 under ISSN 0899-1499.

The authors present a stochastic Petri net model of a replicated file system in a distributed environment where replicated files reside on different hosts and a voting algorithm is used to maintain consistency. Witnesses, which simply record the status of the file but contain no data, can be used in addition to or in place of files to reduce overhead. A model sufficiently detailed to include file status (current or out-of-date) as well as failure and repair of hosts where copies or witnesses reside, is presented. The number of copies and witnesses is not fixed, but is a parameter of the model. Two different majority protocols are examined.>