title: Specification and verification of pharmacokinetic models.
abstract: 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.
authors.affiliation: Microsoft Corp. Redmond, Redmond, WA, USA. ykwon4@cs.uiuc.edu
authors.forename: Youngmin
authors.initials: Y
authors.lastname: Kwon
authors.forename: Eunhee
authors.initials: E
authors.lastname: Kim
mesh_terms: D019295:Computational Biology; D003198:Computer Simulation; D006801:Humans; D007328:Insulin / Q000008:administration & dosage / Q000493:pharmacokinetics; D008390:Markov Chains; D008954:Models, Biological; D015233:Models, Statistical; D010599:Pharmacokinetics; D049490:Systems Biology
chemical_list: D007328:Insulin