Dear Patrick, (Please keep the mailing list in copy so that these explanations get archived and then indexed by search engines.) On Tue, Mar 5, 2019 at 8:58 AM Halder, Patrick <patrick.halder@tum.de> wrote:

When I have the twa_product automaton with its respective acceptance states, how can I find out, to which states of my original Kripke structure they correspond to. I read somewhere in the spot examples that the labeling of the twa_product states (of the form <*,*>) has just cosmetic reasons and does therefor not give any help.

Let's say you have built the product between two automata autx and auty: prod = spot.product(autx, auty) then pairs = prod.get_product_states() will return an array of pairs of the form [(x0,y0),(x1,y1),....]. State i in the product corresponds to states pairs[i][0] in autx, and pairs[i][1] in auty. See https://spot.lrde.epita.fr/ipynb/product.html around cell 10 for a concrete example, and a tip about using show("1") in this context.

Is it even possible to do this, meaning getting directly from the acc states of the product automaton to the acc states/runs of the Kripke structure?

You should probably look for the accepting SCCs of the product, not only its accepting states. You could list all states that belong to acceptings SCCs of the product with something like si = spot.scc_info(prod) n = si.scc_count() for i in range(n): if si.is_accepting_scc(i): for s in si.states_of(i): print(s) Unfortunately, we do not yet have any online example of use of scc_info in Python. You can find some in the test suite, or simply look at the C++ documentation for this class https://spot.lrde.epita.fr/doxygen/classspot_1_1scc__info.html

Or do I have to get the accepting runs of the product automaton, e.g., with the x.intersecting_run(y) method and reason with it about the accepting runs in the Kripke structure?

This will only return one accepting run. -- Alexandre Duret-Lutz