Description
SOEN 331-S Assignment 4
This paragraph refers to Questions 1 – 2: The two binary temporal operators U and W are
duals as one can be expressed in terms of the other.
1. (10 pts) Find a logically equivalent formula for ϕ W ψ and provide a short reasoning
to support your answer. Represent this equivalence between the two expressions with
the appropriate logical connective, and support your reasoning.
2. (10 pts) Find a logically equivalent formula for ϕ U ψ, and provide a short reasoning
to support your answer. Represent this equivalence between the two expressions with
the appropriate logical connective, and support your reasoning.
3. (10 pts) Find a logically equivalent formula for ϕ R ψ in terms of W, and provide a
short reasoning to support your answer. Represent this equivalence between the two
expressions with the appropriate logical connective, and support your reasoning.
This paragraph refers to Questions 4 – 5:
Consider a railroad with a single rail and a
road level-crossing. We introduce the following propositions that represent events:
a : A train is approaching.
c : A train is crossing.
l : The light is blinking.
c : The barrier is down.
4. (15 pts) Express each of the following requirements formally. For each one, proceed to
find a logically equivalent formula that captures the safety property of the system (i.e.
in terms of “something bad never happens”):
(a) (5 pts) When a train is crossing, the barrier must be down.
(b) (5 pts) If a train is approaching or crossing, then the light must be blinking.
(c) (5 pts) If the barrier is up and the light is off, then no train is coming or crossing.
5. (10 pts) Express each of the following requirements formally in terms of the liveness
property (i.e. in terms of “something good eventually happens”):
(a) (5 pts) When a train is approaching, it will eventually cross.
(b) (5 pts) When a train is approaching and nobody is crossing, then the barrier will
eventually go down before the train crosses.
6. (45 pts) The behavior of a program is expressed by the following temporal formula:
✷
start → (ϕ ⊕ ψ)
start → τ
ϕ → ⃝(ψ U χ)
ψ ∧ τ → ⃝(ψ W χ)
τ ∧ ⃝ψ → ⃝ω
ψ ∧ ω → ⃝2χ
ω ∧ ⃝2χ → ⃝2σ
ψ ∧ ⃝σ → ⃝2π
ψ ∧ τ → σ R π
ϕ ∧ ⃝ψ → ⃝2χ
5
(a) (20 pts) Visualize all models of behavior.
(b) (10 pts) Is the set of requirements satisfiable in all models of behavior? Explain
why or why not.
(c) (10 pts) In the case where the set of requirements is not satisfiable, what modification(s) to the requirements would you make (you may temporarily assume the
role of a stakeholder) in order to achieve satisfiability.
(d) (5 pts) Having resolved any possible conflicts in requirements, specify conditions
(models of behavior), if any exist, under which the program can terminate. If
none exist, please indicate so.
4 What to submit
You must prepare all your solutions in LATEX and and produce a single pdf file. Name both
your .tex and .pdf assignment files after the Concordia id of the person who will submit, e.g.
123456.pdf, and submit both .tex and .pdf files at the Electronic Assignment Submission
portal at
(https://fis.encs.concordia.ca/eas)
under Assignment 4.
END OF ASSIGNMENT.
6
