www.cs.ox.ac.uk/teaching/studentprojects/258.html

You are here:

• Home
• Current Students
• Model Checking LTL on Markov Chains

Model Checking LTL on Markov Chains

Supervisor	James Worrell
Suitable for	Mathematics and Computer Science, Part C Computer Science, Part C Computer Science, Part B

Abstract

The aim of this project is to build a tool to compute the probability that an LTL formula satisfies a Markov chain. One of the main tasks in the project is to build a translator from LTL to unambiguous automata and to see to what extent state-of-the-art compression techniques, such as those used in the tool Wring, can be used in the setting of unambiguous automata.