[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

about proving liveness and termination using PVS

Dear PVS users.

I've started using PVS recently. I want to prove some
liveness properties of LUSTRE(data-flow language)-like models.
I am aware that Dr Caspi and his colleages wrote some papers
on this topic, but they dealt with only safety properties,
as far as I am concerned.

I think the problem is related to the proof of termination
using well-foundedness. (Liveness proof using fairness
is not relevant, because the behavior is synchronous to
a common clock.)  I know it is a relatively old topic,
but I couldn't find references dealing with this kind of problem
- using PVS to prove termination (or liveness) with well-foundedness.
If anyone knows some materials on it, please tell me.

Seung Mo Cho.