A Supervisory Control Algorithm Based on
Property-Directed Reachability⋆

arXiv:1711.06501v1 [] 17 Nov 2017

Koen Claessen1 , Jonatan Kilhamn1 , Laura Kovács13 , and Bengt Lennartson2
1

Department of Computer Science and Engineering,
2
Department of Electrical Engineering,
Chalmers University of Technology
3
Faculty of Informatics, Vienna University of Technology
{koen, jonkil, laura.kovacs, bengt.lennartson}@chalmers.se

Abstract. We present an algorithm for synthesising a controller (supervisor) for
a discrete event system (DES) based on the property-directed reachability (PDR)
model checking algorithm. The discrete event systems framework is useful in
both software, automation and manufacturing, as problems from those domains
can be modelled as discrete supervisory control problems. As a formal framework, DES is also similar to domains for which the field of formal methods for
computer science has developed techniques and tools. In this paper, we attempt
to marry the two by adapting PDR to the problem of controller synthesis. The
resulting algorithm takes as input a transition system with forbidden states and
uncontrollable transitions, and synthesises a safe and minimally-restrictive controller, correct-by-design. We also present an implementation along with experimental results, showing that the algorithm has potential as a part of the solution
to the greater effort of formal supervisory controller synthesis and verification.
Keywords: Supervisory control ·Discrete-event systems ·Property-directed reachability ·Synthesis ·Verification ·Symbolic transition system

1 Introduction
Supervisory control theory deals with the problems of finding and verifying controllers
to given systems. One particular problem is that of controller synthesis: given a system
and some desired properties—safety, liveness, controllability—automatically change
the system so that it fulfills the properties. There are several approaches to this problem,
including ones based on binary decision diagrams (BDD) [14, 6], predicates [11] and
the formal safety checker IC3 [18].
In this work we revisit the application of IC3 to supervisory control theory. Namely,
we present an algorithm for synthesising a controller (supervisor) for a discrete event
system (DES), based on property-directed reachability [4] (PDR, a.k.a. the method underlying IC3 [2]). Given a system with a safety property and uncontrollable transitions,
the synthesised controller is provably safe, controllable and minimally restrictive [16].
⋆

The final publication is available at Springer via https://doi.org/10.1007/978-3-319-70389-3_8.

2

1.1 An illustrative example
Let us explain our contributions by starting with an example. Figure 1 shows the transition system of a finite state machine extended with integer variables x and y. The
formulas on the edges denote guards (transition cannot happen unless formula is true)
and updates (after transition, x takes the value specified for x′ in the formula). This
represents a simple but typical problem from the domain of control theory, and is taken
from [17].
x = 0, y = 0
l0

a : y′ = 2

l2

b : y′ = 1

b:⊤
a:⊤

l1

l3

α:y =2∧x>2

l5

c : x′ = x + 1
α:y =2∧x≤2
l4

ω:⊤

Fig. 1. The transition system of the example.

In a controller synthesis problem, a system such as this is the input. The end result
is a restriction of the original system, i.e. one whose reachable state space is a subset of
that of the original one. In this extended finite state machine (denoted as EFSM) representation, this is written as new and stronger guard formulas on some of the transitions.
Our example has two more features: the location l5 , a dashed circle in the figure, is
forbidden, while the event α is uncontrollable. The latter feature means that the synthesised controller must not restrict any transition marked with the event α.
To solve this problem, we introduce an algorithm based on PDR [4] used in a software model checker (Section 3). Intuitively, what our algorithm does is to incrementally
build an inductive invariant which in turn implies the safety of the system. This invariant
is constructed by ruling out paths leading into the bad state, either by proving these bad
states unreachable from the initial states, or by making them unreachable via strengthening the guards.
In our example, the bad state l5 is found to have a preimage under the transition
relation T in l3 ∧ y = 2 ∧ x > 2. The transition from l3 to l5 is uncontrollable, so in
order to guarantee safety, we must treat this prior state as unsafe too. The transitions
leading into l3 are augmented with new guards, so that the system may only visit l3 if
the variables make a subsequent transition to l5 impossible. By applying our work, we
refined Figure 1 with the necessary transition guards and a proof that the new system is
safe. We show the refined system obtained by our approach in Figure 2.

3
x = 0, y = 0
a : y′ = 2

l0

l2

b : y′ = 1

b : y 6= 2 ∨ x ≯ 2
a : y 6= 2 ∨ x ≯ 2

l1

l3

α:y =2∧x>2

l5

c : x′ = x + 1
α:y =2∧x≤2
l4

ω:⊤

Fig. 2. The transition system from the example, with guards updated to reflect the controlled
system.

1.2 Our Contributions
1. In this paper we present a novel algorithm based on PDR for controller synthesis
(Section 3) and prove correctness and termination of our approach (Section 4). To
the best of our knowledge, PDR has not yet been applied to supervisory control
systems in this fashion. We prove that our algorithm terminates (given finite variable domains) and that the synthesised controller is safe, minimally-restrictive, and
respects the controllability constraints of the system. Our algorithm encodes system
variables in the SAT domain; we however believe that our work can be extended by
using satisfiability modulo theory (SMT) reasoning instead of SAT.
2. We implemented our algorithm in the model checker Tip [5]. We evaluated our
implementation on a number of control theory problems and give practical evidence
of the benefits of our work (see Section 6).

2 Background
We use standard terminology and notation from first-order logic (FOL) and restrict
formulas mainly to quantifier-free formulas. We reserve P, R, T, I to denote formulas describing, respectively, safety properties, “frames” approximating reachable sets,
transition relations and initial properties of control systems; all other formulas will be
denoted with φ, ψ, possibly with indices. We write variables as x, y and sets of variables as X, Y . A literal is an atom or its negation, a clause a disjunction of literals, and
a cube a conjunction of literals. We use R to denote a set of clauses, intended to be
read as the conjunction of those clauses. When a formula ranges over variables in two
or more variable sets, we take φ(X, Y ) to mean φ(X ∪ Y ).
For every variable x in the control system, we assume the existence of a unique
variable x′ representing the next-state value of x. Similarly, the set X ′ is the set {x′ |x ∈

4

X}. As we may sometimes drop the variable set from a formula if it is clear from the
context, i.e. write φ instead of φ(X), we take φ′ to mean φ(X ′ ) in a similar fashion.
2.1 Modelling Discrete Event Systems
A given DES can be represented in several different ways. The simple, basic model
is the finite state machine (FSM) [10]. A state machine is denoted by the tuple G =
hQ, Σ, δ, Qi i, where Q is a finite set of states, Σ the finite set of events (alphabet),
δ ⊆ Q × Σ × Q the transition relation, and Qi ⊆ Q the set of initial states.
In this notation, a controller can be represented as a function C : Q → 2Σ denoting
which events are enabled in a given state. For any σ ∈ Σ and q ∈ Q, the statement
σ ∈ C(q) means that the controller allows transitions with the event σ to happen when
in q; conversely, σ ∈
/ C(q) means those transitions are prohibited.
Extended Finite State Machine. The state machine representation is general and monolithic. In order to more intuitively describe real supervisory control problems, other formalisms are also used. Firstly, we have the extended finite state machine (EFSM), which
is an FSM extended with FOL formulas over variables. In effect, we split the states into
locations and variables, and represent the system by the tuple A = hX, L, Σ, ∆, li, Θi.
Here, X is a set of variables, L a set of locations, Σ the alphabet, ∆ the set of transitions, li ∈ L the initial location and Θ(X) a formula describing the initial values of the
variables.
A transition in ∆ is now a tuple hl, a, mi where l, m are the entry and exit locations,
respectively, while the action a = (σ, φ) consists of the event σ ∈ Σ and φ(X, X ′ ).
The interpretation of this is that the system can make the transition from l to m if the
formula φ(X, X ′ ) holds. Since the formula can include next-state variables—φ may
contain arbitrary linear expressions over both X and X ′ —the transition can specify
updated variable values for the new state.
We have now defined almost all of the notation used in the example in Figure 1.
In the figure, we write σ : φ to denote the action (σ, φ). Furthermore, the figure is
simplified greatly by omitting next-state assignments on the form x′ = x, i.e. x keeping
its current value. If a variable does not appear in primed form in a transition formula,
that formula is implied to have such an assignment.
Symbolic Representation. Moving from FSM to EFSM can be seen as “splitting” the
state space into two spaces: the locations and the variables. A given feature of an FSM
can be represented as either one (although we note that one purpose for using variables
is to easier extend the model to cover an infinite state space). Using this insight we can
move to the “other extreme” of the symbolic transition system (STS): a representation
with only variables and no locations.
The system is here represented by the tuple SA = hX̂, T(X̂, X̂ ′ ), I(X̂)i where
X̂ is the set of variables extended by two new variables xL and xΣ with domains L
and Σ, respectively. With some abuse of notation, we use event and variable names to
denote formulas over those variables, such as ln for the literal xL = ln and ¬σ for the
literal xΣ 6= σ. The initial formula I and transition formula T are constructed from the
corresponding EFSM representation as I(X̂) = (xL = li ) ∧ Θ(X) and T(X̂, X̂ ′ ) =
W
′
′
hl,(σ,φ),mi∈∆ (l ∧ σ ∧ φ(X, X ) ∧ m ).

5

In this paper, we will switch freely between the EFSM and STS representations of
the same system, depending on which is the best fit for the situation. Additionally, we
will at times refer to X̂ as only X, as long as the meaning is clear from context. In
either representation, we will use state to refer to a single assignment of location and
variables, and path for a sequence of states s0 , s1 , ..., sk .
2.2 Supervisory Control
The general problem of supervisory control theory is this: to take a transition system,
such as the ones we have described so far, and modify it so that it fulfils some property which the unmodified system does not. There are several terms in this informal
description that require further explanation.
The properties that we are interested in are generally safety, non-blocking, and/or
liveness, which can be seen as a stronger form of non-blocking. Controlling for a safety
property means that in the controlled system, there should be no sequence of events
which enables transitions leading from an initial state to a forbidden state.
Non-blocking and liveness are defined relative to a set of marked state. The former
means that at least one such state is reachable from every state which is reachable from
the initial states. The latter, liveness, implies non-blocking, as it is the guarantee that
the system not only can reach but will return to a marked state infinitely often. In this
work we have reduced the scope of the problem by considering only safety.
Furthermore, we talk about the property of controllability. This is the notion that
some events in a DES are uncontrollable, which puts a restriction on any proposed
controller: in order to be valid, the transitions involving uncontrollable events must
not be restricted. Formally, in an (E)FSM it is enough to split the alphabet into the
uncontrollable Σu ⊆ Σ and the controllable Σc = Σ \ Σu . In an STS, this is expressed
by the transition relation taking the form T = Tu ∨ Tc , where Tc and Tu include
literals xL = σ for, respectively, only controllable and only uncontrollable events σ.
Finally there is the question of what form this “controlled system” takes, since a
controller function C : Q → 2Σ can be impractical. A common method is that of
designating a separate state machine as the supervisor, and taking the controlled system
to be the synchronous composition of the original system and the supervisor [8]. In
short, this means running them both in parallel, but only allowing a transition with a
shared event σ to occur simultaneously in both sub-systems.
However, the formidable theory of synchronised automata is not necessary for the
present work. Instead, we take the view that the controlled system is the original system,
either in the EFSM or STS formulation, with some additions.
In the EFSM case, the controlled system has the exact same locations and transitions, but additional guards and updates may be added. In other words, the controlled
system augments each controllable transition by replacing the original transition formula φ with the new formula φs = φ ∧ φnew . The uncontrollable transitions are left
unchanged. In the STS case, the new transition function is TS = Tu ∨ TSc where
TSc = Tc ∧ Tnew
c . This way, all uncontrollable transitions are guaranteed to be unmodified in the controlled system.
Finally, a controlled system, regardless of which properties the controller is set out
to guarantee, is often desired to be minimally restrictive (eqiv. maximally permissive).

6

The restrictiveness of a controlled system is defined as follows: out of two controlled
versions S1 and S2 of the same original system S, S1 is more restrictive than S2 if there
is at least one state, reachable under the original transition function T, which is reachable under TS2 but unreachable under TS1 . A controlled system is minimally restrictive
if no other (viable) controlled system exists which is less restrictive. The word “viable”
in brackets shows that one can talk about the minimally restrictive safe controller, the
minimally restrictive non-blocking controller and so on; for each combination of properties, the minimally restrictive controller for those properties is different.

3 PDRC: Property-Driven Reachability-Based Control
Property-driven reachability (PDR) [4] is a name for the method underlying IC3 [2],
used to verify safety properties in transition systems. In this paper we present PropertyDriven Reachability-based Control (PDRC), which extends PDR from verifying safety
to synthesising a controller which makes the system safe. In order to explain PDRC, we
first review the main ingredients of PDR.
PDR works by successively blocking states that are shown to lead to unsafe states in
certain number of steps. Blocking a state at step k here means performing SAT-queries
to show that the state is unreachable from the relevant frame Rk . A frame Rk is a
predicate over-approximating the set of states reachable from the initial states I in k
steps.
When a state is blocked—i.e. shown to be unreachable—the relevant frame is updated by excluding that state from the reachable-set approximation. If a state cannot
be blocked at Rk , the algorithm finds its preimage s and proceeds to block s at Rk−1 .
If a state that needs to be blocked intersects with the initial states, the safety property
of the system has been proven false. Conversely, if two adjacent frames Ri , Ri+1 are
identical after an iteration, we have reached a fixed-point and a proof of the property P
in one of them entails a proof of P for the whole system.
With PDRC, we focus on the step where PDR has found a bad cube s (representing unsafe states) in frame Rk , and proceeds to check whether it is reachable from
the previous frame Rk−1 . If it is not, this particular cube was a false alarm: it was in
the over-approximation of k-reachable states, but after performing this check we can
sharpen that approximation to exclude s. If s was reachable, PDR proceeds to find its
preimage t which is in Rk−1 . Note that t is also a bad cube, since there is a path from
t to an unsafe state. However, in a supervisory control setting, there is no reason not
to immediately control the system by restricting all controllable transitions from t to s.
This observation is the basis of our PDRC algorithm.
3.1 Formal Description of PDRC
As PDRC is very similar to PDR, this description and the pseudocode procedures draw
heavily from [4].
Our PDRC algorithm is given in Algorithm 1. As input, we take a transition system
that can be represented by a transition function T(X, X ′ ) = Tc ∨ Tu , i.e. one where
each possible transition is either controllable or uncontrollable; and a safety property

7

Algorithm 1: Blocking and propagation for one iteration of N .
1
2
3
4

5

6
7
8
9
10
11

// finding and blocking bad states
while SAT[RN ∧ ¬P] do
extract a bad state m from the SAT model;
generalise m to a cube s;
recursively block s as per block(s, N );
// at this point R and/or T have been updated to rule
out m
end
// propagation of proven clauses
add new empty frame RN+1 ;
for k ∈ [1, N ] and c ∈ Rk do
if Rk  c′ then
add c to Rk+1 ;
end
end

P(X). The variables in X are boolean, in order to allow the use of a SAT solver –
although see Section 3.2 describing an extension from SAT to SMT.
Throughout the run of the algorithm, we keep a trace: a series of frames Ri , 0 ≤
i ≤ N . Each Ri (X) is a predicate that over-approximates the set of states reachable
from I in i steps or less. R0 = I, where I is a formula encoding the initial states.
V Each frame Ri , i > 0 can be represented by a set of clauses Ri = {cij }j , such that
j cij (X) = Ri (X). An empty frame Rj = {} is considered to encode ⊤, i.e. the
most over-approximating set possible.
We maintain the following invariants:
1. Ri → Ri+1
2. Ri → P, except for i = N
3. Ri+1 is an over-approximation of the image of Ri under T
Starting with N = 1 and R1 = {}, we proceed to do the first iteration of the
blocking and propagation steps, as shown in Algorithm 1.
The “blocking step” consists of the while-loop (lines 1–5) of Algorithm 1, and coming out of that loop we know that RN → P. The propagation step follows (lines 6–11),
and here we consider for each clause in some frame of the trace whether it also holds in
the next frame.
Afterwards, we check for a fix-point in Ri ; i.e. two syntactically equal adjacent
frames Ri = Ri+1 . Unless such a pair is found, we increment N by 1 and repeat the
procedure.
The most important step inside the while loop is the call to block (line 4). This
routine is shown in Algorithm 2. Here, we take care of the bad states in a straightforward way. First, we consider its preimage under the controllable transition function
Tc (line 2). The preimage cube t can be found by taking a model of the satisfiable
query Rk−1 ∧ ¬s ∧ Tc ∧ s′ and dropping the primed variables. Each such cube encodes

8

Algorithm 2: The blocking routine, which updates the supervisor.

1
2
3
4

5
6
7
8
9
10
11
12

Data: A cube s and a frame index k
// first consider the controllable transitions:
while SAT[Rk−1 ∧ ¬s ∧ Tc ∧ s′ ] do
extract and generalise a bad cube t in the preimage of Tc ;
update Tc := Tc ∧ ¬t;
end
// then consider the uncontrollable transitions:
while SAT[Rk−1 ∧ ¬s ∧ Tu ∧ s′ ] do
if k=1 then
throw error: system uncontrollable;
end
extract and generalise a bad cube t in the preimage of Tu ;
call block(t, k − 1);
end
add ¬s to Ri , i ≤ k;

states from which a bad state is reachable in one step. Thus, we update the supervisor to
disallow transitions from those bad states (line 3). This accounts for the first while-loop
in Algorithm 2.
The second while-loop (lines 5–11)is very similar, but considers the uncontrollable
transitions, encoded by Tu , instead. If a preimage cube is found here, we cannot rule it
out by updating the supervisor. That preimage instead becomes a bad state on its own,
to be controlled in the previous frame k − 1.
Example 1. Example, revisited. Recall the example in Figure 1. Since it uses integer
variables it seems to require an SMT-based version of PDRC. This particular example is
so simple, however, that “bit-blasting” the problem into SAT by treating the proposition
x < i as a separate boolean variable for each value of i in the domain of x will yield
the same solution.
PDRC requires 3 iterations to completely supervise the system. In the first, the
clause ¬l5 is added to the first frame R1 , after proving that it is not in the initial states.
In the second, ¬l5 is found again but this time the uncontrollable transition from l3 is
followed backwards, and the clause ¬α ∨ ¬l3 ∨ y 6= 2 ∨ x ≯ 2 is also added to R1 ,
which allows us to add ¬l5 to R2 . Finally, in the third, the trace of preimages lead
to the controllable transitions l1 → l3 and l2 → l3 , and we add new guards to both
(technically, we add new constraints to the transition function).
The updated system is the one shown in Figure 2. The third iteration also proves the
system safe, as we have R1 = R2 . These frames then hold the invariant, (¬α∨¬l3 ∨y 6=
2 ∨ x ≯ 2) ∧ ¬l5 , which implies P and is inductive under the updated T.
3.2 Extension to SMT
Our PDRC algorithm in Algorithm 1 uses SAT queries, and is straightforward to use
with a regular SAT solver on systems with a propositional transition function. However,

9

like in [3, 9] it is possible to extend it to other theories, such as Linear Integer Arithmetic, using an SMT solver. The SAT query in Algorithm 1 provides no diffuculty, but
some extra thought is required for the ones in the blocking procedure, which follow this
pattern:
while SAT[Ri ∧ ¬s ∧ T ∧ s′ ] do
extract and generalise a bad cube t in the preimage of T;
If one only replaces the SAT solver by an SMT solver capable of handling the
theory in question, one can extract a satisfying assignment of theory literals. However,
each of these might contain both primed and unprimed variables, such as the next-state
assignment x′ = x + 1.
These lines effectively ask the solver to generalise a state m—an assignment of
theory literals satisfying some formula F—into a more general cube t, ideally choosing
the t that covers the maximal amount of discrete states, while still guaranteeing t → F.
In the SAT case, this is achieved by dropping literals of t that do not affect the validity
of F(t). An alternate method based on ternary simulation, that is useful when the query
is for a preimage of a transition function T, is given in [4]. For the SMT case, however,
the extent of generalisation depends on the theory and the solver.
In the worst case of a solver that cannot generalise at all, the algorithm is consigned
to blocking a single state m in each iteration. This means that the state space simplification gained from using a symbolic transition function in the first place is lost, since the
reachability analysis checks states one by one. In conclusion, PDRC could be implemented for systems with boolean variables using a SAT-solver with no further issues,
while an SMT version would require carefully selecting the right solver for the domain.
We leave this problem as an interesting task for future work.

4 Properties of PDRC
In this section we prove the soundness and termination of our PDRC algorithm.
4.1 Termination
Theorem 1. For systems with state variables whose domains are finite, the PDRC algorithm always terminates.
The termination of regular PDR is proven in [4]. In the case of an unsafe system—
which for us corresponds to an uncontrollable system—the counterexample proving this
must be finite in length, and thus found in finite time. In the case of a safe system, the
proof is based on the following observations: that each proof-obligation (call to block)
must block at least one state in at least one frame; that there are a finite number of frames
for each iteration (value of N ); that there are a finite number of states of the system;
and that each Ri+1 must either block at least one more state than Ri , or they are equal.
All these observations remain true for PDRC, substituting “uncontrollable” for “unsafe”. This means that the proof of termination from [4] can be used for PDRC with
minimal modification.

10

4.2 Correctness
We claim that the algorithm described above synthesises a minimally restrictive safe
controller for the original system.
Theorem 2. If there exists any safe controller for the system, the controller synthesised
by the PDRC algorithm is safe.
Proof. We prove Theorem 2 by contradiction. Assume there is an unsafe state s, i.e. we
have ¬P(s), that is reachable from an I-state in k steps. We must then have k ≥ N ,
since invariant (2) states that Ri → P, i < N . Let M be the index of the discovered
fix point RM = RM+1 .
Invariant (1) (from Section 3.1) states that Ri → Ri+1 , and this applies for all
values 0 ≤ i ≤ M . Repeated application of this means that any state in any Ri , i < M
is also contained in RM .
Invariant (3) states that Ri+1 is an over-approximation of the image of Ri . This
means that any state reachable from RM should be in RM+1 . Since RM = RM+1 ,
such a state is also in RM itself. Repeated application of this allows us to extend the
trace all the way to Rk = Rk−1 = · · · = RM .
Now, for the bad state s, regardless of the number of steps k needed to reach it, we
know that s is contained in Rk and therefore in RM . Yet when the algorithm terminated
it had at one point found RM ∧ ¬P to be UNSAT. The state s, which is both in RM and
¬P, would constitute a satisfying assignment to this query. This contradiction proves
that s cannot exist.
⊓
⊔
Theorem 3. A controller synthesised by the PDRC algorithm is minimally restrictive.
Proof. We prove Theorem 3 also by contradiction. Assume there is a safe path π =
s0 , s1, . . . , sk through the original system (with transition function T), which is not
possible using the controlled transition function TPDRC ; yet there exists another safe,
controllable supervisor represented by TS where π is possible. By deriving a contradiction, we will prove that no such TS can exist.
Consider the first step of π that is not allowed by TPDRC ; in other words, a pair
(si , si+1 ) where we have ¬TPDRC (si , si+1 ) while we do have both TS (si , si+1 ) and
T(si , si+1 ). The only way that TPDRC is more restrictive than T is due to strengthenings on the form TcPDRC = Tc ∧ ¬m, for some cube m. This means that si must be in
some cube m that PDRC supervised in this fashion.
This happened inside a call block(m, j). Since π is safe, this call cannot have
been made because m itself encoded unsafe states. Instead, there must have been a
previous call block(n, j + 1), where m is a minterm of the preimage of n under Tu .
This cube n is either itself a bad cube, or it can be traced to a bad cube by following the
trace of block calls. Since each step in this block chain only uses Tu , we can find a
series of uncontrollable transitions, starting in some s̃i+1 ∈ n, leading to some cube p
which is a generalisation of a satisfying assignment to the query RN ∧ ¬P.
This proves that TS , whose TSc does not restrict transitions from si , allows for
the system to enter a state s̃i+1 , from which there is an uncontrollable path to an unsafe
state. This contradicts the assumption that TS was safe, proving that the combination of
π and TS cannot exist. This proves that the controller encoded by TPDRC is minimally
restrictive.
⊓
⊔

11

5 Implementation
We have implemented a prototype of PDRC in the model checker Tip (Temporal Inductive Prover [5]). The input format supported by Tip is AIGER [1], where the transition
system is represented as a circuit, which is not a very intuitive way to view an EFSM or
STS. For this reason, our prototype also includes Haskell modules for creating a transition system in a control-theory-friendly representation, converting it to AIGER, and
using the output from the Tip-PDRC to reflect the new, controlled system synthesised by
PDRC. Finally, it also includes a parser from the .wmod format used by WATERS and
Supremica [13], into our Haskell representation. Altogether, our implementation consists of about 150 lines of code added or changed in the Tip source, and about 1600 lines
of Haskell code. Our tools, together with the benchmarks we used, is available through
github.com/JonatanKilhamn/supermini and github.com/JonatanKilhamn/tipcheck.
When converting transition systems into circuits, certain choices have to be made.
Our encoding allows for synchronised automata with one-hot-encoded locations (e.g.
location l3 out of 5 is represented by the bits [0, 0, 1, 0, 0]) and unary-encoded integer
variables (e.g. a variable ranging from 0 to 5 currently having the value 3 is represented
by [1, 1, 1, 0, 0]). Each of these encoding has a corresponding invariant: with one-hot,
exactly one bit must be set to 1; with unary, each bit implies the previous one. However,
these invariants need not be explicitly enforced by the transition relation (i.e. as guards
on every transition), rather, it is enough that they are preserved by all variable updates.
It should be noted that although the PDRC on a theoretical level works equally
well on STS as EFSM, our implementation does assume the EFSM division between
locations and variables for the input system. However, our implementation retains the
generality of PDRC in how the state space is explored—the algorithm described in
Section 3 is run on the circuit representation, where the only difference between the
location variable xL and any other variable is the choice of encoding.

6 Experiments
For an empirical evaluation, we ran PDRC on several standard benchmark problems:
the extended dining philosophers (EDP) [15], the cat and mouse tower (CMT) [15] and
the parallell manufacturing example (PME) [12]. The runtimes of these experiments
are shown in Table 1 below. The benchmarks were performed on a computer with a 2.7
GHz Intel Core i5 processor and 8GB of available memory.
6.1 Problems
For the dining philosophers, EDP(n, k) denotes the problem of synthesising a safe
controller for n philosophers and k intermediary states that each philosopher must go
through between taking their left fork and taking their right one. The transition system
is written so that all philosophers respect when their neighbours are holding the forks,
except for the even-numbered ones who will try to take the fork to their left even if it is
held, which leads (uncontrollably) to a forbidden state.

12

For the cat and mouse problem, CMT(n, k) similarly denotes the problem with n
floors of the tower, k cats and k mice. Again, the transition system already prohibits
cats and mice from entering the same room (forbidden state) except by a few specified
uncontrollable pathways.
Finally, the parallel manufacturing example (PME) represents an automated factory,
with an industrial robot and several shared resources. It differs from the other in that
its scale comes mainly from the number of different synchronised automata. In return,
it does not have a natural parameter that can be set to higher values to increase the
complexity further.
6.2 Results
We compare PDRC to Symbolic Supervisory Control using BDD (SC-BDD) [14, 6],
which is implemented within Supremica. We wanted to include the Incremental, Inductive Supervisory Control (IISC) algorithm [18], which also uses PDR but in another
way. However, the IISC implementation from [18] is no longer maintained. Despite this
failed replication, we include figures for IISC taken directly from [18]—with all the
caveats that apply when comparing runtimes obtained from different machines. Table 1
shows runtimes, where the problems are denoted as above and “×” indicates time-out
(5 min). The parameters for EDP and CMT were chosen to show a wide range from
small to large problems, while still mostly choosing values for which [18] reports runtimes for IISC. We see that while SC-BDD might have the advantage on certain small
problems, PDRC quickly outpaces it as the problems grow larger.
Table 1. Performance of PDRC (our contribution), SC-BDD and IISC on standard benchmark
problems. Note that the IISC implementation was not reproducible by us; the numbers here are
lifted from [18]. “×” indicates timeout (5 min), and “–” means this particular problem was not
included in [18].
Model
CMT(1,5)
CMT(3,3)
CMT(5,5)
CMT(7,7)
EDP(5,10)
EDP(10,10)
EDP(5,50)
EDP(5,200)
EDP(5,10e3)
PME

PDRC IISC[18] SC-BDD
0.09
0.13
0.007
1.3
0.43
1.12
8.3
0.73
×
30.02 0.98
×
0.03
0.98
0.031
0.15
–
0.10
0.03
0.12
0.26
0.06
0.12
×
0.19
0.12
×
0.72
2.3
8.1

7 Discussion
In this section, we relate briefly how BDD-SC [14, 6] and IISC [18] work, in order to
compare and contrast to PDRC.

13

7.1 BDD-SC
BDD-SC works by modelling an FSM as a binary decision diagram (BDD). The algorithm generates a BDD, representing the safe states, by searching backwards from the
forbidden states. However, the size of this BDD grows with the domain of the integer
variables. The reason is that the size of the BDD is quite sensitive to the number of
binary variables, but also the ordering of the variables in the BDD. Even when more recent techniques on partitioning of the problem are used [6], the size of the BDD blows
up, and we see in Table 1 that BDD-SC very quickly goes from good performance to
time-out.
7.2 IISC
It is natural to compare PDRC to IISC [18], since the latter is also inspired by PDR
(albeit under the name IC3). In theory, PDRC has some advantages.
The first advantage is one of representation. IISC is built on the EFSM’s separation
between locations and variables, as described in 2.1. PDRC, on the other hand, handles
the more general STS representation. Specifically, IISC explicitly unrolls the entire substate-space spanned by the locations. This sub-space can itself suffer a space explosion
when synchronising a large number of automata.
To once again revisit our example (Figure 1): IISC would unroll the graph, starting
in l0 , into an abstract reachability tree. Each node in such a tree can cover any combination of variable values, but only one location. Thus, IISC effectively does a forwards
search for bad locations, and the full power of PDR (IC3) is only brought to bear on the
assignment of variables along a particular error trace. Thus, a bad representation choice
w.r.t. which parts of the system are encoded as locations versus as variables can hurt
IISC, while PDRC is not so vulnerable.
PDRC, in contrast, leverages PDR’s combination of forwards and backwards search:
exploring the state space backwards from the bad states in order to construct an inductive invariant which holds in the initial states. One disadvantage of the backwards search
is that PDRC might add redundant safeguards. For example, the safeguard on the transition from l1 to 13 in Figure 2 is technically redundant, as there is no way to reach
l2 with the restricted variable values from the initial states. As shown in [18], IISC
does not add this particular guard. However, since both methods are proven to yield
minimally-restrictive supervisors, any extra guards added by PDRC are guaranteed not
to affect the behaviour of the final system.
The gain, on the other hand, is that one does not need to unroll the whole path from
the initial state to the forbidden state in order to supervise it. Consider: each such error
path must have a “point of no return”—the last controllable transition. When synthesising for safety, this transition must never be left enabled (our proof of Theorem 3 hinges
upon this). In order to find this point, PDRC traverses only the path between the point
of no return and the forbidden state, whereas IISC traverses the whole path. In a sense,
PDRC does not care about how one might end up close to forbidden state, but only
where to put up the fence.
In practice, our results have IISC outperforming PDRC on both PDE and CMT.
We believe the main reason is that unlike IISC which uses IC3 extended to SMT [3],

14

our implementation of PDRC works in SAT. This means that while both algorithms
are theoretically equipped to abstract away large swathes of the state space, IISC does it
much easier on integer variables than PDRC, which needs to e.g. represent each possible
value of a variable as a separate gate.
The one point where PDRC succeeds also in practice is on the PME problem. Here,
most of the system’s complexity comes from the number of different locations across
the synchronised automata, rather than from large variable domains. In order to further
explore this difference in problem type, we would have liked to evaluate PDRC and
IISC on more problems with more synchronised automata, such as EDP(10,10). Sadly,
this was impossible since the IISC implementation is no longer maintained.

8 Conclusions and Future Work
We have presented PDRC, an algorithm for controller synthesis of discrete event systems with uncontrollable transitions, based on property-driven reachability. The algorithm is proven to terminate on all solvable problem instances, and its synthesised controllers are proven to be safe and minimally restrictive. We have also implemented a
prototype in the SAT-based model checker Tip. Our experiments show that even this
SAT-based implementation outperforms a comparable BDD-based approach, but not
the more recent IISC. However, since the implementation of IISC we compare against
uses an SMT solver, not to mention that it is not maintained anymore, we must declare
the algorithm-level comparison inconclusive.
The clearest direction for future research would be to implement PDRC using an
SMT solver, to see if this indeed does realise further potential of the algorithm like we
believe. Both [3] and [9] provide good insights for this task. However, another interesting direction is to use both PDRC and IISC as a starting point to tackling the larger
problem: safe and nonblocking controller synthesis. Expanding the problem domain
like this cannot be done by a trivial change to PDRC, but hopefully the insights from
this work can contribute to a new algorithm. Another technique to draw from is that
of IICTL [7]. As discussed in Section 2.2, by restricting our problem to only safety,
we remove ourselves from real-world applications. For this reason, we do not present
PDRC as a contender for any sort of throne, but as a stepping stone towards the real
goal: formal, symbolic synthesis and verification of discrete supervisory control.

REFERENCES

15

References

[1] Armin Biere. AIGER. 2014. URL: http://fmv.jku.at/aiger/ (visited
on 07/24/2017).
[2] Aaron R. Bradley. “SAT-Based Model Checking without Unrolling”. In: Verification, Model Checking, and Abstract Interpretation: 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings. Ed. by
Ranjit Jhala and David Schmidt. Berlin, Heidelberg: Springer Berlin Heidelberg,
2011, pp. 70–87. ISBN: 978-3-642-18275-4. DOI: 10.1007/978-3-642-18275-4_7.
[3] Alessandro Cimatti and Alberto Griggio. “Software Model Checking via IC3”.
In: Computer Aided Verification: 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings. Ed. by P. Madhusudan and Sanjit
A. Seshia. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012, pp. 277–293.
ISBN : 978-3-642-31424-7. DOI: 10.1007/978-3-642-31424-7_23.
[4] Niklas Eén, Alan Mishchenko, and Robert Brayton. “Efficient Implementation
of Property Directed Reachability”. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design. FMCAD ’11. Austin,
Texas: FMCAD Inc, 2011, pp. 125–134. ISBN: 978-0-9835678-1-3. URL: http://dl.acm.org/citation.
[5] Niklas Eén and Niklas Sörensson. “Temporal Induction by Incremental SAT
Solving”. In: Electronic Notes in Theoretical Computer Science 89.4 (2003),
pp. 543–560. ISSN: 1571-0661. DOI: http://dx.doi.org/10.1016/S1571-0661(05)82542-3.
[6] Z. Fei et al. “A symbolic approach to large-scale discrete event systems modeled
as finite automata with variables”. In: 2012 IEEE International Conference on
Automation Science and Engineering (CASE). Aug. 2012, pp. 502–507. DOI:
10.1109/CoASE.2012.6386479.
[7] Zyad Hassan, Aaron R. Bradley, and Fabio Somenzi. “Incremental, Inductive
CTL Model Checking”. In: Proceedings of the 24th International Conference on
Computer Aided Verification. CAV’12. Springer-Verlag, 2012, pp. 532–547.
[8] C. A. R. Hoare. Communicating Sequential Processes. Upper Saddle River, NJ,
USA: Prentice-Hall, Inc., 1985. ISBN: 0-13-153271-5.
[9] Kryštof Hoder and Nikolaj Bjørner. “Generalized Property Directed Reachability”. In: Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing. SAT’12. Trento, Italy: Springer-Verlag, 2012,
pp. 157–171. ISBN: 978-3-642-31611-1. DOI: 10.1007/978-3-642-31612-8_13.
[10] John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation (3rd Edition). Boston, MA, USA:
Addison-Wesley Longman Publishing Co., Inc., 2006. ISBN: 0321462254.
[11] R. Kumar, V. Garg, and S. I. Marcus. “Predicates and predicate transformers for
supervisory control of discrete event dynamical systems”. In: IEEE Transactions
on Automatic Control 38.2 (Feb. 1993), pp. 232–247. ISSN: 0018-9286. DOI:
10.1109/9.250512.
[12] R. J. Leduc, M. Lawford, and W. M. Wonham. “Hierarchical interface-based
supervisory control-part II: parallel case”. In: IEEE Transactions on Automatic
Control 50.9 (Sept. 2005), pp. 1336–1348. ISSN: 0018-9286. DOI: 10.1109/TAC.2005.854612.
[13] Robi Malik. Waters/Supremica IDE. 2014. URL: http://www.cs.waikato.ac.nz/˜robi/download_w
(visited on 07/24/2017).

16

REFERENCES

[14] S. Miremadi, B. Lennartson, and K. Akesson. “A BDD-Based Approach for
Modeling Plant and Supervisor by Extended Finite Automata”. In: IEEE Transactions on Control Systems Technology 20.6 (Nov. 2012), pp. 1421–1435. ISSN:
1063-6536. DOI: 10.1109/TCST.2011.2167150.
[15] Sajed Miremadi, Knut Akesson, et al. “Solving two supervisory control benchmark problems using Supremica”. In: 2008 9th International Workshop on Discrete Event Systems. May 2008, pp. 131–136. DOI: 10.1109/WODES.2008.4605934.
[16] P.J. Ramadge and W.M. Wonham. “The control of discrete event systems”. In:
Proceedings of the IEEE, Special Issue on Discrete Event Dynamic Systems 77.1
(1989), pp. 81–98. ISSN: 0018-9219.
[17] Mohammad Reza Shoaei. Incremental and Hierarchical Deadlock-Free Control
of Discrete Event Systems with Variables: A Symbolic and Inductive Approach.
PhD thesis, Series 3827. Chalmers University of Technology, Dept. of Signals
and Systems, Automation, 2015, pp. 44–45. ISBN: 978-91-7597-146-9.
[18] Mohammad Reza Shoaei, Laura Kovács, and Bengt Lennartson. “Supervisory
Control of Discrete-Event Systems via IC3”. In: Hardware and Software: Verification and Testing: 10th International Haifa Verification Conference, HVC 2014,
Haifa, Israel, November 18-20, 2014. Proceedings. Ed. by Eran Yahav. Springer
International Publishing, 2014, pp. 252–266.

