Skip to content
GitLab
Open
Issue created by Alexandre Duret-Lutz@adlOwner4 of 7 checklist items completed4/7 checklist items

fusion-star support

This keep tracks of the support for the [:*i..j] operator. This is currently on branch adl/si-psl.

  • documentation of semantics, parsing, pretty-printing, trivial simplifications, translation
  • update ltl2tgba.html to mention the operator
  • non-trivial simplifications
  • is_syntactic_stutter_invariant() following Def.2 of Dax et al. (ATVA'09)
  • generalize remove_x() following function κ and τ in Dax et al. (ATVA'09) (bug this seems bogus, see comment below)
  • investigate why we need a bidirectional check in our implementation of is_stutter_invariant() using Etessami's rewriting, why Dax et al. (ATVA'09) claim that their τ function (based on the paper of Peled & Wilke) is an overapproximation, and therefore would need only one inclusion check. Is it the case that Etessami's function is also an overapproximation and we are doing to much work or is it the case that Etessami's is not an overapproximation?
  • generalize the syntactic version of is_stutter_invariant() to use stutterize_psl()