Jkind vs Kind2 and MBP

[anaisac]

Hi guys :)

I'm new to this whole world of mathematical simulators, so forgive me if my questions are kind of basic.

I have a set of requirements already mapped, If I do the simulation using Kind2 for a certain system the simulation passes with green lights, but if I simulate the exact system with the exact variables in JKind I get a conflict and the requirements are checked as being unrealizable - Ive checked and change the timeout and the trace length in the hope it was just a lack of resources but got the same result. Is it normal to find this kind of contradictions between the mathematical model checkers? Why can this happen?

Also, what is the advantage of adding the MBP simulation to the checkers?

[andreaskatis]

Hi @anaisac

I have a set of requirements already mapped, If I do the simulation using Kind2 for a certain system the simulation passes with green lights, but if I simulate the exact system with the exact variables in JKind I get a conflict and the requirements are checked as being unrealizable - Ive checked and change the timeout and the trace length in the hope it was just a lack of resources but got the same result. Is it normal to find this kind of contradictions between the mathematical model checkers? Why can this happen?

Thanks for opening this thread. In general, the Kind 2 and JKind engines should agree on the realizability checking result i.e. when Kind 2 determines a specification as realizable (respectively, unrealizable), JKind should also declare it as realizable (respectively, unrealizable). The only scenarios where they two may differ is due to either not being able to determine realizability within the provided timeout value.

With that being said, could you please let me know the version of Kind 2 that you are using? If it is version 2.2.0, then I would suggest downgrading to the previous one (version 2.1.1) and see if that fixes the discrepancy. I've noticed the discrepancy you've mentioned and have a fix in our internal repository, which will be made public soon.

If switching to 2.1.1 does not solve this, it would be helpful if you could provide me with a minimal example where you notice the discrepancy, and I will take a closer look.

Also, what is the advantage of adding the MBP simulation to the checkers?

The MBP versions of the Kind 2 / JKind engines are utilizing a procedure called Model Based Projection (hence the MBP acronym). This procedure overapproximates Quantifier Elimination (QE), on which the realizability checking algorithms in Kind 2 / JKind rely to perform the underlying analysis. Currently, the options are there mostly as fallback options in case neither of the standard engines are able to solve the problem within the provide timeout value. Most of the times though, the MBP variants tend to be inferior in performance, compared to the MBP-less options, where Z3's exact QE tactics are being used. Essentially, what I mean to say with this is that you most probably not need to use the MBP options for the majority of your experiments (we haven't so far, at least :) ).

If you are curious to read more about how MBP is used in the realizability checking algorithms, feel free to check out the following publication:

Katis, Andreas, Grigory Fedyukovich, Huajun Guo, Andrew Gacek, John Backes, Arie Gurfinkel, and Michael W. Whalen. "Validity-guided synthesis of reactive systems from assume-guarantee contracts." In Tools and Algorithms for the Construction and Analysis of Systems: 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II 24, pp. 176-193. Springer International Publishing, 2018.

If you have further questions, do let us know.

Best,

Andreas

[anaisac]

Hi @andreaskatis

Regarding question 1:
Currently I'm using the kind2 v2.2.0. I will follow your suggestion and downgrade it to v2.1.1. I will let you know if this solves my problem. In case it doesnt I can share more info and details of my data.

Regarding MBP:
That explanation made so much sense now! Thank you. After learning that, I'm pretty sure my project will not need the MBP variant :) I'm not planning of being able to come up with such a specific use case that the Kind2/Jkind are able to solve.

I will, however, check the publication but I'm not expecting to go that deep on my analysis.

Thank you,
Anaísa