Jump to content

LTL Specification

Recommended Posts


I´m trying to formalize some specification for defined problem using Linear temporal logic and i dont know why it is still not realizable. i´ve already performed so much modification but i dont get a good result.

I put here the 3 different way i´ve already tried

Once A is raised, it must remain high until A && B

G(F( A -> (A U (A && B))) && (G (A && B) -> (X(!A && !B))))

G(F( A -> (A U B)))

arvalid starts as false: !arvalid

arvalid becomes true, it remains true until B becomes true: G((A -> F B)

While arvalid is true arready is false until B becomes true:G (A -> !B U B)

After arready BECOMES TRUE arvalid becomes false: G ( B -> X !A ))

Combined LTL Formula

!A ∧ G((A -> F B) ∧ (A -> !B U B) ∧( B -> X !A ))

I put here the 3 different way i´ve already tried

Link to comment
Share on other sites

Create an account or sign in to comment

You need to be a member in order to leave a comment

Create an account

Sign up for a new account in our community. It's easy!

Register a new account

Sign in

Already have an account? Sign in here.

Sign In Now
  • Create New...