A Note on Digitization of Real-Time Models and Logics

TL;DR

This paper reviews how digitization transforms the verification of real-time systems from dense-time to discrete-time, discussing known results, benefits, limitations, and alternatives.

Contribution

It provides a concise overview of digitization techniques for real-time models and logics, highlighting their theoretical foundations and practical implications.

Findings

Digitization enables sound and complete verification methods.

It reduces dense-time verification problems to discrete-time.

Limitations and alternatives to digitization are discussed.

Abstract

Digitization provides a sound and complete method to reduce the problem of verifying whether a real-time system satisfies a property under dense-time semantics to whether the same real-time system satisfies the property over discrete-time. This is a brief overview of digitization of real-time models and logics covering known results, value, limitations, and alternatives.