About
This extended monthlong reunion is for long-term participants from the program on the Theoretical Foundations of Computer Systems, held in the Spring 2021 semester.
The field of theoretical foundations of computer systems (TFCS) was intensively developed over the last three decades, yielding major improvements in model checking, synthesis, and game-theoretic analysis. A major challenge in the field is the need for computational scalability. The program aimed at bringing together leading researchers on these themes.
The program focused on the following aspects:
- New developments in logic: Logic is often used in TFCS as a specification formalism, describing in a formal and rigorous way the requirements that a system under design or under verification is expected to satisfy.
- New developments in automata: Automata are used in TFCS both as a modeling formalism (for example, transducers are used to model reactive systems) and as reasoning tools, as in the automata-theoretic approach to temporal model checking.
- Probabilistic modeling in the analysis of systems: Probabilistic methods are used in the modeling and analysis of systems that exhibit probabilistic behavior, from randomized algorithms to biological systems.
- The use of games and their equilibria: Games are used in TFCS both as an algorithmic construct (for example, in the usage of alternating automata in temporal model checking) and as a modeling construct (for example, in the design of reactive systems, it is convenient to consider the setting as a game between the system and its environment). Once multiagent systems are considered, equilibria enter in a natural way.
- Techniques for the analysis of cyber-physical systems: Many features of real systems (for example, time and energy usage) are quantitative, and to express these, one needs continuous, real-valued functions and suitable hybrid combinations of discrete and quantitative constructs.
