- Spot - LRE

Test suite for spot installation
by Fraca Santamaria, Estibaliz 21 Mar '23

21 Mar '23

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

2 2

Mac OS Spot Library Installation
by Samuel Hongang Lam 10 Mar '23

10 Mar '23

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

2 1

Deadline Extension: On the Effectiveness of Temporal Logics on Finite Traces in AI
by Antonio Di Stasio 30 Jan '23

30 Jan '23

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/

1 0

[CfP]-Second Call: On the Effectiveness of Temporal Logics on Finite Traces in AI
by Antonio Di Stasio 20 Jan '23

20 Jan '23

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/

1 0

Bug when checking for automata emptiness in print_hoa()
by Beutner, Raven 04 Jan '23

04 Jan '23

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 1

[CfP]: On the Effectiveness of Temporal Logics on Finite Traces in AI
by Antonio Di Stasio 24 Dec '22

24 Dec '22

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, Sapienza University of Rome, distasio(a)diag.uniroma1.it - 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/

1 0

Generating unsatisfiable LTL formulae using randltl
by Pert, Charles 12 Dec '22

12 Dec '22

Hi, I am specifically trying to generate unsatisfiable LTL formulae using the randltl tool in Spot. I am struggling because the default tool is so much more likely to produce consistent and satisfiable formulae. Have you got any tips on how I can alter the generation to produce these types of formulae? Best wishes, Charles Pert

2 1

Bug report: implication prefix
by Liu, Jason Xinyu 30 Nov '22

30 Nov '22

Hello, It seems that Spot cannot parse implication and equivalent operators in prefix order. I tried on both my local machine and the online translator <https://spot.lre.epita.fr/app/>. The installed Spot version is 2.11.1. The commands are - local: spot.formula("-> a b") - online translator: type in -> a b Error message: syntax error, unexpected implication operator Thank you very much for your help and creating the conda package for Spot, that makes the installation very convenient! Happy holidays! Best, Jason

2 2

[bug] ltl2tgba gets stuck with this formula
by Jacopo Binchi 31 Oct '22

31 Oct '22

Dear Spot support team, I am a researcher at Developair Technologies. I write you looking for help with a formula that ltl2tgba cannot handle, possibly a bug. Here at Developair we have been using Spot for the past few months with great satisfaction. However, it seems that *ltl2tgba *cannot process the formula in attached file gb_formula.ltl . We let it run for quite some time (like hours) and it didn't terminate. On the other hand, Owl can process the same formula in a matter of a few milliseconds. We don't have any problem using ltl2tgba with other, similar formulas. It seems strange to us that Spot gets stuck with such a relatively simple formula, especially since in our experience Spot worked reliably well with other, way more complex formulas. Is it maybe a bug or something that we are doing wrong? Could you please help us? Please find some more details (version and command) below. Thank you. Best regards, J. Spot version: ltl2tgba --version > ltl2tgba (spot) 2.10.6 > > Copyright (C) 2022 Laboratoire de Recherche et Développement de l'Epita. > License GPLv3+: GNU GPL version 3 or later < > http://gnu.org/licenses/gpl.html>. > This is free software: you are free to change and redistribute it. > There is NO WARRANTY, to the extent permitted by law. > Command: ltl2tgba -S --deterministic --dot=s --output=output.txt -F gb_formula.ltl Using the "simplest" command "ltl2tgba -F gb_formula.ltl" produces the same result (that is, no result). For comparison, with Owl we used command: owl ltl2ldgba --state-acceptance -i gb_formula.ltl -o owl_gb.txt -- Jacopo Binchi jbinchi(a)developair.es Paseo de Miramón 170 20014 San Sebastián – Donostia Gipuzkoa (Spain) www.developair.es

2 2

Number of states and transitions
by pierreganty＠gmail.com 28 Oct '22

28 Oct '22

Hi all, I did not find how to get the number of states (reachable or not) of an automaton using autfilt (in particular the `--stats` option). The option provided by `autfilt --stats` is for reachable states only. I did find a workaround with `--hoaf` which outputs the automaton in HOA format and then getting the number from the `States:` header. For the number of transitions (reachable or not) I don't have a workaround. Since spot can compute these numbers easily, it seems handy (at least for me) to have a direct access to them thru the `--stats` interface. Thank you, Pierre.

3 3