Previous chapter: Synthesis

This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner

Verification or Synthesis

In applications like verification and synthesis, the automata- and game-theoretic machinery is usually “hidden” behind a logical formulation of the problem.

Logics with corresponding Automata

S1S‘s expressiveness exceeds that of LTL, and
S2S‘s expressiveness exceeds that of CTL* (on binary trees)

Logic	Usage	Example
Linear-time temporal logic (LTL)	sets of infinite words	$\square \Diamond \ell_1$
Computation-tree logic (CTL / CTL*)	sets of infinite trees	$\textsf{EF}\ell_1 \wedge \textsf{EF}m_1$
Monadic second-order logic with one successor (S1S)	logic over infinite words	$\forall x . x \in P \rightarrow S(x) \in P$
Monadic second-order logic with two successors (S2S)	logic over infinite binary trees	$\forall x . x \in P \rightarrow S_1(x) \in P \vee S_2(x) \in P$

Explaination

• $\square \Diamond \ell_1$
  $P_0$ is infinitely often at location $\ell_1$.
• $\textsf{EF}\ell_1 \wedge \textsf{EF}m_1$
  There exists a computation path in which $P_0$ reaches location $\ell_1$, and
  there is a (possibly different) computation path in which $P_1$ reaches location $m_1$.
• $\forall x . x \in P \rightarrow S(x) \in P$
  A (given) set of natural numbers $P$ is either empty, or
  consists of all positions starting from some position of the word.
• $\forall x . x \in P \rightarrow S_1(x) \in P \vee S_2(x) \in P$
  A (given) set of nodes $P$ contains from each node $n \in P$ an entire path starting in $n$.

Previous chapter: Model Checking

This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner

Synthesis

In synthesis, we check automatically if there exists a program that satisfies a given specification.

If the answer is yes, we construct such a program.

We solve it by determine the winner of a two-player game between a system player and an environment player.

	Task	Goal
System player	choose the outputs of the system	meet the specification
Environment player	choose the inputs of the system	falsify the specification

Therefore, the specification is satisfied if the System player wins.
Such winning strategy can be translated into a program that is guaranteed to satisfy the specification.

Example: coffee machine

In this example, we assume there’s a machine that “outputs coffee” whenever users press a button.

This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner

Model Checking

Given a system model, we try to check whether it meets its specification automatically and exhaustively.
To describe/represent the system and specification, we use Automata over infinite objects.

Verification Problem

The verification problem can be solved by:

Constructing the intersection of system, with an automaton for the negation of the specification,
then checking whether the language of the resulting automaton is empty.

$\textbf{Example 1.1. } \text{Consider the concurrent program }\small{\text{TURN}}:$
$$\text{local }t:\text{boolean where initially }t = false$$
$$P_0::\left[ \begin{array}{l}\text{loop forever do}\newline
\hspace{1cm}\left[ \begin{array}{l}
\ell_0: \text{await }\neg t; \newline
\ell_1: \text{critical;} \newline
\ell_2: t := true; \newline
\end{array} \right]\end{array} \right]
\mid\mid P_1::\left[ \begin{array}{l}
\text{loop forever do}\newline
\hspace{1cm}\left[ \begin{array}{l}
m_0: \text{await } t; \newline
m_1: \text{critical;} \newline
m_2: t := false; \newline
\end{array} \right]\end{array} \right]$$

The example above is a simple solution to the mutual exclusion problem:
it ensures that at any given point of time, at most one process is in the critical region.

From Program to automaton

To represent the above program using automaton, we need to define an alphabet $\Sigma$.

Question

Table name: Weather

Column Name	Type
id	int
recordDate	date
temperature	int

There are no different rows with the same recordDate.
This table contains information about the temperature on a certain day.

Write a solution to find all dates' id with higher temperatures compared to its previous dates (yesterday).
Return the result table in any order.

Explaination

Here, we need to learn how to handle the datatype date.
To modify the date, we can use INTERVAL keyword, or DATEADD() function.

INTERVAL <value> <unit>

Interval is a special datatype, that can interact with time and date.

Interval unit includes
microsecond, millisecond, second, minute, hour, day, week, month, year, decade, century, millennium

Question

Table name: Visits

Column Name	Type
visit_id	int
customer_id	int

This table contains information about the customers who visited the mall.

Table name: Transactions

Column Name	Type
transaction_id	int
visit_id	int
amount	int

This table contains information about the transactions made during the visit_id.

Write a solution to find the IDs of the users who visited without making any transactions, and
the number of times they made these types of visits.
Return the result table sorted in any order.

Explaination

This is another typical JOIN query question.
The tricky part is the column we join on doesn’t necessarily be selected.

Question

Table name: Sales

Column Name	Type
sale_id	int
product_id	int
year	int
quantity	int
price	int

Each row of this table shows a sale on the product product_id in a certain year.
Note that the price is per unit.

Table name: Product

Column Name	Type
product_id	int
product_name	varchar

Each row of this table indicates the product name of each product.

Write a solution to report the product_name, year, and price for each sale_id in the Sales table.

Explaination

This question is a basic usage of JOIN query.

Question

Table name: ``

Column Name	Type
user_id	int
name	varchar
mail	varchar

This table contains information of the users signed up in a website. Some e-mails are invalid.

A valid e-mail has a prefix name and a domain.

domain: @leetcode.com.
prefix name is a string that may contain:

• letters (upper or lower case)
• digits
• underscore _
• period .
• dash -

(The prefix name must start with a letter.)

Write a solution to find the users who have valid emails.
Return the result table in any order.

Explaination

Question

Table name: Products

Column Name	Type
product_id	int
product_name	varchar
product_category	varchar

This table contains data about the company’s products.

Table name: Orders

Column Name	Type
product_id	int
order_date	date
unit	int

unit is the number of products ordered in order_date.

Write a solution to get the names of products,
that have at least 100 units ordered in February 2020 and their amount.
Return the result table in any order.

Explaination

Retrieve the amount of products

Question

Table name: Activities

Column Name	Type
sell_date	date
product	varchar

Each row of this table contains the product name and the date it was sold in a market.

Write a solution to find for each date the number of different products sold and their names.
The sold products names for each date should be sorted lexicographically.
Return the result table ordered by sell_date.

Explaination

Again, there are two tasks we need to solve:

1. Count how many types of products are sold in one day
2. List all types of items into a single column

Type of Items

We can simply count how many products are sold using COUNT, groupped by the date they belong to:

Question

Table name: ``

Column Name	Type
id	int
salary	int

Each row of this table contains information about the salary of an employee.

Write a solution to find the second highest distinct salary from the Employee table.
If there is no second highest salary, return null.

Explaination

The key idea of this question is to get the second value. Here I have two ideas that come to my mind immediately

1. First, order the list according to salary, then fetch the second row.
2. First, find the highest salary, then do another SELECT query based on the highest salary.

1. Using LIMIT and OFFSET

Using LIMIT and OFFSET, we can simply retrieve the second row of a database: