19 Feb
2019
19 Feb
'19
11:27 a.m.
Dear Spot Team,
I'm a master's student at Technical University of Munich and I'm currently
writing my Master's Thesis in the research field of path planning for autonomous
cars.
I came across Spot on the internet and I think it's a very nice tool that fits exactly
my needs: I've got a discrete finite automaton (with certain attributes/APs per node)
and I want to check, if this automaton satisfies a certain LTL specification. Especially,
my intention is to find all path in my automaton, that satisfy a LTL specification.
I've already installed Spot on my computer and tried to implement this with Python.
Now I've got the following two questions:
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?
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?
I hope you can help me with my questions and maybe provide some simple code examples.
Thank you very much in advance!
Yours sincerely,
Patrick Halder
21 Feb
21 Feb
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
2327
days inactive
2329
days old
1 comments
2 participants
participants (2)
-
Alexandre Duret-Lutz -
Halder, Patrick