search

fmrchallenge / fmrbenchmark

benchmark problems for research in formal methods for robotics
http://docs.fmrchallenge.org
Other
14 stars 3 forks source link

evaluation framework for integrator chains domain #4

Open vraman opened 8 years ago

vraman commented 8 years ago

Create a script that parses an LTL formula into a Buchi or Rabin automaton and checks that an input string satisfies the specification. Should interface with the trial data from tdstat.py. The script should take as input a time duration for the trial and output success or failure based on appropriately defined acceptance criterion where not obvious (e.g. for liveness properties).

slivingston commented 8 years ago

Note that the integrator_chains domain uses only LTL formulae that can be expressed through two basic reach-avoid templates. As such, we could use a task specification syntax that is accordingly restricted and thus avoid the need for Rabin automaton construction.

slivingston commented 8 years ago

@vraman What do you think about my recommendation of using a restricted syntax? It could be used for an initial implementation and be supplemented or replaced by a design involving Büchi or Rabin automata later.

vraman commented 8 years ago

I agree with the suggestion of using a restricted syntax for an initial implementation.