Name
Abstract | ||
|---|---|---|
Graphical Interval Logic (GIL) is a temporal logic in which all reasoning is done by means of diagrammatic formulæ. It is a discrete linear-time modal logic in which the basic temporal modality is the interval. Future Interval Logic (FIL) provides the logical foundation for GIL. In this paper we present an automata-theoretic decision procedure for FIL with complexity DTIME
(2O(nk ) )(2^{O(n^k )} )
, where n is the size of the formula and k is the depth of interval nesting. For formulæ with bounded depth but length unbounded, the satisfiability problem for FIL is shown to be PSPACE-complete. We believe that this is the first result giving a direct decision procedure of elementary complexity for an interval logic. We also show that the logic is transparent to finite stuttering over the class of -sequences, a feature that is useful for composition and refinement. |
Year | DOI | Venue |
|---|---|---|
1992 | 10.1007/3-540-56287-7_94 | FSTTCS |
Keywords | Field | DocType |
future interval logic,automata-theoretic decision procedure,modal logic,linear time,temporal logic,satisfiability | Discrete mathematics,Modal μ-calculus,Interval temporal logic,Logic optimization,Multimodal logic,Linear temporal logic,Modal logic,Temporal logic,Mathematics,Dynamic logic (modal logic) | Conference |
Volume | ISSN | ISBN |
652 | 0302-9743 | 3-540-56287-7 |
Citations | PageRank | References |
15 | 1.45 | 18 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Y. S. Ramakrishna | 1 | 534 | 45.81 |
| Laura K. Dillon | 2 | 497 | 70.70 |
| l e moser | 3 | 2134 | 233.93 |
| P. M. Melliar-Smith | 4 | 2360 | 512.60 |
| G. Kutty | 5 | 98 | 10.57 |