Problem 1: Verification in the Small
Design a finite automata that recognizes the set of binary strings, i.e., strings drawn from \(\Sigma^* = \{\, 0, 1 \,\}\), that have an even number of \(0\)s. Note that zero \(0\)s is an even number of \(0\)s!
For each of the states of your finite automata, give a property describing the set of strings that, when starting from the initial state, end their execution on that state.
Use the properties you described for each state to argue why your finite automata is correct in a few sentences.
Problem 2: Client-Server Protocols
Imagine designing a software system that stores both public and private information on a server. A user of the system can log into the system and access public information, but they cannot access private information until they authenticate. Finally, a user can log out of the system.
Design a finite automata that captures this protocol between the client and the server. Let the states of the automata be the state of the user as they interact with the system and the alphabet be the set of possible actions the user can take in the system.
Prove that your automata obeys the following property:
Claim: for any sequence of actions the user takes in the system, the user never accesses private information unless they have authenticated.