Journal articles

2022

1. J13

   

   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.

2. J12

   

   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

1. J11

   

   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

   DOI

2018

1. J10

   

   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
2. J09

   

   Computation Tree Measurement Language (CTML)

   Yaping Jing and Andrew S. Miner

   Formal Aspects of Computing, 2018

   DOI

2011

1. J08

   

   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

   Abs DOI PDF

   We propose a new approximate numerical algorithm for the steady–state solution of general structured ergodic Markov models. The approximation uses a state–space encoding based on multiway decision diagrams and a transition rate encoding based on a new class of edge–valued decision diagrams. The new method retains the favorable properties of a previously proposed Kronecker–based approximation, while eliminating the need for a Kronecker–consistent model decomposition. Removing this restriction allows for a greater utilization of event locality, which facilitates the generation of both the state–space and the transition rate matrix, thus extends the applicability of this algorithm to larger and more complex models.

2009

1. J07

   

   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

1. J06

   

   Decision diagrams for the exact solution of Markov models

   Andrew S. Miner

   Proceedings in Applied Mathematics and Mechanics (PAMM), 2007

   DOI
2. J05

   

   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

1. J04

   

   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.

2. J03

   

   Logic and stochastic modeling with SMART

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

   Performance Evaluation, Jun 2006

   DOI

2005

1. J02

   

   Implicit data structures for logic and stochastic systems analysis

   Gianfranco Ciardo and Andrew S. Miner

   SIGMETRICS Performance Evaluation Review, Mar 2005

   DOI

2004

1. J01

   

   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

1. J00

   

   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