2

I have a simple kripke structure, where I have 3 states, with the following transitions:

s1 --> s2
s2 --> s1
s1 --> s3
s3 --> s3

s1 is the only initial state. I do not want the loop s1 to s2 be repeated more than a certain amount (say twice). In other transition systems, I could add a guard on the transition.

Q1: Can Kripke structures have guards on transitions?

Q2: If yes, how can I model it in NuSmv?

Thanks

User 19826
  • 509
  • 2
  • 5
  • 13

1 Answers1

1

You are comparing apples and oranges here. The model with guards (e.g. in NuSMV) defines a state space which again can be seen as a Kripke structure (let's ignore issues like deadlocks here).

Guards are an element of a modelling approach, whereas the Kripke structure is the underlying theoretical concept that is used to describe the state space.

Let's take an example: We have a model with a variable v that can take two values 1 and 2 with 1 as the initial value, and two transitions with guards:

a == WHEN v=1 THEN v:=2
b == WHEN v=2 THEN v:=1

The resulting state space would be:

[v=1] --> [v=2]
[v=2] --> [v=1]

That is actually a Kripke structure (with [v=1] as the only initial state and without any labels defined on the nodes) that does not contain any guards.

Update: An example for set of labels for each node would be all Boolean expressions that evaluate to true there.

To summarize this for your two questions:

  1. No, Kripke structures itself do not have guards.
  2. Nevertheless (as explained, no guards in Kripke structures do not mean that there must not be guards in the model), I think you can regard the conditions in the case statement as a guard for the action right of the colon. Or with TRANS you have the guards implicit in the expression.
danielp
  • 1,179
  • 11
  • 26