Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

870 questions

988 answers


439 users

0 votes

we have 3 different approaches for problem 6 (LTL model checking) in last 3 examinations. How do we convert transition relation to Shannon normal form? How do we do the case distinction? could you please explain this question in exam 31 August 2021?
in * TF "Emb. Sys. and Rob." by (120 points)

1 Answer

0 votes

It is not wise to ask for a standard procedure that may exist, but may not be efficient if applied to any problem. In general, LTL model checking is done as follows to compute the states that satisfy A phi:

  1. translate the negation of the LTL formula phi to an equivalent existential nondeterministic omega-automaton
  2. compute the product of the Kripke structure and the omega-automaton
  3. determine the states that have a path in the product structure that starts in an initial state of the automaton and that satisfies the acceptance condition
How these steps are done in detail, may be different for the particular example that is considered. Sometimes, a big simplification can be done by observing something, mostly by omitting unreachable states, and deadend states. That can be done in many ways, and neither is there a unique solution nor is there a general recipe; just keep your eyes open when looking at such examples. 
by (139k points)
Imprint | Privacy Policy