ltlsynt.org 4.03 KB
 Thibaud Michaud committed Sep 25, 2017 1 2 3 4 5 6 7 8 # -*- coding: utf-8 -*- #+TITLE: =ltlsynt= #+DESCRIPTION: Spot command-line tool for synthesizing AIGER circuits from LTL/PSL formulas. #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html * Basic usage  Maximilien Colange committed Jun 13, 2018 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 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:  Thibaud Michaud committed Sep 25, 2017 26 #+BEGIN_SRC sh :results verbatim :exports both  Maximilien Colange committed Jun 13, 2018 27 ltlsynt --ins=a,b --outs=c -f 'G (a & b <=> c)'  Thibaud Michaud committed Sep 25, 2017 28 29 30 31 32 #+END_SRC #+RESULTS: #+begin_example REALIZABLE  Maximilien Colange committed Jun 13, 2018 33 34 35 36 37 38 39 40 41 42 43 44 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 45 46 #+end_example  Maximilien Colange committed Jun 13, 2018 47 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 state, with two loops labelled by =a & b & c= and =(!a | !b) & !c=.  Thibaud Michaud committed Sep 25, 2017 52   Maximilien Colange committed Jun 13, 2018 53 54 55 56 57 58 59 60 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 61 62  #+BEGIN_SRC sh :results verbatim :exports both  Maximilien Colange committed Jun 13, 2018 63 ltlsynt --ins=a --outs=b -f 'F a'  Thibaud Michaud committed Sep 25, 2017 64 65 66 67 68 69 70 #+END_SRC #+RESULTS: #+begin_example UNREALIZABLE #+end_example  Maximilien Colange committed Jun 13, 2018 71 72 73 74 75 76 77 78 79  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 80 81 82 83 84 * 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 85 86 87 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 88 89  The following four steps show you how a TLSF specification called spec.tlsf can  Thibaud Michaud committed Sep 25, 2017 90 be synthesized using =syfco= and =ltlsynt=:  Thibaud Michaud committed Sep 25, 2017 91 92 93 94 95  #+BEGIN_SRC sh LTL=$(syfco FILE -f ltlxba -m fully) IN=$(syfco FILE -f ltlxba -m fully) OUT=$(syfco FILE -f ltlxba -m fully)  Maximilien Colange committed Jun 13, 2018 96 ltlsynt --formula="$LTL" --ins="$IN" --outs="$OUT"  Thibaud Michaud committed Sep 25, 2017 97 98 99 100 101 102 #+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 103 104 105 106 107 108 109 110 111 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.