# Regular Languages and Automata

The domain of languages and automata encompasses three concrete models, **finite state automata**, **regular expressions** and **linear temporal logic**. They are described separately below.

## Regular Expressions (RegEx)

Regular expressions are discussed in Section 2 of the reader 'Languages'.

### Example

`regular expression re = a + b* . d`

### Syntax RegEx

The syntax of a regular expression always starts with `regular expression <name> =`

. After that, the actual regular expression is written.
Regular expressions are constructed from the following primitives and operators (see the reader):

- the empty set, which is denoted by
`\o`

; - the empty word, which is denoted by
`\e`

; - a symbol from the alphabet is either written by a single upper or lower case letter, such as
`a`

or`Z`

, or an arbitrary sequence of characters, placed between single or double quotes, e.g.,`'.'`

or`"'"`

; - the union of two or more expressions is written by placing the
`+`

symbol between them; - the concatenation of two or more expressions is written by placing the
`.`

symbol between them; - the Kleene closure of a regular expression is written with the
`*`

symbol behind it. - for ω-regular expressions, the indefinite repetition of a regular expression is written with the
`**`

symbols behind it. - parentheses can be used to group expressions, e.g.,
`(a+b)**`

; without parentheses, the order of priority of operators is: Kleene star. ω repetition, concatenation, union.

`where`

clauses can be used to introduce short hand to avoid a lot of repetition of similar subexpressions.

```
regular expression number = @Digit . @Digit* . '.' . @Digit . @Digit*
where Digit = '0' + '1' +'2' +'3' +'4' +'5' +'6' +'7' +'8' +'9'
```

It is used as in the following example. `where`

is added after the expression, followed by a list of definitions of the form `<name> = <regular expression>`

. `@`

followed by the name of a definitions refers to the regular expression of the definition. The regular expressions can in turn use references to their definitions, but definitions cannot be cyclic.

### Operations RegEx

In the workbench, regular expressions support the following operations.

*Convert to FSA*, which converts the regular expression to a non-deterministic finite state automaton that accepts the same language.*Convert ω Regular Expression to NBA*- converts an ω-regular expression to a non-deterministic Büchi automaton (NBA) that accepts the same language;

### Finite State Automata (FSA)

Finite State Automata on finite words are discussed in Section 2 of the reader 'Languages'. Finite State Automata on infinite words, $\omega$-automata or Büchi automata are discussed in Section 4 of that reader.

### Example FSA

```
finite state automaton Model {
S [initial] -- a ----> T [final]
T -- a;b --> S
}
```

### Syntax FSA

Finite State Automata are a graph-like structure and the discussion about syntax of graphs applies.
The syntax of a finite state automaton always starts with `finite state automaton <name> {`

. It ends with a closing curly bracket `}`

.
The core of the description of the FSA is in the form of transitions `S -- a --> T`

. Transitions are labelled with symbols from the alphabet of the FSA (`a`

in the example). A transition without a symbol represents an $\epsilon$ transition. A transition can be labelled with multiple symbols separated by commas, for example `S -- a, b, # --> T`

. This is a short-hand notation for a transition for each of the symbols. In this case, `#`

can be used for an $\epsilon$ transition.

Symbol names are combinations of letters, numbers and the underscore character `_`

that start with a letter. Additionally, arbitrary symbol names can be written by enclosing the name with single or double quotation marks.

State names follow the same requirements, but have the additional possibility of using tuple-like (such as `(S,T)`

) or set-like (such as `{S,t}`

) notation. These can also be mixed arbitrarily, recursively, so that `({A,B},{X,Y})`

is also a valid state name. **It is important to note that in the set-like notation, state names are still compared literally** `{A,B}`

is not the same as `{B,A}`

States can have different annotations to denote if the state is an initial state or a final (accepting) state.
For example, `S [initial; final]`

denotes that `S`

is both an initial state and a final state. Annotations are separated by semicolon `;`

. `final`

can be abbreviated to `f`

. `initial`

can be abbreviated to `i`

and the enclosing square brackets are optional, so `S f;i`

is also valid. Annotations do not need to be repeated every time a state is mentioned, but can be added anywhere.

Generalized acceptance conditions can de specified by adding a label after the `final`

label, e.g., `S final[A]`

, `T final[A,B]`

defines two acceptance sets A = {`S`

,`T`

} and B = {`T`

}. If the model has additional final states that are not labelled with a named acceptance set, then those states together also for a separate acceptance set.

Occasionally there is a need to add states to an FSA that have no adjacent transitions. In that case, unconnected states can be added by adding the keyword `states`

at the end of the description followed by a list of states (possibly including annotations), such as in the following model.

```
finite state automaton A {
S --> T
states U V W f;i
}
```

### Operations FSA

The following operations can be performed on FSA models.

*Convert to DFA*- converts a non-deterministic automaton (NFA) to a deterministic automaton (DFA);*Eliminate $\epsilon$*- eliminates all $\epsilon$ transitions from an NFA;*Make Complete*- make the automaton complete, by adding transitions and a state where needed to make sure that every states has an outgoing transition for every symbol of the alphabet; non-deterministic automata (NFA) are first converted to a DFA.*Check for Emptiness*- analyze if the language defined by the automaton, interpreted as an automaton on finite words is empty or not;

*Synchronous Product*- compute the synchronous product between two automata on finite words. Automata are**not allowed**to take transitions without synchronization on symbols that are not present in the alphabet of the other automaton;

*Complement*- compute the complement of the automaton on finite words;*Check Word Acceptance*- analyze if a given word is accepted by the automaton on finite words;*Check Determinism*- check if the automaton is deterministic;*Determine Alphabet*- determine the alphabet of the automaton;*Check Language Inclusion*- check if the language of one automaton on finite words is included in the language of another automaton;*Minimize*- minimize an automaton. Tries to find a smaller automaton that accepts the same language. Note that it does not necessarily give the smallest possible automaton that accepts the same language;*Relabel States*- replace the state labels of an automaton with labels of the form`S`

followed by a number;*Convert to Regular Expression*- converts the automaton on finite words into a regular expression that defines the same language.

#### Operations NBA

The following operations can be performed on FSA models that represent Büchi automata.

*Check for Emptiness NBA*- analyze if the language defined by the automaton, interpreted as an automaton on infinite words is empty or not;*Synchronous Product NBA*- compute the synchronous product between two automata on infinite words. Automata are**not allowed**to take transitions without synchronization on symbols that are not present in the alphabet of the other automaton;*Minimize*- minimize an automaton. Tries to find a smaller automaton that accepts the same language. Note that it does not necessarily give the smallest possible automaton that accepts the same language;

## Linear Temporal Logic (LTL)

Linear Temporal Logic is discussed in Section 5 of the reader 'Languages'.

### Example LTL

`ltl formula phi = G a => X ((not a) U b)`

### Syntax LTL

The syntax of LTL formulas always starts with `ltl formula <name> =`

. After that, the actual formula is written.
LTL formulas are constructed from the following primitives and operators (see the reader):

- the literals,
`true`

and`false`

; - atomic propositions, e.g.,
`p`

; - conjunctions, formulas joined by the keyword
`and`

, e.g.,`p and q and r`

; - disjunctions, formulas joined by the keyword
`or`

, e.g.,`p or q and r`

; - the until operator
`U`

, e.g.,`p U q`

; - the release operator
`R`

, e.g.,`p R q`

; - the next operator
`X`

, e.g.,`X p`

; - the eventually operator
`F`

, e.g.,`F p`

; - the always operator
`G`

, e.g.,`G p`

; - the negation operator
`not`

, e.g.,`not X q`

; - the implication
`=>`

, e.g.,`p => X not p`

. - parentheses can be used to group expressions, e.g.,
`p and (q or r)`

; without parentheses, the order of priority of operators is: negation, always, eventually, next, implication (which is right-associative), release, until, conjunction, disjunction.

The formula is optionally followed by a definition of the alphabet considered for the language of the formula, for example:

`alphabet {a, b, c}`

If no alphabet is explicitly specified, the alphabet is assumed to consist of all symbols mentioned in the definition

Finally, an optional `where`

clauses can be used to introduce the atomic propositions. It uses the syntax

```
where
p = {a, b}
q = {c}
```

The example above defines the àtomic proposition `p`

to refer to the set of symbols including `a`

and `b`

.
If an atomic proposition `p`

in a formula is not defined in the `where`

clause, it is assumed to be defined as `p = {p}`

.

### Operations LTL

In the workbench, LTL formulas support a single operation, `convert to FSA`

, which converts the formula to a non-deterministic finite state automaton that accepts the same language.