Name
Abstract | ||
|---|---|---|
We present an interval logic, called future interval logic (FIL), for the specification and verification of concurrent systems. Interval logics allow reasoning to be carried out at the level of time intervals, rather than instants. However, unlike some other interval logics, the primitive objects in our semantic model for FIL are not intervals, but instants. An intervals is formed by identifying its end-points, which are instants satisfying given properties. The logic has an intuitive graphical representation, resembling the back-of-the-envelope timing diagrams that designers often draw to reason about concurrent interacting systems. The logic is designed to be insensitive to finite stuttering (a property that facilitates refinement-based multi-level correctness proofs), and is exactly as expressive as the fragment of propositional temporal logic with ''until'' but no ''next''. As the main result of this paper, we show that FIL is elementarily decidable by reduction to the emptiness problem for Buchi Automata. For most other interval logics the decision problem is at best non-elementary and often undecidable. We cosider an extension of FIL with past operators and show that this extension leads to non-elementariness. In a companion paper, we extend the logic to real-time and investigate the decision problem for that extension. |
Year | DOI | Venue |
|---|---|---|
1996 | 10.1016/0304-3975(95)00254-5 | Theor. Comput. Sci. |
Keywords | Field | DocType |
decision procedure,interval logic | Discrete mathematics,T-norm fuzzy logics,Combinatorics,Interval temporal logic,Substructural logic,Description logic,Theoretical computer science,Classical logic,Many-valued logic,Mathematics,Higher-order logic,Intermediate logic | Journal |
Volume | Issue | ISSN |
166 | 1-2 | 0304-3975 |
Citations | PageRank | References |
24 | 1.73 | 19 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Y. S. Ramakrishna | 1 | 534 | 45.81 |
| P. M. Melliar-Smith | 2 | 2360 | 512.60 |
| l e moser | 3 | 2134 | 233.93 |
| L. K. Dillon | 4 | 136 | 13.31 |
| G. Kutty | 5 | 143 | 13.89 |