Conference papers | Andrew S. Miner

2026

C34

Extending PRCTL with Conditional Expected Reward Operators

Eshita Zaman, Gianfranco Ciardo, and Andrew S. Miner

In Automated Technology for Verification and Analysis, Dec 2026
C33

Binary Decision Diagrams Unchained

Jaehyeok Choi and Andrew S. Miner

In Proc. 26th Conf. on Formal Methods in Computer-Aided Design (FMCAD 2026), Sep 2026

Abs DOI PDF

We introduce Unchained Binary Decision Diagrams (UBDDs), a new variant of Binary Decision Diagrams (BDDs) with a simple but expressive set of edge rules, including complement and swap flags. These new UBDDs are able to exploit generalized forms of common patterns that are only partially supported by existing single-rule BDDs, including BDDs and zero-suppressed BDDs, and multiple-rule BDDs, including chained BDDs, tagged BDDs, and RexBDDs. We provide reduction rules for UBDDs and show that the reduced form is canonical, and give some algorithms for UBDD manipulation. We show that UBDDs can never be worse than a constant factor larger than existing forms, and can be arbitrarily smaller for certain functions. Finally, we present experimental evidence that UBDDs can perform extremely well on practical verification applications.

2025

C32

CTL Model Checking Partially Specified Systems

Eshita Zaman, Christopher Johannsen, Andrew S. Miner, and 2 more authors

In International Conference on Integrated Formal Methods (iFM), 2025

Abs DOI PDF

The behavioral specifications of a system are often partial at early stages of development due to pending design decisions. We view such specifications as being parameterized by these decisions and consider the problem of identifying a possible concretization, i.e., taking a subset of these decisions, to ensure that the system conforms to the desired requirements. We capture such a partially specified system as a partially-labeled Kripke structure (plKS), where certain propositions labeling the states of the Kripke structure correspond to pending design decisions, thus may be unknown. We then reduce the verification problem to model checking different plKS instances, each corresponding to a specific set of design decisions taken, inducing a semi-lattice on the instances. Central to our solution strategy is the effective and efficient exploration of this semi-lattice and the application of model checking techniques to plKSs with 3-valued semantics of temporal properties, to take into account unknown state labels. We also address the problem of identifying an optimal instance of a partially-specified system that satisfies a desired property, where the cost of design decisions drive the optimality criterion. We use a prototype implementation of our strategy to validate its viability on a multi-objective path planning problem.

2024

C31

Comparing Lossless Compression Methods for Chess Endgame Data

Dave Gomboc, Christian R. Shelton, Andrew S. Miner, and 1 more author

In European Conference on Artificial Intelligence, 2024

Abs DOI PDF

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.
C30

RexBDDs: Reduction-on-edge complement-and-swap binary decision diagrams

Gianfranco Ciardo, Andrew S. Miner, Lichuan Deng, and 1 more author

In Proc. DAC’24, Jun 2024

Abs DOI PDF

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.

2023

C29

Research Directions in Decision Diagram Technology

Gianfranco Ciardo and Andrew S. Miner

In 2023 IEEE John Vincent Atanasoff Symposium on Modern Computing (JVA), Jul 2023

Abs DOI PDF

Binary decision diagrams (BDDs) have been a huge success story in hardware and software verification and are increasingly applied to a wide range of combinatorial problems. While BDDs can encode boolean-valued functions of boolean-valued variables, many BDD variants have been proposed, not just to improve their efficiency, but to manage multivalued domains (a straightforward extension), multivalued ranges (using several competitive alternatives), and two-dimensional data (relations and matrices instead of sets or vectors). Orthogonally to these extensions, much effort has been spent on variable order heuristics, an essential aspect that can affect memory and time requirements by up to an exponential factor. We survey some of these exciting results and discuss some fruitful research directions for further work.

2022

C28

Inference and Test Generation using Program Invariants in Chemical Reaction Networks

Michael C. Gertin, Alexis L. Marsh, James I. Lathrop, and 3 more authors

In 44th Intl. Conf. on Software Eng. (ICSE ’22), 2022

Abs DOI PDF

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.

2020

C27

Reachability Set Generation Using Hybrid Relation Compatible Saturation

Shruti Biswal and Andrew S. Miner

In Reachability Problems, 2020

Abs DOI PDF

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.

2019

C26

Improving Saturation Efficiency with Implicit Relations

Shruti Biswal and Andrew S. Miner

In Application and Theory of Petri Nets and Concurrency, 2019

Abs DOI PDF

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.
C25

Presentation of the 9th Edition of the Model Checking Contest

Elvio Amparore, Bernard Berthomieu, Gianfranco Ciardo, and 16 more authors

In TACAS 2019, Apr 2019

Abs DOI PDF

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.
C24

i_Rank: A Variable Order Metric for DEDS Subject to Linear Invariants

Elvio Amparore, Gianfranco Ciardo, Susanna Donatelli, and 1 more author

In TACAS 2019, Apr 2019

Abs DOI PDF

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_Rank, a new variable order metric that exploits the knowledge embedded in these invariants. We evaluate i_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.
C23

Binary Decision Diagrams with Edge-Specified Reductions

Junaid Babar, Chuan Jiang, Gianfranco Ciardo, and 1 more author

In TACAS 2019, Apr 2019

Abs DOI PDF

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.

2018

C22

Action and State Based Computation Tree Measurement Language and Algorithms

Yaping Jing and Andrew S. Miner

In QEST 2018, 2018

Abs DOI PDF

The computation tree measurement language (CTML) is a real-valued specification formalism, designed to express performance measures and dependability properties in a single framework. It is a further extension of probabilistic model checking logic in such a way that it expands the input and output value from the range of [0, 1] to the range of [0, ∞]. Unlike probabilistic computation tree logic (PCTL) or continuous stochastic logic (CSL), CTML can nest real values. As such, it turns out that CTML can express a nontrivial subset of probabilistic linear time logic (PLTL) formulas that cannot be expressed by PCTL while keeping the overall computational complexity being polynomial in the size of both an input formula and model. Moreover, it can express queries such as “when a message is sent, what is the expected time until it is received?” that cannot be expressed by an existing probabilistic logic, because they are “probabilistic” at most. While powerful, CTML is a state-based specification formalism. In this work, we introduce a stronger formal query language, called action and state based computation tree measurement language (asCTML). asCTML extends from CTML, for answering performance queries that operates over paths featured by a combination of states and actions. Inspired by the action and state based continuous stochastic logic (asCSL), asCTML supports multiple actions.

2017

C21

Decision Diagrams for Petri Nets: which Variable Ordering?

Elvio Gilberto Amparore, Susanna Donatelli, Marco Beccuti, and 2 more authors

In Proceedings of the International Workshop on Petri Nets and Software Engineering, 2017

Abs PDF

The efficacy of decision diagram techniques for state space generation is known to be heavily dependent on the variable order. Ordering can be done a-priori (static) or during the state space generation (dynamic). We focus our attention on static ordering techniques. Many static decision diagram variable ordering techniques exist, but it is hard to choose which method to use, since only fragmented information about their performance is available. In the work reported in this paper we used the models of the Model Checking Contest 2016 edition to provide an extensive comparison of 14 different algorithms, in order to better understand their efficacy. Comparison is based on the size of the decision diagram of the generated state space. The state space is generated using the Saturation method provided by the Meddly library.
C20

Variable reordering in binary decision diagrams

Chuan Jiang, Junaid Babar, Gianfranco Ciardo, and 2 more authors

In Proc. IWLS, 2017

Abs PDF

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.

2015

C19

Power consumption analysis of replicated virtual applications

Pietro Piazzolla, Gianfranco Ciardo, and Andrew Miner

In 22th Int. Conf. on Analytical and Stochastic Modelling Techniques and Applications (ASMTA’15), May 2015

DOI PDF

2014

C18

Automated Requirements Analysis for a Molecular Watchdog Timer

Samuel J. Ellis, Eric R. Henderson, Titus H. Klinge, and 5 more authors

In Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering, Vasteras, Sweden, 2014

DOI PDF
C17

Explicit State Space and Markov Chain Generation Using Decision Diagrams

Junaid Babar and Andrew Miner

In 11th European Workshop on Performance Engineering (EPEW’14), Sep 2014

Abs DOI PDF

Various forms of decision diagrams have been successfully used for quite some time to generate the state space and Markov chain from models expressed in some high–level formalism. A variety of efficient, “symbolic” algorithms, which manipulate sets of states instead of individual states, are known for this purpose. However, there are cases where explicit generation algorithms are still used. This paper seeks to efficiently use decision diagrams as replacement data structures within an existing explicit generation implementation. The necessary decision diagram algorithms are presented, and small changes to the explicit generation algorithm are suggested to improve the overall generation process. The efficiency of the new algorithms is illustrated using several models.

2010

C16

Meddly: Multi–terminal and Edge–valued Decision Diagram LibrarY

Junaid Babar and Andrew Miner

In 7th Int. Conf. on Quantitative Evaluation of Systems (QEST’10), Sep 2010

Abs PDF

This paper introduces Meddly (Multi-terminal and Edge-valued Decision Diagram LibrarY), an open-source C/C++ library designed from its conception to support Multi-Terminal and Edge-Valued Decision Diagrams. We highlight Meddly’s simple and expert interfaces, its loosely-coupled architecture, and the operations available on decision diagrams and conclude with some performance data.
C15

A Formal Language toward the Unification of Model Checking and Performance Evaluation

Andrew S. Miner and Yaping Jing

In 17th Int. Conf. on Analytical and Stochastic Modelling Techniques and Applications (ASMTA’10), Jun 2010

Abs DOI PDF

There are currently a variety of logics used to describe properties of discrete–state systems, such as linear temporal logic (LTL) and computation tree logic (CTL), and of discrete–state stochastic systems, such as probabilistic CTL (PCTL) and continuous stochastic logic (CSL). While powerful, these logics are by definition limited to producing only true or false responses. In this work, we introduce a query language, CTML, that operates on real–valued quantities to reason over probabilistic systems. CTML is inspired by, and evolves from stochastic logic. It extends until and weak until with arithmetic operations on real values, while still preserving their conventional semantics of temporal logic. We derive mathematical algorithms for computing each of the operators, show how any PCTL property can be expressed in CTML, and illustrate the expressiveness of CTML with some example performance–related queries.
C14

GreatSPN Enhanced with Decision Diagram Data Structures

Junaid Babar, Marco Beccuti, Susanna Donatelli, and 1 more author

In Application and Theory of Petri Nets 2010, Jun 2010

Abs DOI PDF

Decision diagrams (DDs) have made their way into Petri net (PN) tools either in the form of new tools (usually designed from scratch to use DDs) or as enhancements to existing tools. This paper describes how an existing and established tool (GreatSPN) has been enhanced through the use of DDs provided by an existing open-source library (Meddly). We benchmark the enhanced tool and discuss lessons learned while integrating DDs into GreatSPN.

2004

C13

Saturation for a general class of models

Andrew S. Miner

In 1st Int. Conf. on Quantitative Evaluation of Systems (QEST’04), Sep 2004

Abs DOI PDF

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 requires each model event to be expressible as a Kronecker product. In this paper, we develop 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. We apply our algorithm to several examples and give detailed experimental results.
C12

Improving efficiency of implicit Markov chain state classification

Andrew S. Miner and Shuxing Cheng

In 1st Int. Conf. on Quantitative Evaluation of Systems (QEST’04), Sep 2004

Abs DOI PDF

Current efficient symbolic methods to classify the states of a Markov chain into transient and recurrent classes use an iterative approach, where each iteration begins by selecting a “seed” state. In this paper we present heuristics to reduce the number of iterations required. Our core contribution is the use of shortest distance information to select the seed state. Our approach uses multiway decision diagrams to represent sets of states and edge-valued decision diagrams to represent distance information. Experimental results indicate that the distance heuristics can be quite effective, often minimizing the required number of iterations.
C11

Novel machine learning techniques for anomaly intrusion detection

Yanxin Wang, Johnny Wong, and Andrew Miner

In Proceedings of the 10th Americas Conf. on Information Systems, Aug 2004
C10

Anomaly intrusion detection using one class SVM

Yanxin Wang, Johnny Wong, and Andrew Miner

In 5th Annual IEEE Information Assurance Workshop, Jun 2004

Abs PDF

Kernel methods are widely used in statistical learning (or many fields, such as protein classification and image processing). We recently extend kernel methods to intrusion detection domain by introducing a new family of kernels suitable for intrusion detection. These kernels, combined with an unsupervised learning method - one-class Support Vector Machine, are used for anomaly detection. Our experiments show that the new anomaly detection methods are able to achieve better accuracy rates than the conventional anomaly detectors.

2003

C09

Logical and stochastic modeling with SMART

Gianfranco Ciardo, Robert Jones, Andrew Miner, and 1 more author

In 13th Int. Conf. on Modelling Techniques and Tools for Computer Performance Evaluation, Sep 2003

Abs DOI PDF

We describe the main features of SMART, a software package providing a seamless environment for the logic and probabilistic analysis of complex systems. SMART can combine diﬀerent formalisms in the same modeling study. For the analysis of logical behavior, both explicit and symbolic state-space generation techniques, as well as symbolic CTL model-checking algorithms, are available. For the study of stochastic and timing behavior, both sparse-storage and Kronecker numerical solution approaches are available when the underlying process is a Markov chain. In addition, discrete-event simulation is always applicable regardless of the stochastic nature of the process, but certain classes of non-Markov models can still be solved numerically. Finally, since SMART targets both the classroom and realistic industrial settings as a learning, research, and application tool, it is written in a modular way that allows for easy integration of new formalisms and solution algorithms.
C08

Computing response time distributions using stochastic Petri nets and matrix diagrams

Andrew S. Miner

In 10th Int. Workshop on Petri Nets and Performance Models (PNPM’03), Sep 2003

Abs PDF

In this paper, we consider random variables expressed in terms of the time required for the state of a stochastic Petri net to pass from a set of starting markings to a set of stopping markings. These random variables have continuous phase-type distributions when the all transitions have exponentially-distributed firing delays. We demonstrate how to numerically compute the distribution of the random variable using both explicit techniques and an implicit approach based on multi-way decision diagrams and matrix diagrams. We present an efficient matrix-vector multiplication algorithm for matrix diagrams that is necessary for numerical solution. We demonstrate the efficiency of our approaches using several models. The lower storage requirements of the implicit approach effectively increases the size of models that can be analyzed by about an order of magnitude.
C07

Using distance to improve implicit state classification of Markov chains

Andrew S. Miner and Shuxing Cheng

In 6th Int. Workshop on Performability Modeling of Computer and Communication Systems (PMCCS-6), Sep 2003

PDF
C06

Comparing implicit representations of large CTMCs

Gianfranco Ciardo, Massimo Forno, Paul Grieco, and 1 more author

In 4th Int. Conf. on the Numerical Solution of Markov Chains (NSMC’03), Sep 2003

Abs PDF

High-level formalisms of stochastic structures can express very large continuous-time Markov chains (CTMC). State explosion poses interesting challenges in terms of data structures and numerical solution algorithms. Implicit representations exploit structural properties of the high-level model, to avoid storing each nonzero matrix entry explicitly. Implicit structures used to store the CTMC include Kronecker algebra, multi-terminal BDDs, and matrix diagrams, all of which require specialized multiplication algorithms. These methods can be very compact in practice, although in the worst case they require more memory than explicit storage. In this paper, we begin an in-depth comparison of implicit CTMC techniques, we present some initial observations and discuss the currently-known tradeoffs between the various techniques. We identify several questions that are worth further investigation.

2002

C05

Efficient state space generation of GSPNs using decision diagrams

Andrew S. Miner

In 2002 Int. Conf. on Dependable Systems and Networks (DSN 2002), Jun 2002

Abs PDF

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.

2001

C04

Efficient Solution of GSPNs Using Canonical Matrix Diagrams

Andrew S. Miner

In 9th Int. Workshop on Petri Nets and Performance Models (PNPM’01), Sep 2001

Abs DOI PDF

The solution of a generalized stochastic Petri net (GSPN) is severely restricted by the size of its underlying continuous-time Markov chain. In recent work, matrix diagrams built from a Kronecker expression for the transition rate matrix of certain types of GSPNs were shown to allow for more efficient solution; however, the GSPN model requires a special form, so that the transition rate matrix has a Kronecker expression. In this paper, we extend the earlier results to GSPN models with partitioned sets of places. Specifically, we give a more restrictive definition for matrix diagrams and show that the new form is canonical. We then present an algorithm that builds a canonical matrix diagram representation for an arbitrary non-negative matrix, given encodings for the sets of rows and columns. Using this algorithm, a Kronecker expression is not required to construct the matrix diagram. The efficient matrix diagram algorithms for numerical solution presented earlier are still applicable. We apply our technique to several example GSPNs.

2000

C03

Using the exact state space of a Markov model to compute approximate stationary measures

Andrew S. Miner, Gianfranco Ciardo, and Susanna Donatelli

In 2000 ACM SIGMETRICS Conf. on Measurement and Modeling of Computer Systems, Jun 2000

Abs PDF

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 diﬀerent 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.

1999

C02

A data structure for the efficient Kronecker solution of GSPNs

Gianfranco Ciardo and Andrew S. Miner

In 8th Int. Workshop on Petri Nets and Performance Models (PNPM’99), Sep 1999

Abs DOI PDF

Kronecker-based approaches have been proposed for the solution of structured GSPNs with extremely large state spaces. Representing the transition rate matrix using Kronecker sums and products of smaller matrices virtually eliminates its storage requirements, but introduces various sources of overhead. We show how, by using a new data structure which we call matrix diagrams, we are able to greatly reduce or eliminate many of these overheads, resulting in a very efficient overall solution process.
C01

Efficient reachability set generation and storage using decision diagrams

Andrew S. Miner and Gianfranco Ciardo

In Application and Theory of Petri Nets 1999, Jun 1999

Abs DOI PDF

We present a new technique for the generation and storage of the reachability set of a Petri net. Our approach is inspired by previous work on Binary and Multi-valued Decision Diagrams but exploits a concept of locality for the effect of a transition’s firing to vastly improve algorithmic performance. The result is a data structure and a set of manipulation routines that can be used to generate and store enormous sets extremely efficiently in terms of both memory and execution time.

1997

C00

Storage alternatives for large structured state spaces

Gianfranco Ciardo and Andrew S. Miner

In 9th Int. Conf. on Modelling Techniques and Tools for Computer Performance Evaluation, Jun 1997

Abs DOI PDF

We consider the problem of storing and searching a large state space obtained from a high-level model such as a queueing network or a Petri net. After reviewing the traditional technique based on a single search tree, we demonstrate how an approach based on multiple levels of search trees offers advantages in both memory and execution complexity. Further execution time improvements are obtained by exploiting the concept of "event locality". We apply our technique to three large parametric models, and give detailed experimental results.