Previous chapter: From Linear Arithmetic to Automata
This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner
In order to find system executions that violate a given LTL formula, we negate the formula and build an automaton that is equivent to the negated formula. For this, we can use the translaton from LTL to alternating automata from Section 7.2 (Construction 7.1) followed by the Miyano-Hayashi translation from alternating Büchi automata to nondeterministic Büchi automata from Section 7.3 (Construction 7.2).
We represent the system executions as a safety automaton, which is then intersected (using Construction 3.2 from Section 3.3) with the Büchi automaton for the negated LTL formula. The actual search for a violating execution then happens as the emptiness check of the resulting Büchi automaton. In the remainder of this section, we first quickly discuss the representation of the system as a safety automaton, using sequential circuits as an example, and then focus on the emptiness check of Büchi automata.
Next chapter: Model Checking Sequential Circuits
Please cite the source for reprints, feel free to verify the sources cited in the article, and point out any errors or lack of clarity of expression. You can comment in the comments section below or email to GreenMeeple@yahoo.com