Andrew S. Miner
Associate Professor

Office: 233 Atanasoff Phone: (515) 294-2392 Fax: (515) 294-0258 Email: asminer@cs.iastate.edu Homepage: http://www.cs.iastate.edu/~asminer/homepage.html

Research Interests

Performance and reliability analysis of systems;
model checking and formal methods;
binary decision diagrams (and variants);
algorithms for model analysis;
Petri nets and stochastic modeling;
tool development.

Research Areas

Software Engineering, Software Systems

Research Statement

Research overview

Dr. Miner's primary research goal is to develop techniques for analyzing complex discrete-event systems (including computer communication networks, multi-threaded software, network protocols, and others). He has worked in the areas of model checking and performance evaluation, and is particularly interested in techniques that are applicable to both of these areas. Dr. Miner also works on developing software tools that incorporate these techniques. See http://www.cs.iastate.edu/~asminer for details.

Model checking research

Model checking is the process of determining if a system, described as a (usually nondeterministic) model, satisfies some properties. These properties are expressed using an appropriate logic, such as the temporal logics LTL or CTL. If the system model describes a finite state machine, then the model checking problem is decidable. In practice, however, the finite state machines can be extremely large. Researchers use a variety of techniques to overcome this; Dr. Miner has focused past efforts on techniques that utilizea data structure called decision diagrams. He has made several contributions in this areadeveloping improved reachability set generation algorithms (a core problem in model checking) for decision diagrams, especially for models of asynchronous systems. Dr. Miner is currently working with Dr. Basu to apply these techniques to multi-threaded software.

Performance evaluation research

If a system is described using a stochastic model, rather than a nondeterministic model, then the model ultimately generates a stochastic process. Properties of the system can then either be queried (e.g., "What is the probability that a packet is lost") or expressed using a stochastic logic such as pCTL or CSL (e.g., "The probability of a lost packet is less that 10^-6"). In either case, these properties are determined by analyzing the underlying stochastic process, which is typically a Markov chain. Dr. Miner has contributed to this area by adapting decision diagram algorithms used for model checking for use with Markov chains. This research is currently supported by an NSF CAREER grant.

Tool development

Dr. Miner is a co-designer and developer of the software tool SMART (Stochastic Model-checking Analyzer for Reliability and Timing), which contains implementations of traditional as well as state-of-the-art techniques in model checking and performance evaluation. The tool was designed for instructional, research, and industrial use.

Dr. Miner and Ph.D. student Junaid Babar are working on a stand-alone decision diagram library. The advanced decision diagram algorithms of SMART will be migrated to the library, allowing easy integration of those techniques into other tools.

Education

Ph.D.   College of William and Mary, Williamsburg, VA.   2000

Current Grants

CAREER: Composition approaches for the analysis of complex systems. Andrew Miner. NSF (2006-2011). $400,000.

Representative Publications

Refereed Journal and Conference Publications

G. Ciardo, G. Luttgen, A. Miner. Exploiting Interleaving Semantics in Symbolic State-Space Generation. Formal Methods in System Design. Vol. 31. No. 1. pp. 63-100, 2007.

Andrew S. Miner. Saturation for a general class of models. IEEE TSE. Vol. 32. No. 8. pp. 559-570, 2006.

G. Ciardo, R. Jones, A. Miner, R. Siminiceanu. Logic and Stochastic Modeling with Smart. Performance Evaluation. Vol. 63. No. 6. pp. 578-608, 2006.

Andrew S. Miner and Shuxing Cheng. Improving efficiency of implicit Markov chain state classification. QEST-04 (Int. Conf. on Quantitative Evaluation of Systems), Enschede, The Netherlands, IEEE. pp. 262-271, 2004.

Andrew Miner. Implicit GSPN reachability set generation using decision diagrams. Performance Evaluation. Vol. 56. pp. 145-165, 2004.

Andrew S. Miner, Gianfranco Ciardo, and Susanna Donatelli. Using the exact state space of a large structured Markov model to compute approximate stationary measures. ACM SIGMETRICS 2000, Santa Clara, CA, ACM. pp. 207-216, 2000.

Gianfranco Ciardo and Andrew S. Miner. A data structure for the efficient Kronecker solution of GSPNs. PNPM-99 (Int. Workshop on Petri Nets and Performance Models), Zaragoza, Spain, IEEE. pp. 22-31, 1999.

Book Chapters

Andrew Miner and David Parker. Symbolic Representations and Analysis of Large Probabilistic Systems. In: Validation of Stochastic Systems (Ed. Christel Baier, Boudewijn Haverkort, Holder Hermanns, Joost-Pieter Katoen, Markus Siegle), Springer, LNCS 2925 2004.