Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • Spot Spot
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 132
    • Issues 132
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • SpotSpot
  • SpotSpot
  • Issues
  • #51
Closed
Open
Issue created Jan 15, 2015 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()
Assignee
Assign to
Time tracking