21 Feb
2019
21 Feb
'19
10:54 a.m.
Hi Patrick,
On Wed, Feb 20, 2019 at 8:13 AM Halder, Patrick <patrick.halder(a)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
https://spot.lrde.epita.fr/ipynb/ltsmin-dve.html#Saving-Kripke-structures-t…
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)
1
>> k.new_edge(s2, s2)
2
>> 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
--BODY--
State: [0&1] 0 "0"
1
State: [0&!1] 1 "1"
1
--END--
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
https://spot.lrde.epita.fr/tut21.html#orgcaea215
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.
--
Alexandre