PhD position in Utah State University (Probabilistic Verification Methodology for Synthetic Biology and Nanotechnology) – High-confidence Embedded and Cyberphysical Systems (HECS)

A PhD position is available (fully paid for 4 years with the possibility of extension) at the Electrical 
and Computer Engineering Department of Utah State University. The expected 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
========================================


ECE Department at USU:

The place of employment is the Electrical and Computer Engineering Department at Utah State University. 
The university is located in Logan, Utah, 88 miles (about 142 km) north of Salt Lake City. The mission of 
the Department of Electrical and Computer Engineering is to serve society through excellence in learning, 
discovery, and outreach. We provide undergraduate and graduate students an education in electrical and 
computer engineering, and we aspire to instill in them attitudes, values, and visions that will prepare 
them for lifetimes of continued learning and leadership in their chosen careers. Through research, the 
department strives to generate and disseminate new knowledge and technology for the benefit of the State 
of Utah, the nation, and beyond. The detailed graduate program description can be found at: 
https://engineering.usu.edu/ece/students/graduate/index