Towards a Theory of Time-Bounded Verification

Abstract. We propose a theory of time-bounded verification for realtime systems, in which verification queries are phrased over time intervals of fixed, bounded duration. We argue that this theory is both pertinent, in that it is fully adequate to handle a large proportion of `real-world' real-time systems and specifications; and effective, in that the restriction to bounded time domains reclaims as decidable several of the key decision problems of unbounded real-time verification. Finally, we discuss several directions of ongoing and future work.

• Type: Conference
• Year: 2010
• Where: ICALP
• Authors: Joël Ouaknine, James Worrell
• Keywords: ICALP 2010, Programming Languages, Time Intervals, Time-bounded Verification, Verification Queries