Spot

spot@lrde.epita.fr

209 discussions

by Jonah Romero

Hello, I was just curious if there were any plans to support building Spot on windows? Or maybe any plans to use CMake in the future? If not, are there any suggestions for building on windows? Thanks, Jonah

1 year, 8 months

APT install of python3-spot requires python version <<3.10

by mgerber59＠gmail.com

Hi, I'm a master student at RWTH Aachen, and am using spot as part of my master thesis. Thank you very much for developing and providing this awesome tool! However, I noticed that when attempting to install python3-spot via `apt install`, it fails with: ``` The following packages have unmet dependencies: python3-spot : Depends: python3 (< 3.10) but 3.10.6-1~22.04 is to be installed E: Unable to correct problems, you have held broken packages. ``` Checking out the package index at https://www.lrde.epita.fr/repo/debian/stable/Packages (Cmd-F for `python3-spot_2.11.5.0-1`), I notice that the package indeed specifies `python3 >= 3.9, python3 << 3.10` as a dependency, making it so it can only be installed alongside Python 3.9. I don't know what this restriction is used for, and would greatly appreciate it if it can be removed. Thank you, Marcel

1 year, 9 months

Possible to allow for product_or without completing left/right automata

by Marcel Gerber

Hello, I notice that `product_or` necessarily runs `complete` on both input automata [see this line in spot/twaalgos/product.cc <https://gitlab.lre.epita.fr/spot/spot/-/blob/b487ff4190cdec4094154486bb8c04…>]. In contrast, this is not the case for the "normal" `product`. If my thinking is correct, this would not be necessary if both input automata are Büchi automata, correct? Because the union of two incomplete Büchi automata is an incomplete Büchi automaton again, and the product automaton construction applies as normal as far as I can tell. Would it be possible to allow for this, potentially by introducing another method or exposing the `product_aux` function (incl. from Python)? Right now, running `product_or`, even on small input automata, produces absolutely unwieldy automata that are impossible to interpret. This is mostly due to my use case, where I'm using letters of an alphabet more akin to a standard DFA model, and encoding a symbol of `a` into the preposition formula `a & !b & !c` etc. This works well with single automata and with intersections, but not with unions sadly. Your help would be very much appreciated, Marcel

1 year, 9 months

APT install of python3-spot requires python version <<3.10

by Marcel Gerber

Hi, I'm a master student at RWTH Aachen, and am using spot as part of my master thesis. Thank you very much for developing and providing this awesome tool! However, I noticed that when attempting to install python3-spot via `apt install`, it fails with: The following packages have unmet dependencies: python3-spot : Depends: python3 (< 3.10) but 3.10.6-1~22.04 is to be installed E: Unable to correct problems, you have held broken packages. Checking out the package index at https://www.lrde.epita.fr/repo/debian/stable/Packages (Cmd-F for `python3-spot_2.11.5.0-1`), I notice that the package indeed specifies `python3 >= 3.9, python3 << 3.10` as a dependency, making it so it can only be installed alongside Python 3.9. I don't know what this restriction is used for, and would greatly appreciate it if it can be removed. Thank you, Marcel

1 year, 9 months

Spot bus error

by Beutner, Raven

Dear spot team, I think I found a bug in spot. When I run % cat foo.hoa HOA: v1 States: 1 Start: 0 AP: 3 "l0" "l1" "l2" acc-name: generalized-Buchi 0 Acceptance: 0 t --BODY-- State: 0 [(0&1)] 0 [(2)] 0 [(!2)] 0 —-END-- %autfilt --small -S foo.hoa I get a bus error. It seems that options —small and -S are both necessary to reproduce the bug. Similarly, none of the transitions in the automaton can be removed. I am running spot version 2.11.4 on an MacBook Pro with M1 Pro CPU compiled with --disable-python. Given that this seems to be a “low-level” system error, it could very well be that it is an issue with my machine setup. In this case: Do you have any idea how to fix this? Thanks already for your help! All the best, Raven PS: The current download link for the most recent version of spot (https://spot.lre.epita.fr/install.html) claims to download version 2.11.4 but actually still points to version 2.11.3.

1 year, 9 months

Test suite for spot installation

by Fraca Santamaria, Estibaliz

Hi, I'm trying to install spot in my machine. I run make check and I got two errors (Fail : 2). I am just reporting it as it is asked. Please find test-suite.log attached. The installation did fail. I would like to ask if you know why did it fail and what could I do to install it. Thank you

1 year, 10 months

Mac OS Spot Library Installation

by Samuel Hongang Lam

Hello All, I am a PhD student that has been working on a project recently with a code base using the Spot library. The code was written on a Linux machine, but I have a MacBook running macOS. There seem to be some dependencies in the Spot library on glibc functions, such as strverscmp. I am inexperienced with setting up the libraries and such properly. Is there anywhere I can get help with setting up Spot to be able to access the features I need on a Mac? Any assistance would be greatly appreciated. Thank you! Sincerely, Samuel Lam

1 year, 11 months

Deadline Extension: On the Effectiveness of Temporal Logics on Finite Traces in AI

by Antonio Di Stasio

CALL FOR PAPERS "On the Effectiveness of Temporal Logics on Finite Traces in AI" Part of the AAAI 2023 Spring Symposium Series <https://aaai.org/Symposia/Spring/sss23.php> March 27-29, 2023, Hyatt Regency San Francisco Airport, CA, USA Website: https://ltlf-symposium.github.io/ Temporal logics, such as Linear Temporal Logic (LTL), are widely adopted as a logical specification language in Formal Methods. They are also getting increasing attention from the AI Community. In AI, however, there is often a need to interpret such logics over finite traces, rather than the traditional infinite-trace interpretation. This is evident, for instance, in works on Planning, Reinforcement Learning, and Business Process Management. An important computational feature of working with finite traces is that it allows one to use standard finite-state automata to model and reason, rather than the more complex omega-automata used for infinite traces. This is a great simplification that has already had a significant impact on many areas of AI and CS. This symposium aims to bring together researchers working with temporal logics on finite traces, in basic research and applications, in order to discuss current results and future directions, and to facilitate the emergence of teams working across different areas. Topics Topics of interest span the use of temporal logics over finite traces, including (but not limited to) the following areas: - AI Planning - Verification and Synthesis - Reinforcement Learning - Automated Reasoning - Knowledge Representation - Multi-Agent Systems - Robotics - Motion and Task Planning - Discrete-Event Control - Workflow Management - Conversational Systems - Automated Service Composition - Business Process Management - Fintech - Cyber Security - Human Computer Interaction - Natural Language Processing Submissions Submissions should have a single main author, who will be the speaker, and each speaker can have no more than one submission. Each submission must not exceed 2 pages, including references (in AAAI style), and may refer to joint work with other collaborators to be credited in the presentation. There will be no formal proceedings and we encourage submissions of work presented or submitted elsewhere (no copyright transfer is required, only permission to post the abstract on the workshop site). Submissions should be uploaded via the AAAI SSS-23 EasyChair site. <https://easychair.org/conferences/?conf=sss23> Important Dates - *February 6, 2023*: Paper submission deadline (AoE). - *February 11, 2023*: Author notification (AoE). - March 27-29: AAAI Spring Symposium Series. Invited Speakers - Rance Cleaveland <https://www.cs.umd.edu/people/wcleavel>, University of Maryland, USA - Giuseppe De Giacomo <https://www.diag.uniroma1.it//degiacom/>, University of Oxford & Sapienza University of Rome, Italy - Lydia Kavraki <https://www.cs.rice.edu/~kavraki/>, Rice University, Houston, TX, USA - Shiela A. Mcilraith <https://www.cs.toronto.edu/~sheila/>, University of Toronto, Canada - Marco Montali <https://www.unibz.it/it/faculties/computer-science/academic-staff/person/31…>, University of Bolzano, Italy - Kristin Y. Rozier <https://www.engineering.iastate.edu/people/profile/kyrozier/>, Iowa State University, USA - Ufuk Topcu <https://www.ae.utexas.edu/people/faculty/faculty-directory/topcu>, University of Texas at Austin, TX, USA - Moshe Vardi <https://www.cs.rice.edu/~vardi/>, Rice University, Houston, TX, USA Organizing Committee - Suguman Bansal <https://suguman.github.io/>, Co-Chair, Georgia Institute of Technology, suguman(a)gatech.edu - Antonio Di Stasio <https://antoniodistasio.github.io/>, Co-Chair, University of Oxford, antonio.distasio(a)cs.ox.ac.uk - Sasha Rubin <https://sasharubin.github.io/>, Co-Chair, University of Sydney, sasha.rubin(a)sydney.edu.au - Shufang Zhu <https://shufang-zhu.github.io/>, Co-Chair, Sapienza University of Rome, zhu(a)diag.uniroma1.it Format The symposium will be conducted in a hybrid style, in-presence and on Zoom. Website For more information, please see the symposium website: https://ltlf-symposium.github.io/

2 years

[CfP]-Second Call: On the Effectiveness of Temporal Logics on Finite Traces in AI

by Antonio Di Stasio

CALL FOR PAPERS "On the Effectiveness of Temporal Logics on Finite Traces in AI" Part of the AAAI 2023 Spring Symposium Series <https://aaai.org/Symposia/Spring/sss23.php> March 27-29, 2023, Hyatt Regency San Francisco Airport, CA, USA Website: https://ltlf-symposium.github.io/ Temporal logics, such as Linear Temporal Logic (LTL), are widely adopted as a logical specification language in Formal Methods. They are also getting increasing attention from the AI Community. In AI, however, there is often a need to interpret such logics over finite traces, rather than the traditional infinite-trace interpretation. This is evident, for instance, in works on Planning, Reinforcement Learning, and Business Process Management. An important computational feature of working with finite traces is that it allows one to use standard finite-state automata to model and reason, rather than the more complex omega-automata used for infinite traces. This is a great simplification that has already had a significant impact on many areas of AI and CS. This symposium aims to bring together researchers working with temporal logics on finite traces, in basic research and applications, in order to discuss current results and future directions, and to facilitate the emergence of teams working across different areas. Topics Topics of interest span the use of temporal logics over finite traces, including (but not limited to) the following areas: - AI Planning - Verification and Synthesis - Reinforcement Learning - Automated Reasoning - Knowledge Representation - Multi-Agent Systems - Robotics - Motion and Task Planning - Discrete-Event Control - Workflow Management - Conversational Systems - Automated Service Composition - Business Process Management - Fintech - Cyber Security - Human Computer Interaction - Natural Language Processing Submissions Submissions should have a single main author, who will be the speaker, and each speaker can have no more than one submission. Each submission must not exceed 2 pages, including references (in AAAI style), and may refer to joint work with other collaborators to be credited in the presentation. There will be no formal proceedings and we encourage submissions of work presented or submitted elsewhere (no copyright transfer is required, only permission to post the abstract on the workshop site). Submissions should be uploaded via the AAAI SSS-23 EasyChair site. <https://easychair.org/conferences/?conf=sss23> Important Dates - January 30, 2023: Paper submission deadline (AoE). - February 4, 2023: Author notification (AoE). - March 27-29: AAAI Spring Symposium Series. Invited Speakers - Rance Cleaveland <https://www.cs.umd.edu/people/wcleavel>, University of Maryland, USA - Giuseppe De Giacomo <https://www.diag.uniroma1.it//degiacom/>, University of Oxford & Sapienza University of Rome, Italy - Lydia Kavraki <https://www.cs.rice.edu/~kavraki/>, Rice University, Houston, TX, USA - Shiela A. Mcilraith <https://www.cs.toronto.edu/~sheila/>, University of Toronto, Canada - Marco Montali <https://www.unibz.it/it/faculties/computer-science/academic-staff/person/31…>, University of Bolzano, Italy - Kristin Y. Rozier <https://www.engineering.iastate.edu/people/profile/kyrozier/>, Iowa State University, USA - Ufuk Topcu <https://www.ae.utexas.edu/people/faculty/faculty-directory/topcu>, University of Texas at Austin, TX, USA - Moshe Vardi <https://www.cs.rice.edu/~vardi/>, Rice University, Houston, TX, USA Organizing Committee - Suguman Bansal <https://suguman.github.io/>, Co-Chair, Georgia Institute of Technology, suguman(a)seas.upenn.edu - Antonio Di Stasio <https://antoniodistasio.github.io/>, Co-Chair, University of Oxford, antonio.distasio(a)cs.ox.ac.uk - Sasha Rubin <https://sasharubin.github.io/>, Co-Chair, University of Sydney, sasha.rubin(a)sydney.edu.au - Shufang Zhu <https://shufang-zhu.github.io/>, Co-Chair, Sapienza University of Rome, zhu(a)diag.uniroma1.it Website For more information, please see the symposium website: https://ltlf-symposium.github.io/

2 years

Bug when checking for automata emptiness in print_hoa()

by Beutner, Raven

Dear spot Team, I think I have found a bug in the emptiness checker of spot. When I use the following automation: HOA: v1 States: 8 Start: 0 Start: 1 AP: 0 acc-name: generalized-Buchi 2 Acceptance: 2 Inf(0)&Inf(1) --BODY-- State: 0 {0} [(t)] 2 [(t)] 3 State: 1 {0} [(t)] 4 [(t)] 5 State: 2 {0} [(t)] 2 [(t)] 3 State: 3 {0} [(t)] 6 [(t)] 7 State: 4 {1} [(t)] 4 [(t)] 5 State: 5 {1} [(t)] 6 [(t)] 7 State: 6 [(t)] 6 [(t)] 7 State: 7 [(t)] 6 [(t)] 7 --END-- And invoke "autfilt --is-empty aut.hoa” (where aut.hoa contains the above automaton) I get the following error: autfilt: print_hoa(): automaton has transition-based acceptance despite prop_state_acc()==true This seems to be related to a similar bug that was fixed in version 2.7.1, so should (hopefully) be easy to fix. I used version 2.11.3 on a MacBook Pro with M1 Pro CPU. All the best, Raven

2 years, 1 month

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Spot