14 Oct
2014
14 Oct
'14
10:07 p.m.
Hi Amélie,
If you download the tarball for the last version of Spot, you can find
the list of LTL (and PSL) simplifications implemented in the file
doc/tl/tl.pdf
I hope this can inspire you to devise simplifications for ALTL.
My experience with simplifying LTL formulas is that the notion of
"simpler" for the human reader is not necessarily the same as
"simpler" for some particular algorithm (say, a translation to
automata): I have found some rewriting rules in the literature that,
while they shortened the formula, would cause larger automata to be
output (at least in the tableau construction I use). So you really
should check the effect of the simplification you implement.
2014-10-14 17:07 GMT+02:00 Amélie DAVID <adavid(a)ibisc.univ-evry.fr>fr>:
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
_______________________________________________
Spot mailing list
Spot(a)lrde.epita.fr
https://lists.lrde.epita.fr/listinfo/spot
--
Alexandre Duret-Lutz