In my project, there is one important step to automatically verify a timed automata with TCTL formulae. I briefly surveyed the tool UPPAAL that provides a GUI to construct a timed automata and to specify CTL formulae. However, I didn't find the api to invoke.

Is there any tools with api provided for verifying TCTL formulae over timed automata can be imported into my project? Such that I can automatically send the timed automata and the TCTL formulae to the tool and get the satisfaction result.

And, the tool UPPAAL can only verify a CTL subset of TCTL over a timed automata. On this constraint, if I want to verify a TCTL formula with interval constraint $\Phi$ (such as $\exists (\Phi_1 U^J \Phi_2)$), I have to extend each location $l$ of the automata with an extra clock $z$, and verify each state $l\{z:=0\}\models \exists (\Phi_1 U (z\in J \wedge \Phi_2))$. And I have to wrap a CTL detection algorithm for nested formulae. Is there any tool can directly verify TCTL formulae over a timed automata?

  • $\begingroup$ Note that requests for programming related stuff are generally offtopic here. I'll let the community decide in this case since the subject is so deeply CS that you are unlikely to get an answer from anyone but CS researchers. $\endgroup$ – Raphael Jan 15 '14 at 8:43
  • 1
    $\begingroup$ @Raphael I think this is perfectly on-topic. It's not a question about how to write a particular program but, essentially, a reference request. I don't think it's any different from asking if there are any papers dealing with a particular topic, for example. $\endgroup$ – David Richerby Jan 15 '14 at 9:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.