Previous chapter: Automata-based LTL Model Checking
This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner
As an illustration of how automata can be used to represent system behaviors, we consider the representation of sequential circuits to safety automata. For a more general discussion of how to represent different types of systems, such as protocols or software, we refer the reader to textbooks on model checking, such as “Principles of Model Checking” by Baier and Katoen.
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