Hello,
My name is Dennis Park and I'm a student at the University of British
Columbia. I am using the Spot library in a research project I am currently
working on and I wanted to ask whether the Spot library supports negation
propagation.
More specifically, I would like to take an ltl formula
spot::ltl::formula* f
and propagate all negations in f so that negations only occur before atomic
propositions. Does the Spot library support such a functionality? If so,
where in the documentation could I find information on it (I tried to look
for something like it in the documentation but had trouble finding
anything).
Thank you,
Dennis Park
Bonjour,
Je suis en doctorat d'informatique à l'université d'Evry et je travaille
sur la logique ATL. Je viens de découvrir votre outil Spot et en
particulier l'outil de simplification des formules.
Je suis entrain de développer des méthodes de tableaux pour ATL, et je
souhaiterais également pouvoir simplifier les formules fournies en
entrée de l'outil. J'aurais donc voulu savoir s'il existait une
référence dans la littérature ou une compilation de l'ensemble (ou en
tout cas la majorité) de ces simplifications. J'ai beau chercher depuis
un petit moment et je n'ai rien trouvé à l'exception de votre outil Spot.
Merci d'avance pour l'aide que vous pourriez m'apporter concernant cette
question.
Bien cordialement,
Amélie DAVID