A Clinical Practice Guideline defines best practices to be fol- lowed by clinicians to manage a particular disease. Checking the quality of such guidelines is a very important issue, e.g., designers of the guide- lines should ensure their consistency. A formal modelling approach is an appropriate choice due to the complexity of these guidelines. In this pa- per, we develop a metric interval-based temporal logic, which is suitable for such modelling and then propose a method for checking the satisfi- ability of such guidelines, to assure their consistency. As a case study, we use the logic to model a real-life guideline, the Active Tuberculosis Diagnosis guideline.
