Name
Abstract | ||
|---|---|---|
In this article, we propose a language, Asynchronous Propositional Temporal Logic (APTL), for the specification and verification of distributed hard real-time sytems. APTL extends the logic TPTL by dealing explicitly with multiple local clocks. We propose a distributed-system model which permits definition of inequalities asserting the temporal precedence of local clock readings. We show the expressiveness of APTL through two nontrivial examples. Our logic can be used to specify and reason about such important properties as bounded clock rate drifting. We then give a 220(n) tableau-based decision procedure for determining APTL satisfiability, where n is the size (number of bits) of the input formula. |
Year | DOI | Venue |
|---|---|---|
1993 | 10.1145/158431.158434 | ACM Trans. Softw. Eng. Methodol. |
Keywords | Field | DocType |
aptl satisfiability,propositional temporal logic,logic tptl,real-time systems,asynchronous propositional temporal logic,multiple local clock,local clock reading,multiclock system model,bounded clock rate drifting,important property,verification,bounded clock rate,hard real-time sytems,specification,asynchronous,input formula,real-time system specification,distributed-system model,distributed system,satisfiability,real time systems,temporal logic,system modeling | Propositional temporal logic,Asynchronous communication,Programming language,Computer science,Satisfiability,Real-time operating system,Theoretical computer science,Clock rate,Expressivity,Bounded function | Journal |
Volume | Issue | Citations |
2 | 4 | 18 |
PageRank | References | Authors |
1.20 | 17 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Farn Wang | 1 | 154 | 13.80 |
| Aloysius K. Mok | 2 | 662 | 86.52 |
| e allen emerson | 3 | 7683 | 1183.13 |