You are here
Techniques for automated parameter estimation in computational models of probabilistic systems
| Title: | Techniques for automated parameter estimation in computational models of probabilistic systems. |
 34 views 17 downloads |
|---|---|---|
| Name(s): |
Hussain, Faraz, Author Jha, Sumit, Committee Chair Leavens, Gary, Committee CoChair Turgut, Damla, Committee Member Uddin, Nizam, Committee Member University of Central Florida, Degree Grantor |
|
| Type of Resource: | text | |
| Date Issued: | 2016 | |
| Publisher: | University of Central Florida | |
| Language(s): | English | |
| Abstract/Description: | The main contribution of this dissertation is the design of two new algorithms for automatically synthesizing values of numerical parameters of computational models of complexstochastic systems such that the resultant model meets user-specified behavioral specifications.These algorithms are designed to operate on probabilistic systems (-) systems that, in general,behave differently under identical conditions. The algorithms work using an approach thatcombines formal verification and mathematical optimization to explore a model's parameterspace.The problem of determining whether a model instantiated with a given set of parametervalues satisfies the desired specification is first defined using formal verification terminology,and then reformulated in terms of statistical hypothesis testing. Parameter space explorationinvolves determining the outcome of the hypothesis testing query for each parameter pointand is guided using simulated annealing. The first algorithm uses the sequential probabilityratio test (SPRT) to solve the hypothesis testing problems, whereas the second algorithmuses an approach based on Bayesian statistical model checking (BSMC).The SPRT-based parameter synthesis algorithm was used to validate that a given model ofglucose-insulin metabolism has the capability of representing diabetic behavior by synthesizingvalues of three parameters that ensure that the glucose-insulin subsystem spends at least 20minutes in a diabetic scenario. The BSMC-based algorithm was used to discover the valuesof parameters in a physiological model of the acute inflammatory response that guarantee aset of desired clinical outcomes.These two applications demonstrate how our algorithms use formal verification, statisticalhypothesis testing and mathematical optimization to automatically synthesize parameters ofcomplex probabilistic models in order to meet user-specified behavioral properties | |
| Identifier: | CFE0006117 (IID), ucf:51200 (fedora) | |
| Note(s): |
2016-05-01 Ph.D. Engineering and Computer Science, Computer Science Doctoral This record was generated from author submitted information. |
|
| Subject(s): | parameter estimation -- parameter discovery -- formal verification -- algorithms -- automated synthesis -- model synthesis -- computational modeling -- high-performance computing -- parallel programming -- MPI | |
| Persistent Link to This Record: | http://purl.flvc.org/ucf/fd/CFE0006117 | |
| Restrictions on Access: | public 2016-05-15 | |
| Host Institution: | UCF |
