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.

Chemical reaction networks (CRNs) are an emerging distributed computational paradigm where programs are encoded as a set of abstract chemical reactions. CRNs can be compiled into DNA strands which perform the computations in vitro, creating a foundation for intelligent nanodevices. Recent research proposed a software testing framework for stochastic CRN programs in simulation, however, it relies on existing program specifications. In practice, specifications are often lacking and when they do exist, transforming them into test cases is time-intensive and can be error prone. In this work, we propose an inference technique called ChemFlow which extracts 3 types of invariants from an existing CRN model. The extracted invariants can then be used for test generation or model validation against program implementations. We applied ChemFlow to 13 CRN programs ranging from toy examples to real biological models with hundreds of reactions. We find that the invariants provide strong fault detection and often exhibit less flakiness than specification derived tests. In the biological models we showed invariants to developers and they confirmed that some of these point to parts of the model that are biologically incorrect or incomplete suggesting we may be able to use ChemFlow to improve model quality.

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.

Abstract In this work, we present a formal language, CTML, to reason over probabilistic systems. CTML extends stochastic temporal logics in a way that it takes a real value as input and output a real value in the range of [ 0 , ∞ ) , as opposed to 0/1 values as input and output, and it can nest real values. This allows CTML to express a rich set of queries towards the unification of model checking and performance evaluation. In fact, CTML covers PCTL. It can express a nontrivial subset of PLTL formulas that cannot be expressed by PCTL. The significance of this result is that the overall complexity of CTML is linear, as opposed to exponential as it is with PLTL, in the size of the operators for a given formula, and polynomial in the size of a given model. Moreover, CTML can express real-valued performance queries such as: “if a system encounters a failure, what is the expected time to reach a recovery state?” that cannot be expressed by a probabilistic model checking logic, because they are “probabilistic” at most. Along with the specification language, we present a set of algorithms for the evaluation of the language and show proofs for their correctness. Additionally, we include an application example and show experimental results.

Dynamic systems in DNA nanotechnology are often programmed using a chemical reaction network (CRN) model as an intermediate level of abstraction. In this paper, we design and analyze a CRN model of a watchdog timer, a device commonly used to monitor the health of a safety critical system. Our process uses incremental design practices with goal-oriented requirements engineering, software verification tools, and custom software to help automate the software engineering process. The watchdog timer is comprised of three components: an absence detector, a threshold filter, and a signal amplifier. These components are separately designed and verified, and only then composed to create the molecular watchdog timer. During the requirements-design iterations, simulation, model checking, and analysis are used to verify the system. Using this methodology several incomplete requirements and design flaws were found, and the final verified model helped determine specific parameters for biological experiments.

Model checking is usually applied at the design phase to verify that preliminary high-level design specifications conform to their requirements. Source code analysis, on the other hand, is used to check for correctness of implementation once it is realized from the design specifications. However, the current practice of validating a design and its implementation in isolation makes it necessary to employ rigorous testing analysis to empirically ensure that the implementation satisfies the design specification. This article describes a formal framework that allows design models to contain embedded partial implementations as components; these models are then formally analyzed to ensure that global requirements are satisfied. This framework can be utilized to incrementally develop and ensure correctness of the design and the corresponding implementation. Realization of this framework requires consolidation and expansion of traditional formal verification techniques by integration of model checking, program analysis and constraint solving

Implicit techniques for construction and representation of the reachability set of a high-level model have become quite efficient for certain types of models. In particular, previous work developed a "saturation" algorithm that exploits asynchronous behavior to efficiently construct the reachability set using multiway decision diagrams, but using a Kronecker product expression to represent each model event. For models whose events do not naturally fall into this category, use of the saturation algorithm requires adjusting the model by combining components or splitting events into subevents until a Kronecker product expression is possible. In practice, this can lead to additional overheads during reachability set construction. This paper presents a new version of the saturation algorithm that works for a general class of models: models whose events are not necessarily expressible as Kronecker products, models containing events with complex priority structures, and models whose state variables have unknown bounds. Experimental results are given for several examples

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.

Implicit techniques for representing and generating the reachability set of a high-level model have become quite efficient. However, such techniques are usually restricted to models whose events have equal priority. Models containing events with differing classes of priority or complex priority structure, in particular models with immediate events, have thus been required to use explicit reachability set generation techniques. In this paper, we present an efficient implicit technique, based on multi-valued decision diagram representations for sets of states and matrix diagram representations for next-state functions, that can handle models with complex priority structure. If the model contains immediate events, the vanishing states can be eliminated either during generation, by manipulating the matrix diagram, or after generation, by manipulating the multi-valued decision diagram. We apply both techniques to several models and give detailed results.

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.