Reactive Synthesis: Towards Output-Sensitive Algorithms
Bernd Finkbeiner Felix Klein


              

    


Reactive Synthesis




B. Finkbeiner, F. Klein
Universität des Saarlandes


  Reactive synthesis is a technology for the automatic construction
  of reactive systems from logical specifications.
  In these lecture notes, we study different
  algorithms for the reactive synthesis problem of linear-time
  temporal logic (LTL).  The classic game-based synthesis algorithm is
  input-sensitive in the sense that its performance is asymptotically
  optimal in the size of the specification, but it produces
  implementations that may be larger than necessary.  We contrast this
  algorithm with output-sensitive algorithms for reactive synthesis,
  i.e., algorithms that are optimized towards the size or structural
  complexity of the synthesized system. We study the bounded synthesis
  algorithm, which produces an implementation with a minimal number of
  states, and the bounded cycle synthesis algorithm, which
  additionally guarantees that the number of cycles of the
  implementation is minimal.
 


reactive systemssynthesistemporal logicoutput-sensitive algorithms



empty
empty



§ INTRODUCTION


Hardware circuits, communication protocols, and embedded controllers
are typical examples of reactive systems <cit.>, i.e., computer
systems that maintain a continuous interaction with their
environment. Reactive systems play a crucial role in many applications
in transport systems, building technology, energy management, health
care, infrastructure, and environmental protection.  Designing
reactive systems is difficult, because one needs to anticipate every possible behavior of the environment and prepare an appropriate response.

Synthesis is a technology that constructs reactive systems 
automatically from a
logical specification: that is, after the specification of the system is complete, no
further manual implementation steps are necessary. The developer focuses on “what”
the system should do instead of “how” it should be done. Because
synthesis analyzes objectives, not implementations, it can be applied
at an early design stage, long before the system has been
implemented. The vision is that a designer analyzes the design
objectives with a synthesis tool, automatically identifies competing
or contradictory requirements and obtains an error-free prototype
implementation. Coding and testing, the most expensive stages of
development, are eliminated from the development process.

The automatic synthesis of implementations from specifications is one
of the grand challenges of computer science. Its pursuit dates back at
least to Alonzo Church <cit.> and has ignited
research on many fundamental topics, notably on the connection between
logics and automata, on algorithmic solutions of infinite games over
finite graphs <cit.>, and on the theory of automata over
infinite objects <cit.>. It is only in the
last decade, however, that the theoretical ideas have been translated
into practical tools (cf. <cit.>).
The tools have made it possible to tackle real-world design problems, such as the synthesis of an arbiter for the  AMBA AHB bus, an open industrial standard for the on-chip communication and management of functional blocks in system-on-a-chip (SoC) designs <cit.>.

A common argument against synthesis is its complexity. It is natural to compare synthesis with the verification problem, where the implementation is already given, and
one needs to check whether the specification is satisfied.  For both
synthesis and verification, the most commonly used specification
language is linear-time temporal logic (LTL).  Measured in the size of
an LTL specification, the synthesis of a single-process finite-state
machine is 2EXPTIME-complete, while the corresponding verification
problem is in PSPACE.







But is this
comparison between verification and synthesis fair? The high
complexity of synthesis is due to the fact that there exist small
LTL formulas that can only be realized by very large implementations. 







As a result, synthesis
“looks” much more expensive than verification, because the size of the implementation is an explicit
parameter in the complexity of verification, and left implicit in the
complexity of synthesis.





This paper gives an introduction to a new class of synthesis algorithms, whose
performance is measured not only in the size of the specification, i.e., the
input to the synthesis algorithm, but also in the size and complexity of
the implementation, i.e., the output of the synthesis algorithm. Such
algorithms are called output sensitive.
The prototypical output-sensitive synthesis approach is bounded synthesis.
In bounded synthesis, we look for an implementation where the number of states
is limited by a given bound. By incrementally increasing the bound, bounded
synthesis can be used to find a minimal implementation.

We first describe the classic game-theoretic approach
to synthesis in Section <ref>, and then the bounded synthesis
approach in Section <ref>.
The two approaches differ fundamentally. The game-based approach is to translate the given LTL formula
into an equivalent deterministic automaton, and then use the state
space of the deterministic automaton to define a two-player game.
In this game, the “output player” sets the outputs of the system
and attempts to satisfy the specification, i.e., ensures that the
resulting play is accepted by the automaton, and the “input player”
sets the inputs and attempts to ensure that the play violates the
specification, i.e., is rejected by the automaton.
This game can be solved automatically, and a winning strategy for
the output player can, if it exits, be translated into an
implementation that is guaranteed to satisfy the specification.
Unfortunately, the translation from LTL to deterministic automata
is doubly exponential, which results in the 2EXPTIME complexity.
In bounded synthesis, the LTL formula is not translated to a
deterministic automaton; instead, its negation is translated to a nondeterministic automaton.
This translation is single, rather than double exponential.
The nondeterministic automaton suffices to check if a given
implementation is correct: the implementation is correct if its
product with the automaton does not contain an accepting path. In bounded synthesis, we “guess”
an implementation of bounded size and make sure it is correct. This is
done via propositional constraint solving: we build a constraint system
that is satisfiable if and only if an implementation that is correct with
respect to the automaton.













The reduction of the synthesis problem to a constraint solving problem
opens the possibility to add further constraints in order to focus the
search towards the most desirable solutions.  In
Section <ref>, we describe such an
extension: bounded cycle synthesis.  In addition to the number of
states, bounded cycle synthesis also bounds the number of cycles in
the implementation. This leads to implementations that are not only
small but also structurally simple.




§ THE SYNTHESIS PROBLEM


In reactive synthesis, we transform a temporal specification into an implementation that is guaranteed to satisfy the specification for all possible inputs of the environment. In the following, we consider formulas of linear-time temporal logic (LTL) over a set of atomic propositions = I ∪̇O that is partitioned into a set of inputs I and a set of outputs O.
A trace t is an infinite sequence over subsets of the atomic propositions. We define the set of traces 𝑇𝑅 (2^𝐴𝑃)^ω.
An LTL formula describes a subset of 𝑇𝑅. The idea is that in each step of a computation, the inputs are chosen by the environment, and the outputs are chosen by the system under construction. In a correctly synthesized system, all possible sequences satisfy the LTL formula.



  
Linear-time temporal logic (LTL).


Linear-time temporal logic (LTL) <cit.> combines the usual Boolean connectives with temporal modalities such as the Next operator  and the Until operator . The syntax of LTL is given by the following grammar:

    φ     p  |  φ  |  φ∨φ  |  φ  |  φ φ

where p ∈𝐴𝑃 is an atomic proposition.
φ means that φ holds in the next position of a trace; φ_1 φ_2 means that φ_1 holds until φ_2 holds.
There are several derived operators, such as
φ≡𝑡𝑟𝑢𝑒 φ,
φ≡φ, and φ_1  𝒲 φ_2 ≡ (φ_1 φ_2) ∨φ_1.  
φ states that φ will eventually hold in the future and φ states that φ holds globally; 𝒲 is the weak version of the until operator. 


We use the following notation to manipulate traces:
let t ∈𝑇𝑅 be a trace and i ∈ℕ be a natural number. t[i] denotes the i-th element of t. Therefore, t[0] represents the starting element of the trace. Let j ∈ℕ and j ≥ i, then t[i,j] denotes the sequence t[i] t[i+1]… t[j-1] t[j], and t[i, ∞] denotes the infinite suffix of t starting at position i. Let p ∈𝐴𝑃 and t ∈𝑇𝑅.
The semantics of an LTL formula is defined as the smallest relation  that satisfies the following conditions:

    t  p        iff p ∈ t[0] 
        t ψ       iff t ψ
        t ψ_1 ∨ψ_2        iff t ψ_1 or t ψ_2 
        t ψ       iff t [1,∞] ψ
        t ψ_1 ψ_2        iffthere exists i ≥ 0 : t[i,∞] ψ_2 
             and for all 0 ≤ j < i we have t[j,∞] ψ_1



  
Suppose, for example, we are interested in constructing an
arbiter circuit. Arbiters are used when more than one client 
needs access to some shared resource, such as a communication bus. To
access the resource, the client sends a request signal
 and waits until it receives a grant signal 
from the arbiter. The task of the arbiter is to answer each request
with a grant without giving grants to the two clients at the same
time. In LTL, an arbiter with two clients can be specified as a
conjunction of three properties:

    [ (_1 ∨_2)         ; (_1 →_1)         ; (_2 →_2)         ;          ]

The mutual exclusion property states that at every point in
time x, at most one grant signal can be set; the response
properties state that if a request is made at some point in time, then
there must exist a point in time, either immediately or later, where the
corresponding grant signal is set.




  
Implementations.
We represent the result of the synthesis process as a finite-state machine.
Let the set = I ∪̇O of atomic propositions be, as before, partitioned into the inputs I and the outputs O.
A Mealy machine over I and O  has the form
= (S, s_0, δ, γ) where S is a finite
set of states, s_0∈ S is the initial state,
δ S × 2^I → S is the transition
function, and γ S × 2^I → 2^O
is the output function. The output of the Mealy machine thus depends on the
current state and the last input letter. A path
of a Mealy machine is an infinite sequence
p = (s_0,σ_0)(s_1,σ_1)(s_2,σ_2) …∈ (S × 2^)^ω of states and sets of atomic propositions that starts with the
initial state s_0 and where
δ(s_n,I ∩σ_n) = s_n+1 and
γ(t_n,I ∩σ_n) = O ∩σ_n
for all n ∈ℕ.
We refer to the projection of a path p to its second component 
π = σ_0σ_1σ_2…∈Σ^ω,
as a computation of the Mealy machine.
The Mealy machine satisfies the LTL
formula φ, denoted by M φ, if all its computations satisfy φ.





Figure <ref> shows two Mealy machines that implement
the arbiter specification from Example <ref>. The Mealy machine shown on the left carefully answers every request and only issues a grant if there is an open request. The machine on the right always issues the grant to the same client, initially to the first client, and switches to the other client as soon as there is a request from the other client.
Both machines satisfy the specification from Example <ref>.




  
Realizability and Synthesis. We say that an LTL formula φ is realizable if there exists a Mealy machine  over the same inputs I and outputs O as φ such that φ. The synthesis problem of an LTL formula φ is to determine whether φ is realizable and, if the answer is yes, to construct a Mealy machine  such that φ.



§ MODEL CHECKING


Before we address the synthesis problem, we take a quick detour into model checking. In model checking, the implementation is already given and we are interested in determining whether the implementation is correct. 

Given a Mealy machine  and an LTL formula φ, model checking determines whether  satisfies φ. In case of a negative answer, model checking produces a counterexample, i.e., a trace t ∈ (2^)^ω that is a computation of  that does not satisfy φ.

To model check a given Mealy machine, we translate the negation of the specification into an equivalent automaton, and then check the intersection of the Mealy machine with that automaton for language emptiness. LTL specifications can be represented as Büchi automata.

A nondeterministic Büchi automaton over the alphabet Σ
is a tuple =(Q,q_0,Δ,F), where Q is a finite set of
states, q_0 ∈ Q is an initial state,
Δ⊆ Q ×Σ× Q a set of transitions, and
F ⊆ Q a subset of accepting states.  A
nondeterministic Büchi automaton accepts an infinite word
w = w_0w_1w_2…∈Σ^ω iff there exists a run r of
 on w, i.e., an infinite sequence
r_0r_1r_2…∈ Q^ω of states such that r_0 = q_0 and
(r_i, w_i, r_i+1) ∈Δ for all i ∈ℕ, such that
r_j ∈ F for infinitely many j ∈ℕ. The set of
sequences accepted by  is called the language
() of .





  Consider the negation of the arbiter specification from Example <ref>, i.e., the LTL formula

    [              (_1 ∧_2);          ∨   (_1 ∧_1);          ∨ (_2 ∧_2) .;            ]

A nondeterminstic Büchi automaton that accepts exactly the traces that satisfy this formula, i.e., all traces that violate the arbiter specification, is shown in Fig. <ref>.



Let _φ=(Q_φ,q^0_φ,Δ_φ,F_φ) be a Büchi automaton that accepts all
sequences in (2^)^ω that satisfy φ, and therefore
violate φ.

In model checking, we verify the Mealy machine  against a specification φ by building the product _ϕ of the Mealy machine =(S,s_0,δ,γ) over inputs I and outputs O, and the Büchi automaton _ϕ=(Q_φ,q^0_φ,Δ_φ,F_φ) with alphabet 2^I∪ O.
The product is a directed graph (V,E) with vertices
V = T × Q  and edges
E ⊆ V × V, where (s,q,s',q') ∈ E iff there is an input i⃗∈ 2^I such that δ(s,i⃗) = s'  and  q' ∈Δ_φ(q, i⃗∪γ(s,i⃗)).
The Mealy machine satisfies φ iff there is no path in  _ϕ that visits an accepting state of _ϕ infinitely often.




  Figure <ref> shows the product _φ of the small Mealy machine  shown on the right in Fig. <ref> with the Büchi automaton _φ from Fig. <ref>. The only infinite paths are the self-loops from t_0,q_0 and t_1,q_0 and the path that oscillates forever between t_0,q_0 and t_1,q_0. These paths do not visit any accepting states.  thus satisfies φ.




§ GAME-BASED SYNTHESIS



In the classic game-based approach to synthesis <cit.>, the problem is analyzed in terms of a two-player game.
The game is played between two players: the input player Player I determines the inputs to the system with the goal of violating the specification. The output player Player O controls the outputs of the system with the goal of satisfying the specification.
A winning strategy for Player I can be translated into an implementation that is guaranteed to satisfy the specification. To solve the synthesis problem, we must therefore check whether Player I has a winning strategy.



In order to turn the specification into a game, we translate
the LTL formula into a deterministic automaton that accepts all
traces that satisfy the formula.  An automaton is
deterministic if each state and input has unique successor
state, i.e., the set of transitions Δ is a total function
from Q ×Σ to Q.
Since
deterministic Büchi automata are not expressive enough to represent
every possible LTL specification, we must use a more expressive acceptance condition
such as the 
parity condition. Whereas a Büchi acceptance
condition identifies a set F ⊆ S of accepting
states, which have to be visited infinitely often, a parity condition c: S →ℕ labels every state with a natural
number. We call such a number the color of the state. A run of a
parity automaton is accepting if the smallest color that appears
infinitely often as a label of the states of the run is even. This
introduces a hierarchy in the acceptance condition, as from some
point on, every odd color has to be answered by a smaller even color.
The Büchi acceptance condition is a special case of the parity condition, where the accepting states are colored with 0
and the remaining states are colored with 1.





  Figure <ref> shows a deterministic parity automaton,
  whose language consists of all traces that satisfy the arbiter specification from
  Example <ref>. The colors of the states are shown
  in the lower part of the state labels.


The deterministic automaton is then translated into an infinite game over a finite graph.
A game graph is a directed graph (V,E) with vertices V and edges E.
The vertices V = V_I∪̇V_O are partitioned into the vertices V_I controlled by Player I and the
vertices V_O controlled by Player O. A parity game (V,E,c) consists of a game graph (V,E) and a
parity condition c: V →ℕ. To play the
game, a token is placed on some initial vertex v,
which is then moved by the player owning the vertex to one of its
successors v', i.e., such that (v,v') ∈ E. This is repeated ad infinitum, resulting in an infinite sequence of
vertices, called a play of the game. If the underlying color
sequence, i.e., the sequence resulting by the reduction of the
vertices to their labels, satisfies the parity condition, Player O
wins the game, otherwise Player I wins the game. 

The game for the synthesis problem is obtained from the deterministic automaton 
by separating the moves of Player I, namely the choice of the
inputs I to the system, and the moves of Player O, i.e., the choice of the
outputs O.

We are interested in finding a winning strategy for Player O, i.e., an appropriate
choice of output after every possible prefix of a play. We call such a
prefix a history of the play. A
useful property of parity games is that they are memoryless determined,
which means that if one of the players has a winning strategy, then there
also exists a winning strategy that only depends on the last vertex of
the history, ignoring the previously visited vertices.
For parity games, it is possible to automatically compute the set of
vertices from which Player O has a winning strategy. This set of
vertices is called the winning region.
If the vertex corresponding to the initial state of the automaton is in the
winning region, then there exists a solution to the synthesis problem.






  Figure <ref> shows the parity game for the synthesis problem
  of the arbiter specification from Example <ref>.
  The game was constructed by first translating the LTL formula into
  the deterministic automaton shown in
  Fig. <ref>, and then separating the moves of the
  input and output players.
  In Fig. <ref>, vertices controlled by Player I are
  depicted as rectangles, vertices controlled by Player O as
  circles. The winning region of Player O is marked by the highlighting. 
   Since the initial vertex
  is in the winning region, the specification can be
  realized. The (memoryless) winning strategy
  is indicated by the thick edges.


Game-based synthesis is asymptotically optimal in the size of the input. However, the synthesized implementations are often much larger than necessary. Compare, for example, the size of the winning strategy in Fig. <ref> with the small Mealy machine on the right in Fig. <ref>.





§ BOUNDED SYNTHESIS



In bounded synthesis <cit.>, we set a bound on the number of states of the synthesized Mealy machine. By incrementally increasing the bound, we can use bounded synthesis to find a Mealy machine with a minimal number of states. The Mealy machine is found as a solution of a constraint system.
To ensure that all solutions of the constrain system satisfy the specification, we encode not only the states, transitions, and outputs of the Mealy machine, but, additionally, an annotation of the states of the Mealy machine that ensures that the given LTL specification is satisfied.
This annotation essentially ensures that the model checking of the Mealy machine succeeds, i.e., that the language of the product with the Büchi automaton corresponding to the negation of the specification is empty.

Let V,E be the product of a Mealy machine  and a Büchi automaton _φ for the negation of the specification.
An annotation λ : S × Q →{}∪ℕ is a function that maps nodes from the run graph to either unreachable  or a natural number k.

An annotation is valid if it satisfies the following conditions:

  
  * the initial vertex s_0,q_0 is labeled by a natural number: λ(t_0,q_0) ≠, and
  
  * if a vertex s,q is annotated with a natural number, i.e., λ(t,q) = k ≠, then for every i⃗∈ 2^I and q' ∈Δ__φ(q, i⃗∪γ(s,i⃗),q'), the successor pair τ(s,i⃗),q') is annotated with a greater or equal number, which needs to be strictly greater if q' is a rejecting state. That is, λ(t',q') > k if q' ∈ F and ≥λ(t',q') ≥ k otherwise.







  Figure <ref> shows the
annotated product of the simple Mealy machine from the right in Fig. <ref> with the Büchi automaton from Fig. <ref>.
  One can verify that the annotation is correct by checking every edge individually.
  For example, the annotation has to increase from t_0,q_0→t_1,q_3 and from t_1,q_0→t_0,q_1 as q_1 and q_3 are rejecting.



















The existence of a Mealy machine with a corresponding annotation of the product graph can be expressed as a propositional constraint. For this purpose, we encode the Mealy machine and the annotation with Boolean variables.




  * tνt' for all t,t' ∈ S and
  ν∈ 2^, for the transition function δ S × 2^I → S of the Mealy machine = (S, s_0, δ, γ).


  * tνx for all t ∈ S,
  ν∈ 2^ and x ∈, for the output function δ S × 2^I → S.


  * tq for all t ∈ T and q ∈ Q, to
  encode the reachable states of the product graph G of  and
  _φ, i.e., those state pairs ⟨ t,q ⟩ where λ(t,q) ≠.


  * tqi for all t ∈ T, q ∈ Q and
  0 < i ≤log(n · k), where n is the bound on the size of the Mealy machine and k is the number of states of the Büchi automaton. The variables encode the numerical annotation of a state pair
  (t,q) of G. We use a logarithmic number of bits to
  encode the annotated value in binary. 






Given an LTL formula φ and a bound
n on the states of the Mealy machine, we solve the
bounded synthesis problem by checking the satisfiability of the propositional
formula _BS(φ,n), consisting of the following
constraints:










  








  * The pair of initial states ⟨ s_0,q_0⟩ for some
  arbitrary, but fixed, s_0 is reachable and annotated with 1. 
  
    rgstate(s_0,q_0) ∧11 = 1





  * Each annotation of a vertex of the product graph bounds the number
  of visited accepting states, not counting the current vertex itself:
  
  
    ⋀_t ∈ T,  q ∈ Qtq→⋀_σ∈ 2^Σoutput(t,σ)
        →⋀_t' ∈ Tt∩σt'→

  
    ⋀_q' ∈Δ(q,σ)t'q'∧tq≺_qt'q'

  
  where ≺_q equals < if q ∈ R and equals ≤
  otherwise. The
  formula output(t,σ) ensures that the output corresponds to the output function of the Mealy machine, i.e.,
  
    output(t,σ) = ⋀_x ∈∩σ t∩σx∧⋀_x
        ∈∖σt∩σx .


  




  For an LTL formula φ and a bound n ∈, the propositional formula _BS(φ,n) is
  satisfiable if and only if there is a Mealy machine  with
  = n that satisfies φ.


























































The propositional constraint can be solved by a standard SAT
solver. In addition to the encoding as a propositional constraint, the
bounded synthesis problem has also been reduced to the satisfiability of quantified Boolean
formulas (QBF) and dependency quantified Boolean formulas
(DQBF) <cit.>, as well as to satisfability modulo theories (SMT) <cit.>. Such encodings are more concise than
the encoding as a Boolean formula. Even though the satisfiability
problems of these logics are more expensive than propositional
satisfiability, in particular the QBF encoding has proven advantageous
in experiments (cf. <cit.>).

Another powerful optimization is lazy synthesis <cit.>, which avoids the
full construction of the constraint system.  Lazy synthesis alternates
between constraint solving, where a model is constructed for an
incomplete constraint system, and verification, where errors in the
previously constructed model are identified and used to extend the
constraint system.




§ BOUNDED CYCLE SYNTHESIS




Bounded cycle synthesis <cit.> extends bounded synthesis by bounding not
only the number of states, but also the number of cycles of the Mealy machine. Bounded cycle synthesis allows us to find
implementations that are not only small but also structurally simple.

























A cycle is a path of a Mealy machine that ends in the same state it started in.
Even Mealy machines with a small number of states can have many cycles: the number of cycles can
be exponential in the number of states. The explosion of the number of circles is in fact worse than the explosion of
the number of states: while a realizable LTL formula has an implementation with at most doubly exponentially many states,
there exist LTL formulas where the number of cycles in the Mealy machine is triply exponential <cit.>. 
This makes the number of cycles a particularly interesting metric for output-sensitive synthesis algorithms.





















Let G = (V,E) be a directed graph. A (simple) cycle c
of G is a a tuple (C,η), consisting of a non-empty set C
⊆ V and a bijection η C ↦ C such that 




  * ∀ v ∈ C. (v,η(v)) ∈ E and 


  * ∀ v ∈ C. n ∈. η^n(v) = v
   ⇔ n C = 0,



where η^n denotes n times the application of
η.  In other words, a cycle of G is a path through G
that starts and ends at the same vertex and visits every vertex of
V at most once. We say that a cycle c = (C,η) has length
n iff C = n.

We extend the notion of a cycle of a graph G to Mealy
machines = (T, t_I, δ, λ), such that
c is a cycle of  iff c is a cycle of the graph
(T,E) for
E =  (t,t') |∃ν∈ 2^. δ(t,ν) =
  t'.
Thus, we ignore the input labels of the edges of .  The set
of all cycles of a Mealy machine  is denoted by
𝒞().



 §.§ Counting Cycles


A classical algorithm for counting the number of cycles of a directed
graph is due to Tiernan <cit.>. We review this
algorithm here as a preparation for the bounded cycle synthesis
encoding.













  
Algorithm 1. Given a directed graph G = (V,E), we
count the cycles of G using the following algorithm:




  (1) Initialize the cycle counter c to c := 0 and some
  set P to P := ∅.


  (2) Pick some arbitrary vertex v_r of G, set
  v := v_r and P :=  v_r.


  (3) For all edges (v,v') ∈ E, with
  v' ∉ P ∖ v_r:




  (3a) If v' = v_r, increase c by one.


  (3b) Oherwise, set v := v', add v' to P and recursively execute
  (3). Afterwards, reset P to its value before the recursive call.




  (4) Obtain the sub-graph G', by removing v_r from G:




  (4a) If G' is empty, return c.


  (4b) Otherwise, continue from (2) with G'.





The algorithm starts by counting all cycles that contain
the first picked vertex v_r. This is done by an unfolding of the
graph into a tree, rooted in v_r, such that there is no repetition
of a vertex on any path from the root to a leaf. The number of
vertices that are connected to the root by an edge of E then
represents the corresponding number of cycles through v_r. The
remaining cycles of G do not contain v_r and, thus, are
cycles of the sub-graph G' without v_r, as well. Hence, we
count the remaining cycles by recursively counting the cycles of
G'. The algorithm terminates as soon as G' becomes empty.

The algorithm, as described so far, has the disadvantage that the number of 
unfolded trees is exponential in the size of the
graph, even if none of their vertices is connected to the root, i.e.,
even if there is no cycle to be counted. This drawback can be
avoided by first reducing the graph to all its strongly connected
components (SCCs) and then counting the cycles of each SCC
separately <cit.>. This reduction is
sound, as a cycle never leaves an SCC of the graph.

The improved algorithm is exponential in
the size of G, and linear in the number of cycles m.
Furthermore, the time between two detections of a cycle, during the
execution, is bounded linear in the size of G.




  To see Tiernan's algorithm in action, we count the number of simple cycles
  of the larger Mealy machine on the left in Fig. <ref>. The
  execution is shown in Fig. <ref>. In this example, we do not need to apply the
  reduction to individual SCCs, because the Mealy machine consists of a single SCC. 
  As result we obtain that the Mealy machine has four
  simple cycles.




 §.§ The Bounded Cycle Synthesis Encoding


Like in the bounded synthesis approach, we solve the bounded cycle synthesis problem via a reduction to
propositional satisfiability. We extend the constraint system from bounded synthesis with additional
constraints that ensure that the number of cycles, as determined by Tiernan's algorithm, does not exceed the given bound.









We call a tree that witnesses m cycles in G, all containing
the root r of the tree, a witness-tree _r,m of G.
Formally, a witness-tree _r,m of G = (V,E) is a labeled
graph _r,m = ((W,B∪ R),τ), consisting of a graph
(W,B ∪ R) with m = R and a labeling function
τ W → V, such that:




  * The edges are partitioned into blue edges B and red
  edges R.

  

  


  * All red edges lead back to the root:

  

    R ⊆ W × r

  

    
  

  * No blue edges lead back to the root:
  
  

    B ∩ W × r  = ∅
  
  

    


  * Each non-root has at least one blue incoming edge:

  

    ∀ w' ∈ W ∖ r . ∃ w ∈ W. (w,w')
  ∈ B 

  


  * Each vertex has at most one blue incoming edge:

  

    ∀ w_1,w_2,w ∈ W. (w_1,w) ∈ B ∧ (w_2,w) ∈
  B ⇒ w_1 = w_2

  

    


  * The graph is labeled by an unfolding of G:

    ∀ w,w' ∈ B ∪ R. (τ(w),τ(w')) ∈ E, 

  


  * The unfolding is complete: 

  

    ∀ w ∈ W. ∀ v' ∈ V. (τ(w),v') ∈ E
  ⇒∃ w' ∈ W. (w,w') ∈ B ∪ R ∧τ(w') =
  v'

  

  


  * Let w_i, w_j∈ W be two different vertices that appear
  on a path from the root to a leaf in the r-rooted tree
  (W,B)[Note that the tree property is enforced by
    Conditions <ref> –
    <ref>.]. Then the labeling of w_i and
  w_j differs, i.e., τ(v_i) ≠τ(v_j).

  

  


  * The root of the tree is the same as the corresponding vertex of
  G, i.e., τ(r) = r.

  




  Let G = (V,E) be a graph consisting of a single SCC, r ∈ V
  be some vertex of G and m be the number of cycles of G
  containing r. Then there is a
  witness-tree _r,m = ((W,B ∪ R),τ) of G with
  W≤ m ·V.
  




  Let G = (V,E) be a graph consisting of a single SCC and let
  _r,m be a witness-tree of G. Then there are at most
  m cycles in G that contain r.
  


From Lemma <ref>
and <ref> we derive that _r,m is a
suitable witness to bound the number of cycles of an
implementation . Furthermore, from
Lemma <ref>, we also obtain an upper bound on the
size of _r,m.




  Figure <ref> shows the witness trees for the larger
  Mealy machine on the left of Fig. <ref>. Each red edge,
  leading back to s_0 and s_1 on the first tree level,
  captures one cycle of the machine. Thereby, the properties of the
  tree enforce that all cycles are captured by these trees.




We now encode the bound on the number of cycles as a propositional constraint. First,
we construct a simple directed graph G out of the
implementation .  Then, we guess all the sub-graphs,
obtained from G via iteratively removing vertices, and split them
into their corresponding SCCs. Finally, we guess the witness-tree for
each such SCC.

In order to keep the encoding compact, we introduce some further
optimizations. First, we do not need to introduce a fresh copy for
each SCC, since the SCC of a vertex is always unique. Thus, it
suffices to guess an annotation for each vertex. Second, we have to guess n trees _r_i,m_i, i=1 … n, each
consisting of at most m_i · n vertices, such that the sum of
all m_i is equal to the overall number of cycles m. One possible
solution would be to overestimate each m_i by m. Another
possibility would be to guess the exact distribution of the cycles
over the different witness-trees _r_i,m_i. In our encoding, we guess all trees together in a single graph
bounded by m · n. We annotate each vertex with its
corresponding witness-tree _r_i,m_i. Instead of
bounding the number of red edges separately for each _r_i,m_i by m_i,
we just bound the number of all red edges in the whole forest by m.
In this way, we not only reduce the size of the encoding, but also avoid
additional constrains that would be needed to sum up the
different witness-tree bounds i to m.











Let T be some ordered set with T = n and
S = T × 1,2,…, m. We use T to denote the
vertices of G and S to denote the vertices of the forest of
_r_i,m_i s. Further, we use M = T × 1 to
denote the roots and N = S ∖ M to denote the non-roots of
the corresponding trees.  We introduce the following Boolean variables:




  * tt' for all t,t' ∈ T, denoting the edges of
  the abstraction of  to G.


  * ss' for all s ∈ S and
  s' ∈ N, denoting a blue edge.


  * ss' for all s ∈ S and s' ∈ M, denoting a
  red edge.


  * si for all s ∈ S, 0 < i ≤log(n),
  denoting the witness-tree for each s. Thereby, each tree is
  referenced by a unique number encoded in binary using a logarithmic
  number of bits. 
 
 
 
 
 
 


  * st for all s ∈ S and t ∈ T, denoting
  the set of all vertices t, already visited at s, since
  leaving the root of the corresponding witness-tree.


  * ci for all 0 < c ≤ m,
  0 < i ≤log (n · m), denoting an ordered list of all red
  edges, bounding the red edges of the forest.


  * kti for all 0 < k ≤ n, t ∈ T, and
  0 ≤ i < log n, denoting the SCC of t in the k-th
  sub-graph of G. The sub-graphs are obtained 
  by iteratively removing vertices of T, according to the
  pre-defined order. This way, each sub-graph contains exactly all
  vertices that are larger than the root.
 

Note that, by the definition of S, we introduce m
explicit copies for each vertex of G. This is sufficient, since
each cycle contains each vertex at most once. Thus, the labeling
τ of a vertex s can be directly derived from the first
component of s.



Given the respective bounded synthesis encoding for the
specification φ and a bound n on the states of the
resulting implementation , and a bound m on the number
of cycles of , we encode the bounded cycle synthesis problem
as the propositional formula


    = _BS(φ,n)  ∧ _CS(n,m)  ∧ _→ G(φ,n)  ∧ _SCC(n)


The constraints of _BS(φ,n) represent the
bounded synthesis encoding. The constraints of
_→ G(φ,n) simplify the representation of
the Mealy machine  to G.  The constraints of
_CS(,n,m) bound the cycles of the system and are
presented in Table <ref>. The constraints of
_SCC(n) enforce that each vertex is labeled by a
unique SCC <cit.>.








  For an LTL formula φ and a pair of bounds n, m ∈, the propositional 
  formula  is satisfiable if and
  only if there is a Mealy machine  with
  = n and 
  that satisfies φ.



Using our encoding, we can now 
search for the implementation of the arbiter specification from Example <ref> with the smallest number of states and, additionally, smallest number of cycles.
It turns out that neither Mealy machine from
Fig. <ref> is the minimal solution.
The smallest implementation for the arbiter specification, with respect
to the number of states and cycles is shown in
Fig. <ref>. The minimal implementation switches the grant at
every time step, completely ignoring the requests. This solution only
requires two states and a single cycle. The solution may not be the
best choice with respect to a possible target application, but it is
definitely the smallest one.


In general, it is not always possible to minimize the two parameters simultaneously.
There are specifications for which the
smallest possible number of states and the smallest possible number of
cycles cannot be realized within a single
solution <cit.>. In such situations it may be helpful to have an explicit
optimization function specified by the user that resolves the trade-off.



§ CONCLUSIONS


We have studied three different algorithms for the reactive synthesis problem.
The classic game-based synthesis algorithm is input-sensitive in the sense that its performance is asymptotically
optimal in the size of the specification, but it produces implementations that may be larger than necessary.
Bounded synthesis produces implementations with a minimal number of states. Bounded cycle synthesis
additionally minimizes the number of cycles. Bounded synthesis and bounded cycle synthesis belong
to the new class of output-sensitive synthesis algorithms.






















A direct comparison of the three algorithms is shown in
Fig. <ref>. The figure depicts the shape of the synthesized
implementations from the AMBA TBURST4 specification <cit.> using, from left to right, game-based
synthesis, bounded synthesis, and bounded cycle synthesis.
Even just based on a superficial visual comparison, it is immediately clear that the output-sensitive
algorithms produce dramatically simpler implementations.










  
Acknowledgement.
This work was partially supported by the European Research Council (ERC) Grant OSARES (No. 683300).

abbrv


