Representing Imperfect Information of Procedures with Hyper Models - Logic and Its Applications - page 229

M

=( S,

→ , → ∃

Definition 7 (Semantics). Thesemantics of EPDL onhyper models

, → ∀ ,V ) is defined similarlyasthesemantics of EAL onhyper models, with the follow-

ing clauses replacing theclauses for

a ˆ formulasin thecase of EAL:

M,s 0 ˀˆ ⃔∃t ∈ S : s w

ₒ t for some w ∈ ˀ such that M,t 0 ˆ
M,s ˀˆ ⃔∃T 0 ,...,T k ↆ S, ∃ˀ 1 ,...,ˀ k ∈ ʠ Σ :( s ∈ T 0 ,T 0

ˀ k
ₒ ∃ T k , ( ˀ 1 ; ··· ; ˀ k ) ↆ ˀ

ˀ
ₒ ∃ ···

ˆ )
M,s ♦ ˀˆ ⃔∀T 0 ,...,T k ↆ S, ∀ˀ 1 ,...,ˀ k ∈ ʠ Σ :(( s ∈ T 0 ,T 0

and ∀t ∈ T k : M,t

ˀ k
ₒ ∀ T k ,ˀↆ ( ˀ 1 ; ··· ; ˀ k ))

ˀ
ₒ ∀ ···

( ∃t ∈ T k : M,t ♦ ˆ ))
It is not hard to see that on simple hyper models the above semantics coincides
with the semantics of EAL on

implies

aˆ formulas. This justifies ourabuse of for both

EPDL and EAL. The semantics says that the agent knows that ˀˆ at s if there is a

ˀ )such that each ˀ i step can be realized by a ˀ i

'refinement' of ˀ (( ˀ 1 ; → ∃

transition, and in the end it will certainly reach a ˆ -state. Note that it is not necessary
that ˀ 1 ;

··· ; ˀ k ) ↆ

; ˀ k = ˀ ,sincewejust need to guarantee there exists an execution of ˀ .
We now prove the analogue of Lemma 1.
Lemma 2. Fo r all the pointed hyper model

···

M ,s , any EPDL formula ˆ the following

two hold: (1) M ,s ˆ implies M ,s 0 ˆ ;(2) M ,s 0 ˆ implies M ,s ♦ ˆ .

Therefore M ,s ˆ implies M ,s ♦ ˆ .

ˀ ˈ .Suppose M ,s ˀ ˈ then:

Proof. We only need to show the case of

ˀ k
ₒ ∃

ˀ 1
ₒ ∃ ··· ∃T 0 ,...,T k ↆ S, ∃ˀ 1 ,...,ˀ k ∈ ʠ : s ∈ T 0 ,T 0 T k ,ˀ 1 ; ··· ; ˀ k ↆ

ˀ and ∀t ∈ T k : M,t ˈ.
Let t 0 = s . By the definition of hyper model, there exist t i ∈ T i and w i ∈ ˀ i for
1 ≤ i ≤ k such that t i− 1

w i
→ t i . It is clear that w 1 ···w k ∈ ˀ 1 ; ··· ; ˀ k .Since

ˀ 1 ; ··· ; ˀ k ↆ ˀ , w 1 ··· w k ∈ ˀ .ThusbyIH, M ,s 0 ˀ ˈ .

ˈ then there is a t ⓦ such that s w

t ⓦ

M ,s 0 ˀ →

Now for the second claim, suppose

M,t ⓦ 0 ˈ .ByIH, M,t ⓦ ♦ ˈ .Nowsuppose towards contradiction

for a w ∈ ˀ and

that M,s ♦ ˀˈ then according to the semantics we have:

∃T 0 ,...,T k ↆ S, ∃ˀ 1 ,...,ˀ k ∈ ʠ : s ∈ T 0 ,T 0

ˀ 1
ₒ ∀ ···

ˀ k
ₒ ∀ T k ,ˀↆ ˀ 1 ; ··· ; ˀ k and ∀t ∈

T k : M,t ♦ ˈ
Obviously, if we can show that t ⓦ ∈

T k then a contradiction is derived. In the following

we prove that t ⓦ ∈

T k .Since ˀ ↆ ˀ 1 ; ··· ; ˀ k and w ∈ ˀ , w ∈ ˀ 1 ; ··· ; ˀ k . Therefore

there exist w i ∈ ; w k ( w i can be an empty

string). According to the definition of hyper model, if s w 1 ···w i

ˀ i for 1 ≤ i ≤ k such that w = w 1 ; ···

→ t then t ∈ T i for all

k . In particular if s w 1 ···w k

T k .
Based on this lemma and the proof of Theorem 1, the following theorem holds im-
mediately.
Theorem 2. DIST , T , 4 , and 5 are valid for EPDL onhyper models.
It is easy to verify that the EPDL analogies of Proposition 1 and Proposition 2 also hold.

≤ i ≤ → t then t ∈ T k . Now it is clear that t ⓦ ∈

1

4 Discussion and Future work

So far, we have only laid out the basics of an alternative semantics for EPDL based
on hyper models where epistemic relations are replaced by two approximations of the