Use Spot for timed automata verification
Spot currently only handles finite systems. Supporting timed systems would be a nice extension. The easiest way to do this is through the integration of a tool that manipulates timed systems. TChecker is such a tool.
In short, TChecker reads timed automata and builds a semantically equivalent finite graph, called a zone graph. A first task is to present such zone graphs as twa to Spot, so that we could use the emptiness checks available in Spot directly. There are in fact several ways to build a zone graph, so this interface should be able to handle the various zone graphs that TChecker is able to produce (see the file semantics/zg.[hh,cc] in TChecker).
Conversely, TChecker has no idea about LTL and omega-automata in general, it just manipulates Büchi timed automata. Another task is thus to use Spot inside TChecker, to parse a LTL/PSL formula to check on a timed automaton, build a corresponding Büchi automaton for the formula and synchronize it (using TChecker synchronized product) with the timed automaton read by TChecker.
Those two tasks are a priori independent one from the other, they could be implemented in any order.
EDIT: The type of files used by TChecker is XML produced by Uppaal. This program gives also the access to a parser library called libutap which is under the LGPL license. An adaptation of this parser is needed in Spot to handle these files.