Projects suggested by Dr Nir Piterman
I am a research fellow in Imerial College and a visiting fellow in the computer lab.
Applying algorithms in Verification, Model Checking, Games, and Automata
jTLV (java Temporal Logic Verifier) is an eclipse plugin that allows
to conveniently implement in java algorithms that have to do with verification,
automata, games, and logic.
jTLV takes care of handling sets of states through BDDs and already includes
a few algorithms for model checking, game analysis, and synthesis
of designs from temporal specifications.
The idea in this project would be to extend jTLV's capabilities by adding to it more algorithms.
Possible applications include:
- Translation of Linear Temporal Logic to Automata -
this is a basic tool to be used in model checking of linear time properties.
A standard application for practically all major hardware manufacturers.
Interfacing jTLV with a SAT solver for bounded model checking.
Extending the game solving libraries of jTLV.
Add Mocha interface for jTLV.
Implement a pi-calculus/CCS/other converter into jTLV.
Create a jTLV-SPIN connection.
Manipulation of Finite Automata
In this project we suggest to implement algorithms that work on
The project is quite open to your own ideas and personal taste, with
a wide choice of extensions to the package that can be implemented.
A GUI for inputing these automata in graphical format
Interaction with graphical presentation tools
(like dotty or others of your choice).
Implementing different automata algorithms like: checking emptiness, checking universality, determinization, complementation, minimization, and so on.
Translation of MTL to Timed Automata
The idea in this project is to implement a recent algorithm for the conversion of Metric Temporal Logic formulas to timed automata.
Metric temporal logic is a linear time temporal logic.
It characterizes sets of timed sequences of events.
Timed automata are machines that manipulate clocks and accept the same kinds of sequences.
The translation from logic to machine is important for reasoning about the logic,
verification, and synthesis of timed controllers.
The project can also include a theoretical part that extends the construction
to handle past temporal operators.
The student will have to learn the concpets of the logic, timed automata, and implement
an automatic translation of MTL files to automata in one of the
packages Kronos or Upaal.