[Spot] Questions regarding handling of Kripke structures in Spot

Halder, Patrick patrick.halder at tum.de
Tue Feb 19 11:27:06 CET 2019

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.lrde.epita.fr/pipermail/spot/attachments/20190219/7f06e96d/attachment.html>

More information about the Spot mailing list