A model checking technique to specify and verify temporal properties of drug disposition changes is proposed. In pharmacokinetics and pharmaceutics, drug kinetics is often modeled as single or multiple compartment models. In this paper, a probabilistic temporal logic, called iLTL, is introduced to specify many interesting properties of drug kinetics. Given a specification, a computerized technique, called model checking [1], is used to check whether all drug disposition changes of a compartment model comply with the specification. © 2010 Springer Science+Business Media, LLC.
CITATION STYLE
Kwon, Y., & Kim, E. (2010). Specification and verification of pharmacokinetic models. In Advances in Experimental Medicine and Biology (Vol. 680, pp. 465–472). https://doi.org/10.1007/978-1-4419-5913-3_52
Mendeley helps you to discover research relevant for your work.