News
About Project2
Written on 10.01.2019 16:00 by Daniel Stan
Dear students,
An important remark was reported by some of you: the persistence checking asks to give up the search as soon as a terminal state is found. This assumption is made in order to reject models that have terminal states.
In the next question, the product of a system with a NBA of a LTL formula may introduce new terminal states ! The NBA is indeed not assumed to be total, and some trace fragments may not have a corresponding run in the NBA. Please construct in this question a product system that doesn't introduce new terminal states.
This can be implemented in the following ways (non-exhaustive list):
* Make the NBA total, by adding a sink non-accepting state (you can add a [true] guard from each states to the sink, since the NBA doesn't have to be deterministic);
* Add a sink state to the product LTS, whenever no other successor has been produced.
I hope this extra specification clarifies the subject and makes the last question easier.
Best,
--
Daniel