Name
Abstract | ||
|---|---|---|
We present axiomatizations for Until Temporal Logic (UTL) and for Since/Until Temporal Logic (SUTL). These logics are intended for use in specifying and reasoning about concurrent systems. They employ neither a next nor a previous operator, which obstruct the use of hierarchical abstraction and refinement, and make reasoning about concurrency difficult. We also provide a procedure for translating SUTL formulas into UTL formulas, and demonstrate that the axiomatizations are sound and complete with respect to the class of ω-sequences. We show, however, that the axiomatization of UTL admits models that the axiomatization of SUTL does not, thereby demonstrating that the logics are not equivalent. |
Year | DOI | Venue |
|---|---|---|
1994 | 10.3233/FI-1994-2141 | Fundam. Inform. |
Keywords | Field | DocType |
hierarchical abstraction,sutl formula,concurrent system,temporal logics,temporal logic,present axiomatizations,previous operator,utl formula | Discrete mathematics,Abstraction,Concurrency,Operator (computer programming),Soundness,Temporal logic,Completeness (statistics),Mathematics | Journal |
Volume | Issue | Citations |
21 | 4 | 5 |
PageRank | References | Authors |
0.63 | 16 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| L.E. Moser | 1 | 10 | 1.32 |
| P.M. Melliar-Smith | 2 | 10 | 1.32 |
| G. Kutty | 3 | 143 | 13.89 |
| Y.S. Ramakrishna | 4 | 10 | 1.66 |