Implementing the functions pre∃ and pre∀

فيسبوك تويتر جوجل + لينكدين  واتساب  طباعة

It remains to show how an OBDD for pre∃(X) and pre∀(X) can be computed,

given OBDDs BX for X and B→ for the transition relation →. First

we observe that pre∀ can be expressed in terms of complementation and

pre∃, as follows: pre∀(X) = S − pre∃(S − X), where we write S − Y for the

set of all s ∈ S which are not in Y . Therefore, we need only explain how to

compute the OBDD for pre∃(X) in terms of BX and B→. Now (6.4) suggests

that one should proceed as follows:

1. Rename the variables in BX to their primed versions; call the resulting OBDD

BX .

2. Compute the OBDD for exists(ˆx , apply(·,B→,BX )) using the apply and

exists algorithms 

تنبية هام

لا يسمح بنقل الموضوع بدون ذكر المصدر فى نهاية الموضوع المنقول ووضع رابط الموضوع الأصلى للكاتب

مواضيع مهمة أيضا