# Hardware Model Checking Algorithms and Techniques
## 2 Background and Notation
### Formal Languages  
A formal language is a mathematical object that describes the syntax of a set of finite _strings_ of _symbols_. A formal language is a purely syntactic tool and can be completely defined without making any reference to an interpretation for its symbols. In the following, we provide some basic notions from the field of _formal language theory_ (we refer the interested reader to [23] for an more in depth discussion on the subject).  
**Definition 1** (Alphabet and Words).: _An alphabet \(\Sigma\) is any non-empty finite set of symbols. A word over \(\Sigma\) is any finite or infinite string of symbols in \(\Sigma\). The set of all finite words over \(\Sigma\) is denoted by \(\Sigma^{*}\) (called the Kleene closure of \(\Sigma\))._  
**Definition 2** (Formal Languages).: _Given an alphabet \(\Sigma\), a formal language \(\mathcal{L}\) over \(\Sigma\) is any set of finite words over \(\Sigma\), i.e., \(\mathcal{L}\subseteq\Sigma^{*}\)._  
A formal language \(\mathcal{L}\) is often described by a set of rules that determine how its words are formed (_rules of formation_). Many formalisms can be used to describe the rules of formation of a formal language, such as formal grammars, regular expressions and automata [23].  
**Definition 3** (Well-formed Formulas).: _Given a formal language \(\mathcal{L}\) over \(\Sigma\), a word \(w\in\Sigma^{*}\) is said to be a well-formed formula of \(\mathcal{L}\), often abbreviated with \(\mathrm{wff}\), iff \(w\in\mathcal{L}\)._  
Note that a formal language can be identified with the set of its well-formed formulas. Throughout the rest of this paper, we simply use the term _formula_ to refer to a well-formed formula of a given formal language.  
Formal languages are entirely syntactic in nature but may be given interpretations that provide meaning to their symbols and sentences. Given a formal language \(\mathcal{L}\), from the semantic standpoint, the symbols of \(\mathcal{L}\) may be subdivided into logical symbols and non-logical symbols.  
**Definition 4** (Logical Symbols).: _A symbol of a formal language is said to be a logical symbol if it always has the same meaning, independently from the language interpretation._  
Examples of logical symbols in the context of propositional and first-order logic are logical connectives (\(\
eg\), \(\wedge\), \(\vee\), etc.), quantifiers (\(\forall\), \(\exists\), etc.) and the equality predicate (\(=\)).  
**Definition 5** (Non-logical Symbols and Signature).: _A symbol of a formal language is said to be a non-logical symbol if it has a meaning only when one is assigned to it by means of a language interpretation. Given a formal language \(\mathcal{L}\), its signature \(\sigma\) is defined as the set of its non-logical symbols._  
Note that non-logical symbols may have different meanings under different language interpretations. Examples of non-logical symbols in the context of propositional and first-order logic are variables and symbols for constants, function and relation.  
A fundamental problem in formal language theory is that of determining the membership of a given word in a formal language.  
**Definition 6** (Membership Problem).: _Given a formal language \(\mathcal{L}\) and a word \(w\in\Sigma^{*}\), the membership problem is the problem to determine whether \(w\in\mathcal{L}\), i.e., whether \(w\) is a \(\mathrm{wff}\) of \(\mathcal{L}\)._  
As we show later in Section 2.6, each problem in the important computational class of _decision problems_ can be represented as a membership problem for a formal language. SAT-based model checking algorithms encode state reachability problems, defined on a model of the system, as instances of a particular decision problem known as Boolean Satisfiability (SAT).