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.
more »
« less
Reachability Set Generation Using Hybrid Relation Compatible Saturation
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.
more »
« less
- Award ID(s):
- 1642397
- PAR ID:
- 10207896
- Date Published:
- Journal Name:
- Lecture notes in computer science
- Volume:
- 12448
- ISSN:
- 0302-9743
- Page Range / eLocation ID:
- 37-51
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
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.more » « less
-
We argue for the use of Petri nets as a modeling language for the iterative development process of interactive robotic systems. Petri nets, particularly Timed Colored Petri nets (TCPNs), have the potential to unify various phases of the development process-design, specification, simulation, validation, implementation, and deployment. We additionally discuss future directions for creating a domain-specific variant of TCPNs tailored specifically for HRI systems development.more » « less
-
Conditional preference networks (CP-nets) are an intuitive and expressive representation for qualitative preferences. Such models must somehow be acquired. Psychologists argue that direct elicitation is suspect. On the other hand, learning general CP-nets from pairwise comparisons is NP-hard, and --- for some notions of learning --- this extends even to the simplest forms of CP-nets. We introduce a novel, concise encoding of binary-valued, tree-structured CP-nets that supports the first local-search-based CP-net learning algorithms. While exact learning of binary-valued, tree-structured CP-nets --- for a strict, entailment-based notion of learning --- is already in P, our algorithm is the first space-efficient learning algorithm that gracefully handles noisy (i.e., realistic) comparison sets.more » « less
-
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 when the full compression algorithm can be run. Decision DAGs and multiterminal binary decision diagrams are comparable and offer the best querying times, with decision diagrams providing better compression.more » « less