2

enter image description here

I am given the above system for atomic propositions {a,b,c}.

I'm then meant to say if certain LTL formulae hold (such as ♢☐c).

I understand what the LTL formulae mean (eventually forever c holds) but I have no idea how to read the diagram and relate it to the LTL.

I assume it's like a flow chart in that we start from the top left, /{a} and can go through the different states. But what does each of it mean divided by a?

Community
  • 1
  • 1
Aequitas
  • 2,205
  • 1
  • 25
  • 51

1 Answers1

2

Looks like FSM/transduser rather than a Kripke structure. Input/output or more generally precondition/postcondition is a common notation for FSM and its kin. precondition/postcondition (a and b and ...) / (x and y and...). So a in the state q1. In next states either only b in q4 or b and c or q3. Might be of course or instead of and in precondition, otherwise the system might halt..

Serge
  • 3,387
  • 3
  • 16
  • 34