Personal tools
You are here: Home Graduate Study Decision procedures for infinite state systems

Decision procedures for infinite state systems

The aim is to extend techniques of model checking and equivalence checking from finite to infinite state systems.

Infinite state systems include pushdown automata, systems with data, systems with binding, and so on. There are many significant open  technical problems (such as: is equivalence of higher-order schema decidable?) and many open conceptual issues (such as: is there a good notion of tree automaton that can recognize families of higher-order terms?).

Prospective Supervisors


Colin Stirling

Document Actions