Pnueli proposes reasoning about programs that are never meant to halt (operating systems, controllers) with a logic of time. He reduces most correctness claims to two kinds: invariance (something holds at every step of every execution) and eventuality (whenever p happens, q follows at some later point). He gives two proof systems, the second an adaptation of the tense logic Kb with operators G (always) and F (eventually), and shows the propositional future fragment is complete and decidable.
Findings
- Invariance covers partial correctness, mutual exclusion and deadlock freedom; eventuality covers total correctness and accessibility (a process that asks for its critical section eventually gets it).
- The pattern G(p ⊃ F q), “whenever p, eventually q”, is written down here, and it is still the standard way to state a response requirement.
- Proving eventualities in concurrent programs needs an explicit fairness assumption: no enabled action is delayed forever. Pnueli adds it as an axiom.
- The system model is deliberately general. The paper lists “robot driving programs” among the systems a discrete transition model can describe.
Limits
- Proof systems for humans, with no algorithm for checking a running system. Model checking and monitoring came later and built on this logic.
- Discrete time with no metric distances. “Eventually” has no deadline, which is the gap timed logics later filled (timed automata, MTL, STL).
- I read a scanned copy with poor OCR, so I skipped the detailed proofs.
Relevance
Every LTL monitor for a robot (LTL3, ROSMonitoring) inherits the safety and liveness split from here. See runtime monitoring and long-term autonomy.
Links
- DOI
- Subfield: Safety and verification