ltlsynt.org 4.26 KB
Newer Older
Thibaud Michaud's avatar
Thibaud Michaud committed
1
2
3
# -*- coding: utf-8 -*-
#+TITLE: =ltlsynt=
#+DESCRIPTION: Spot command-line tool for synthesizing AIGER circuits from LTL/PSL formulas.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
4
#+INCLUDE: setup.org
Thibaud Michaud's avatar
Thibaud Michaud committed
5
#+HTML_LINK_UP: tools.html
6
#+PROPERTY: header-args:sh :results verbatim :exports both
Thibaud Michaud's avatar
Thibaud Michaud committed
7
8
9

* Basic usage

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:
27
#+BEGIN_SRC sh
28
ltlsynt --ins=a,b --outs=c -f 'G (a & b <=> c)'
29
30
31
32
33
#+END_SRC

#+RESULTS:
#+begin_example
REALIZABLE
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--
46
47
#+end_example

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
52
  state, with two loops labeled by =a & b & c= and =(!a | !b) & !c=.
53

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's avatar
Thibaud Michaud committed
62

63
#+BEGIN_SRC sh :epilogue true
64
ltlsynt --ins=a --outs=b -f 'F a'
Thibaud Michaud's avatar
Thibaud Michaud committed
65
66
67
#+END_SRC

#+RESULTS:
68
: UNREALIZABLE
Thibaud Michaud's avatar
Thibaud Michaud committed
69

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's avatar
Thibaud Michaud committed
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.
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's avatar
Thibaud Michaud committed
87

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
88
The following four steps show you how a TLSF specification called =FILE= can
89
be synthesized using =syfco= and =ltlsynt=:
Thibaud Michaud's avatar
Thibaud Michaud committed
90

91
#+BEGIN_SRC sh :export code
Thibaud Michaud's avatar
Thibaud Michaud committed
92
LTL=$(syfco FILE -f ltlxba -m fully)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
93
94
IN=$(syfco FILE --print-input-signals)
OUT=$(syfco FILE --print-output-signals)
95
ltlsynt --formula="$LTL" --ins="$IN" --outs="$OUT"
Thibaud Michaud's avatar
Thibaud Michaud committed
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
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.
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