LTL Specification

[dnay]

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

1. 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 ))

[c.klo...@gmail.com]

Have a look at the temporal spec patterns:

https://matthewbdwyer.github.io/psp/

More specifically the LTL ones:

https://matthewbdwyer.github.io/psp/patterns/ltl.html

Universality, P is true :

Between Q and R []((Q & !R & <>R) -> (P U R))
After Q until R [](Q & !R -> (P W R))

In your case, P=Q=A, R=B, so:

A is true :

Between A and B []((A & !B & <>B) -> (A U B))
After A until B [](A & !B -> (A W B))

At least, that's what I've understood.

Best,
Christos