Really visual temporal reasoning
- 30 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 262-273
- https://doi.org/10.1109/real.1993.393490
Abstract
Real-Time Future Interval Logic (RTFIL) is a visual logic with formulae that resemble timing diagrams. It is a dense real-time temporal logic that is based on two simple temporal primitives: interval modalities for the purely qualitative part and duration predicates for the quantitative part. We present the logic, and illustrate its use in specifying the railroad crossing example and in proving some of its properties. The logic is decidable by reduction to the emptiness problem of Timed Buchi Automata. An automated theorem prover based on this decision procedure has been implemented as part of a graphical proof environment. The proofs of the railroad crossing example have been verified using this theorem prover. An automated theorem prover and a graphical specification language greatly facilitate the task of verifying real-time proofs. This convenience apart, RTFIL is invariant under real-time stuttering and does not admit instantaneous states. These properties facilitate proof methods based on abstraction and refinement.Keywords
This publication has 20 references indexed in Scilit:
- A hardware semantics based on temporal intervalsPublished by Springer Nature ,2005
- Automata for modeling real-time systemsPublished by Springer Nature ,2005
- An implementation of three algorithms for timing verification based on automata emptinessPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Symbolic model checking for real-time systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- A Graphical Interval Logic toolset for verifying concurrent systemsPublished by Springer Nature ,1993
- Putting time into proof outlinesPublished by Springer Nature ,1992
- Graphical specifications for concurrent software systemsPublished by Association for Computing Machinery (ACM) ,1992
- A propositional modal logic of time intervalsJournal of the ACM, 1991
- Specifying real-time properties with metric temporal logicReal-Time Systems, 1990
- Extending interval logic to real time systemsPublished by Springer Nature ,1989