This lecture introduces runtime verification using epistemic temporal logic and automata theory. Monitors decide, from partial runtime observations, whether a system run meets or violates a specification.

This lecture aims to give a sense of what verification of neural networks means and to explore its theoretical possibilities and limitations.

The lecture covers basic automata-theoretic concepts and logical formalisms for the modeling and verification of concurrent and distributed systems.

The lecture covers several aspects of weighted automata, including recognizable series, probabilistic finite automata, and weighted logic.