Specification Synthesis for Deontic Input-Output Automata

This page contains supplementary material to our paper:
The following zipped file contains a version of LTSA extended to perform specfication synthesis over deontic IO LTS.

Unizipping the file generates a folder containing the following files:

There's no user manual. The above examples show the new LTSA commands to use to generate the weakest deontic IO LTS realising a goal in a domain as described in the paper. Use of our extension assumes familiarity with LTSA.

Contact us if you have any question: e.letier@ucl.ac.uk


LTSA is a tool developed by Jeff Kramer and Jeff Magee's group at Imperial College London. The standard version of the tool is available here.