ltlsynt.org 4.26 KB
Newer Older
 Thibaud Michaud committed Sep 25, 2017 1 2 3 # -*- coding: utf-8 -*- #+TITLE: =ltlsynt= #+DESCRIPTION: Spot command-line tool for synthesizing AIGER circuits from LTL/PSL formulas.  Alexandre Duret-Lutz committed Jun 27, 2018 4 #+INCLUDE: setup.org  Thibaud Michaud committed Sep 25, 2017 5 #+HTML_LINK_UP: tools.html  Alexandre Duret-Lutz committed Apr 17, 2019 6 #+PROPERTY: header-args:sh :results verbatim :exports both  Thibaud Michaud committed Sep 25, 2017 7 8 9  * Basic usage  Maximilien Colange committed Jun 13, 2018 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 This tool synthesizes controllers from LTL/PSL formulas. Consider a set $I$ of /input/ atomic propositions, a set $O$ of output atomic propositions, and a PSL formula \phi over the propositions in $I \cup O$. A =controller= realizing \phi is a function $c: 2^{I \cup O} \times 2^I \mapsto 2^O$ such that, for every \omega-word $(u_i)_{i \in N} \in (2^I)^\omega$ over the input propositions, the word $(u_i \cup c(u_0 \dots u_{i-1}, u_i))_{i \in N}$ satisfies \phi. =ltlsynt= has three mandatory options: - =--ins=: a comma-separated list of input atomic propositions; - =--outs=: a comma-separated list of output atomic propositions; - =--formula= or =--file=: a LTL/PSL specification. The following example illustrates the synthesis of a controller acting as an =AND= gate. We have two inputs =a= and =b= and one output =c=, and we want =c= to always be the =AND= of the two inputs:  Alexandre Duret-Lutz committed Apr 17, 2019 27 #+BEGIN_SRC sh  Maximilien Colange committed Jun 13, 2018 28 ltlsynt --ins=a,b --outs=c -f 'G (a & b <=> c)'  Thibaud Michaud committed Sep 25, 2017 29 30 31 32 33 #+END_SRC #+RESULTS: #+begin_example REALIZABLE  Maximilien Colange committed Jun 13, 2018 34 35 36 37 38 39 40 41 42 43 44 45 HOA: v1 States: 1 Start: 0 AP: 3 "b" "c" "a" acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic --BODY-- State: 0 [0&1&2] 0 [!0&!1 | !1&!2] 0 --END--  Thibaud Michaud committed Sep 25, 2017 46 47 #+end_example  Maximilien Colange committed Jun 13, 2018 48 49 50 51 The output is composed of two parts: - the first one is a single line REALIZABLE or UNREALIZABLE; - the second one is an automaton describing the controller (if the input specification is realizable). In this example, the controller has a single  Alexandre Duret-Lutz committed Jul 21, 2020 52  state, with two loops labeled by =a & b & c= and =(!a | !b) & !c=.  Thibaud Michaud committed Sep 25, 2017 53   Maximilien Colange committed Jun 13, 2018 54 55 56 57 58 59 60 61 If a controller exists, then one with finite memory exists. Such controllers are easily represented as automata (or more specifically as I/O automata or transducers). In the automaton representing the controller, the acceptance condition is irrelevant and trivially true. The following example illustrates the case of an unrealizable specification. As =a= is an input proposition, there is no way to guarantee that it will eventually hold.  Thibaud Michaud committed Sep 25, 2017 62   Alexandre Duret-Lutz committed Apr 17, 2019 63 #+BEGIN_SRC sh :epilogue true  Maximilien Colange committed Jun 13, 2018 64 ltlsynt --ins=a --outs=b -f 'F a'  Thibaud Michaud committed Sep 25, 2017 65 66 67 #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Apr 17, 2019 68 : UNREALIZABLE  Thibaud Michaud committed Sep 25, 2017 69   Maximilien Colange committed Jun 13, 2018 70 71 72 73 74 75 76 77 78  By default, the controller is output in HOA format, but it can be output as an [[http://fmv.jku.at/aiger/][AIGER]] circuit thanks to the =--aiger= flag. This is the output format required for the [[http://syntcomp.org/][SYNTCOMP]] competition. The generation of a controller can be disabled with the flag =--realizability=. In this case, =ltlsynt= output is limited to REALIZABLE or UNREALIZABLE.  Thibaud Michaud committed Sep 25, 2017 79 80 81 82 83 * TLSF =ltlsynt= was made with the [[http://syntcomp.org/][SYNTCOMP]] competition in mind, and more specifically the TLSF track of this competition. TLSF is a high-level specification language created for the purpose of this competition.  Maximilien Colange committed Jun 13, 2018 84 85 86 Fortunately, the SYNTCOMP organizers also provide a tool called [[https://github.com/reactive-systems/syfco][=syfco=]] which can translate a TLSF specification to an LTL formula.  Thibaud Michaud committed Sep 25, 2017 87   Alexandre Duret-Lutz committed Jun 18, 2019 88 The following four steps show you how a TLSF specification called =FILE= can  Thibaud Michaud committed Sep 25, 2017 89 be synthesized using =syfco= and =ltlsynt=:  Thibaud Michaud committed Sep 25, 2017 90   Alexandre Duret-Lutz committed Apr 17, 2019 91 #+BEGIN_SRC sh :export code  Thibaud Michaud committed Sep 25, 2017 92 LTL=$(syfco FILE -f ltlxba -m fully)  Alexandre Duret-Lutz committed Jun 18, 2019 93 94 IN=$(syfco FILE --print-input-signals) OUT=$(syfco FILE --print-output-signals)  Maximilien Colange committed Jun 13, 2018 95 ltlsynt --formula="$LTL" --ins="$IN" --outs="$OUT"  Thibaud Michaud committed Sep 25, 2017 96 97 98 99 100 101 #+END_SRC * Algorithm The tool reduces the synthesis problem to a parity game, and solves the parity game using Zielonka's recursive algorithm. The full reduction from LTL to  Maximilien Colange committed Jun 13, 2018 102 103 104 105 106 107 108 109 parity game is described in the following paper: - *Reactive Synthesis from LTL Specification with Spot*, /Thibaud Michaud/, /Maximilien Colange/. In Proc. of SYNT@CAV'18. to appear. You can also ask =ltlsynt= to print to obtained parity game into [[https://github.com/tcsprojects/pgsolver][PGSolver]] format, with the flag =--print-pg=. Note that this flag deactivates the resolution of the parity game, which is to be deferred to one of the solvers from PGSolver.  Alexandre Duret-Lutz committed Jul 21, 2020 110 111 112 113 114  # LocalWords: utf ltlsynt AIGER html args mapsto SRC acc aiger TLSF # LocalWords: UNREALIZABLE unrealizable SYNTCOMP realizability Proc # LocalWords: syfco ltlxba Zielonka's Thibaud Michaud Maximilien # LocalWords: Colange PGSolver