First, I will talk about Defender’s Forcing, a technique introduced by Jancar and Srba that is used for proving lower bounds in bisimilarity checking of infinite state systems, i.e. the problem, given two infinite state systems, to decide whether they are bisimilar. I plan to apply this simple but powerful technique to some classes of infinite state systems for which simple representations exist, such as for prefix-recognisable graphs, Petri Nets or PA processes.

Second, I will recall two classical results from complexity theory (i) PSPACE is serializable meaning roughly that for determining whether a word lies in a fixed PSPACE language one only needs to check if the yield (the leaf string) of the computation tree of an NP machine lies in a fixed regular language (ii) Converting a natural number in binary to its Chinese remainder representation is in NCˆ1. I plan to use these results for proving lower bounds for reachability problems and model checking problems for one-counter automata and timed automata, respectively.