Journal articles | Andrew S. Miner

2022

The footprint form of a matrix: definition, properties, and an application

Elvio G. Amparore, Gianfranco Ciardo, and Andrew S. Miner

Linear Algebra and Its Applications, 2022

Abs DOI PDF

We propose an alternative to the well-known row echelon form of a matrix, focused on its “footprint”, that is, on the position of both the leading and trailing nonzero entries of each row. When a matrix is in footprint form, its leading entries are all in different positions (as in the echelon form) but, in addition, its trailing entries are also in different positions. This new form has several interesting properties. In particular, a matrix in footprint form has the smallest footprint among the matrices obtainable from it through elementary row operations, and supports an efficient way to compute the rank of any of its submatrices with a particular shape. This is critical for our application: scoring potential variable orders for the decision diagram encoding all solutions to a set of linear integer constraints, with the goal of finding an order that minimizes the decision diagram size. We then experimentally evaluate the effectiveness of this scoring, on several problem instances small enough to compare all possible orders.
CESRBDDs: binary decision diagrams with complemented edges and edge-specified reductions

Junaid Babar, Gianfranco Ciardo, and Andrew Miner

Intl. Jnl. on Software Tools for Technology Transfer, 2022

Abs DOI PDF

We introduce CESRBDDs, a form of binary decision diagrams (BDDs) that can exploit reduction opportunities beyond those allowed by reduced ordered BDDs (elimination of redundant nodes), zero-suppressed BDDs (elimination of “high-zero” nodes), and recent proposals merging the two (chained or tagged BDDs). CESRBDDs also incorporate complemented edges, thus never store both the encoding of a function and of its complement. We prove that CESRBDDs are canonical and show how their storage requirements and computational efficiency compare very favorably against previous alternatives, both theoretically and experimentally, using an extensive set of benchmarks. Another advantage of CESRBDDs over chained or tagged BDDs is that their nodes only require one byte to store reduction and complement information.

2019

Runtime Fault Detection in Programmed Molecular Systems

Samuel J. Ellis, Titus H. Klinge, James I. Lathrop, and 4 more authors

ACM Trans. on Software Engineering and Methodology, Mar 2019

2018

Decision Diagrams for Petri Nets: A Comparison of Variable Ordering Algorithms

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

Trans. on Petri Nets and Other Models of Concurrency XIII, 2018

DOI
Computation Tree Measurement Language (CTML)

Yaping Jing and Andrew S. Miner

Formal Aspects of Computing, 2018

DOI

2011

Approximate steady–state analysis of large Markov models based on the structure of their decision diagram encoding

Min Wan, Gianfranco Ciardo, and Andrew S. Miner

Performance Evaluation, 2011

DOI PDF

2009

Advanced features in SMART: the Stochastic Model checking Analyzer for Reliability and Timing

Gianfranco Ciardo, Andrew S. Miner, and Min Wan

SIGMETRICS Performance Evaluation Review, Mar 2009

DOI

2007

Decision diagrams for the exact solution of Markov models

Andrew S. Miner

Proceedings in Applied Mathematics and Mechanics (PAMM), 2007

DOI
Exploiting Interleaving Semantics in Symbolic State–Space Generation

Gianfranco Ciardo, Gerald Lüttgen, and Andrew S. Miner

Formal Methods in System Design, Aug 2007

Abs DOI PDF

Symbolic techniques based on Binary Decision Diagrams (BDDs) are widely employed for reasoning about temporal properties of hardware circuits and synchronous controllers. However, they often perform poorly when dealing with the huge state spaces underlying systems based on interleaving semantics, such as communications protocols and distributed software, which are composed of independently acting subsystems that communicate via shared events. This article shows that the efficiency of state–space exploration techniques using decision diagrams can be drastically improved by exploiting the interleaving semantics underlying many event–based and component–based system models. A new algorithm for symbolically generating state spaces is presented that (i) encodes a model’s state vectors with Multi–valued Decision Diagrams (MDDs) rather than flattening them into BDDs and (ii) partitions the model’s Kronecker–consistent next–state function by event and subsystem, thus enabling multiple lightweight next–state transformations rather than a single heavyweight one. Together, this paves the way for a novel iteration order, called saturation, which replaces the breadth–first search order of traditional algorithms. The resulting saturation algorithm is implemented in the tool SMART, and experimental studies show that it is often several orders of magnitude better in terms of time efficiency, final memory consumption, and peak memory consumption than existing symbolic algorithms.

2006

Saturation for a general class of models

Andrew S. Miner

IEEE Transactions on Software Engineering, Aug 2006

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 uses 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 sub-events until a Kronecker product expression is possible. In practice, this can lead to additional overheads during reachability set construction. This article 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.
Logic and stochastic modeling with SMART

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

Performance Evaluation, Jun 2006

DOI

2005

Implicit data structures for logic and stochastic systems analysis

Gianfranco Ciardo and Andrew S. Miner

SIGMETRICS Performance Evaluation Review, Mar 2005

DOI

2004

Implicit GSPN reachability set generation using decision diagrams

Andrew S. Miner

Performance Evaluation, Mar 2004

Abs DOI 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 less-efficient 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. We adapt an efficient Kronecker-based reachability set generation algorithm to work with matrix diagrams. 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 experimental results.

2000

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

Andrew S. Miner, Gianfranco Ciardo, and Susanna Donatelli

SIGMETRICS Performance Evaluation Review, Jun 2000

DOI