(CPT301/25-26/S1)
Notes:
◼ To obtain full marks for each question, relevant and clear steps should be included in the answers.
◼ Partial marks may be awarded depending on the degree of completeness and clarity.
Section I: Short Answer Questions
Question A: Basic Logic [20 marks]
a) The following temporal logic formulas are not simple enough. Each formula could be replaced with a concise version that presents the same property. Please refine these formulas and justify your answer. (“concise” means “small” or “have few symbols”)
i. (□◊r) U (p U q) [2 marks]
ii. ¬◊¬(p S q) [2 marks]
b) Prove the validity of the logic expression below using both Truth Table and Natural Deduction: ((p → q)) ├ (r∨p) → (r∨q) [7 marks]
c) Is the following temporal logic property valid? Here, p and q are arbitrary state formulas. (◊□q∨◊□(¬p)) ⇒ ◊□(p→□q) [4 marks]
d) Let p be a Boolean variable of a system. The property is described as follows:
In a sequence q0, q1, q2, q3, … of states, t holds in even states q0, q2, q4, … and has arbitrary values in the other states.
Construct Büchi automata according to the following requirements:
i. Accepting exactly all behaviors that do NOT satisfy the above property. [2 marks]
ii. Accepting exactly all behaviors that have no suffix that satisfies the property. In other words, for any suffix qn, qn+1, qn+2, qn+3 … it should NOT be the case that p is true in all of the states qn, qn+2, qn+4, … [3 marks]
Please justify your answer.
Question B: Z Specification [25 marks]
Define types STATE ::= Alive | Dead and CELL = ℤ × ℤ.
CW game can be represented as an infinite two-dimensional grid where each cell is either alive or dead. Formally, this can be modeled as a function
CWState : CELL → STATE
where CELL denotes the set of all grid positions (for example, Z
2
), and STATE is the set
{Alive,Dead}.
a) Define a schema CWState that contains exactly one schema variable, CWState. [2 marks]
The schema’s state predicate must ensure that every possible value of boardState corresponds to a valid board configuration.
b) Write the schemas ∆CWState and ΞCWState in full. [4 marks]
c) Write a schema InitCW which inputs a variable piece? : CELL → STATE , and sets the board up according to piece? . [4 marks]
d) The cell (x , y) is adjacent to the cell (xt
, yt
) when they share an edge or a corner. For instance, the grey squares below are adjacent to the black square:
Write a predicate adjacent on CELL×CELL such that adjacent ((x , y ), (x
t
, yt
)) is true precisely when (x , y ) and (x
t
, yt
) are adjacent. [4 marks]
e) Specify ln : CELL → (CELL → STATE ) → ℕ which returns the number of Alive neighbours of a cell under a given board s : CELL → STATE. Use adjacent to count only neighbours of c. [2 marks]
f) Using ln, define a total function
nextCell : CELL × (CELL → STATE) → STATE
that encodes exactly these transitions:
An Alive cell with fewer than 2 Alive neighbours becomes Dead.
An Alive cell with 2 or 3 Alive neighbours stays Alive.
An Alive cell with more than 3 Alive neighbours becomes Dead.
A Dead cell with exactly 3 Alive neighbours becomes Alive.
Write a schema CWTransition specifying the transitions of the board. [6 marks]
g) Write a schema Tick that relates the board before and after one clock tick by pointwise application of nextCell. Use a change schema and make the post-state equal to the cellwise update. [3 marks]
Question C: Temporal Specification [15 marks]
a) This question concerns the representation of natural language descriptions in temporal logic.
Consider the following transition system T and the list of LTL formulae φ1, . . . , φ4.
φ1 :□(a ⇒ ◊c) [2 marks]
φ2 : ◊(b ⇒ ¬a) [2 marks]
φ3 : ◊□ (b∧c) [2 marks]
φ4 : (a∨b∨c) U c [2 marks]
For each formula φi, i : 1 ≤ i ≤ 4, check whether T |= φi holds or not. Justify your answer for each formula.
b) Write a temporal logic formula that precisely captures the semantics of the following program fragment. The formula should describe the evolution of the variables a and b over the next one or two steps, depending on the branch taken. Necessary explanations are required. ( || means nondeterministic choice: the system may execute either a := 2*a or b := 2*b, but not both.) [7 marks]
if (a > b) then
a := a - b;
b := b + 1;
elseif (a < b) then
b := b - a;
a := a + 1;
else
( a := 2*a || b := 2*b ) // nondeterministic choice, one step
End
Section II: Short Report [40 marks]
Question D: Model Checking
Model: Use the provided Promela system with processes P, Q, shared x,y,b, and rendezvous channel t. See the following given Promela code.
byte x = 0;
byte y = 0;
bool b = false;
chan t = [0] of { bit };
active proctype P() {
do
:: x < 20 -> atomic { x = 20; b = true }
:: x >= 0 -> if
:: x < 30 -> x++
:: else -> x = 10
fi
:: t?1 -> y++
od
}
active proctype Q() {
do
:: (x >= 10 && b) -> t!1
:: (x < 10) -> atomic { x = 0; b = false }
:: else -> skip
od
}
Report
1. Behavior. overview: Describe plausible executions and outcomes (e.g., unlatched vs. latched regimes; effects on x, y, b) with 1–2 short execution sketches.
2. Property set: Specify ≥3 safety and ≥3 liveness properties relevant to this model. Provide the exact formulas you verify.
3. Verification experiments: Show command lines and results. For each property, report Hold / Fail / Inconclusive with brief evidence (stats; short annotated counterexample for failures).
4. Impact of model variants (≥2): Propose two minimal changes (e.g., channel capacity, adjusting/removing atomic, guard tweaks, progress/fairness modeling). Predict effects, re-verify, and compare results concisely (before/after table + root-cause note).
5. Word limit: ≤1000 words.
Note: The use of generative artificial intelligence tools is not permitted in the preparation of this report. All text, analysis, and arguments must be produced independently by the student without AI assistance.
Presentation (Scheduled for Week 13).
• 8 minutes to present your approach and findings.
• 5 minutes for Q&A.
Marking Scheme
Report [20 marks]
R1. Property design & correctness [8 marks]
• 0–3: Fewer than 3 safety or 3 liveness; major logic mistakes or poor relevance.
• 4–5: Meets minimum; mostly well-formed temporal logic; some mismatch/redundancy.
• 6–7: Clear, relevant, non-trivial set; good coverage of key behaviors; sound justification.
• 8: Precise, minimal, insightful portfolio; captures edge cases; excellent rationale.
R2. Verification experiments & rigor [6 marks]
• 0–2: Minimal setup; unclear commands/options; sparse evidence.
• 3–4: Commands shown; at least one option varied; basic stats reported.
• 5: Multiple options compared; reproducible workflow; coherent methodology.
• 6: Systematic exploration; well-organized, easily reproducible; clear justification of choices.
R3. Evidence & counterexample analysis [2 marks]
• 0: Results stated without explanation; trails missing/uninterpreted.
• 1: At least one failing property with a correct, concise trail explanation.
• 2: Clear, minimal trails for all failures; explains enabling guards/interleavings and why they repeat.
R4. Impact of model variants — [4 marks]
• 0–1: No variants or purely speculative discussion.
• 2-3: One variant tested well or two variants lightly tested; partial before/after evidence.
• 4: ≥2 variants tested with before/after tables and concise root-cause analysis of differences.
Presentation [20 marks]
P1. Understanding [8 marks]
• 0–3: Disorganized; unclear model behavior; confuses safety vs. liveness.
• 4–5: Mostly clear storyline; basic grasp of regimes and properties.
• 6–7: Cohesive, accurate narrative tying model, properties, and results.
• 8: Crisp, insightful synthesis; highlights key subtleties (e.g., scheduling/fairness) accessibly.
P2. Live demo / walkthrough of verification [6 marks]
• 0–2: No demo or non-reproducible steps; superficial.
• 3–4: Basic run shown (commands/results); limited option variation.
• 5: Competent walkthrough with options and interpreting outputs.
• 6: Polished, reproducible demo; anticipates pitfalls; connects outputs to properties and traces.
P3. Slides/visuals & time management [2 marks]
• 0–1: Cluttered slides; over/under time.
• 1–2: Clean visuals (tables/flows/trails screenshots); well-paced within allotted time.
P4. Q&A [4 marks]
• 0: Unable to address questions.
• 1-2: Addresses basics; minor inaccuracies.
• 3-4: Accurate, confident answers; can reason about “what-if” changes.