Dissertation: Robust Probabilistic Bisimilarity

• Investigated the continuity of the probabilistic bisimilarity distance (provides a quantitative measure of behavioural difference) under small perturbations of transition probabilities.
• Introduced robust probabilistic bisimilarity for labelled Markov chains which ensures the continuity of the bisimilarity distance for bisimilar pairs of states.
• Designed an efficient algorithm to compute robust probabilistic bisimilarity and validated its practical performance via experiments.
• Defined the notions of robust probabilistic bisimilarity distance and proximity, which, loosely speaking, provide an upper bound on the probabilistic bisimilarity distance when the transition probabilities are slightly perturbed.
• Developed polynomial-time and policy-iteration-based algorithms to compute the proximity.

Thesis: Probabilistic Model Checking of Randomized Java Code (slides)

• Developed jpf-label, an extension for the model checker Java PathFinder (JPF), leveraging Java bytecode to enable users to label states in the Markov chains extracted from Java programs.
• Implemented a converter which leads to the first model checking tool that can check probabilistic properties randomized algorithms written in Java via integration with the probabilistic model checker PRISM.
• Implemented three established algorithms for probabilistic bisimilarity to minimize the state space of labelled Markov chains and mitigate state-space explosion.
• Boosted the performance of these algorithms by improving frequently executed code, and benchmarked their runtime and memory consumption against PRISM's default algorithm.

Distributed Computing, Concurrency and Verification Group

• Curated a large collection of realistic instances of probabilistic models and implemented randomized algorithms in Java.
• Assessed the impact of parameters on the properties of a Markov chain.

Award: Third Place Poster Presentation at the Lassonde Summer Student Research Conference

Molecular Communication and Information Theory Laboratory

• Implemented steady-state probability distributions and entropy calculations in Python to determine the mutual information between the number of RNA molecules produced by a two-state promoter and the promoter concentration.

Integrated Circuits and Systems Laboratory

• Created the backend of a wireless EEG headband; optimized for low weight, compact form factor, and power efficiency to improve patient comfort and battery life.
• Designed and tested a PCB in Altium Designer for electrophysiological signal acquisition.
• Wrote software in Verilog to decode and organise recorded signals on an FPGA.
• Developed C firmware to transmit processed data via bluetooth (BLE 5.0) to a base station that provides diagnostic algorithms.

Award: Students' Choice at the Lassonde Summer Student Research Conference