Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman are contemporary computer scientists known for foundational work in formal verification, temporal logics, and game-theoretic approaches to reactive systems. Their joint contributions include developing Alternating-time Temporal Logic (ATL) and advancing the theory of multi-agent verification, which bridges logic, automata theory, and game semantics.
Co-developed Alternating-time Temporal Logic (ATL) for reasoning about multi-agent systems
Advanced game-theoretic semantics for verification of open reactive systems
Contributed to the theory of module checking and strategy logic
Pioneered work connecting temporal logic with game theory for concurrent systems