Innovative

Model Checking: How is everything connected Introduction This is the final blog in our series on Model Checking. Since we now have knowledge of typical modelling techniques (mainly Kripke structures) and property specification (using LTL and CTL), we are ready to understand how to check the correctness of properties in a given model. Verification of LTL Formulas Intersection of Büchi Automata For two Büchi automata (B) and (B’), we can build a Büchi automaton for the intersection of their (omega)-languages. The construction is similar to that of finite automata, where the resulting automaton’s states are pairs of states from both automata. This is also similar to the synchronous product of Kripke structures discussed in the previous blog. The algorithm is defined as follows: Input: Two Büchi automata (B = (Q, Sigma, delta, Q_0, F)) and (B’ = (Q’, Sigma, delta’, Q’_0, F’)). Construct a new Büchi automaton (B_{cap}) whose state space is (Q times Q’). The initial states are all pairs ((q, q’)) where (q in Q_0) and (q’ in Q’_0). The transition relation is defined synchronously: ((q, q’) xrightarrow{a} (r, r’)) if (q xrightarrow{a} r) in (B) and (q’ xrightarrow{a} r’) in (B’). The set of accepting states is (F times F’). Return the Büchi automaton (B_{cap}). Emptiness Problem on Büchi Automata Checking whether a Büchi automaton can produce any (omega)-word at all is often called the emptiness problem. This is an efficient algorithm that traverses the automaton and checks for the existence of a lasso with at least one accepting state in its cycle. A lasso is a path from an initial state to a state that is reachable from itself. The algorithm for checking whether a Büchi automaton is empty is given by: Input: A Büchi automaton (B = (Q, Sigma, delta, Q_0, F)). Compute the set of states reachable from the initial states (Q_0). Compute the strongly connected components (SCCs) of the reachable subgraph. Check whether there exists an SCC that contains at least one accepting state from (F) and at least one cycle. If such an SCC exists, return non-empty. Otherwise, return empty. LTL Model Checking In the previous blog, we discussed the transformation of both LTL formulae and Kripke structures into Büchi automata. These transformations form the core of LTL model checking. Let us assume that we have the automata (B_M) for the model and (B_{varphi}) for the LTL formula (varphi). Checking the property on the model is equivalent to proving that the language of all possible paths generated by the model is a subset of the language generated by the formula. In other words, every execution of the model satisfies the property: [ L(B_M) subseteq L(B_{varphi}) ] This can be rewritten as: [ L(B_M) cap overline{L(B_{varphi})} = emptyset ] Using this formulation, the LTL model checking algorithm can be defined as follows: Input: A Kripke structure (M) and an LTL formula (varphi). Build the Büchi automaton (B_M) for the model (M). Build the Büchi automaton (B_{varphi}) for the LTL formula (varphi). Construct the complement (overline{B_{varphi}}) (using Safra’s construction, later optimized by Piterman). Build the intersection of (B_M) and (overline{B_{varphi}}). Check whether the resulting Büchi automaton generates any word. Return whether (B_M cap overline{B_{varphi}}) is empty. However, the construction in step 4 is expensive and often infeasible for large models, as it has a worst-case complexity of (2^{O(n log n)}). For this reason, practical model checkers avoid explicit complementation. Instead, we build the Büchi automaton for the negated formula (lnot varphi), leading to a more efficient algorithm: Input: A Kripke structure (M) and an LTL formula (varphi). Build the Büchi automaton (B_M) for the model (M). Build the Büchi automaton (B_{lnot varphi}) for the LTL formula (lnot varphi). Build the intersection of (B_M) and (B_{lnot varphi}). Check whether the resulting Büchi automaton generates any word. Return whether (B_M cap B_{lnot varphi}) is empty. Verification of CTL Formulas Unlike LTL, CTL model checking is performed directly on the Kripke structure without translating formulas into automata. CTL formulas are evaluated using graph-based algorithms that rely on fixpoint computations, strongly connected components, and backward reachability. The following two algorithms are examples for CTL Model Checking, where the output are all the states on which the formula holds. Checking if a Kripke structure satisfies a CTL property is then checking if an initial state is in the set of the returned states. EG Operator The formula (EG , varphi) holds in a state if there exists a path starting from that state such that (varphi) holds globally along the entire path. Compute the set of states that satisfy (varphi). Restrict the Kripke structure to these states. Compute the strongly connected components of the restricted graph. Mark states that belong to SCCs containing a cycle. Return all states that can reach such SCCs. EU Operator The formula (varphi , EU , psi) holds in a state if there exists a path where (psi) eventually holds and (varphi) holds at all preceding states. Initialize a set with all states that satisfy (psi). Iteratively add states that satisfy (varphi) and have a transition to a state already in the set. Repeat until a fixpoint is reached. Return the resulting set of states. Conclusion Model checking provides a powerful and fully automated technique for verifying complex systems, especially in security-critical and safety-critical domains. By rigorously exploring all possible executions, it can uncover subtle errors that are difficult to detect through testing alone. Understanding the theoretical foundations behind model checking, including automata theory and temporal logic, allows practitioners to better appreciate its strengths, limitations, and practical optimizations. This knowledge is essential for effectively applying model checking to real-world systems. Previous Post Popular Posts Probabilistic Generative Models Overview Gaussian Mixture Models Explained Top 7 AI writing tools for Engineering Students Top AI Posting Tools Every Engineering Student Should Use to Be Innovative Without Design Skills Living in Germany as Engineering Student : Why is it hard living in Germany without speaking German?

What does Computational Tree Logic (CTL) do? 1. Introduction To define the model’s properties, we used LTL in the previous blog. Yet, can we express something like: “There is a possibility that (p) stays always true”? The short answer is NO. The long answer is, however, this blog itself, where we look at another logic used in Model Checking: Computational Tree Logic (CTL). 2. Why is LTL not enough? We take the following Kripke structure and the property we want to define: “There is a possibility that (p) stays always true”. Clearly, the given Kripke structure satisfies that property for the path (s_0, s_1, s_1, s_1, dots) However, using only LTL, we cannot define this property correctly because LTL works on all possible paths and not on some of them. Here, (G,p) is an incorrect suggestion, since(p) is not always satisfied on all paths (not in (s_0, s_2, s_2, s_2, dots)). What we want to express is rather something like: (exists) Path (P) such that: (P models G,p) which we generally write as: (P models EG,p) This is exactly the syntax of Computational Tree Logic (CTL). 3. Computational Tree Logic (CTL) 3.1 Definition of syntax Similar to LTL formulas, we define CTL over a set of atomic propositions (AP) as one of the following expressions: True and False (like LTL) (p in AP): a propositional variable (varphi lor psi) where (varphi) and (psi) are CTL formulas (lnot varphi) where (varphi) is a CTL formula (EX,varphi) (exists next) (varphi EU psi) (exists until) (EG,varphi) (exists globally) 3.2 Definition of semantics 3.2.1 Computational Trees While LTL is evaluated over a single path of a Kripke structure, CTL is evaluated over a tree containing all possible paths starting at a state. For instance, take the following Kripke structure: Then the computational tree of ( s_0 ) is defined as follows (The tree is infinite) 3.2.2 Semantics A CTL formula is evaluated to true/false over the computational tree of a Kripke structure. For a Kripke structure (M) and state (s_0), we write ((M, s_0) models psi) when the computational tree starting at (s_0) satisfies (psi). (M, s_0 models True) always holds. (M, s_0 models False) never holds. (M, s_0 models p) exactly when (p in L(s_0)) (M, s_0 models varphi lor psi) if (M, s_0 models varphi) or (M, s_0 models psi) (M, s_0 models lnot varphi) if (M, s_0 notmodels varphi) (M, s_0 models EX,varphi) if (exists s’) with ((s_0, s’) in R) and (M, s’ models varphi), i.e. it holds exactly when at least one of the next states of ( s_0 ) satisfies ( varphi ) (M, s_0 models varphi EU psi) if (exists k ge 0) and a path (s_0, s_1, dots) such that:[forall i,; 0 le i < k: M, s_i models varphiquadtext{and}quadM, s_k models psi]In other words, there must be way for ( psi) to eventually hold, and for ( varphi )  to hold at every state before the first time ( psi) holds. In particular, if ( psi)  already holds at the s0, then ( varphi , EU , psi) holds immediately. (M, s_0 models EG,varphi) if (exists) a path (s_0, s_1, dots) such that (forall i ge 0, M, s_i models varphi) That is exactly what we wanted to describe previously as „There is a possibility that (varphi)  stays always true “. 3.3 Syntactic sugar Similar to LTL, we define further operators for CTL to help us deal directly with more complex situations while making it still readable. This includes mainly the operators EF, AF, AG and AU. Like the “E” prefix stans for “Exists”, A stands for “All”. Notation Meaning Derived from (varphi land psi) Both hold (lnot(lnot varphi lor lnot psi)) (varphi rightarrow psi) If (varphi) then (psi) (lnot varphi lor psi) (EF,varphi) Eventually holds in some path (True EU varphi) (AF,varphi) Eventually holds in all paths (lnot EG,lnot varphi) (AG,varphi) Always holds in all reachable states (lnot EF,lnot varphi) (varphi AU psi) Until holds for all paths ( ((lnot psi) , EU , lnot (varphi lor psi)) land EG , (lnot psi) ) 3.4. Examples We take the same Kripke structure as the previous blog. Decide whether each of the following CTL formulae hold. 3.4.1. The Kripke structure: 3.4.2. The formulae: (F_1 = AF,p) (F_2 = EG,p) (F_3 = EX,q) (F_4 = EX,EG,q) (F_5 = EX,AF(lnot p land lnot q)) (F_6 = AF,EG,q) (F_7 = EX,lnot p) (F_8 = AG,EF,p) (F_9 = EF,AG,q) (F_{10} = AX,AX,(EG,q Rightarrow lnot p)) (F_{11} = (p land q); E,U; (p land lnot q)) (F_{12} = AXbigl((AX,p); A,U; (AX,q)bigr)) 3.4.3. Solution and explanation Formula Truth value Explanation (F_1) True “In all paths, (p) will eventually hold,” which is true because (p) holds in the initial state. (F_2) True “There is a path at which (p) will always hold” is true for the path (s_0, s_1, s_0, s_1, s_0, s_1, dots). (F_3) False “(q) holds in one of the next states” is false as all the next states do not contain (q) in their labels. (F_4) False “There is one path starting at one of the next states at which (q) will always hold.” This is false because (q) does not hold at any of the next states. (F_5) True “There is a next state at which all paths will reach a state where neither (p) nor (q) holds.” This is true because (s_3) is always reachable from any state. (F_6) True “We reach in all possible paths a state from which at least a path will satisfy (q) forever.” The state we can reach is (s_2), from which we can stay at (s_2) forever, meaning that (EG,q) holds at that state. As this state is always reachable, the expression is true. (F_7) True “One of the next states does not satisfy (p)” is true for the next state being (s_3). (F_8) True “In all possible paths it will always hold that we can reach a state where (p) holds.” This is true because all the states are able to reach

Model Checking: Learn Linear Temporal Logic (LTL) 1. Introduction While our previous blog post focused mainly on the different models used in Model Checking (Kripke structures, Labelled Transition Systems and Program Graphs), this blog focuses only on Kripke structures. One reason is that we can transform the other models into a Kripke structure as well. The transformations needed will, however, be discussed in detail in later posts. Our focus in this post is to study the properties of a system. For instance, how can one tell if a system does what it should actually do? For that, we first need to define what we mean by “the system should do so-and-so.” This definition of properties is in general easier to verify on Kripke structures. The automatic verification process will be reserved for a later blog. Our main focus in this post is one way fr defining the property’s syntax and semantics: The Linear Time Logic (LTL). 2. Why not typical Propositional or Predicate Logic? The main reason is that these types of logics generally lack information that we want to express about our model. For instance, suppose we have the model of an elevator and we want to check the property “The elevator will eventually run out-of-service.” This is hard to define in propositional or predicate logic because of their lack of temporal information: they describe how the system is now, but not how it will eventually be in the future. This motivates the need for a more sophisticated type of logic that can express what will happen to our system over time. This is where Linear Temporal Logic (LTL) and Computational Tree Logic (CTL) come into the picture. Our focus in this blog will be Linear Temporal Logic, and we reserve the next blog to study CTL and its difference to LTL. 3. Linear Temproal Logic (LTL) 3.1. Definition of syntax Every LTL formula over a set of atomic propositions AP is defined as one of the following expressions: True (similar to propositional/predicate logic) False (similar to propositional/predicate logic) p ∈ AP: a propositional variable (similar to propositional logic) ϕ ∨ ψ (the OR operator, similar to propositional logic), where ϕ and ψ are LTL formulas ¬ϕ (the NOT operator, similar to propositional logic), where ϕ is an LTL formula Xϕ (sometimes written as ∘ϕ), where ϕ is an LTL formula. The X operator is called “next.” ϕ U ψ, where ϕ and ψ are LTL formulas. The U operator is called “until.” 3.2. Definition of semantics An LTL formula is evaluated (to True/False) over a single path of a Kripke structure. For a path P = (s_0 s_1 s_2 s_3 dots) we write P ⊨ ψ when the path P satisfies the LTL formula ψ. Satisfaction is defined recursively over the syntax of LTL formulas: P ⊨ True always holds. P ⊨ False never holds (also written as P ⊭ False). P ⊨ p holds exactly when (p in L(s_0)), i.e. when p holds at the first state of the path. P ⊨ ϕ ∨ ψ holds exactly when P ⊨ ϕ or P ⊨ ψ (at least one of the formulas holds). P ⊨ ¬ϕ holds exactly when P ⊭ ϕ. P ⊨ Xϕ holds exactly when the suffix path (s_1 s_2 s_3 dots) satisfies ϕ (i.e. the next operator checks the property starting at the next state). P ⊨ ϕ U ψ holds exactly when there exists an (i in mathbb{N} cup {0}) such that:for all (0 le k < i): the suffix (s_k s_{k+1} s_{k+2} dots ⊨ ϕ), and at position (i) we have the suffix (s_i s_{i+1} dots ⊨ ψ). In other words, ψ must eventually hold, and ϕ must hold at every state before the first time ψ holds. Informally, the path looks like (ϕϕϕ dots ϕψ text{True True True} dots). In particular, if ψ already holds at the beginning, then ϕ U ψ holds immediately. We say that an LTL formula holds in a state of a Kripke structure if it holds on all possible paths starting at that state. We say it holds on the Kripke structure if it holds on all of its initial states. 3.3. Syntactic sugar Other operators in LTL are derived from the basic syntax. The following table summarizes commonly used derived operators, their meaning, and their derivation from the original LTL syntax. Our focus, however, will be on F, G, X, and U. Notation Explanation Derived from ϕ ∧ ψ And: both ϕ and ψ must hold now. ¬(¬ϕ ∨ ¬ψ) ϕ → ψ Implication: if ϕ holds now, then ψ holds now. ¬ϕ ∨ ψ F ϕ Finally: ϕ must hold eventually (at some future point). True U ϕ G ϕ Globally: ϕ must hold on all states of the path. ¬(F ¬ϕ) ψ W ϕ Weak until: ψ must hold at least until ϕ; if ϕ never becomes true, ψ must remain true forever. (G ϕ) ∨ (ψ U ϕ) ψ M ϕ Strong release: ϕ must be true until and including the point where ψ first becomes true, which must hold at the current or a future position. ¬(¬ψ W ¬ϕ) ψ R ϕ Release: ϕ must be true until and including the point where ψ first becomes true; if ψ never becomes true, ϕ must remain true forever. ϕ W (ϕ ∧ ψ) While combinations of these operators can get complex, two commonly used combinations are: GF ψ: ψ holds infinitely many times. For example, GF idle expresses that an elevator always becomes idle infinitely often (it cannot stay moving forever). FG ψ: ψ will hold forever from some point onward (not necessarily now). For example, FG oos expresses that the elevator will eventually become out-of-service and remain out-of-service forever. 3.4. Examples We take the following Kripke structure and decide whether each of the following LTL formulae holds. 3.4.1. The Kripke structure: 3.4.2. The formulae: (F_1 = Fp) (F_2 = F(neg p land neg q)) (F_3 = Gp) (F_4 = X

Model Checking: How to model my system? Introduction As the goal of this series is to learn how model checking works and how it helps us check the correctness of models, our first step is to define the model of our system. This clearly requires a full understanding of the system and its components. In general, one would like to see the model in front of their eyes to check if it satisfies the system’s properties and requirements. On the other hand, one would not like to exaggerate the description of the system to the point where it becomes more complex than our brain can process. This is why, in general, one defines independent components without their actual interaction with the other components. Then, using our brain delegate, the computer, we can connect those interacting components into one big model. In this blog, we will investigate the data structures used in modelling and the possible “combination techniques” which allow the generation of our model from the smaller interactive components. Kripke structures Kripke structures are transition systems in the form of directed graphs which allow the modelling of a system using states and propositions. Formally, for a given set of propositions (i.e. Boolean variables), a Kripke structure is defined as a tuple of: A set of states S A set of initial states I A set of edges, called transitions R. Each transition is a directed edge going from one state to another. A labelling function L, i.e. a mapping from states to proposition sets. The labelling of a state characterizes it by the fact that every proposition in the labelling is true and every other is false. For example, for a set of propositions {a, b, c}, at the state s labelled by L(s) = {a}, only the proposition a holds; b and c do not. To understand this structure more, we can directly start with an example. An elevator in a building with 3 floors (including the ground floor) can be working or out of service, and can be at one of the floors 1, 2, or 3. With this information, we can define the set of propositions: AP = {w, f1, f2, f3} where w represents the proposition “Elevator is working” and each fi represents the proposition “Elevator is at floor i”. With that, one can model the elevator with the following Kripke structure. The model defines 6 states, s1 to s6. We directly wrote the labelling of each state (the corresponding proposition set) within the state in the given diagram. We suppose that the elevator is initially working without knowing its current position. This is why we defined the states s1, s2, and s3 as initial states. The states s4 to s6 represent the out-of-service elevator states which can happen at any floor. We suppose, in our case, that the failure is permanent, i.e. it cannot cure by itself once it happens. This is the reason we only have a loop for the elevator at these states, as they can only stay at the same floor and can never become working again. A path produced by a Kripke structure is an infinite list of states, starting with an initial state and only moving to one of the states to which it is connected. In our example, the path s2, s3, s3, s2, s3, s3, s1, s4, s4, s4… is produced by the given Kripke structure. This is, however, not the case for the path s1, s2, s3, s1, s4, s4… because we cannot move from s3 to s1 directly. An execution is the infinite list of labels of a path. For example, for s1, s2, s3, s1, s4, s4…, we have the execution {w,f1}{w,f2}{w,f3}{w,f1}{f1}{f1}{f1}… Transition systems A (labelled) transition system (LTS) is very similar to a Kripke structure except for one big point of difference: an LTS defines the properties/actions of the model on its transitions, while a Kripke structure defines them on the states. Again, an LTS is defined as a tuple of: A set of states S A set of initial states A set of actions A A set of edges, called transitions R. Each transition is a directed edge going from one state to another and is labelled with an action. There are special edges connected directly to the initial states and are only labelled with guards which are the conditions that the graph must satisfy if it starts at that state. An LTS concentrates more on the dynamics of the system, i.e. how, when, and under which conditions it actually changes, instead of what should hold at each state. To model our previous example as an LTS, we define the set of actions A = {goto1, goto2, goto3, oos} (oos stands for out-of-service) and initial s1, and define it as follows: A path produced by an LTS is, again, a valid infinite list of states. An execution is an infinite list of actions that is valid in our LTS. For example, s1, s2, s3, s2, s3, s2, s3… is a path produced by our example LTS. The execution [goto1][goto2][goto1]… is not valid in our LTS as s1, our initial state, cannot execute the action goto1. Program Graphs Although program graphs are harder to define, they are in general the most intuitive ones to use when you model your system. This is especially the case when you have parallel subsystems interacting with each other, yet able to run some of their subtasks independently. Imagine having three independent elevators that can work. Modelling this system is a challenge, as each state must contain information on all elevators at the same time. Let’s do some computation: Each elevator can be in one of 6 states (as in the example Kripke structure), which means that their combination will have 6*6*6 = 216 states! You can see that looking at such a Kripke structure and probably looking for a mistake you made while modelling could be hell, especially given the fact that this resulting Kripke structure will

Model Checking: Essential Logic and Automata Theory You Need to Know In today’s interconnected world, the reliability and safety of software and hardware systems are paramount. From autonomous vehicles to medical devices and critical infrastructure, a single flaw can have catastrophic consequences. This is where Model Checking comes in: a powerful set of techniques designed to systematically verify the correctness of systems, ensuring they behave exactly as intended, every single time. This blog post marks the beginning of our comprehensive series on Model Checking. We’ll embark on a journey from foundational concepts to practical applications, equipping you with the knowledge to understand and implement these vital verification methods. In this post, we’ll lay the groundwork by exploring the core theoretical pillars that underpin model checking: the principles of logic, formal verification and automata theory. Get ready to master how we can build truly robust and hazard-free systems! 1. Logic Logic is the field of mathematics responsible for studying Boolean expressions, i.e., expressions which can either be true or false. Simple examples are “the weather is hot” and “I love you”. Although studying those sorts of phrases is not optimal for mathematicians, logic is still one of the core branches and is very widely used in different engineering fields, especially electrical and computer engineering, but also in computer science. One differs mainly between propositional logic, which consists of the known Boolean operators (especially AND, OR and NOT) and of Boolean variables called propositions. An example of a propositional logical formula is: [ (p text{ OR } (text{NOT } q)) text{ AND } p. ] The second important type of logic is predicate logic. This is widely seen as the general version of propositional logic, where the variables are not necessarily Booleans, but can be of any sort. In addition, we have, other than the Boolean operands, the quantifiers ( forall ) (forall) and ( exists) (there exists). Lemmas and axioms in mathematics are mostly written in predicate logic. For example, we can define a sort called Group, a constant ( e ) of the sort Group, an operation (*), and then use the Group Axioms to define the relations between elements of the Group: ( forall x. exists y. space space x * y = e ) ( forall x. forall y. forall z. space space x * (y * z) = (x * y) * z ) (forall x. space space x * e = x ) 2. Formal Verification Given a formula in propositional logic, it is generally easy to prove or disprove its validity using a set of rules. For predicate logic, this gets harder as one has to define a set of axioms, which in many cases can contradict each other, leading to all the rules to be false. For axioms that do not contradict each other (called consistent), one can prove, with enough knowledge, if a formula is true. One can extrapolate the formal verification to programs, where one can study a program’s properties and its states. This includes the values of some of its variables, the termination of the program and the correctness of a returned value. This enriches the propositional logic by other operands, such as the diamond operator (langle.rangle), which tells for a program (p) and a formula (phi): [ langle p rangle phi text{ is true}] [text{ if and only if} ] [ p text{ always terminates and } phi text{ holds after the program } p text{ terminates} ] 3. Model Checking Model Checking is the study of a modeled system for correctness and safety constraints. In many safety-critical systems (aircrafts, robots, railway crossings…), modeling the system and proving its safety criteria always hold is a critical step, because: Testing the system itself instead of a model has extremely high costs. Imagine having to test a railway crossing by driving a train and cars in different situations, each with the possibility to lead to a collision. Testing the system a few (or even many) times cannot be considered safe, as long as there is no warranty that the model cannot lead to an issue in a rare case that only appears under very specific conditions (especially if there are parallel tasks involved). This is why the main role of model checking is ensuring a hazard-free system in all possible cases. For this, model checking defines two other types of logic to define the changes happening inside a model at different steps. As computers only handle discrete values and structures and cannot work with continuous values (like real numbers), model checking runs on discretized times. The two logics are called Linear Time Logic and Computation Tree Logic and will be discussed in detail in the next blogs of this model checking series. 4. Automata and Languages In computer science, we define an alphabet as a finite set of characters, a word as a string composed of these characters, and a language as a set of such words. For example: (A = {a, b}) is an alphabet. “aab”, “bb”, “a” and the empty word “” are all words over (A). (L = {“aab”, “bba”, “a”, “”}) and (L’ = {w mid w text{ word over } A text{ that starts with an } a}) are languages over (A). Deterministic Finite Automata (DFAs) One of the main cores of theoretical computer science are automata, which can be used in various use cases, including pattern matching (this is the case with regular expressions, for example, where we only want to validate strings having a special form), compiler building (where we want to build a syntax tree from a given code to generate its machine code version) as well as model checking. For the sake of simplicity, we define in this blog Deterministic Finite Automata (DFAs) only. These are directed graphs, where the nodes are called states and the edges are called transitions. Each transition is annotated with a letter, and some of the states are marked and in that case they are called final

Diffusion models are a class of generative models that learn to generate complex data (like images) by reversing a gradual, simple process of adding Gaussian noise to the training data. The process involves two stages: a fixed forward diffusion process (adding noise) and a learned reverse diffusion process (denoising).

Generative Adversarial Networks GANs are a class of generative models that learns to produce new data instances with the same characteristics as the training data through a game-theoretic scenario (a minimax game) between two competing neural networks: a generator and a discriminator.

Normalizing Flows are a class of probabilistic generative models that builds a complex probability distribution by passing a simple base distribution (like a standard Gaussian) through a sequence of invertible, differentiable transformations (the “flow”). The model learns the parameters of these transformations.

A Variational Autoencoder (VAE) is a generative model that learns a compressed, continuous representation (a latent space) of data. It consists of an encoder network that maps data to a distribution in the latent space and a decoder network that reconstructs data from samples drawn from that latent distribution.