<h1 style="text-align:center">CONCURRENCY THEORY EXERCISE 1</h1>
<h5 style="text-align:center">Deadline: 04.11.2019 17:00</h5>

---
**Group members:**
- Eugen Kamyschnikow (392886)
- Junhan Sui (404194)
- Luxiaowei Li (414717)
- Yu Wei Huang (414525)

---

## Encoding Programs as Automaton
**Solution:**

Task 1:

digraph finitestatemachine {
	rankdir=LR;
	size="8,5"
	node [shape = circle];
    "" [shape = none]
    "" -> 2 
	2 -> 1 [ label = "Acquire" ]
    1 -> 2 [ label = "Release" ]
    1->0 [ label = "Acquire" ]
    0 ->1 [label = "Release"]
	0 [shape=doublecircle]
   
}

Task 2:
We use Pushdown automaton to make a reentrant lock. Assume a$M=(Q,\sum,\Gamma,\delta,q0,Z0,F)$

digraph finite_state_machine {
        size="8,5"
        rankdir=LR;
        node[shape=circle]
        ""[shape= none]
        ""->p0[ ]
        p0->p0[label="lock,Z0/lock
        lock,lock/lock"]
        p0->p1[label="unlock,lock/pop"] 
        p1->p0[label="unlock,Z0/epsilon"]
        p0[shape=doublecircle]
        p1[shape=doublecircle]
        }

when start from p0 and an empty stack, we can lock the process mutiple times. Then we only have the chace to unlock them if there is lock state in the stack.

## Longest (Worst Case) Shortest Counterexample to a Safety Property for Automata
**Solution:**

**Q1**: In the worst case, the shortest word in the product DFAs $P_s = m * n - 1$.

**Q2**: Consider a DFA shown as below:

digraph finite_state_machine {
        size="8,5"
        rankdir=LR;
        node [shape = circle];
        init [shape = none, label = ""];
        
        init -> A;
        A -> B [ label = "1" ];
        B -> C [ label = "1" ];
        C -> A [ label = "1" ];
        C [shape = doublecircle];
    }
}

It accepts the word of size $w$ where $(|w| \mod 3) = 2$.Take the product of two DFAs in a similar fashion $(|w| \mod m) = m-1$ and $(|w| \mod n) = n-1$ where $m$ and $n$ are different prime numbers. The first accepted word has size $m * n - 1$.

**Q3**: First, we know a word of size $m∗n−1$ visit at most $m∗n$ different states, if the path it passes through is acyclic. Any word longer than that will no doudt visit one state twice and, therefore, it cannot be the shortest accepted word.

**Q4**: The product is growing exponentially with the increasing number of automation, thus it leads to exploring exponentially longer executions to testing and debuging with many copies of the program in parallel.

## The Need for Multiple Final States for DFAs
**Solution:**

There is no DFA with a single final state whose language `L = {a|aa}`.
Without the ability to count the number of `visits` for a certain connection, a specific amount of letters can only be achieved by a corresponding final state. In this case "1" for $a$ and "2" for $aa$.

digraph finite_state_machine {
  rankdir=LR;

  "" [shape=none]
  "start" [shape=circle]
  "1" [shape=doublecircle]
  "2" [shape=doublecircle]
  "end" [shape=circle];
  "" -> "start";
  "start" -> "1" [label = "a"];
  "1" -> "2" [label = "a"];
  "2" -> "end" [label = "a"];
  "end" -> "end" [label = "a"];
}