[Spot] Questions regarding handling of Kripke structures in Spot

Alexandre Duret-Lutz adl at lrde.epita.fr
Thu Feb 21 10:54:24 CET 2019

Hi Patrick,

On Wed, Feb 20, 2019 at 8:13 AM Halder, Patrick <patrick.halder at tum.de> wrote:
> my intention is to find all path in my automaton, that satisfy a LTL specification

there might be an infinite number of those

> 1. What is the most simple and fastest way of defining a spot kripke graph, based on my own automaton (which is basically just a dictionary with nodes, that hold certain attributes and parent/child relations) ? Is there a possibility of including my nodes and transitions step by step into a spot kripke graph or do I have to convert my automaton at first into e.g. the HOA format and afterwards import this HOA-string as a kripke graph?

You can represent a Kripke structure as a state-labeled ω-automaton
with "t" acceptance in the HOA format.  The result can be loaded as a
classical transition-based automaton (the twa_graph class of Spot), or
as an explicite Kripke structure (the kripke_graph).  See
for an example of the latter.  The major difference currently is just
memory consumption (label attached to transitions vs states), but the
semantics are similar.  Maybe in the future, some algorithms will take
advantage of the fact that Kripke structure are state-labeled, but
that isn't the case currently as far as I recall.

You can also build the kripke_graph yourself using an interface
similar to that of twa_graph for which you can see some example at
https://spot.lrde.epita.fr/tut22.html#orgc87539a the only difference
is that labels will be passed to new_state().

>>> import spot
>>> import buddy
>>> bdict = spot.make_bdd_dict()
>>> k = spot.make_kripke_graph(bdict)
>>> p1 = buddy.bdd_ithvar(k.register_ap("p1"))
>>> p2 = buddy.bdd_ithvar(k.register_ap("p2"))
>>> s1 = k.new_state(p1 & p2)
>>> s2 = k.new_state(p1 & -p2)
>>> k.new_edge(s1, s2)
>>> k.new_edge(s2, s2)
>>> print(k.to_str('HOA'))
HOA: v1
States: 2
Start: 0
AP: 2 "p1" "p2"
acc-name: all
Acceptance: 0 t
properties: state-labels explicit-labels state-acc deterministic
State: [0&1] 0 "0"
State: [0&!1] 1 "1"

The kripke_graph class is old, but its Python bindings were just
introduced in Spot 2.7.1 so you'll probably encounter some rough edges
(please report them so they can be fixed): for instance I discovered
that set_init_state() did not work because of some type issue (until
this is fixed, make sure the first state you create with new_state()
is the initial state).

> 2. Building the product of a LTL formula (resp. the Büchi automaton) with the kripke graph leads to a object of the class twa_product. Is there a possibility of transforming this product back into a kripke structure or exporting it as a simple dictionary, so that I can make further computations on this "reduced" graph?

otf_product(x, y) constructs a twa_product, i.e., a product automaton
that is built on-the-fly: use that for large product on which you just
want to do emptiness check.
product(x, y) construct a twa_graph, i.e., a product entirely built
and stored as a graph, this is probably what you want.

The product of a Büchi automaton and a Kripke structure is necessarily
a Büchi automaton; it's not clear to me what you mean by transforming
that into a Kripke structure or exporting it as a dictionary.

If you want to explore the product twa_graph and store it into a
different data structure, see
In the past someone asked how to convert the transition structure to a
Python dictionary with key of the form (state, letter), and the list
of possible destinations value.  See the attached script if this the
kind of thing you want.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: ba2dict.py
Type: text/x-python
Size: 1177 bytes
Desc: not available
URL: <http://lists.lrde.epita.fr/pipermail/spot/attachments/20190221/be6deee4/attachment.py>

More information about the Spot mailing list