Specification and verification of pharmacokinetic models

Area of Science:

• Pharmacokinetics and Pharmaceutics
• Computational Toxicology
• Systems Biology

Background:

• Drug disposition is commonly modeled using single or multiple compartment models in pharmacokinetics.
• Verifying temporal properties of these models is crucial for understanding drug behavior.
• Existing methods may lack the precision to capture complex temporal dynamics.

Purpose of the Study:

• To introduce a model checking technique for specifying and verifying temporal properties of drug disposition.
• To present a probabilistic temporal logic, iLTL, for defining drug kinetic properties.
• To enable automated verification of pharmacokinetic models against temporal specifications.

Main Methods:

• Development of a probabilistic temporal logic (iLTL) for specifying temporal properties.
• Application of model checking, a computerized verification technique.
• Testing the technique on compartment models of drug disposition.

Main Results:

• The proposed iLTL logic can specify various temporal properties of drug kinetics.
• Model checking successfully verifies whether compartment models adhere to the specified temporal properties.
• The technique provides a formal method for assessing drug disposition changes.

Conclusions:

• Model checking offers a robust method for verifying temporal properties in pharmacokinetic models.
• iLTL provides a powerful language for expressing complex temporal drug disposition characteristics.
• This technique enhances the reliability and predictability of drug kinetic modeling.