Neue Frage
0

# 2016.09.06 : Question4_a

gefragt 2017-08-22 18:07:02 +0200

Dieser Post ist als Wiki-Post markiert

Das ist ein Wiki-Beitrag. Jeder mit Karma >75 darf diesen Beitrag verbessern.

aktualisiert 2017-08-22 18:07:02 +0200

arsinux Gravatar-Bild

As I checked with global model checking it holds for all initial states (so it holds for s2), but in the solution (for local model checking) it doesn't hold. I have two other question in local/ global model checking : 1. should we eliminate the states without successor or the ones which do not have an infinite path? 2. By the way here in this question we can reach to state s8 in one step or to state s1 in two steps which in both states "c | a" holds. As "si |= <>x" results in all OR of successor states of si, then by local model checking (K, s2) |= S1Bildbeschreibung

bearbeiten retag Als beleidigend melden schließen löschen

1 Antwort

2

geantwortet 2017-08-22 18:47:04 +0200

PS Gravatar-Bild

I don't see that: The solutions for global and local model checking as computed by http://es.cs.uni-kl.de/tools/teaching/ModelChecking.html both state that the formula holds in state s2. Global model checking computes

〖nu x. (a | c | <>x)〗= {s0;s1;s2;s3;s4;s5;s6;s7;s8}

and the proof tree for local model checking s2 ⊢ nu x. (a | c | <> x) is as shown below. I guess that you read "0:" in the wrong way; it does not say that the proof goal is wrong, it just means that here is the node with number/name 0. For checking whether a proof goal in the tree was proved or disproved, you have to check the symbols ⊢ for being proved or ⊬ for being disproved. The proof tree below proves that the formula holds in s2 which is consistent with global model checking.

Bildbeschreibung

Answers to your other questions:

  • Should we eliminate the states without successor or the ones which do not have an infinite path? No, you must not do that, it will make the results for µ-calculus incorrect. It is the case that for LTL model checking, only infinite paths are considered, so for temporal logics, you may safely remove the finite paths. However, that is not the case with the µ-calculus.
  • You are right with that, if I understand it correctly. Looking at the local model checking proof tree, we could ignore nodes 2,3,4, and could branch from node 5 to the successor state s8 that directly will prove a|c. Yes, that will make the local model checking proof shorter, but still correct (since <> already holds if we can prove it for one successor).
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-22 18:07:02 +0200

Gesehen: 32 mal

Letztes Update: Aug 22