Abstractions

Title: Abstractions

Research Question: How can we simplify the process of verifying liveness properties under a fairness condition, especially when using abstraction?

Methodology: The researchers proposed a more abstract notion than truth under fairness, specifically the concept of a property being satisfied within fairness. They established that deciding satisfaction within fairness is a PSPACE-complete problem and showed that properties satisfied within fairness can always be satisfied by some fair implementation. They then studied the interaction between behavior abstraction and satisfaction within fairness, proving that satisfaction of properties within fairness can be verified on behavior abstractions if the abstraction homomorphism is weakly continuation-closed.

Results: They found that the concept of a property being satisfied within fairness is a suitable abstraction of truth under fairness, making it easier to verify in the context of abstraction. They also showed that satisfaction within fairness can be verified on behavior abstractions if the abstraction homomorphism is weakly continuation-closed.

Implications: This research provides a more abstract and general way of understanding truth under fairness, which can simplify the process of verifying liveness properties under a fairness condition, especially when using abstraction. It also offers new insights into the interaction between behavior abstraction and satisfaction within fairness, which can be useful in other areas of computer science and engineering.

Link to Article: https://arxiv.org/abs/0101017v1 Authors: arXiv ID: 0101017v1