At first, we described a metric interval-based language called IMPNL and then we introduced the CPG analyzer.

#### 3.1. IMPNL - A Metric Interval-Based Temporal Logic

The language of IMPNL consists of a set, AP, of propositional variables, logical operators, *atomic negation *(¬), *or* (∨), and *and* (∧), and temporal operators, ◊_{r} and ◊_{l}, corresponding to Allen’s relations *meet *and its inverse, *met-by*. This logic has two constants ⊤ (True) and ⊥ (False), defined as usual.

The formulas, denoted by φ, ψ, ..., are recursively defined using BNF (Backus Naur Form), where p_{k} is a propositional variable. Notably, the subscript of an atomic formula denotes the length of the interval, on which it should be evaluated. However, the subscript of a non-atomic formula denotes an index, and is used to distinguish the formula from other formulas.

ψ = p_{k} |¬p_{k} |⊤_{k} |⊥_{k} |ψ_{1} ∨ ψ_{2} |ψ_{1} ∧ ψ_{2} |◊_{r}ψ|◊_{l}ψ where k ∈ N

In IMPNL, a user must specify the length of an interval as a subscript of a propositional variable. Therefore, it is not possible to have a propositional variable as an atomic formula without specifying the length.

The semantics of IMPNL is based on a 3-tuple structure M = ⟨D, I(D)^{−}, V⟩, where the pair ⟨D, I(D)^{−}⟩ is a strict interval structure and V: I(D)^{−} → 2^{AP} is a valuation function that assigns to every interval a set of propositional variables which are true on that interval. A *satisfaction relation* is defined as follows:

It is stated that a formula ψ is satisfiable if there exists a structure M and an interval [c_{0}, c_{1}] s.t. M, [c_{0}, c_{1}] ⊨ ψ. Moreover, it is easy to show that M, [i, j] ⊨ ◊_{z}(ψ_{1} ∨ ψ_{2}) if and only if M, [i, j] ⊨ ◊_{z}ψ_{1} ∨ ◊_{z}ψ_{2} (z ∈ {r, l}), and if M, [i, j] ⊨ ◊_{z}(ψ_{1} ∧ ψ_{2}), then M, [i,j] ⊨ ◊_{z}ψ_{1} ∧ ◊_{z}ψ_{2} (z ∈ {r, l}).

Notably, in IMPNL, only an atomic formula can be negated and there is no negation for a complex formula. In addition, the length of each atomic formula must be specified. Finally, IMPNL has a homogeneity assumption, i.e. if a formula is true (false) on an interval, it is true (false) in every subinterval of that interval.

#### 3.2. CPG Analyzer

In this section, we presented our tool which uses IMPNL to model a CPG and checks its satisfiability and consistency using the tableau-based satisfiability checking algorithm for IMPNL formulas.

Our analyzer has different modules. One module is responsible for processing IMPNL and constructing the corresponding tableau tree. This module is implemented using NodeJS and C++. The client part of the analyzer, responsible for inputting formula and showing the corresponding tableau tree along with calendar and other provided information, is a web-based application.

As we already mentioned earlier, manual checking of satisfiability of a CPG is difficult, time-consuming, and error-prone. Sometimes, we need a loop in a guideline [See section 6.1 of Yousef Sanati study (2)]. To analyze such a loop, we should expand the formula and apply the algorithm on the expanded version. This needs hard work and is impossible to be performed manually. Moreover, it is crucial to detect points where inconsistencies occur. Our tool deals with all these problems. Here, we modeled a real-life guideline using our tool and showed that the CPG was consistent. Further, we described a situation, in which inconsistency points occurred. Finally, it is important to note that we developed the analyzer based on formal software engineering guidelines to have a user-friendly software. For example, a wizard helps clinicians to enter the formula and analyze it. Moreover, the analyzer’s interface is straightforward and makes sense for the majority of clinicians. In addition, the analyzer results are visualized (e.g., in the format of a tree or calendar) for clinicians and thus are more understandable.

#### 3.3. HIV/AIDS Guideline Analysis

In this section, we modeled a real-life guideline for the diagnosis and treatment of HIV/AIDS from previous study (2). Due to the lack of space, we briefly described the guideline and refer the reader to Yousef Sanati study (2) for full details.

Generally, HIV/AIDS has three major stages as follows: *acute infection* (lasts 6 - 8 weeks), *clinical latency* (lasts 8 - 10 years), and AIDS (lasts 0 - 20 years). The diagnosis and treatment processes of the disease are similar for any HIV/AIDS patient in each of the stages. Figure 1 shows the entire process of the HIV/AIDS clinical practice guideline.

Figure 1.
The HIV/AIDS CPG (2)
As can be observed in Figure 1, blood-work should be performed three times to ensure that the patient has an HIV infection. Each blood-work and registration process take 1 day and 4 days, respectively. Routinely, the blood level, of CD4 (Cluster of Differentiation 4) of an infected patient should be investigated every 3 months. If the level is fine and the patient has no sign of AIDS (e.g., Candidiasis of bronchi), no medication is needed. However, if the level is not acceptable, or there is at least one sign of AIDS, the patient should take three medications every day. Furthermore, the patient should be visited by a physician every 30 days to ensure that he/she takes the right medications with the right dosages. The prescriptions for the patient should be also renewed. Here, we considered one combination of medications, i.e. *Kaletra, Tenofovir*, and *Lamivadin*, from different possible combinations used for the treatment (2).

To enter a CPG formula, conventions in Figure 2 are used. Here, *gn* can be any granularity including d (days), mon (months), y (years), h (hours), min (minutes), and s (seconds).

Figure 2.
The input conventions
Figure 3 represents the analyzer syntax of the HIV/AIDS CPG. After the analysis, the IMPNL syntax of the formula and the result of the satisfiability of the CPG are shown in Figures 4 and 5. As can be observed in the figure, the CPG is satisfiable. This indicates that the guideline is consistent and can be used for patients.

Figure 3.
The input interface
Figure 4.
The original formula in the IMPNL syntax
Figure 5.
The result of satisfiability checking
#### 3.4. Concrete Model of the CPG

Another important feature of the analyzer is the ability to generate a concrete model for a CPG in two forms as follows: tree model and calendar model. Whatever model is desired, the start date and time should be provided by the designer (Figure 5).

#### 3.4.1. Tree Model

The tree model is constructed using the tableau-based algorithm presented in previous studies (2, 3). Figure 6 displays a part of the tree model of the HIV/AIDS CPG. As can be observed in the figure, two branches exist. The left branch represents the status, in which a patient is not in the AIDS stage of the disease whereas the right branch demonstrates the treatment process in the AIDS stage. Every node in the tree contains the medical activity and the interval, on which the activity should be carried out.

Figure 6.
A part of the HIV/AID CPG tree model
#### 3.4.2. Calendar Model

The main aim of the analyzer is to help CPG designers to check the satisfiability of a CPG; however, a physician can also use the calendar model to check whether a patient is coherently treated with the HIV/AIDS CPG (Figure 7).

Figure 7.
A part of the calendar model
Accordingly, this is a vital feature that increases the safety of the patient and prevents many medical errors.

#### 3.5. Inconsistency Point Detection

One of the important features of the tool is the ability to help designers to easily find inconsistencies. They can use this feature to determine and fix problems.

Generally, the two following types of inconsistencies can be detected by the analyzer.

#### 3.5.1. Medical Activity Duration Inconsistency

This type of inconsistency occurs when the duration of a medical activity is not equal to the length interval, on which the activity should be performed. As an example, the formula [TakeKaletra, 100 d] and [TakeRifampin, 30 d] is unsatisfiable, because [TakeKaletra, 100 d] and [TakeRifampin, 30 d] are inconsistent. There should be an interval, on which a patient should simultaneously take Kaletra and Rifampin for the entire duration of the interval. This is impossible since Kaletra should be taken for 100 days whereas Rifampin should be taken for 30 days.

#### 3.5.2. Medical Activities Conflicts

During the analysis, there may be an interval, in which two conflicting medical activities should be performed. This problem must be detected and avoided by the designer during CPG designing. Suppose that there is an interval, on which Kaletra should be used and should not be used. This is an inconsistency and must be fixed by changing the CPG formula.

In the tree model, inconsistent nodes are shown in red. A designer can click on a red node and observe a hint which indicates why the medical activity corresponding to the node is inconsistent. Moreover, if there is a conflicting medical activity to this node, the node corresponding to the activity turns black. In order to show this feature, we remove ![HasAIDS, 1 h] (in IMPNL ~HasAIDS*1h*) from the formula and add ><(![TakeKaletra, 100 d]) (in IMPNL ◊_{r }◊_{l} (~TakeKaletra*100d*)) to the end of it. Figure 8 illustrates inconsistent nodes (red and black nodes).

Figure 8.
Inconsistent medical activities
## LEAVE A COMMENT HERE: