0
$\begingroup$

Imagine that we are designing a system in which we have the action to brake or not brake. How can we write an LTL specification that guarantees that we cannot switch between braking and not braking within three time steps?

$\endgroup$

1 Answer 1

1
$\begingroup$

You can simply require that whenever there is a switch (i.e., the braking status changed from one to another), the status will not change for the next three steps. Technically, let $b$ denote the propositions that brake is on, then we have the following: $$G((\neg b\wedge Xb)\to (XXb\wedge XXXb) )\wedge G((b\wedge X\neg b)\to (XX\neg b\wedge XXX\neg b) )$$ Note that you can put the two conditions inside one $G$ operator. I just find this way easier to read.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.