Neue Frage
0

Compute the set of states from which the states satisfy b<->(c->b) can be reached symbolically

gefragt 2017-08-19 19:54:26 +0100

herle Gravatar-Bild

aktualisiert 2017-08-22 14:41:20 +0100

What is the meaning of this statement. what I have to find for this kind of questions in KRIPKE structure where Initital state φI= !(a->c), φR=!((next(c)<->c)|!a|next(b)).

bearbeiten retag Als beleidigend melden schließen löschen

1 Antwort

2

geantwortet 2017-08-19 20:57:50 +0100

PS Gravatar-Bild

aktualisiert 2017-08-19 21:01:10 +0100

We are considering here a Kripke structure with variables {a,b,c} that is symbolically represented by the following two formulas

  • initial states: !(a->c)
  • transitions: !((next(c)<->c)|!a|next(b))

The Kripke structure is shown below and since the formula b<->(c->b) is equivalent to b|c, the considered set of states are given in green color.

Bildbeschreibung

We shall now compute the existential predecessors, since these are the states that have a successor in the state set, and therefore can reach it. A symbolic computation can be done as follows:

∃next(a).∃next(b).∃next(c).!((next(c)<->c)|!a|next(b))&(next(b)<->(next(c)->next(b)))
  = ∃next(b).∃next(c).!(!a|(c<->next(c))|next(b))&((next(c)->next(b))<->next(b))
  = ∃next(c).!(!a|(c<->next(c)))&next(c)
  = !(c|!a)

Hence, the existential predecessors are symbolically represented by !(c|!a), i.e., !c&a which are the states s6:{a,b} and s4:{a}, and yes, indeed, these are the only two states having a transition towards the green states.

You can use the online tool at http://es.cs.uni-kl.de/tools/teaching/SymbolicStateTrans.html by leaving the field for input variables empty, declaring a;b;c as state variables, and using the initial state formula and transition relation above.

If you enter as state set predicate b<->(c->b) and select existential predecessors, your problem will be solved by the tool.

The above operation is very important for symbolic model checking, and is usually carried out using BDDs for the formulas. In that case, special BDD algorithms will compute the state set directly as a BDD.

bearbeiten Als beleidigend melden löschen publish Link mehr

Ihre Antwort

Du kannst deinen Eintrag bereits als Gast verfassen. Deine Antwort wird zwischengespeichert, bis du dich eingeloggt oder registriert hast.
Bitte nur konstruktive Antworten auf diese konkrete Frage posten.
Falls du eine Frage stellen willst, dann stelle eine neue Frage.
Für kurze Diskussionen und Nachfragen benutze bitte die Kommentar-Funktion.
Deine Fragen und Antworten kannst du jederzeit nachbearbeiten und verbessern.
Gute Fragen und Antworten kannst du mit einem Upvote oder Downvote bewerten.

Schreibe deine Antwort auf diese Frage

[Vorschau ausblenden]

Fragen-Tools

Beobachten
1 Follower

Statistik

Gefragt: 2017-08-19 19:54:26 +0100

Gesehen: 70 mal

Letztes Update: Aug 19