Numbers, Logic, and Decidability for Cyber-Physical Systems
summary
Encoding bounded-time reachability for linear ODEs into the first-order theory of the reals reduces the verification problem to satisfiability in a logic with +, ×, exp and trig, and decidability of that logic is shown to hinge on a deep transcendental-number conjecture (Schanuel). The work cites analytic solutions (matrix exponentials), Lindemann–Weierstrass type results, and McIntyre–Wilkie reductions; MPI follow-up fills gaps to handle trigonometric functions, yielding decidability conditional on Schanuel, not a practical solver but a precise theory-to-number‑theory reduction.
AI-written summary · about
chapters (14)
- 0:00Intro
- 1:28The Reachability Problem
- 3:09Axiomatic Reasoning: Logical Encoding
- 4:48What about continuous state, continuous time?
- 5:48Cyber-Physical Systems
- 8:09The Logical View
- 11:08Related Theories
- 15:29Rational Numbers
- 22:22A similar argument works for
- 26:21Are all real numbers algebraic?
- 28:33Digression: Cantor's First Proof
- 32:28Transcendental Numbers
- 33:48An explicit transcendental number
- 41:42A Simple Reachability Question
related talks
01h 05mVerifying Infinitely Many Programs at Once
28mReasoning about Distributed Reconfigurable Systems
34mLogic in Computer Science, Engineering and Industry
27mUnrealizability Logic
22mExecution Time Program Verification With Tight Bounds
21mMechanised Hypersafety Proofs about Structured Data
48mBeyond SAT - Proofs for QBF, and more
23mVerifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach