Search for: All records

Generating the state space of any finite discrete-state system using symbolic algorithms like saturation requires the use of decision diagrams or compatible structures for encoding its reachability set and transition relations. For systems that can be formally expressed using ordinary Petri Nets(PN), implicit relations, a static alternative to decision diagram-based representation of transition relations, can significantly improve the performance of saturation. However, in practice, some systems require more general models, such as self-modifying Petri nets, which cannot currently utilize implicit relations and thus use decision diagrams that are repeatedly rebuilt to accommodate the changing bounds of the system variables, potentially leading to overhead in saturation algorithm. This work introduces a hybrid representation for transition relations, that combines decision diagrams and implicit relations, to reduce the rebuilding overheads of the saturation algorithm for a general class of models. Experiments on several benchmark models across different tools demonstrate the efficiency of this representation. 

Decision diagrams (DDs) are widely used in system verification to compute and store the state space of finite discrete events dynamic systems (DEDSs). DDs are organized into levels, and it is well known that the size of a DD encoding a given set may be very sensitive to the order in which the variables capturing the state of the system are mapped to levels. Computing optimal orders is NP-hard. Several heuristics for variable order computation have been proposed, and metrics have been introduced to evaluate these orders. However, we know of no published evaluation that compares the actual predictive power for all these metrics. We propose and apply a methodology to carry out such an evaluation, based on the correlation between the metric value of a variable order and the size of the DD generated with that order. We compute correlations for several metrics from the literature, applied to many variable orders built using different approaches, for 40 DEDSs taken from the literature. Our experiments show that these metrics have correlations ranging from "very weak or nonexisting" to "strong." We show the importance of highly correlating metrics on variable order heuristics, by defining and evaluating two new heuristics (an improvement of the well-known Force heuristic and a metric-based simulated annealing), as well as a meta-heuristic (that uses a metric to select the "best" variable order among a set of different variable orders). 

Decision diagrams are a well-established data structure for reachability set generation and model checking of high-level models such as Petri nets, due to their versatility and the availability of efficient algorithms for their construction. Using a decision diagram to represent the transition relation of each event of the high-level model, the saturation algorithm can be used to construct a decision diagram representing all states reachable from an initial set of states, via the occurrence of zero or more events. A difficulty arises in practice for models whose state variable bounds are unknown, as the transition relations cannot be constructed before the bounds are known. Previously, on-the-fly approaches have constructed the transition relations along with the reachability set during the saturation procedure. This can affect performance, as the transition relation decision diagrams must be rebuilt, and compute-table entries may need to be discarded, as the size of each state variable increases. In this paper, we introduce a different approach based on an implicit and unchanging representation for the transition relations, thereby avoiding the need to reconstruct the transition relations and discard compute-table entries. We modify the saturation algorithm to use this new representation, and demonstrate its effectiveness with experiments on several benchmark models. 

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 

Multivalued decision diagrams are an excellent technique to study the behavior of discrete-state systems such as Petri nets, but their variable order (mapping places to MDD levels) greatly affects efficiency, and finding an optimal order even just to encode a given set is NP-hard. In state-space generation, the situation is even worse, since the set of markings to be encoded keeps evolving and is known only at the end. Previous heuristics to improve the efficiency of the saturation algorithm often used in state-space generation seek a variable order minimizing a simple function of the Petri net, such as the sum over each transition of the top variable position (SOT) or variable span (SOS). This, too, is NP-hard, so we cannot compute orders that minimize SOT or SOS in most cases but, even if we could, it would have limited effectiveness. For example, SOT and SOS can be led astray by multiple copies of a transition (giving more weight to it), or transitions with equal inputs and outputs (giving weight to transitions that should be ignored). These anomalies inspired us to define SOUPS, a new heuristic that only takes into account the \emph{unique} and \emph{productive} portion of each transition. The SOUPS metric can be easily computed, allowing us to use it in standard search techniques like simulated annealing to find good orders. Experiments show that SOUPS is a much better proxy for the quantities we really hope to improve, the memory and time for MDD manipulation during state-space generation. 

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. 

An advantage of model checking is its ability to generate witnesses or counterexamples. Approaches exist to generate small or minimum witnesses for simple unnested formulas, but no existing method guarantees minimality for general nested ones. Here, we give a definition of witness size, use edge-valued decision diagrams to recursively compute the minimum witness size for each subformula, and describe a general approach to build minimum tree-like witnesses for existential CTL. Experimental results show that for some models, our approach is able to generate minimum witnesses while the traditional approach is not. 

The size of a BDD heavily depends on its variable order. Significant efforts have been made to find good variable orders, statically or dynamically. This paper concentrates on a related issue, transforming a BDD from one variable order to another, as needed when an application must cope with BDDs having different variable orders. Instead of rebuilding BDDs as done in previous work, we accomplish such transformation through a sequence of adjacent variable swaps. Since there are many ways to schedule these swaps, we propose and compare several heuristics to determine good schedules.