Transition-System

Description

一个六元组

\[T = (S,Act,\rightarrow,S_0,AP,L)\]

• \(S\), set of states
• \(Act\), set of actions
• \(\rightarrow ~ \subseteq S \times Act \times S\), 3-tuple-relation
• \(S_0 \subseteq S\), initial states
• \(AP\), a set of atomic propositions (原子命题?)
• \(L: S \rightarrow 2^{AP}\), the labeling funciton

举饮料机为例

与 Finite State Automata 的三个主要区别

1. Numbers of state can be infinite
2. There is not something like an accepting state
3. It exhibits certain actions

Change the labeling doesn't affect the transition. 教授回答了学生一个提问,改变 label 没有改变 trasition.

Behavior

What is the possible behavior of TS.

1. Start

   select nondeterministically an initial state $s \in S_0$

   As for a series of initial states, select nondeterministically. Possibility. No difference.

2. After

   WHILE $s$ is non-terminal DO
   
       select nondeterministically a transition $s \stackrel{\alpha}{\rightarrow} s'$
   
       excute the action $\alpha$ and put $s := s'$
   
   OD

   We find another nondeterministically choice.

Describes what the system can do (privately, on its own).

executions: maximal "transition sequences"

rechable fragement: set of all reachable states.

Model checking

Map the real complicated system to the TS just learned as one of the input of model checker. The other one is specification built from requirements.

syntactic description of system -> semantics interpretation to TS

!The lecture of today is that Transition Systems are the elementary models and basically almost everything you can think about.

Example: hardware circuits and sequential programs.

Modelling of sequential circuits by TS

Describe by means of two things: transition functions and ouput functions.

Take 1 bit input and 1 bit register as an example.

4 states (2 * 2)

Initial states rely on the assumptions. If we assumpt the registor should be 0 in the beginning, then the initial states will be 2/4 which r1 = 0.

Get the transition from the transition function(s).

As for the number of states: the number of inputs and the number of registers that is decisive on the size of the transition system.

In this example, the number of state may big but always finite.

Data-dependent systems

TS-representation of conditional branchings?

Progrm graph(program system) -> transition system.

states of the transition system: locations + relevent data.

state?

Initial states also depend on our assumptions. In the video, the prof. assupmt x=2 and y = 0. Actions (change of state) like alpha (x:=x-1) beta (y:=y+1) and loop_exist. Loop exist action doesn't change the value of x/y but it does change the program location(program counter) which is also the component of the states we difined. So the state changes.

Effect-function for actions

Eval map Variable to Values.

\(Effect:~ Act \times Eval(Var) \rightarrow Eval(Var)\)

Program graph (PG)

Let \(Var\) be a set of typed variables.

A program graph over \(Var\) is a tupple

\[P = (Loc, Act, Effect, \rightarrow, Loc_0, g_0)\] where

!!Now define a mapping from PG to TS.

Show the transition system of the beverage machine.