A Note on Digitization of Real-Time Models and Logics
Janardan Misra

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Real-Time Systems Scheduling · Embedded Systems Design Techniques
