Dnay Posted May 18 Share Posted May 18 Hello, 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 More sharing options...

## Recommended Posts

## 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