A Survey of Relevant Literature - The Unknown Component Problem: Theory and Applications - page 88

starting from the seminal papers of the 1960s by Grasselli and Luccio [50, 65], and
then extended in the 1990s to PNDFSMs [32, 67, 143]. A comprehensive survey on
state minimization of FSMs can be found in [66]. Using state minimizers to exploit
the flexibility has two drawbacks: (1) exact state minimization is a computationally
hard problem; (2) reducing the number of states does not guarantee a smaller logic
realization.
The problem of FSM encoding in the context of a network of FSMs is even more
complex than for a monolithic FSM (because symbolic variables may be shared
among components) and it has received up to now scant attention in the literature.
Optimization techniques for sequential circuits at the netlist level are in a more
mature stage than state-based methods, since they achieve good results on large
circuits; however, manipulating symbolic (state-based) information is indispensable
for computing the flexibility of a component in an FSM network. To handle
this issue, Wang proposed in [141] an algorithmic strategy which takes a circuit
implementation as the starting point and computes the flexibility at the symbolic
level, but exploitation is directly at the netlist logic level.

5.1.6 FSM Network Synthesis by WS1S

It is known since the seminal work of Buchi and Elgot in the sixties that regular
languages play a role in decidability questions of formal logic [19]. For instance,
it was shown that WS1S (Weak Second-Order Logic of 1 Successor) is decidable,
because the set of satisfying interpretations of a subformula is represented by a finite
automaton, and so the automaton for a formula can be constructed by induction,
noticing that logical connectives correspond to operations on automata such as
product, projection and subset construction. Validity, satisfiability or unsatisfiability
of a formula can be established by answering questions on the corresponding
automaton. So WS1S can be seen as another notation for regular languages, as
also regular expressions are. WS1S features first-order variables that denote natural
numbers (they can be compared and added to constants), and second-order variables
that denote finite sets of numbers. We sketch next the basic steps that show the
equivalence between WS1S logic and automata [70].
In WS1S any formula can be put in a form where atomic subformulas denoting
either a subset, or a set difference, or a successor relation are operated upon by
logical operators denoting either a negation, or a conjunction, or an existential
quantification.
Given a formula , its semantics is defined inductively relative to a string w
over the alphabet

k ,where

B Df 0;1 g and k is the number of variables in .
Assign to every variable of a unique index i in the range 1;2;:::;k and denote
as P i the variable whose index is i. The interpretation of P i under the string w is
the finite set w .P i / Df j j P i Œj D 1 g ,whereP i Œj D 1 denotes that the j-th
bit in the P i -th track is 1. The notation w ˆ , read w satisfies , means that w
makes true. The inductive construction follows the rules: w

B

6ˆ 0 ; ˆ: iff w