Questions regarding handling of Kripke structures in Spot
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
Hi Patrick, On Wed, Feb 20, 2019 at 8:13 AM Halder, Patrick <patrick.halder@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?
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
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-to... 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(). 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
participants (2)
-
Alexandre Duret-Lutz -
Halder, Patrick