Research
Reverse Engineering of RML Models with Machine Learning
An unsupervised pipeline that recovers the guarded commands of an RML (Reactive Modules Language) model, as used by PRISM, from observed state transitions, using DBSCAN and the Hough Transform to find each command and logistic regression to infer its guard.
The problem
PRISM is a probabilistic model checker. Its models are written in RML, the Reactive Modules Language: modules hold state variables, and guarded commands describe how the state changes. A command looks like [action] guard -> probability : update. The guard says when the command can fire; the update says how the variables change.
The goal: given only observed behaviour of a system (cyber-physical systems, in this project), reverse-engineer a readable RML model of it, so its behaviour can be explained and checked.
What I built
An unsupervised machine-learning pipeline in Python (scikit-learn, PyTorch), with custom graph-temporal features:
- Plot each observed transition as its start state against its end state. Transitions produced by the same command follow the same update rule, so they line up. For example,
x' = x + 1puts all its points on one straight line. - Find the commands: the Hough Transform detects those lines, and DBSCAN clusters the transitions into groups. Each group is one command with its update.
- Infer the guards: for each command, logistic regression learns the boundary between states where it fires and states where it doesn’t. PRISM guards are usually linear conditions on the state, so a linear boundary maps straight back to a guard.
The output is a set of guarded commands: an RML model that explains the observed behaviour.
Result
TODO: A result: for example, how many commands or guards were recovered correctly on a test model.
What I learned
TODO: One or two sentences in my own words.