Answer Happy

Question 4 For any integer k>0, a k-counter is a system which stores an integer value between 0 and k (inclusively). The k-counter can be: • incremented, as long as its value is less than k; • decremented, as long as its value is greater than 0; and • tested if its value is zero. We can give the following definition for a 2-counter: der def iszero.C2 + inc.c) c inc.cz + dec.cz cz der dec.c} (a) List the actions, states and the transitions of the system C2. [3 marks] (b) Draw the labelled transition system for C2. [2 marks] (c) For each state of this system, give a property of the modal logic M which distinguishes that state from the other states. [2 marks] (d) Give a definition for a 3-counter C3, and draw its labelled transition system. [3 marks]