Miscellaneous papers

2025

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

2024

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

   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

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

   DOI
2. RexBDDs: Reduction-on-Edge Complement-and-Swap Binary Decision Diagrams

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

   In DAC 2023 (Work-in-Progress Poster), Jul 2023

2022

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

2020

1. Reachability Set Generation Using Hybrid Relation Compatible Saturation

   Shruti Biswal and Andrew S. Miner

   In Reachability Problems (RP 2020), 2020

2019

1. Improving Saturation Efficiency with Implicit Relations

   Shruti Biswal and Andrew S. Miner

   In Application and Theory of Petri Nets and Concurrency, 2019

   DOI
2. Presentation of the 9th Edition of the Model Checking Contest

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

   In Proc. TACAS, Apr 2019

   Abs

   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.

3. i_\mathrmRank: A Variable Order Metric for DEDS Subject to Linear Invariants

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

   In TACAS 2019, 2019
4. Binary Decision Diagrams with Edge-Specified Reductions

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

   In TACAS 2019, 2019

2018

1. Action and State Based Computation Tree Measurement Language and Algorithms

   Yaping Jing and Andrew S. Miner

   In QEST 2018, 2018

   DOI

2017

1. 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
2. Variable reordering in binary decision diagrams

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

   In Proc. IWLS, 2017

2016

1. Power Consumption Analysis of Replicated Virtual Applications in Heterogeneous Architectures

   Gianfranco Ciardo, Marco Gribaudo, Mauro Iacono, and 2 more authors

   2016

   DOI

2015

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

2014

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

   DOI

2010

1. 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
2. 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
3. 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 (Proc. 31st Int. Conf. on Applications and Theory of Petri Nets), Jun 2010

2007

1. Approximating stationary measures of structured continuous-time Markov models using matrix diagrams

   Gianfranco Ciardo, Andrew S. Miner, Min Wan, and 1 more author

   In Performance (poster presentation), Oct 2007

2006

1. Verification of software via integration of design and implementation

   Andrew S. Miner and Samik Basu

   In Parallel and Distributed Processing Symposium, 2006, Apr 2006

2004

1. SMART: the Stochastic Model checking Analyzer for Reliability and Timing

   Gianfranco Ciardo and Andrew S. Miner

   In 1st Int. Conf. on Quantitative Evaluation of Systems (QEST’04), Sep 2004
2. Improving Feature Selection in Anomaly Intrusion Detection Using Specifications

   Yanxin Wang, Andrew S. Miner, Johnny Wong, and 1 more author

   In Int. Conf. on Distributed Computing and Internet Technology, Dec 2004
3. Saturation for a general class of models

   Andrew S. Miner

   In 1st Int. Conf. on Quantitative Evaluation of Systems (QEST’04), Sep 2004
4. 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
5. Symbolic Representations and Analysis of Large State Spaces

   Andrew Miner and David Parker

   In Validation of Stochastic Systems, 2004
6. 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
7. Anomaly intrusion detection using one class SVM

   Yanxin Wang, Johnny Wong, and Andrew Miner

   In 5th Annual IEEE Information Assurance Workshop, Jun 2004

2003

1. 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
2. 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
3. Logical and stochastic modeling with SMART

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

   In Proc. 13th Int. Conf. on Modelling Techniques and Tools for Computer Performance Evaluation, Sep 2003
4. 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

2002

1. SMART: Stochastic Model-checking Analyzer for Reliability and Timing

   Gianfranco Ciardo, Robert L. Jones, Robert M. Marmorstein, and 2 more authors

   In Proc. Int. Conf. on Dependable Systems & Networks (DSN), _gfc, Jun 2002

   Abs

2. Efficient state space generation of GSPNs using decision diagrams

   Andrew S. Miner

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

2001

1. SMART: Stochastic Model Analyzer for Reliability and Timing

   Gianfranco Ciardo, Robert L. Jones, Andrew S. Miner, and 1 more author

   In Tools of Int. Multiconf. Measurement, Modelling and Evaluation of Computer-Communication Systems, _gfc, Sep 2001

   Abs

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

2000

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

   Andrew S. Miner, Gianfranco Ciardo, and Susanna Donatelli

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

   Abs

2. Structural Approaches for SPN Analysis

   Gianfranco Ciardo and Andrew S. Miner

   In High Performance Computing 2000, Grand Challenges in Computer Simulation, Apr 2000

1999

1. 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), inbook, Sep 1999

   Abs

   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.

2. Efficient reachability set generation and storage using decision diagrams

   Andrew S. Miner and Gianfranco Ciardo

   In Application and Theory of Petri Nets 1999 (Proc. 20th Int. Conf. on Applications and Theory of Petri Nets), , Jun 1999

   Abs

   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

1. SMART: Simulation and Markovian Analyzer for Reliability and Timing

   Gianfranco Ciardo and Andrew S. Miner

   In Tool Descriptions from the 9th Int. Conf. on Modelling Techniques and Tools for Computer Performance Evaluation and the 7th Int. Workshop on Petri Nets and Performance Models, Jun 1997
2. Storage alternatives for large structured state spaces

   Gianfranco Ciardo and Andrew S. Miner

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

   Abs

   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.

1996

1. SMART: Simulation and Markovian Analyzer for Reliability and Timing

   Gianfranco Ciardo and Andrew S. Miner

   In Proc. IEEE International Computer Performance and Dependability Symposium (IPDS’96), Sep 1996

1995

1. The Fluid Stochastic Petri Net Simulator

   David M. Nicol and Andrew S. Miner

   In 6th Int. Workshop on Petri Nets and Performance Models (PNPM’95), inbook, Oct 1995