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

1.1k questions

1.2k answers

1.6k comments

529 users

0 votes
as per my kripke structure the answer i am getting is

a&!p &q &!next(p)&!next(q)&next(a) | a&!p&!q&next(p)&!next(q)&next(a) | a&p&!q&next(p)&next(q)&next(a) | a&p&q&next(p)&next(q)&next(a)

but the solution is wrong can you tell me what is the mistake
related to an answer for: exercise sheet 5 question 1
in * TF "Emb. Sys. and Rob." by (300 points)

2 Answers

0 votes

We consider a Kripke structure with variables p,q,a, initial states !p&!q and the following transition relation R:

    a & !p &  q & !next(p) & !next(q) |
    a & !p & !q &  next(p) & !next(q) |
    a &  p & !q &  next(p) &  next(q) |
    a &  p &  q &  next(p) &  next(q)

The Kripke structure looks as follows:

Looking at the Kripke structure, you can see

  • initial states s0,s4 described by !a&!p&!q|!a&!p&q
  • deadend states s0,s1,s2,s3 described by !a
  • unreachble states s1,s5 described by !a&!p&q|a&!p&q

We now want to clean up the Kripke structure in that we remove transitions to deadend states and transitions from unreachable states.

a) Initial states without deadend states are only s4, i.e., a&!p&!q

b) As Martin said, we should consider in this part states that are reachable from the new initial states, but do not yet make changes to the transition relation.

I would say from s4 (the only initial state), states s2,s3,s4,s6,s7 are reachable.

c) Removing transitions to deadend states is done by using the following transition relation

    (
     a & !p &  q & !next(p) & !next(q) |
     a & !p & !q &  next(p) & !next(q) |
     a &  p & !q &  next(p) &  next(q) |
     a &  p &  q &  next(p) &  next(q)
    )
    & next(a)

which looks as follows

d) Removing transitions among unreachable states yields the following transition relation and Kripke structure

    (
     a & !p &  q & !next(p) & !next(q) |
     a & !p & !q &  next(p) & !next(q) |
     a &  p & !q &  next(p) &  next(q) |
     a &  p &  q &  next(p) &  next(q)
    )
    & next(a)
    & !(!a&!p&q|a&!p&q)

This is the Kripke structure you have constructed, and probably you have also use it already to solve part b), but that was maybe too early. Am I right?

by (166k points)
0 votes
a&!p &q &!next(p) is unreachable.
by (25.6k points)

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy
...