Projects suggested by Dr Nir Piterman

I am a research fellow in Imerial College and a visiting fellow in the computer lab. My homepage

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. See jTLV hompeage.

The idea in this project would be to extend jTLV's capabilities by adding to it more algorithms. Possible applications include:

  1. 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.
  2. Interfacing jTLV with a SAT solver for bounded model checking.
  3. Extending the game solving libraries of jTLV.
  4. Add Mocha interface for jTLV.
  5. Implement a pi-calculus/CCS/other converter into jTLV.
  6. Create a jTLV-SPIN connection.

Manipulation of Finite Automata

In this project we suggest to implement algorithms that work on finite automata. 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. For example:
  1. A GUI for inputing these automata in graphical format
  2. Interaction with graphical presentation tools (like dotty or others of your choice).
  3. 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.