AbstractThe most natural, compositional, way of modeling real-time systems uses a dense domain for time. The satisfiability of timing constraints that are capable of expressing punctuality in this model, however, is known to be undecidable. We introduce a temporal language than can constrain the time difference between events only with finite, yet arbitrary, precision and show the resulting logic to be EXPSPACE-complete. This result allows us to develop an algorithm for the verification of timing properties of real-time systems with dense semantics.
The abstract is also available as a LaTeX file, a DVI file, or a PostScript file.
Categories and Subject Descriptors: D.3 [Programming Languages] -- real-time systems; D.2.1 [Software Engineering]: Requirements/Specifications -- languages; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs -- logics of programs, mechanical verification, specification techniques; F.4.3 [Mathematical Logic and Formal Languages]: Formal Languages -- classes defined by automata, decision problems
General Terms: Theory, Verification
Additional Key Words and Phrases: Model checking, real time, temporal logic, timed automata
Selected references
- Rajeev Alur, Costas Courcoubetis, and David Dill. Model-checking in dense real-time. Information and Computation, 104(1):2-34, May 1993.
- Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 25 April 1994. Fundamental Study.
- Rajeev Alur and Thomas Henzinger. Real-time logics: Complexity and expressiveness. Information and Computation, 104(1):35-77, May 1993.
- Rajeev Alur and Thomas A. Henzinger. A really temporal logic. Journal of the ACM, 41(1):181-204, January 1994.
- Edmund M. Clarke Jr., E. Allen Emerson, and A. Prasad Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244-263, April 1986.
- Eyal Harel, Orna Lichtenstein, and Amir Pnueli. Explicit clock temporal logic. In Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, pages 402-413, Philadelphia, Pennsylvania, 4-7 June 1990. IEEE Computer Society Press.
- David Harel, Amir Pnueli, and Jonathan Stavi. Propositional dynamic logic of nonregular programs. Journal of Computer and System Sciences, 26(2):222-243, April 1983.
- Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193-244, June 1994.
- Harry R. Lewis. A logic of concrete time intervals (extended abstract). In Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, pages 380-389, Philadelphia, Pennsylvania, 4-7 June 1990. IEEE Computer Society Press.
- Orna Lichtenstein and Amir Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, pages 97-107, New Orleans, Louisiana, January 1985.
- A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. Journal of the ACM, 32(3):733-749, July 1985.