Abstract | ||
---|---|---|
. Future Interval Logic (FIL) is a linear-time temporal logic that isintended for specification and verification of reactive and concurrent systems.To make FIL useful for specifying and reasoning about practical systems, wepresent a first-order extension of FIL, including equality and n-ary functionand predicate symbols, and a set of sound proof rules for reasoning in the logic.We illustrate the use of the logic by specifying a sliding window protocol andproving that the specifications... |
Year | DOI | Venue |
---|---|---|
1994 | 10.1007/BFb0013989 | ICTL |
Keywords | Field | DocType |
first-order future interval logic,first order,sliding window | Computation tree logic,Programming language,Sequential logic,Interval temporal logic,Logic optimization,Computer science,Correctness,Algorithm,Linear temporal logic,Temporal logic,Rule of inference | Conference |
ISBN | Citations | PageRank |
3-540-58241-X | 3 | 0.70 |
References | Authors | |
11 | 5 |
Name | Order | Citations | PageRank |
---|---|---|---|
G. Kutty | 1 | 98 | 10.57 |
l e moser | 2 | 2134 | 233.93 |
P. M. Melliar-Smith | 3 | 2360 | 512.60 |
Laura K. Dillon | 4 | 497 | 70.70 |
Y. S. Ramakrishna | 5 | 534 | 45.81 |