Hi Doron: I was supposed to think some more about the non-vacuity definitions. Below are some notes on the thoughts I have had. I am not sure that these definitions are good, but there are at least some good properties that result. It would be good to check whether any of the definitions below satisfies the finite prefix intuition. I have not checked them. I think that further review and discussion are needed. J.H. -------------------------------------------------------------------------- My intuition is fairly strong that if there is a finite prefix u <= w on which p is "decided", i.e. such that either u\bot^\omega |= p or u\top^\omega |/= p (modulo the problems with intersection that we know exist with this formulation), then we should have w |=^{non} p iff u |=^{non} p. Here are some possible definitions that seem intuitively reasonable to me: w |=^{non} always p iff there exists 0 <= i < |w| such that w^{i..} |=^{non} p and such that for all 0 <= j < i, w^{j..} |= p w |=^{non} s_eventually p iff there exists 0 <= i < |w| such that w^{i..} |=^{non} p and such that for all 0 <= j < i, w^{j..} |= not p SANITY CHECK 1: w |=^{non} not always not p iff w |=^{non} always not p iff there exists 0 <= i < |w| such that w^{i..} |=^{non} not p and such that for all 0 <= j < i, w^{j..} |= not p iff there exists 0 <= i < |w| such that w^{i..} |=^{non} p and such that for all 0 <= j < i, w^{j..} |= not p iff w |=^{non} s_eventually p //// Here is a somewhat weak definition of |=^{non} for the untils: w |=^{non} p until q iff w |=^{non} p until_with q iff w |=^{non} p s_until q iff w |=^{non} p s_until_with q iff there exists 0 <= i < |w| such that (either w^{i..} |=^{non} p or w^{i..} |=^{non} q) and such that for all 0 <= j < i, w^{j..} |= p and not q Let vacuous_false = 0 |-> 0. vacuous_true = not(vacuous_false) Assume that w is a non-empty natural word (i.e., no letter of w is \top or \bot). Then w |/= vacuous_false and w |/=^{non} vacuous_false w |= vacuous_true and w |/=^{non} vacuous_true SANITY CHECK 2: Assume that w is a natural word (i.e., no \top or \bot letter): w |=^{non} p until vacuous_false iff there exists 0 <= i < |w| such that (either w^{i..} |=^{non} p or w^{i..} |=^{non} vacuous_false) and such that for all 0 <= j < i, w^{j..} |= p and not vacuous_false iff there exists 0 <= i < |w| such that w^{i..} |=^{non} p and such that for all 0 <= j < i, w^{j..} |= p iff w |=^{non} always p //// SANITY CHECK 3: Assume that w is a natural word (i.e., no \top or \bot letter): w |=^{non} vacuous_true s_until p iff there exists 0 <= i < |w| such that (either w^{i..} |=^{non} vacuous_true or w^{i..} |=^{non} p) and such that for all 0 <= j < i, w^{j..} |= vacuous_true and not p iff there exists 0 <= i < |w| such that w^{i..} |=^{non} p and such that for all 0 <= j < i, w^{j..} |= not p iff w |=^{non} s_eventually p //// SANITY CHECK 4: w |=^{non} not(not p until_with not q) iff w |=^{non} (not p until_with not q) iff there exists 0 <= i < |w| such that (either w^{i..} |=^{non} not p or w^{i..} |=^{non} not q) and such that for all 0 <= j < i, w^{j..} |= not p and not not q iff there exists 0 <= i < |w| such that (either w^{i..} |=^{non} p or w^{i..} |=^{non} q) and such that for all 0 <= j < i, w^{j..} |= q and not p iff w |=^{non} q s_until p //// Note that w |=^{non} (p until q) and s_eventually q iff either w |=^{non} (p s_until q) or w |=^{non} s_eventually q <= w |=^{non} p s_until q but this is not an equivalence if q has a non-vacuous evaluation on a suffix of a word on which p fails vacuously (e.g., take p to be vacuous_false). -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Mon Jan 14 06:10:47 2008
This archive was generated by hypermail 2.1.8 : Mon Jan 14 2008 - 06:10:58 PST