Title :
A new technique for proving real-time properties
Author_Institution :
Rand Corp., Santa Monica, CA, USA
Abstract :
A technique is presented for proving temporal properties of dynamic systems. The technique is based on expressing temporal properties in terms of questions about event occurrences. It is illustrated by proving a safety property about the abstract behavior of a set of real-time programs. It offers two main advantages. First, it is simple, because it utilizes well-developed intuitions about causality and top-down inference. Second, it allows proofs of properties involving continuous time and state
Keywords :
inference mechanisms; real-time systems; temporal logic; theorem proving; abstract behavior; causality; continuous time; dynamic systems; event occurrences; proofs; real-time programs; real-time properties; safety property; temporal properties; top-down inference; well-developed intuitions; Arithmetic; Clocks; Contracts; Logic; Research and development; Safety; US Government;
Conference_Titel :
AI, Simulation and Planning in High Autonomy Systems, 1990., Proceedings.
Conference_Location :
Tucson, AZ
Print_ISBN :
0-8186-2043-9
DOI :
10.1109/AIHAS.1990.93916
