Model Checking, Synthesis, and Learning

His works on verification, in finite state systems, learning, testing, probabilistic systems, timed systems, and distributed systems reflect both the diversity and the depth of his research.