ltlsynt.org 4.02 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
6
7
8
#+HTML_LINK_UP: tools.html

* Basic usage

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

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

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=.
52

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

#+BEGIN_SRC sh :results verbatim :exports both
63
ltlsynt --ins=a --outs=b -f 'F a'
Thibaud Michaud's avatar
Thibaud Michaud committed
64
65
66
67
68
69
70
#+END_SRC

#+RESULTS:
#+begin_example
UNREALIZABLE
#+end_example

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

The following four steps show you how a TLSF specification called spec.tlsf can
90
be synthesized using =syfco= and =ltlsynt=:
Thibaud Michaud's avatar
Thibaud Michaud committed
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)
96
ltlsynt --formula="$LTL" --ins="$IN" --outs="$OUT"
Thibaud Michaud's avatar
Thibaud Michaud committed
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
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.