This is one of the important topics in model checking and verification in the last 20 or so years. The topic has deep connections to complexity theory, graph algorithms, and automata. The key task is to design an algorithm that, given a game specification in a given graph with opposing pla

A finite automaton is a simplest model of computation. The goal in this project is to use finite automata to represent infinite algebraic structures. A good example is the algebraic structure consisting of integers with the addition operation. When the integers are represented in binary, y

Nowadays networks with millions and many billion nodes can easily be found. Examples include social networks, various biological networks, particle systems such as crystals. Understanding such large graphs is among the most challenging problems in many areas of computer science, mathematic

This is one of the key areas on modern computability and logic. What is a computable structure? What does it mean that two computable structures are similar? What does it mean for a graph or tree to be computable? These questions are hard and they have been addressed by famous experts in c