TLA in Pictures.
Predicate-action diagrams, which are similar to standard state-transition diagrams, are precisely defined as formulas of TLA (the Temporal Logic of Actions). We explain how these diagrams can be used to describe aspects of a specificationand those descriptions then proved correcteven when the complete specification cannot be written as a diagram. We also use the diagrams to illustrate proofs.
Introduction
Pictures aid understanding. A simple flowchart is easier
to understand than the equivalent programming-language
text. However, complex pictures are confusing. A large,
spaghetti-like flowchart is harder to understand than a
properly structured program text.
Pictures are inadequate for specifying complex systems,
but they can help us understand particular aspects of a
system. For a picture to provide more than an informal
comment, there must be a formal connection between the
complete specification and the picture. The assertion that
the picture is a correct description of (some aspect of) the
system must be a precise mathematical statement.
We use TLA (the Temporal Logic of Actions) to specify
systems. In TLA, a specification is a logical formula describing
all possible correct behaviors of the system. As an
aid to understanding TLA formulas, we introduce here a
type of picture called a predicate-action diagram. These diagrams
are similar to the various kinds of state-transition
diagrams that have been used for years to describe sys-
tems, starting with Mealy and Moore machines [1], [2]. We
relate these pictures to TLA specifications by interpreting
a predicate-action diagram as a TLA formula. A diagram
denoting formula D is a correct description of a system
with specification S iff (if and only if) S implies D. We
therefore provide a precise statement of what it means for
a diagram to describe a specification.
We use predicate-action diagrams in three ways that we
believe are new for a precisely defined formal notation:
ffl To describe aspects of a specification even when it is
not feasible to write the complete specification as a
diagram.
ffl To draw different diagrams that provide complementary
views of the same system.
ffl To illustrate formal correctness proofs.
Section II is a brief review of TLA; a more leisurely introduction
to TLA appears in [3]. Section III describes
predicate-action diagrams, using an n-input Muller C-element
as an example. It shows how diagrams are used to
describe aspects of a complete specification, and to provide
complementary views of a system. Section IV gives another
example of how predicate-action diagrams are used to describe
a system, and shows how they are used to illustrate
a proof.
II. TLA
We now describe the syntax and semantics of TLA. The
description is illustrated with the formulas defined in Figure
1. (The symbol \Delta
means equals by definition.)
We assume an infinite set of variables (such as x and
y) and a class of semantic values. Our variables are the
flexible variables of temporal logic, which are analogous to
variables in a programming language. TLA also includes
the rigid variables of predicate logic, which are analogous
to constant parameters of a program, but we ignore them
here. The class of values includes numbers, strings, sets,
and functions.
A state is an assignment of values to variables. A behavior
is an infinite sequence of states. Semantically, a TLA
formula is true or false of a behavior. Syntactically, TLA
formulas are built up from state functions using Boolean
operators (:, -, ) [implication], and j [equivalence])
and the operators 0 and 2, as described below. TLA also
has a hiding operator 999 999, which we do not use here.
A state function is a nonBoolean expression built from
variables, constants, and constant operators. Semantically,
it assigns a value to each state-for example assigns
to state s one plus the value that s assigns to the variable
x. A state predicate (often called just a predicate) is
a Boolean expression built from variables, constants, and
constant operators such as +. Semantically, it is true or
false for a state-for example the predicate Init \Phi is true of
state s iff s assigns the value zero to both x and y.
An action is a Boolean expression containing primed and
unprimed variables. Semantically, an action is true or false
of a pair of states, with primed variables referring to the
second state-for example, action M 1 is true for hs; ti iff
the value that state t assigns to x equals one plus the value
that state s assigns to x, and the values assigned to y by
states s and t are equal. A pair of states satisfying an
action A is called an A step. Thus, an M 1 step is one that
increments x by one and leaves y unchanged.
If f is a state function or state predicate, we write f 0
for the expression obtained by priming all the variables of
f . For example
\Phi equals
0). For an action A and a state function v,
Init \Phi
Fig. 1. The TLA formula \Phi describing a simple program that repeatedly
increments x or y.
we define [A] v to equal A- (v so a [A] v step is either
an A step or a step that leaves the value of v unchanged.
Thus, a [M 1
step is one that increments x by one and
leaves y unchanged, or else leaves the ordered pair hx; yi
unchanged. Since a tuple is unchanged iff each component
is unchanged, a [M 1
step is one that increments x by
one and leaves y unchanged, or else leaves both x and y
unchanged. We define hAi v to equal A - (v 0 6= v), so an
step is an M 1 step that changes x or y. Since an
unchanged, an hM 1 i hx;yi
step is a step
that increments x by 1, changes the value of x, and leaves
y unchanged.
We say that an action A is enabled in state s iff there
exists a state t such that hs; ti is an A step. For example,
M 1 is enabled iff it is possible to take a step that increments
x by one, changes x, and leaves y unchanged. Since
natural number x, action hM 1 i hx;yi
is
enabled in any state in which x is a natural number. If
is not enabled in a state
in which x equals 1.
A TLA formula is true or false of a behavior. A predicate
is true of a behavior iff it is true of the first state. An action
is true of a behavior iff it is true of the first pair of states.
As usual in temporal logic, if F is a formula then 2F is
the formula meaning that F is always true. Thus, 2Init OE
is true of a behavior iff x and y equal zero for every state in
the behavior. The formula 2[M] hx;yi
is true of a behavior
iff each step (pair of successive states) of the behavior is a
step.
Using 2 and "enabled" predicates, we can define fairness
operators WF and SF. The
asserts of a behavior that there are infinitely many hAi v
steps, or there are infinitely many states in which hAi v is
not enabled. In other words, WF v (A) asserts that if hAi v
becomes enabled forever, then infinitely many hAi v steps
occur. The strong fairness formula SF v (A) asserts that either
there are infinitely many hAi v steps, or there are only
finitely many states in which hAi v is enabled. In other
words, asserts that if hAi v is enabled infinitely of-
ten, then infinitely many hAi v steps occur.
The standard form of a TLA specification is Init -
Init is a predicate, N is an action, v
is a state function, and L is a conjunction of fairness con-
ditions. This formula asserts of a behavior that (i) Init is
true for the initial state, (ii) every step of the behavior is an
N step or leaves v unchanged, and (iii) L holds. Formula
\Phi of

Figure

1 is in this form, asserting that (i) initially x
and y both equal zero, (ii) every step either increments x
by one and leaves y unchanged, increments y by one and
leaves x unchanged, or leaves both x and y unchanged, and
(iii) the fairness condition WF hx; yi
holds. Formula WF hx; yi (M 1 ) asserts that there are infinitely
many
steps or hM 1 i hx;yi
is infinitely
often not enabled. Since (i) and (ii) imply that x is
always a natural number, hM 1 i hx;yi
is always enabled.
Hence, WF hx; yi (M 1 ) implies that there are infinitely many
steps, so x is incremented infinitely often. Simi-
larly, WF hx; yi (M 2 ) implies that y is incremented infinitely
r
e
l
e
e
out
Fig. 2. A Muller C-element.
often. Putting this all together, we see that \Phi is true
of a behavior iff (i) x and y are initially zero, (ii) every
step increments either x or y by one and leaves the other
unchanged or else leaves both x and y unchanged, and
(iii) both x and y are incremented infinitely many times.
The formula Init - 2[N ] v is a safety property [4]. It
describes what steps are allowed, but it does not require
anything to happen. (The formula is satisfied by a behavior
satisfying the initial condition in which no variables
ever change.) Fairness conditions are used to specify that
something must happen.
III. Predicate-Action Diagrams
A. An Example
We take as an example a Muller C-element [5]. This is a
circuit with n binary inputs one binary
output out , as shown in Figure 2. As the figure indicates,
we are considering the closed system consisting of the C-element
together with its environment. Initially, all the
inputs and the output are equal. The output becomes 0
when all the inputs are 0, and it becomes 1 when all the
inputs are 1. After an input changes, it must remain stable
until the output changes.
The behavior of a 2-input C-element and its environment
is described by the predicate-action diagram of Figure 3(a),
where C is defined by
The short arrows, with no originating node, identify the
nodes labeled C(0; 0; 0) and C(1; 1; 1) as initial nodes.
They indicate that the C-element starts in a state satisfying
1). The arrows connecting nodes
indicate possible state transitions. For example, from a
state satisfying C(1; 1; 1), it is possible for the system
to go to a state satisfying either C(0; 1; 1) or C(1; 0; 1).
More precisely, these arrows indicate all steps in which
the triple hin[1]; in[2]; outi changes-that is, transitions in
which at least one of in[1], in[2], and out changes. Steps
that change other variables-for example, variables representing
circuit elements inside the environment-but leave
hin[1]; in[2]; outi unchanged are also possible.
The predicate-action diagram of Figure 3(a) looks like a
standard state-transition diagram. However, we interpret
it formally not as a conventional state machine, but as the
(a) A predicate-action diagram.
\Delta-
AU
A
AU
\Delta-
\Delta-
AU
A
AU
\Delta-
@ @R @ @R
(b) The corresponding TLA formula.
Fig. 3. Predicate-Action diagram of hin[1]; in[2]; outi for a 2-input C-element, and the corresponding TLA formula.
TLA formula of Figure 3(b). 1 This formula has the form
Init is a state predicate and there is
one conjunct F o for each node o. The predicate Init is
Each F describes the possible state
changes starting from a state described by node o. For
example, the formula F o for the node labeled C(1; 1; 0) is
A predicate-action diagram represents a safety property; it
does not include any fairness conditions.

Figure

3(a) is a reasonable way to describe a 2-input
C-element. However, the corresponding diagram for a 3-
input C-element would be quite complicated; and there is
no way to draw such a diagram for an n-input circuit. The
general specification is written directly as a TLA formula
in

Figure

4. The array of inputs is represented formally
by a variable in whose value is a function with domain
brackets denote function applica-
tion. (Formally, n is a rigid variable-one whose value is
constant throughout a behavior.) We introduce two pieces
of notation for representing functions:
denotes the function f with domain S
such that f [i] equals e(i) for every i in S.
ffl [f except denotes the function g that is the
same as f except that g[i] equals e.
The formulas defined in Figure 4 have the following interpretation

Init C A state predicate asserting that out is either 0 or
1, and that in is the function with domain ng
such that in[i] equals out for all i in its domain.
Input(i) An action that is enabled iff in [i] equals out .
It complements in[i], leaves in [j] unchanged for j 6= i,
and leaves out unchanged. (The symbol i is a param-
eter.)
Output An action that is enabled iff all the in[i] are different
from out . It complements out and leaves in
unchanged.
list of formulas bulleted by - or - denotes their conjunction or
disjunction; - and - are also used as ordinary infix operators.
Init C
ng 7! out ]
- in
ng : in [i] 6= out
- in
Next ng : Input(i)
-WF hin ;outi (Output)
Fig. 4. A TLA specification of an n-input C-element.
Next An action that is the disjunction of Output and all
the Input (i) actions, for ng. Thus, a Next
step is either an Output step or an Input(i) step for
some input line i.
\Pi C A temporal formula that is the specification of the
C-element (together with its environment). It asserts
that (i) Init C holds initially, (ii) every step is either
a Next step or else leaves hin ; outi unchanged, and
(iii) Output cannot be enabled forever without an Output
step occurring. The fairness condition (iii) requires
the output to change if all the inputs have; inputs
are not required to change. (Since predicate-action
diagrams describe only safety properties, the fairness
condition is irrelevant to our explanation of the dia-
grams.)
The specification \Pi C is short and precise. However, it is
not as reader-friendly as a predicate-action diagram. We
therefore use diagrams to help explain the specification,
beginning with the predicate-action diagram of Figure 5.
It is a diagram of the state function hin [i]; outi, meaning
that it describes transitions that change hin[i]; outi. It is
a diagram for the formula \Pi C , meaning that it represents
a formula that is implied by \Pi C . The diagram shows the
synchronization between the C-element's ith input and its
output.
We can draw many different predicate-action diagrams
oe
ae
oe
ae
oe
ae
oe
ae
\Omega \Omega \Omega OE J
\Omega \Omega \Omega AE
Fig. 5. A predicate-action diagram of hin[i]; outi for the specification
\Pi C of an n-input C-element, where 1
in
Y
Fig. 6. Another predicate-actiondiagram of hin[i]; outi for \Pi C , where
for the same specification. Figure 6 shows another diagram
of hin [i]; outi for \Pi C . It is simpler than the one in Figure 5,
but it contains less information. It does not indicate that
the values of in[i] and out are always 0 or 1, and it does
not show which variable is changed by each transition. The
latter information is added in the diagram of Figure 7(a),
where each transition is labeled with an action. The label
Input (i) on the left-to-right arrow indicates that a transition
from a state satisfying in out to a state satisfying
in[i] 6= out is an Input(i) step. This diagram represents
the TLA formula of Figure 7(b).
Even more information is conveyed by a predicate-action
diagram of hin; outi, which also shows transitions that leave
in[i] and out unchanged but change in[j] for some j 6= i.
Such a diagram is drawn in Figure 8(a). Figure 8(b) gives
the corresponding TLA formula.
There are innumerable predicate-action diagrams that
can be drawn for a specification. Figure 9 shows yet another
diagram for the C-element specification \Pi C . Since
we are not relying on these diagrams as our specification,
but simply to help explain the specification, we can show as
much or as little information in them as we wish. We can
(a) A predicate-action diagram of hin[i]; outi.
in
Y
Output
(b) The corresponding TLA formula.
Fig. 7. A more informative predicate-action diagram of hin[i]; outi
for \Pi C , and the corresponding TLA formula.
(a) A predicate-action diagram of hin; outi.
in
- in [i] 6= out
Y
Output
U
U
(b) The corresponding TLA formula.
- in
Fig. 8. A predicate-action diagram of hin; outi for \Pi C , and the
corresponding TLA formula, where 1
in
- in [i] 6= out
Y
in
out
U U
Fig. 9. Yet another predicate-action diagram of hin; outi for \Pi C .
draw multiple diagrams to illustrate different aspects of a
system. Actual specifications are written as TLA formulas,
which are much more expressive than pictures.
B. A Formal Treatment
B.1 Definition
We first define precisely the TLA formula represented by
a diagram. Formally, a predicate-action diagram consists
of a directed graph, with a subset of the nodes identified as
initial nodes, where each node is labeled by a state predicate
and each edge is labeled by an action. We assume
a given diagram of a state function v and introduce the
following notation.
N The set of nodes.
I The set of initial nodes.
E(n) The set of edges originating at node n.
d(e) The destination node of edge e.
Pn The predicate labeling node n.
e The action labeling edge e.
The formula \Delta represented by the diagram is defined as
follows.
Init \Delta
An
When no explicit label is attached to an edge e, we take
e to be true. When no set of initial nodes is explicitly
indicated, we take I to be N . With the usual convention
for quantification over an empty set, An is defined to equal
false if there are no edges originating at node n.
B.2 Another Interpretation
Another possible interpretation of the predicate-action
diagram is the formula b
\Delta, defined by
This is perhaps a more obvious interpretation-especially
if the diagram is viewed as a description of a next-state
relation. We now show that \Delta always implies b
\Delta, and that
the converse implication holds if the predicates labeling the
nodes are disjoint.
\Delta.
simple invariance proof, using rule INV1 of [3,

Figure

5, page 888], shows that \Delta implies 2(9 n
We then have:
conjunction and 8, and
is equivalent to
[ by predicate logic, since B ) C implies 2[B]v
holds for all m, n in N with m 6= n, then
implies \Delta.
propositional logic, the hypothesis implies
The result then follows from simple temporal reasoning,
essentially by the reverse of the string of equivalences and
implication used to prove (A).
We usually label the nodes of a predicate-action diagram
with disjoint predicates, in which case (A) and (B) imply
that the interpretations \Delta and b
are equivalent. Diagrams
with nondisjoint node labels may occasionally be useful; \Delta
is the more convenient interpretation of such diagrams.
C. Proving a Predicate-Action Diagram
Saying that a diagram is a predicate-action diagram for
a specification \Pi asserts that \Pi implies the formula \Delta represented
by the diagram. Formula \Pi will usually have the
form Init \Pi - 2[M] u - L, where L is a fairness condition.
To
prove \Pi ) \Delta, we prove:
1. Init \Pi
2. Init \Pi - 2[M] u for each node n.
The first condition is an assertion about predicates; it is
generally easy to prove. To prove the second condition,
one usually finds an invariant Inv such that Init \Pi - 2[M] u
implies 2Inv , so \Pi implies 2[M- Inv ] u . The second condition
is then proved by showing that [M - Inv ] u implies
for each node n. Usually, u and v are tuples
and every component of v is a component of u, so
v. In this case, one need show only
that M-Inv implies [P n for each n. By definition
of An , this means proving
for each node n. This formula asserts that an M step
that starts with Pn and Inv true and changes v is an Em
step that ends in a state satisfying P d(m) , for some edge m
originating at node n.
IV. Illustrating Proofs
In TLA, there is no distinction between a specification
and a property; they are both formulas. Verification means
proving that one formula implies another. A practical, relatively
complete set of rules for proving such implications
is described in [3]. We show here how predicate-action diagrams
can be used to illustrate these proofs. We take as our
example the same one treated in [3], that the specification
\Psi defined in Section IV-A below implies the specification
\Phi defined in Section II above.
A. Another Specification
We define a TLA formula \Psi describing a program with
two processes, each of which repeatedly loops through the
sequence of operations P (sem); increment ; V (sem), where
one process increments x by one and the other increments
y by one. Here, P (sem) and V (sem) denote the usual operations
on a semaphore sem. To describe this program
formally, we introduce a variable pc that indicates the control
state. Each process has three control points, which we
call "a", "b", and "g". (Quotes indicate string values.)
We motivate the definition of \Psi with the three predicate-
action diagrams for \Psi in Figure 10. In these diagrams, the
predicate PC (p; q) asserts that control is at p in process 1
and at q in process 2. Figure 10(a) shows how the control
state changes when the P (sem), V (sem), and increment
actions are performed. Variables other than pc not mentioned
in an edge label are left unchanged by the indicated
steps-for example, steps described by the edge labeled
leave y and sem unchanged-but this is not
asserted by the diagram. The next-state action N is written
as the disjunction N 1 - N 2 of the next-state actions
of each process; and each N i is written as the disjunction
Figure 10(b) illustrates this decomposition.
Finally, the predicate-action diagram of Figure 10(c) describes
how the semaphore variable sem changes.
To write the specification \Psi, we let pc be a function with
domain f1; 2g, with pc[i] indicating where control resides
in process i. The formula PC (p; q) can then be defined by
(a)
\Phi \Phi \Phi \Phi \Phi*
\Upsilon
R
(b)
\Phi \Phi \Phi \Phi \Phi*
\Upsilon
R
(c)
Y
U
Fig. 10. Three predicate-action diagrams of hx;
The semaphore actions P and V are defined by
sem
sem
sem
Missing from Figure 10 are a specification of the initial values
of x and y, which we take to be zero, and a fairness con-
dition. One could augment predicate-action diagrams with
some notation for indicating fairness conditions. However,
the conditions that are easy to represent with a diagram
are not expressive enough to describe the variety of fairness
requirements that arise in practice. The WF and SF formu-
las, which are expressive enough, are not easy to represent
graphically. So, we have not attempted to represent fairness
in our diagrams. We take as the fairness condition for
our specification \Psi strong fairness on the next-state action
N i of each process. The complete definition of \Psi appears
in

Figure

11.
B. An Illustrated Proof
The proof of \Psi ) \Phi is broken into the proof of three
conditions:
1. Init \Psi ) Init \Phi
2. Init \Psi - 2[N
3. \Psi ) WF hx;yi
We illustrate the proofs of conditions 2 and 3 with the
predicate-action diagram of hx; for \Psi in Figure
12, where Q is defined by
and Nat is the set of natural numbers.
First, we must show that the diagram in Figure 12
is a predicate-action diagram for \Psi. This is easy using
the definition in Section III-B.1; no invariant is needed.
For example, the condition to be proved for the node labeled
is that an N step that starts with
true is an M 1 step (one that increments x and
leaves y unchanged) that makes Q 0 ("g"; "a") true. This
follows easily from the definitions of Q and N , since an N
step starting with PC ("b"; "a") true must be a fi 1 step.
To prove condition 2, it suffices to prove that every step
allowed by the diagram of Figure 12 is a [M] hx;yi
step. The
steps not shown explicitly by the diagram are ones that
leave w unchanged. Such steps leave hx; yi unchanged, so
they are [M] hx;yi
steps. The actions labeling all the edges
of the diagram imply [M] hx;yi
, so all the steps shown ex-
7Init \Psi
sem
sem
Fig. 11. The specification \Psi.
\Phi \Phi \Phi \Phi \Phi*
\Upsilon
R
Fig. 12. Another predicate-action diagram of hx;
plicitly by the diagram are also [M] hx;yi
steps. This proves
condition 2.
We now sketch the proof of condition 3. To prove
WF hx;yi
suffices to show that infinitely many
steps occur. We first observe that each of the
predicates labeling a node in the diagram implies that either
enabled. The fairness condition
of \Psi then implies that a behavior cannot remain forever
at any node, but must keep moving through the diagram.
Hence, the behavior must infinitely often pass through
the node. The predicate Q 1 ("a"; "a") implies
that both hN 1 i w and hN 2 i w are enabled. Hence, the fairness
condition implies that infinitely
many hN 1 i w steps and infinitely many hN 2 i w steps must
occur. Action hN 1 i w is enabled only in the three nodes of
the top loop. Taking infinitely many hN 1 i w steps is therefore
possible only by going around the top loop infinitely
many times, which implies that infinitely many M 1 steps
occur, each starting in a state with Q 0 ("b"; "a") true. Since
Nat, an M 1 step starting with
so it is an hM 1 i hx;yi
step.
Hence, infinitely many hM 1 i hx;yi
steps occur. Similarly,
taking infinitely many hN 2 i w steps implies that infinitely
many
steps occur. This completes the proof of
condition 3.
Using the predicate-action diagram does not simplify the
proof. If we were to make the argument given above rigor-
ous, we would go through precisely the same steps as in the
proof described in [3]. However, the diagram does allow us
to visualize the proof, which can help us to understand it.
V. Conclusion
We have described three uses of diagrams that we believe
are new for diagrams with a precise formal semantics:
ffl To describe particular aspects of a complex specification
with a simple diagram. An n-input C-element
cannot be specified with a simple picture. However,
we explained the specification with diagrams describing
the synchronization between the output and each
individual input.
ffl To provide complementary views of the same system.
Diagrams (b) and (c) of Figure 10 look quite different,
but they are diagrams for the same specification.
ffl To illustrate proofs. The disjunction of the predicates
labeling the nodes in Figure 12 equals the invariant I
of the proof in Section 7.2 of [3]. The diagram provides
a graphical representation of the invariance proof.
TLA differs from traditional specification methods in two
important ways. First, all TLA specifications are interpreted
over the same set of states. Instead of assigning
values just to the variables that appear in the specifica-
tion, a state assigns values to all of the infinite number
of variables that can appear in any specification. Second,
TLA specifications are invariant under stuttering. A formula
can neither require nor rule out finite sequences of
steps that do not change any variables mentioned in the
formula. (The state-function subscripts in TLA formulas
are there to guarantee invariance under stuttering.)
These two differences lead to two major differences between
traditional state-transition diagrams and predicate-
action diagrams. In traditional diagrams, each node represents
a single state. Because states in TLA assign values to
an infinite number of variables, it is impossible to describe
a single state with a formula. Any formula can specify
the values of only a finite number of variables. To draw
diagrams of TLA formulas, we let each node represent a
predicate, which describes a set of states. In traditional di-
agrams, every possible state change is indicated by an edge.
Because TLA formulas are invariant under stuttering, we
draw diagrams of particular state functions-usually tuples
of variables.
TLA differs from most specification methods because it
is a logic. It uses simple logical operations like implication
and conjunction instead of more complicated automata-based
notions of simulation and composition [6]. Everything
we have done with predicate-action diagrams can be
done with state-transition diagrams in any purely state-based
formalism. However, conventional formalisms must
use some notion of homomorphism between diagrams to
describe what is expressed in TLA as logical implication.
Most formalisms employing state-transition diagrams are
not purely state-based, but use both states and events.
Nodes represent states, and edges describe input and output
events. The meaning of a diagram is the sequence of
events it allows; the states are effectively hidden. In TLA,
there are only states, not events. Systems are described in
terms of changes to interface variables rather than in terms
of interface events. Variables describing the internal state
are hidden with the existential quantifier 999 999 described in [3].
Changes to any variable, whether internal or interface, can
be indicated by node labels or edge labels. Hence, a purely
state-based approach like TLA allows more flexibility in
how diagrams are drawn than a method based on states
and events.



--R

"A method for synthesizing sequential circuits,"
"Gedanken-experiments on sequential machines,"
"The temporal logic of actions,"
"Defining liveness,"
Introduction to VLSI Systems
"Conjoining specifications,"
--TR

--CTR
M. Lusini , E. Vicario, Engineering the usability of visual formalisms: a case study in real time logics, Proceedings of the working conference on Advanced visual interfaces, May 24-27, 1998, L'Aquila, Italy
Harold Thimbleby, User interface design with matrix algebra, ACM Transactions on Computer-Human Interaction (TOCHI), v.11 n.2, p.181-236, June 2004
Jules Desharnais , Marc Frappier , Ridha Khdri , Ali Mili, Integration of sequential scenarios, ACM SIGSOFT Software Engineering Notes, v.22 n.6, p.310-326, Nov. 1997
Jules Desharnais , Marc Frappier , Ridha Khdri , Ali Mili, Integration of Sequential Scenarios, IEEE Transactions on Software Engineering, v.24 n.9, p.695-708, September 1998
L. E. Moser , Y. S. Ramakrishna , G. Kutty , P. M. Melliar-Smith , L. K. Dillon, A graphical environment for the design of concurrent real-time systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.6 n.1, p.31-79, Jan. 1997
specification;concurrency;state-transition diagrams;temporal logic