Institute for Mathematical Sciences Event Archive



Online registration form




      Scientific aspects


Automata, Logic and Games
(22 August - 25 September 2016)


Organizing Committee · Visitors and Participants · Overview · Activities · Venue


 Organizing Committee




 Visitors and Participants




As computing systems become larger, more complex, and increasingly distributed and interactive, there is a pressing need for formal methods that guarantee their reliability, correctness, and efficiency. The enormous cost of validating new designs has driven the search for powerful techniques of construction, modelling and verification of computing systems. Unlike physical systems, computing systems are "discontinuous", in the sense that a minor change in the input may cause major changes in the output behaviour. Consequently, standard methods of testing that are common in engineering sciences, while still useful, cannot be sufficient. A consensus is emerging in both industry and academic that the use of appropriate mathematics backed up by computer-aided design and verification tools is no longer a luxury, but a necessity.

Logic and automata-theoretic methods have been used in the specification, design and verification of hardware and software systems for decades, starting from early work on digital circuit design. A breakthrough was achieved in the 1960s by Church, Buchi, Rabin and others who showed the expressive equivalence of automata and logical systems (monadic second-order logic over infinite words and trees, in particular). Their work is the basis of a general framework for reasoning about implementation (automata) and specification (logic), yielding algorithms for checking consistency of specifications and correctness of implementations.

The study of games is a thread that runs through logic and algorithm. We are mainly concerned with two-player games on (finite or infinite) graphs with (finite or infinite) plays. Games capture in a natural and intuitive way the interaction between an (open) system and its environment. This games perspective has led to new algorithmic directions in verification on the one hand, and given rise to innovative methods of giving semantics of computation on the other.

More generally, the triumvirate of logic, automata and games is the basis of an elegant and powerful theory for the algorithmic and semantic analysis of computing systems. The model checking technology for the automatic verification of computing systems, which is based on these foundations, has seen substantial developments in the last three decades.

The proposed programme is concerned with both the theory and practice of verification. An objective of the programme is to promote interactions between researchers working in the theory and foundations of automata, logic and games, and those who build tool implementations of model checking algorithms, perform empirical studies, and work with the verification industry.

The five-week programme will focus on the following topics:


  • Communicating, Distributed and Parameterized Systems
  • Constraint Solving
  • Higher-Order Model Checking
  • Probabilistic Model Checking
  • Timed Systems




Tuesday, 30 August 2016



Performance Hall, Yale-NUS College, 18 College Avenue West 138528


6:30pm - 7:30pm

Humans, Machines, and Work: The Future is Now
Moshe Y. Vardi, Rice University, USA






Thursday, 1 September 2016



Lecture Theatre 31, National University of Singapore
Block S16, Level 3, 6 Science Drive 2, Singapore 117546


6:30pm - 7:30pm

The Automated-Reasoning Revolution: From Theory to Practice and Back
Moshe Y. Vardi, Rice University, USA


Please note that our office will be closed on the following public holiday.

- 12 Sep 2016 (Hari Raya Haji)


Students and researchers who are interested in attending these activities are requested to complete the online registration form.

The following do not need to register:

  • Those invited to participate.




Organizing Committee · Visitors and Participants · Overview · Activities · Venue

Best viewed with IE 7 and above