Name
Abstract | ||
|---|---|---|
The paper presents a new deductive rule for verifying response properties under the assumption of compassion (strong fairness) requirements. It improves on previous rules in that the premises of the new rule are all first order.We prove that the rule is sound, and present a constructive completeness proof for the case of finite-state systems. For the general case, we present a sketch of a relative completeness proof. We report about the implementation of the rule in PVS and illustrate its application on some simple but non-trivial examples. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-78163-9_21 | VMCAI |
Keywords | Field | DocType |
non-trivial example,new rule,verifying response property,previous rule,new deductive rule,relative completeness proof,general case,constructive completeness proof,strong fairness,finite-state system,first order | Compassion,Constructive,Computer science,Theoretical computer science,Linear temporal logic,Artificial intelligence,Completeness (statistics),Sketch | Conference |
Volume | ISSN | ISBN |
4905 | 0302-9743 | 3-540-78162-5 |
Citations | PageRank | References |
13 | 0.82 | 19 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Amir Pnueli | 1 | 12964 | 2377.59 |
| Yaniv Sa'ar | 2 | 230 | 14.70 |