[isabelle] on formalization of predicate abstraction

Dear experts:
  Do you know who have done formalization in Isabelle or other theorem
 for predicate abstraction in advanced model checking theory, and
 prove that the abstarcted system
can simulates the original system?

Thanks in advance


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.