Topics: Deductive reasoning (first-order computation tree logic aka FO-CTL)
Given
- Every user who submits a request will eventually receive a receipt on every possible notification path. [1]
- If a user receives a receipt, then on every possible notification path the user will eventually receive a confirmation. [2]
- Alice has submitted a request. [3]
- Alice is a user. [4]
Find
Will Alice eventually receive a confirmation on every possible notification path?
Solution
Definition:
U(x): x is a user.
R1(x): x has submitted a request.
R2(x): x has received a receipt.
C(x): x has received a confirmation.
A: All paths — Aφ means that φ is true on all possible future paths.
(- E: Exists a path — Eφ means that φ is true on at least one possible future path.)
Additional: LTL operators (X, F, G, U), see Math – Exercise 12 (Logic).
Representation:
[1]: ∀x AG((U(x)∧R1(x))→AF R2(x))
[2]: ∀x AG(R2(x)→AF C(x))
[3]: R1(Alice)
[4]: U(Alice)
Deduction:
Instantiate x=Alice in [1]: ∀x AG((U(Alice)∧R1(Alice))→AF R2(Alice)),
with [3] and [4] we conclude: AF R2(Alice).
Instantiate x=Alice in [2]: ∀x AG(R2(Alice)→AF C(Alice)),
with AF R2(Alice) we conclude: AF C(Alice).
Answer
Yes, Alice will eventually receive a confirmation on every possible notification path.