COMP525: Reasoning About Action and Change 1st assignment: Linear Time Temporal Logic (Deadline: Monday 16th March 2020 at 14.00) Worth 12.5% of the final mark (assignment one of two) The coursework for this module is 25% of the total module. This piece of coursework is worth half of the coursework marks, i.e. 12.5% of the module. To pass the module students do not have to pass each individual piece of coursework. Please note the University and Departmental guidelines relating to coursework and assessment, in particular, relating to late submissions and academic integrity. Your solutions (hand written, typeset or a mixture) should be scanned and submitted electronically as one single pdf doc- ument. When you are asked to run NuSMV make sure you include the NuSMV output in your solutions. Similarly, include a copy of the NuSMV programs you are asked to write in questions 3(a) and 4(b) in your solutions (and the properties in NuSMV syntax that you are checking). Upload your files to https://sam.csc.liv.ac.uk/COMP/Submissions.pl?strModule=COMP525 (you will need to log in using the relevant username and password). You must combine your solutions into one single pdf document making it clear which pages relate to which question. Those submitting multiple documents will have a mark penalty imposed. This assignment covers the following learning outcomes. • Provide formal specifications, using a logical language, of informal problem descriptions. • Verify properties of models and produce simple logical proofs. • Understand and use model checkers. • Understand and be able to explain and formulate properties (such as “safety”, “fairness” and “liveness”) of a given system. There are four questions and each question is worth 25 marks. 1. Foundations of linear time temporal logic (a) Construct a model for each of the following LTL formulae i. (©p) ∧ (♦q) ii. (p ∨ q) iii. (p ∧ r) W (p ∧ q) iv. (p ∧ q) U (©r) 8 marks (b) Consider the following model σ. r q¬q ¬r r r ¬q ¬q¬q r 0 1 2 3 Do the following formulae hold at state 0? In each case, briefly justify your answer concisely. 1 i. q W r ii. ¬q U (q ∧ r) iii. ©r ∧©© r iv. ♦r 8 marks (c) Using the tableau method for LTL show that ♦p→ (p ∨©♦p) is a valid formula. 9 marks 2. Specification using Linear Time Temporal Logic Consider three processes 1, 2, and 3 processing synchronously. Each controls a variable x1, x2 and x3 respectively. Initially x1 and x2 and x3 are all true. Each process has the following behaviour. • Process 1 sets the value of x1 in the next moment to be true if both x2 and x3 are true (now), otherwise it sets x1 to be false. • Process 2 sets the value of x2 in the next moment to be true if either x1 or x3 are true (now), otherwise it sets x2 to be false. • Process 3 sets the value of x3 in the next moment to be true if both x1 and x2 are false (now), otherwise it sets x3 to be false. (a) Draw the transition system for the combined system. Make sure you draw all logi- cally possible states (one for each possible value of x1, x2 and x3, including possibly unreachable ones). 8 marks (b) Write LTL formulae to specify the initial conditions and the three processes. 13 marks (c) Suggest one non-trivial safety property and one non-trivial liveness property which hold for the above transition system. 4 marks 3. Synchronous LTL Logic Model Checking (a) Write a NuSMV input file describing the system described in question 2. [Hint: this is similar to a system described in lecture 9.] 9 marks (b) Add to the NuSMV input file the properties mentioned in question 2 and run NuSMV to make sure the properties do hold. 4 marks (c) The property ♦(x1 ∧ x2 ∧ x3) should not hold for this system. Rewrite this property in the correct syntax for NuSMV. Add to the input file and run it. Using the output from NuSMV construct a counter model and draw this. 6 marks (d) Suggest another property that will not hold for this system. Repeat part (3c) using this property. 6 marks 4. Asynchronous LTL Model Checking Now again consider the system described in question 2 but assume it is asynchronous (a) Draw the transition system representing the asynchronous system. [Hint: the states will be the same as for the synchronous version but the transitions will change. Also you need to consider which process’s turn it is to move. To do this give labels to the transitions indicating which process is responsible for that transition.] 8 marks (b) Write a new version of the NuSMV input file which is now asynchronous. Also specify the fairness constraint that each process gets a turn to go infinitely often. Add the two properties from question 3(b) and run NuSMV. 6 marks (c) Find a property (different from the ones you have already mentioned) that is true for the synchronous system and not for the asynchronous system with fairness (or vice versa). Run NuSMV with this property for each input file. Draw the path for the property that fails. 5 marks 2 (d) Consider now the asynchronous system both with and without fairness. Find a non- trivial property that holds when each process gets a turn to go infinitely often (i.e. with fairness) but doesn’t hold without this fairness constraint. Show NuSMV running in each case and explain why the property fails in the second case. 6 marks 3
