Abstract | ||
---|---|---|
In this paper we present our PVS implementation of a linear temporal logic verification system. The system includes a set of theories defining a temporal logic, a number of proof rules for proving soundness and response properties, and strategies which aid in conducting the proofs. In addition to implementing a framework for existing rules, we have also derived new methods which are particularly useful in a deductive LTL system. A distributed rank rule for the verification of response properties in parameterized systems is presented, and a methodology is detailed for reducing compassion requirements to justice requirements (strong fairness to weak fairness). Special attention has been paid to the verification of unbounded systems - systems in which the number of processes is unbounded - and our verification rules are appropriate to such systems. |
Year | DOI | Venue |
---|---|---|
2003 | 10.1007/978-3-540-39910-0_26 | LECTURE NOTES IN COMPUTER SCIENCE |
Keywords | Field | DocType |
linear temporal logic,temporal logic | Discrete mathematics,Functional verification,Systems theory,Computer science,Runtime verification,Linear temporal logic,Mathematical proof,Soundness,Temporal logic,Linear logic | Conference |
Volume | ISSN | Citations |
2772 | 0302-9743 | 15 |
PageRank | References | Authors |
1.14 | 6 | 2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Amir Pnueli | 1 | 12964 | 2377.59 |
Tamarah Arons | 2 | 278 | 14.59 |