Verification Holger Hermanns, Daniel Stan

News

About Project2

Written: 10.01.2019 16:00 Written 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



Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators