extension) at the Electrical and Computer Engineering Department of Utah
State University. The earliest starting date is early January 2020. PhD
application information is available at:
https://engineering.usu.edu/ece/files/pdfs/ece-graduate-program-application-info.pdf
Abstract:
Synthetic biology and nanotechnology place increasing demands on design
methodologies to ensure dependable and robust operation. Consisting of
noisy and unreliable components, these complex systems have large and often
infinite state spaces that include extremely rare error states.
Probabilistic model checking techniques have demonstrated significant
potential in quantitatively analyzing such system models under extremely
low probability. Unfortunately, they generally require enumerating the
model's state space, which is computationally intractable or impossible.
Therefore, addressing these design challenges in emerging technologies
requires enhancing the applicability of probabilistic model checking.
Motivated by this problem, this project investigates an automated
probabilistic verification framework that integrates approximate
probabilistic model checking and counterexample-guided rare-event
simulation to improve the analysis accuracy and efficiency.
This multi-institution collaborative project focuses on verifying
infinite-state continuous-time Markov chain (CTMC) models with rare-event
properties. It addresses the scalability problem by first applying
property-guided and on-the-fly state truncation techniques to prune
unlikely states to obtain finite state representations that are amenable to
probabilistic model checking. In the case of false or indeterminate
verification results, probabilistic counterexamples are generated and
utilized to improve the accuracy of the state reductions. Furthermore, it
mines these critical counterexamples as automated guidance to improve the
quality and efficiency for rare-event probabilistic simulations. This
verification framework will be integrated within existing state-of-the-art
probabilistic model checking tools (e.g., the PRISM model checking tool),
and benchmarked on a wide range of real-world case studies in synthetic
biology and nanotechnology.
========================================
Project description:
The PhD position at Utah State University will be advancing and developing
efficient model abstraction and state space truncation techniques for the
infinite-state CTMC models. In particular, we are interested in
investigating:
- Model abstraction techniques on chemical reaction networks for synthetic
biology
- Approximation techniques for state space truncation and abstraction
- Property-guided state space pruning techniques
========================================
Qualifications:
Applicants must have a bachelor's degree in Computer Science, Computer
Engineering, or a related field. A master's degree is preferred. The
successful candidate is expected to demonstrate strong background and
interest in formal methods and algorithms, and preferably basic knowledge
of probability and random process. He/She should be confident in
independently developing academic software tools. Good writing and
presentation skills in English are important as well. Knowledge of
synthetic biology is preferred, but not required.
========================================
Contact:
For questions about this position, please contact:
Dr. Zhen Zhang, zhen.zhang@usu.edu,
https://engineering.usu.edu/ece/faculty-sites/zhen-zhang/index
========================================
**********************************************************
*
* Contributions to be spread via DMANET are submitted to
*
* DMANET@zpr.uni-koeln.de
*
* Replies to a message carried on DMANET should NOT be
* addressed to DMANET but to the original sender. The
* original sender, however, is invited to prepare an
* update of the replies received and to communicate it
* via DMANET.
*
* DISCRETE MATHEMATICS AND ALGORITHMS NETWORK (DMANET)
* http://www.zaik.uni-koeln.de/AFS/publications/dmanet/
*
**********************************************************
Posts
