Introduction to Logic and Automatic Verification

Author

Your Name

Published

February 5, 2025

Introduction

This lecture introduces the fundamental concepts of logic and automatic verification. The primary goal is to understand how logic can be used as a precise mathematical language to specify properties of systems, particularly in the context of computer science. We will explore the importance of formal methods in verifying system correctness and the role of automata in modeling system behavior. Key topics include the distinction between testing and automatic verification, the concept of a model, the definition of system behavior, and the model checking problem.

Logic as a Formal Language: We will see how logic provides a precise and unambiguous way to express properties of systems, in contrast to the inherent ambiguity of natural language.
Formal Methods and Verification: We will discuss the limitations of traditional testing methods and the need for formal methods that provide exhaustive verification of system correctness.
Automatic Verification: The lecture will introduce automatic verification as a set of techniques that use computers to perform exhaustive checks, ensuring no case is missed and reducing human error.
Models and Automata: We will learn how to abstract complex systems into simplified models using finite automata, which are finite graphs representing system states and transitions.
System Behavior: The concept of system behavior will be defined as the set of all possible computations or sequences of actions that a system can execute.
Model Checking Problem: Finally, we will introduce the model checking problem, which is the core computational problem of determining whether all behaviors of a model satisfy a given specification expressed as a logical formula.

The lecture will also touch upon historical examples of system failures due to inadequate verification, highlighting the practical importance of the concepts discussed. We will see how these concepts are interconnected and lay the foundation for more advanced topics in automatic verification and formal methods.

Why Logic?

Logic serves as a precise mathematical language to formalize statements about systems. Unlike natural language, which is inherently ambiguous, logic provides a rigorous framework for expressing properties and reasoning about systems.

Precision: Logic eliminates ambiguity, ensuring that statements about systems are clear and unambiguous.
Generality: Logic is versatile, applicable to expressing system properties, proving theorems, and more. It’s a general tool that can be used in many different contexts.
Succinctness: Logical formulas are concise, yet capable of expressing complex properties. They allow us to say a lot with a little.

There are many different logical formalisms, and we will see three or four during the course. These are classical logics, but you should keep in mind that there are hundreds of variations and dialects of logic.

Formal Methods and Verification

Formal methods provide mathematically robust techniques for specifying and verifying systems. Verification ensures that a system behaves correctly under all possible scenarios, which is crucial for critical applications. It’s about checking that the system does what it’s supposed to do, in all cases.

Testing vs. Verification:
- Testing: Involves checking specific cases. It is inherently incomplete as it cannot cover all possible behaviors. You can test a system a million times, but there’s always a chance you missed a case.
- Verification: Aims to provide exhaustive checks, ensuring no case is missed. It’s like testing, but done in a way that guarantees you’ve considered every possibility.
Automatic Verification: Uses computers to perform exhaustive checks automatically, reducing human error and increasing efficiency. We let the computer do the hard work of checking all cases, so we don’t have to.

Historical Examples of Failures

Several historical examples highlight the consequences of inadequate verification. These examples show us what can go wrong when we don’t verify systems properly:

Intel Pentium Bug (1994): A flaw in the floating-point division algorithm led to incorrect results. This cost Intel over half a billion dollars. The bug was in the hardware, and it caused errors in calculations. It was a tiny error, but it could propagate and cause big problems in simulations and other applications.
Ariane 5 Rocket Explosion: An integer overflow error caused the rocket to explode shortly after launch. This was a software error that could have been caught with better verification techniques.
Financial Trading Algorithms: Errors in automatic trading algorithms have led to significant financial losses. These algorithms are very complex, and if there’s a bug, it can cause a lot of damage very quickly.

These examples underscore the need for rigorous verification methods in various domains. They show that the cost of not verifying a system can be enormous, both in terms of money and safety. Automatic verification can help us avoid these kinds of errors.

Models and Automata

Models

A model is a mathematical abstraction of a system or program. It simplifies a complex system into a manageable form for analysis and verification. Think of it as a simplified representation that captures the essential aspects of the system.

Definition 1 (Model). A model is a mathematical abstraction of a system, often represented as a finite automaton or a finite graph. Other terms used are Kripke structure* or Labeled Transition System.*

Finite Automata

A finite automaton is a finite graph used to model the behavior of a system. It consists of nodes (states) representing system configurations and edges (transitions) representing computation steps. The main idea is that we can represent the possible states of a system as nodes in a graph, and the possible transitions between states as edges.

States (Nodes): Represent configurations of the system. Each node corresponds to a specific state the system can be in.
Transitions (Edges): Represent single computation steps or actions. An edge from one node to another means that the system can move from one state to another.
Labels: Represent events or actions that trigger transitions. The labels tell us what event or action caused the transition.
Initial State: The state where the system starts. It is usually marked with an incoming arrow.
Final States: States that represent successful termination or acceptance. They are usually marked with a double circle.

Definition 2 (Labeled Transition System). A labeled transition system is a synonym for a finite automaton, emphasizing the labels on transitions that denote events or actions.

A finite state machine is equivalent to a finite automaton. It’s a system with a finite number of states and transitions, meaning it can only be in a finite number of configurations.

Example: Coffee Machine

Consider a simplified model of a coffee machine. This is a very abstract example, but it helps us understand the basic concepts:

States: Different configurations of the machine (e.g., initial state, after inserting 10 cents, after inserting 5 cents).
Transitions: Actions like inserting coins, pressing the reset button, or dispensing coffee.
Labels: Events such as "10 cents", "5 cents", "reset", "coffee". These are the events that can happen in our coffee machine.

In this example, S0 is the initial state. The machine can take 10 cents (A) or 5 cents transitions. From S1, we can only take a reset (B) transition back to S0. From S2, we can take a 10 cents (A) transition to S3. From S3, we can only take a coffee (C) transition, which loops back to S3.

Note: This is a simplified example. A real coffee machine would be more complex, with more states and transitions. Also, the choice between 10 cents or 5 cents is made by the user (the environment), not the machine. We are treating internal and external events the same way for simplicity, but later we will make a distinction.

System Behavior and Computations

Behavior

The behavior of a system is defined as a sequence of actions or events that the system can execute. It is modeled as a path through the automaton. The behavior is what the system does, not what it is.

Definition 3 (Behavior/Computation). A behavior or computation is a sequence of transitions starting from the initial state, representing a possible execution of the system. It can be either a finite or infinite sequence of transitions.

Finite Behavior: A sequence of actions that has a finite length.
Infinite Behavior: A sequence of actions that has an infinite length, it does not terminate.

Example of Behavior

For the coffee machine, an example of a finite behavior is: \[\text{10 cents} \rightarrow \text{reset} \rightarrow \text{5 cents} \rightarrow \text{10 cents} \rightarrow \text{coffee}\] This corresponds to the path $S0 \rightarrow S1 \rightarrow S0 \rightarrow S2 \rightarrow S3$. Another example of a finite behavior could be: \[\text{10 cents} \rightarrow \text{reset}\] This corresponds to the path $S0 \rightarrow S1 \rightarrow S0$.

An example of an infinite behavior could be: \[\text{10 cents} \rightarrow \text{reset} \rightarrow \text{10 cents} \rightarrow \text{reset} \rightarrow \text{10 cents} \rightarrow \text{reset} \rightarrow \dots\] This corresponds to the infinite path $S0 \rightarrow S1 \rightarrow S0 \rightarrow S1 \rightarrow S0 \rightarrow S1 \rightarrow \dots$

If we abstract away the events by letters, e.g., A for 10 cents, B for reset, and C for coffee, the first example of a finite behavior becomes the string ABAC. The second example becomes AB. The infinite behavior becomes ABABAB...

Language

The set of all possible behaviors of a system is called its language. It’s the set of all the things the system can do.

Definition 4 (Language). A language is a set of strings (sequences of symbols) representing all possible behaviors of a system.

Regular Language: A language recognized by a finite automaton. These are the simplest kind of languages we will consider. They correspond to systems with finite memory.
Context-Free Language: A language recognized by a pushdown automaton (automaton with a stack). These languages are more complex than regular languages. They correspond to systems with a memory that can grow arbitrarily large (the stack).

Regular languages are a fundamental concept in computer science. You might have encountered them when using regular expressions (regex). Regular expressions are another way to describe regular languages.

In this course, we will mostly consider finite state automata and regular languages. The set of behaviors of a finite state automaton is a regular language. The semantics of an automaton is the language it recognizes.

Specifications and Formulas

Specifications

A specification is a property that we want to verify about the system’s behavior. It is formalized using logical formulas. The specification describes what we expect the system to do, or not do. It’s a way of saying what’s correct and what’s not.

Formulas

A formula is a statement in a logical formalism that expresses a property of the system’s behavior. Formulas are built using logical connectives and temporal operators.

Boolean Connectives: Operators like AND ($\land$), OR ($\lor$), NOT ($\neg$). These are used to combine simpler formulas into more complex ones. For example, if we have a formula $\phi$ that says "the light is on" and a formula $\psi$ that says "the door is open", we can combine them to form a new formula $\phi \land \psi$ that says "the light is on and the door is open".
Temporal Operators: Operators that describe properties over time, such as "until" ($U$). These operators allow us to talk about how the system’s behavior evolves over time. For example, we might want to say that "the light will stay on until the door is closed".

Example Formula

Consider the formula: \[\text{(10 cents} \lor \text{5 cents}) \, U \, (\text{coffee} \lor \text{reset} \lor \text{kick})\] This formula states that either a "10 cents" or "5 cents" event will occur until a "coffee", "reset", or "kick" event happens. In other words, the machine will keep accepting 10 or 5 cents coins until one of the events "coffee", "reset", or "kick" occurs. The "until" operator has a temporal aspect: it says something about what happens before something else happens.

Let’s break down the example formula:

$(10 \text{ cents} \lor 5 \text{ cents})$: This part says that either a "10 cents" event or a "5 cents" event will occur. The $\lor$ symbol means "or".
$(\text{coffee} \lor \text{reset} \lor \text{kick})$: This part says that a "coffee" event, a "reset" event, or a "kick" event will happen.
$U$: This is the "until" operator. It connects the two parts of the formula and says that the first part will be true until the second part becomes true.

This is an example of a property we might want to verify about our coffee machine. We want to make sure that the machine behaves according to this specification. This formula is written in a mix of natural language and logical notation. Later, we will learn how to write formulas in a purely formal way.

Model Checking Problem

Definition

The model checking problem is the computational problem of determining whether all behaviors of a model satisfy a given formula. It’s about checking if the system, as represented by the model, always does what it’s supposed to do according to the specification.

Definition 5 (Model Checking Problem). Given a model $M$ and a formula $\phi$, determine whether all behaviors of $M$ satisfy $\phi$.

This is a computational problem, meaning we want an algorithm that can solve it automatically. We want to be able to give the model and the formula to a computer and have it tell us whether the model satisfies the formula or not.

Approach

To solve the model checking problem, we can negate the formula and check for the existence of a violating behavior. This is often easier than directly checking that all behaviors satisfy the formula. The idea is that if we can’t find a behavior that violates the formula, then all behaviors must satisfy it.

Original Question: Do all computations satisfy $\phi$? This is a universally quantified question.
Negated Question: Does there exist a computation that satisfies $\neg \phi$? This is an existentially quantified question.

Checking for the existence of something is usually easier than checking that something holds for all cases.

The reason we negate the formula is that it transforms a universal quantification (for all) into an existential quantification (there exists). Existential quantifications are generally easier to handle algorithmically.

Example

For the formula $\phi = (10 \text{ cents} \lor 5 \text{ cents}) \, U \, (\text{coffee} \lor \text{reset} \lor \text{kick})$, the negation is $\neg \phi = \square (10 \text{ cents} \lor 5 \text{ cents})$, meaning "forever 10 cents or 5 cents".

Example Explanation: If the original formula $\phi$ says that "10 cents or 5 cents will happen until coffee, reset, or kick", the negation $\neg \phi$ says that it’s not the case that "10 cents or 5 cents will happen until coffee, reset, or kick". This can be rephrased as "there exists a behavior where 10 cents or 5 cents happens forever, and coffee, reset, or kick never happens". In this particular case, we can express this with the $\square$ (always) operator as $\neg \phi = \square (10 \text{ cents} \lor 5 \text{ cents})$.

Important Note: The precise negation of the "until" ($U$) operator depends on the specific temporal logic being used. In some logics, the negation might involve other temporal operators. We will learn more about how to negate formulas in later lectures. The teacher will provide a more detailed explanation of how to systematically derive the negation of temporal logic formulas.

Solving the Model Checking Problem

One way to solve the model checking problem is to:

Negate the formula $\phi$ to get $\neg \phi$.
Construct an automaton $A_{\neg \phi}$ that accepts all behaviors satisfying $\neg \phi$.
Check if the intersection of the language of the model $M$ and the language of the automaton $A_{\neg \phi}$ is empty.

If the intersection is empty, it means there are no behaviors that satisfy $\neg \phi$, which means all behaviors satisfy $\phi$. If the intersection is not empty, it means there is at least one behavior that satisfies $\neg \phi$, which means not all behaviors satisfy $\phi$. In this case, we can also provide a counterexample, which is a behavior that violates the original formula.

Input: Model $M$, Formula $\phi$ Output: "Yes" if $M$ satisfies $\phi$, "No" otherwise $\neg \phi \gets \text{negate}(\phi)$ $A_{\neg \phi} \gets \text{constructAutomaton}(\neg \phi)$ $L(M) \gets \text{language}(M)$ $L(A_{\neg \phi}) \gets \text{language}(A_{\neg \phi})$ "Yes" "No"

Complexity Analysis (Conceptual):

Line [alg:line:negate]: Negating the formula can usually be done in linear time in the size of the formula.
Line [alg:line:construct]: Constructing the automaton for the negated formula can be exponential in the size of the formula in the worst case.
Lines [alg:line:language] and [alg:line:language2]: Computing the language of an automaton can be done in linear time in the size of the automaton.
Line [alg:line:intersection]: Checking the intersection of two languages can be done in time proportional to the product of the sizes of the automata.

The overall complexity is dominated by the construction of the automaton for the negated formula, which can be exponential.

Note: This is a high-level overview of the algorithm. The actual implementation involves many details that we will cover in later lectures.

Conclusion

This lecture introduced the foundational concepts of logic, formal verification, and automata theory. We explored how models abstract systems, how behaviors represent system executions, and how formulas specify desired properties. The model checking problem was presented as a key computational problem in verifying system correctness. We learned that:

Logic provides a precise language for specifying properties of systems.
Formal methods, particularly automatic verification, offer a way to ensure system correctness beyond what is possible with traditional testing.
Automata theory provides a framework for modeling systems and their behaviors.
The model checking problem is a central problem in automatic verification, and it can be solved algorithmically.

Follow-up Questions:

How can we derive the negation of temporal logic formulas systematically? This is important for applying the model checking approach we outlined.
What are the different types of temporal logic operators and their semantics? We’ve seen the "until" operator, but there are many others. Understanding their meaning is crucial for writing meaningful specifications.
How can we implement an algorithm to solve the model checking problem for a given model and formula? We’ve seen a conceptual algorithm, but the actual implementation requires more detail.
What are the limitations of finite state automata in modeling real-world systems, and how can we extend them? Finite state automata are powerful, but they have limitations. We might need more expressive models for certain systems.
How can we use these techniques in practice? What are some real-world applications of automatic verification?

Remark: Understanding these concepts is crucial for further study in automatic verification and formal methods. The next lecture will delve deeper into temporal logic and model checking algorithms. We will also discuss different types of temporal logic and their applications.

--- title: "Introduction to Logic and Automatic Verification" author: "Your Name" date: "2025-02-05" format: html: toc: true # Table of Contents toc-depth: 2 code-tools: true theme: cosmo # Or "journal" for Distill-like minimalism --- # Introduction This lecture introduces the fundamental concepts of logic and automatic verification. The primary goal is to understand how logic can be used as a precise mathematical language to specify properties of systems, particularly in the context of computer science. We will explore the importance of formal methods in verifying system correctness and the role of automata in modeling system behavior. Key topics include the distinction between testing and automatic verification, the concept of a model, the definition of system behavior, and the model checking problem. - **Logic as a Formal Language**: We will see how logic provides a precise and unambiguous way to express properties of systems, in contrast to the inherent ambiguity of natural language. - **Formal Methods and Verification**: We will discuss the limitations of traditional testing methods and the need for formal methods that provide exhaustive verification of system correctness. - **Automatic Verification**: The lecture will introduce automatic verification as a set of techniques that use computers to perform exhaustive checks, ensuring no case is missed and reducing human error. - **Models and Automata**: We will learn how to abstract complex systems into simplified models using finite automata, which are finite graphs representing system states and transitions. - **System Behavior**: The concept of system behavior will be defined as the set of all possible computations or sequences of actions that a system can execute. - **Model Checking Problem**: Finally, we will introduce the model checking problem, which is the core computational problem of determining whether all behaviors of a model satisfy a given specification expressed as a logical formula. The lecture will also touch upon historical examples of system failures due to inadequate verification, highlighting the practical importance of the concepts discussed. We will see how these concepts are interconnected and lay the foundation for more advanced topics in automatic verification and formal methods. # Why Logic? Logic serves as a precise mathematical language to formalize statements about systems. Unlike natural language, which is inherently ambiguous, logic provides a rigorous framework for expressing properties and reasoning about systems. - **Precision**: Logic eliminates ambiguity, ensuring that statements about systems are clear and unambiguous. - **Generality**: Logic is versatile, applicable to expressing system properties, proving theorems, and more. It's a general tool that can be used in many different contexts. - **Succinctness**: Logical formulas are concise, yet capable of expressing complex properties. They allow us to say a lot with a little. There are many different logical formalisms, and we will see three or four during the course. These are classical logics, but you should keep in mind that there are hundreds of variations and dialects of logic. ## Formal Methods and Verification Formal methods provide mathematically robust techniques for specifying and verifying systems. **Verification** ensures that a system behaves correctly under all possible scenarios, which is crucial for critical applications. It's about checking that the system does what it's supposed to do, in all cases. - **Testing vs. Verification**: - **Testing**: Involves checking specific cases. It is inherently incomplete as it cannot cover all possible behaviors. You can test a system a million times, but there's always a chance you missed a case. - **Verification**: Aims to provide exhaustive checks, ensuring no case is missed. It's like testing, but done in a way that guarantees you've considered every possibility. - **Automatic Verification**: Uses computers to perform exhaustive checks automatically, reducing human error and increasing efficiency. We let the computer do the hard work of checking all cases, so we don't have to. ## Historical Examples of Failures Several historical examples highlight the consequences of inadequate verification. These examples show us what can go wrong when we don't verify systems properly: - **Intel Pentium Bug (1994)**: A flaw in the floating-point division algorithm led to incorrect results. This cost Intel over half a billion dollars. The bug was in the hardware, and it caused errors in calculations. It was a tiny error, but it could propagate and cause big problems in simulations and other applications. - **Ariane 5 Rocket Explosion**: An integer overflow error caused the rocket to explode shortly after launch. This was a software error that could have been caught with better verification techniques. - **Financial Trading Algorithms**: Errors in automatic trading algorithms have led to significant financial losses. These algorithms are very complex, and if there's a bug, it can cause a lot of damage very quickly. ::: tcolorbox These examples underscore the need for rigorous verification methods in various domains. They show that the cost of not verifying a system can be enormous, both in terms of money and safety. Automatic verification can help us avoid these kinds of errors. ::: # Models and Automata ## Models A **model** is a mathematical abstraction of a system or program. It simplifies a complex system into a manageable form for analysis and verification. Think of it as a simplified representation that captures the essential aspects of the system. :::: tcolorbox ::: definition **Definition 1** (Model). *A model is a mathematical abstraction of a system, often represented as a finite automaton or a finite graph. Other terms used are *Kripke structure* or *Labeled Transition System*.* ::: :::: ## Finite Automata A **finite automaton** is a finite graph used to model the behavior of a system. It consists of nodes (states) representing system configurations and edges (transitions) representing computation steps. The main idea is that we can represent the possible states of a system as nodes in a graph, and the possible transitions between states as edges. - **States (Nodes)**: Represent configurations of the system. Each node corresponds to a specific state the system can be in. - **Transitions (Edges)**: Represent single computation steps or actions. An edge from one node to another means that the system can move from one state to another. - **Labels**: Represent events or actions that trigger transitions. The labels tell us what event or action caused the transition. - **Initial State**: The state where the system starts. It is usually marked with an incoming arrow. - **Final States**: States that represent successful termination or acceptance. They are usually marked with a double circle. :::: tcolorbox ::: definition **Definition 2** (Labeled Transition System). *A labeled transition system is a synonym for a finite automaton, emphasizing the labels on transitions that denote events or actions.* ::: :::: ::: tcolorbox A finite state machine is equivalent to a finite automaton. It's a system with a finite number of states and transitions, meaning it can only be in a finite number of configurations. ::: ## Example: Coffee Machine Consider a simplified model of a coffee machine. This is a very abstract example, but it helps us understand the basic concepts: - **States**: Different configurations of the machine (e.g., initial state, after inserting 10 cents, after inserting 5 cents). - **Transitions**: Actions like inserting coins, pressing the reset button, or dispensing coffee. - **Labels**: Events such as \"10 cents\", \"5 cents\", \"reset\", \"coffee\". These are the events that can happen in our coffee machine. ::: center ::: In this example, S0 is the initial state. The machine can take 10 cents (A) or 5 cents transitions. From S1, we can only take a reset (B) transition back to S0. From S2, we can take a 10 cents (A) transition to S3. From S3, we can only take a coffee (C) transition, which loops back to S3. **Note**: This is a simplified example. A real coffee machine would be more complex, with more states and transitions. Also, the choice between 10 cents or 5 cents is made by the user (the environment), not the machine. We are treating internal and external events the same way for simplicity, but later we will make a distinction. # System Behavior and Computations ## Behavior The **behavior** of a system is defined as a sequence of actions or events that the system can execute. It is modeled as a path through the automaton. The behavior is what the system *does*, not what it *is*. :::: tcolorbox ::: definition **Definition 3** (Behavior/Computation). *A behavior or computation is a sequence of transitions starting from the initial state, representing a possible execution of the system. It can be either a finite or infinite sequence of transitions.* ::: :::: - **Finite Behavior**: A sequence of actions that has a finite length. - **Infinite Behavior**: A sequence of actions that has an infinite length, it does not terminate. ## Example of Behavior For the coffee machine, an example of a finite behavior is: $$\text{10 cents} \rightarrow \text{reset} \rightarrow \text{5 cents} \rightarrow \text{10 cents} \rightarrow \text{coffee}$$ This corresponds to the path $S0 \rightarrow S1 \rightarrow S0 \rightarrow S2 \rightarrow S3$. Another example of a finite behavior could be: $$\text{10 cents} \rightarrow \text{reset}$$ This corresponds to the path $S0 \rightarrow S1 \rightarrow S0$. An example of an infinite behavior could be: $$\text{10 cents} \rightarrow \text{reset} \rightarrow \text{10 cents} \rightarrow \text{reset} \rightarrow \text{10 cents} \rightarrow \text{reset} \rightarrow \dots$$ This corresponds to the infinite path $S0 \rightarrow S1 \rightarrow S0 \rightarrow S1 \rightarrow S0 \rightarrow S1 \rightarrow \dots$ If we abstract away the events by letters, e.g., A for 10 cents, B for reset, and C for coffee, the first example of a finite behavior becomes the string ABAC. The second example becomes AB. The infinite behavior becomes ABABAB\... ## Language The set of all possible behaviors of a system is called its **language**. It's the set of all the things the system can do. :::: tcolorbox ::: definition **Definition 4** (Language). *A language is a set of strings (sequences of symbols) representing all possible behaviors of a system.* ::: :::: - **Regular Language**: A language recognized by a finite automaton. These are the simplest kind of languages we will consider. They correspond to systems with finite memory. - **Context-Free Language**: A language recognized by a pushdown automaton (automaton with a stack). These languages are more complex than regular languages. They correspond to systems with a memory that can grow arbitrarily large (the stack). ::: tcolorbox Regular languages are a fundamental concept in computer science. You might have encountered them when using regular expressions (regex). Regular expressions are another way to describe regular languages. ::: In this course, we will mostly consider finite state automata and regular languages. The set of behaviors of a finite state automaton is a regular language. The semantics of an automaton is the language it recognizes. # Specifications and Formulas ## Specifications A **specification** is a property that we want to verify about the system's behavior. It is formalized using logical formulas. The specification describes what we *expect* the system to do, or not do. It's a way of saying what's correct and what's not. ## Formulas A formula is a statement in a logical formalism that expresses a property of the system's behavior. Formulas are built using logical connectives and temporal operators. - **Boolean Connectives**: Operators like AND ($\land$), OR ($\lor$), NOT ($\neg$). These are used to combine simpler formulas into more complex ones. For example, if we have a formula $\phi$ that says \"the light is on\" and a formula $\psi$ that says \"the door is open\", we can combine them to form a new formula $\phi \land \psi$ that says \"the light is on and the door is open\". - **Temporal Operators**: Operators that describe properties over time, such as \"until\" ($U$). These operators allow us to talk about how the system's behavior evolves over time. For example, we might want to say that \"the light will stay on *until* the door is closed\". ## Example Formula Consider the formula: $$\text{(10 cents} \lor \text{5 cents}) \, U \, (\text{coffee} \lor \text{reset} \lor \text{kick})$$ This formula states that either a \"10 cents\" or \"5 cents\" event will occur until a \"coffee\", \"reset\", or \"kick\" event happens. In other words, the machine will keep accepting 10 or 5 cents coins until one of the events \"coffee\", \"reset\", or \"kick\" occurs. The \"until\" operator has a temporal aspect: it says something about what happens *before* something else happens. ::: tcolorbox Let's break down the example formula: - $(10 \text{ cents} \lor 5 \text{ cents})$: This part says that either a \"10 cents\" event or a \"5 cents\" event will occur. The $\lor$ symbol means \"or\". - $(\text{coffee} \lor \text{reset} \lor \text{kick})$: This part says that a \"coffee\" event, a \"reset\" event, or a \"kick\" event will happen. - $U$: This is the \"until\" operator. It connects the two parts of the formula and says that the first part will be true until the second part becomes true. ::: This is an example of a property we might want to verify about our coffee machine. We want to make sure that the machine behaves according to this specification. This formula is written in a mix of natural language and logical notation. Later, we will learn how to write formulas in a purely formal way. # Model Checking Problem ## Definition The **model checking problem** is the computational problem of determining whether all behaviors of a model satisfy a given formula. It's about checking if the system, as represented by the model, always does what it's supposed to do according to the specification. :::: tcolorbox ::: definition **Definition 5** (Model Checking Problem). *Given a model $M$ and a formula $\phi$, determine whether all behaviors of $M$ satisfy $\phi$.* ::: :::: This is a *computational* problem, meaning we want an algorithm that can solve it automatically. We want to be able to give the model and the formula to a computer and have it tell us whether the model satisfies the formula or not. ## Approach To solve the model checking problem, we can negate the formula and check for the existence of a violating behavior. This is often easier than directly checking that all behaviors satisfy the formula. The idea is that if we can't find a behavior that violates the formula, then all behaviors must satisfy it. - **Original Question**: Do all computations satisfy $\phi$? This is a universally quantified question. - **Negated Question**: Does there exist a computation that satisfies $\neg \phi$? This is an existentially quantified question. Checking for the existence of something is usually easier than checking that something holds for all cases. ::: tcolorbox The reason we negate the formula is that it transforms a universal quantification (for all) into an existential quantification (there exists). Existential quantifications are generally easier to handle algorithmically. ::: ## Example For the formula $\phi = (10 \text{ cents} \lor 5 \text{ cents}) \, U \, (\text{coffee} \lor \text{reset} \lor \text{kick})$, the negation is $\neg \phi = \square (10 \text{ cents} \lor 5 \text{ cents})$, meaning \"forever 10 cents or 5 cents\". ::: mdframed **Example Explanation:** If the original formula $\phi$ says that \"10 cents or 5 cents will happen until coffee, reset, or kick\", the negation $\neg \phi$ says that it's not the case that \"10 cents or 5 cents will happen until coffee, reset, or kick\". This can be rephrased as \"there exists a behavior where 10 cents or 5 cents happens forever, and coffee, reset, or kick never happens\". In this particular case, we can express this with the $\square$ (always) operator as $\neg \phi = \square (10 \text{ cents} \lor 5 \text{ cents})$. ::: **Important Note:** The precise negation of the \"until\" ($U$) operator depends on the specific temporal logic being used. In some logics, the negation might involve other temporal operators. We will learn more about how to negate formulas in later lectures. The teacher will provide a more detailed explanation of how to systematically derive the negation of temporal logic formulas. ## Solving the Model Checking Problem One way to solve the model checking problem is to: 1. Negate the formula $\phi$ to get $\neg \phi$. 2. Construct an automaton $A_{\neg \phi}$ that accepts all behaviors satisfying $\neg \phi$. 3. Check if the intersection of the language of the model $M$ and the language of the automaton $A_{\neg \phi}$ is empty. If the intersection is empty, it means there are no behaviors that satisfy $\neg \phi$, which means all behaviors satisfy $\phi$. If the intersection is not empty, it means there is at least one behavior that satisfies $\neg \phi$, which means not all behaviors satisfy $\phi$. In this case, we can also provide a counterexample, which is a behavior that violates the original formula. ::::: tcolorbox :::: algorithm ::: algorithmic **Input:** Model $M$, Formula $\phi$ **Output:** \"Yes\" if $M$ satisfies $\phi$, \"No\" otherwise $\neg \phi \gets \text{negate}(\phi)$ []{#alg:line:negate label="alg:line:negate"} $A_{\neg \phi} \gets \text{constructAutomaton}(\neg \phi)$ []{#alg:line:construct label="alg:line:construct"} $L(M) \gets \text{language}(M)$ []{#alg:line:language label="alg:line:language"} $L(A_{\neg \phi}) \gets \text{language}(A_{\neg \phi})$ []{#alg:line:language2 label="alg:line:language2"} []{#alg:line:intersection label="alg:line:intersection"} \"Yes\" \"No\" ::: []{#alg:model_checking label="alg:model_checking"} :::: ::::: **Complexity Analysis (Conceptual)**: - Line [\[alg:line:negate\]](#alg:line:negate){reference-type="ref" reference="alg:line:negate"}: Negating the formula can usually be done in linear time in the size of the formula. - Line [\[alg:line:construct\]](#alg:line:construct){reference-type="ref" reference="alg:line:construct"}: Constructing the automaton for the negated formula can be exponential in the size of the formula in the worst case. - Lines [\[alg:line:language\]](#alg:line:language){reference-type="ref" reference="alg:line:language"} and [\[alg:line:language2\]](#alg:line:language2){reference-type="ref" reference="alg:line:language2"}: Computing the language of an automaton can be done in linear time in the size of the automaton. - Line [\[alg:line:intersection\]](#alg:line:intersection){reference-type="ref" reference="alg:line:intersection"}: Checking the intersection of two languages can be done in time proportional to the product of the sizes of the automata. The overall complexity is dominated by the construction of the automaton for the negated formula, which can be exponential. **Note**: This is a high-level overview of the algorithm. The actual implementation involves many details that we will cover in later lectures. # Conclusion This lecture introduced the foundational concepts of logic, formal verification, and automata theory. We explored how models abstract systems, how behaviors represent system executions, and how formulas specify desired properties. The model checking problem was presented as a key computational problem in verifying system correctness. We learned that: - Logic provides a precise language for specifying properties of systems. - Formal methods, particularly automatic verification, offer a way to ensure system correctness beyond what is possible with traditional testing. - Automata theory provides a framework for modeling systems and their behaviors. - The model checking problem is a central problem in automatic verification, and it can be solved algorithmically. **Follow-up Questions**: - How can we derive the negation of temporal logic formulas systematically? This is important for applying the model checking approach we outlined. - What are the different types of temporal logic operators and their semantics? We've seen the \"until\" operator, but there are many others. Understanding their meaning is crucial for writing meaningful specifications. - How can we implement an algorithm to solve the model checking problem for a given model and formula? We've seen a conceptual algorithm, but the actual implementation requires more detail. - What are the limitations of finite state automata in modeling real-world systems, and how can we extend them? Finite state automata are powerful, but they have limitations. We might need more expressive models for certain systems. - How can we use these techniques in practice? What are some real-world applications of automatic verification? ::: tcolorbox **Remark**: Understanding these concepts is crucial for further study in automatic verification and formal methods. The next lecture will delve deeper into temporal logic and model checking algorithms. We will also discuss different types of temporal logic and their applications. :::