Introduction - with insightful view

When reading the introduction, i would be more happy to view from a view point where nobody has provided. And feel bored when read something repeated in many papers like safety property is "something bad never happen", I hope those could be introduced as little ad as concise as possible.

Interleave and Skip

In the interleave expression, the Skip Process can't be run unless all processes in the interleave process becomes Skip.
Skip||a->Skip||b->Skip
For example, for above expression, it has two possible next steps, which is events {a,b}，but the Skip cannot go.

The reason the operational semantics of sequential expression is defined as
P->(CompleteEvent)P'
-------------------------
P;Q->(tau)P';Q

and Skip process is defined as

--------------
Skip->(CompleteEvent)Stop

now let P=Skip||a->Skip||b->Skip
if P allows that Skip to go, all other expression will force to stop!

Go for simplistic research prototype

Recently am building a research prototype, I have tried to add as many fancy non-technical features as it could be, it turns up that most are wasteful result. Now, I would try to go for a simplistic style. Logically, this is a better way to go. Let's try.

How to enjoy doing research

To write a paper, I have read quite a few paper.

Avoid Pressure
We have to maintain the peaceful mind when reading paper, don't press yourself too much(current pressure), yet not be distracted by other thing(future pressure); to enjoy, first we have to avoid pressure.

In my past, I always like to go outside do something like eating(at least 30 minutes), or just surfing web(more than an hour) when feel like to do it (normally, when I get something done). Don't do that, save the time to finish your thing...you can keep all the entertainment at one time slot, but don't just do it whenever you FEEL LIKE to do it, you WILL lost control of your time! Although you have worked a day, but essentially the real working hour is much less than that, maybe just 3 hours I assumed?

Plan well, then you can start forget the schedule. Let yourself control by your dicipline/schedule, not what you FEEL like to do.

Enjoy the hippie moment, forget about the schedule
When you are doing thing according to your schedule, you can start forget about the time. Enjoy your research (in a progressive manner, not reading one thing for whole few days which will make you pressure later for lot of work not being done) or enjoy your entertainment. Doing research is just like playing a game. You could win or lost. Enjoy its excitment. Let's go about the schedule. you could set a google alarm to remind yourself day is up, in case you enjoy it too much :) For reading paper, the moment I feel enjoy is to successful grab the normally simple yet very logical idea behind each paper, this is the hippie moment of reading paper. The hippie moment of writing a paper is to put across an excellent idea or think of a better way to explain or convince the audience. The hippie moment of writing a program is to get it done and get a paper published. And of course the most hippie moment is the relax feeling of getting a research done! Let the excitement excite you ALL THE WAY.

Try to let the happiness of research keep you going on, DURING WORKING HOUR, finding happiness from this source is far better than listening to music, watching TV and so on. Because, you can benefit from the hapiness, be less future pressurize, stay motivated, and be a successful researcher!

Writing Paper

When proposed a method, you have to elaborate the following thing:

a. Reviewer want to understand clearly – Elaborate it clearly with simple example, treat the reviewer just like your student, lead the people in reading your story, follow your story, ultimately convince them your method is great!

b. What’s great - Illustrate the greatness of approach in the eye of expert, don’t expect the expert have the eye to the greatness of your approach. Researcher would be fascinated when they see a GREAT thing. For this you can read the Tony Hoares and Robert Milner books, see how experts in the field convince their reader that their approach is great, in a peaceful, yet confident manner.

c. What’s new - How this method compare to previously proposed method, and what is the new observation that make this method a great methodology and let other people possible to extend on it?

d. Showing Limitation - Show the limitation of the methods, and no people would believe that your method is perfect, if you show the limitation, this shows to people that you are not purposely hiding something.

Proof-like flow of thinking

Learning proof is just learning how to think logically, and completely.
As a researcher in FM, proving thing is just like eating, it is part and parcel of everyday job. Thus to make it easy, one would have to learnt it, digest it, make use of it FREQUENTLY, and hopefully master it.
After thousand of years of human history, some of the common pattern of thinking/proofing is known to be powerful, and it is used to tackle many important problems again and again.

Proof By Contradiction
This proof method is somewhat surprising yet very extremely powerful.
Basically we assume something is false, get a consequences from that which we can REVERT IT EASILY.

Proof By Structural Induction

Some FM common terminology

Complete vs Incomplete
A checking method is incomplete means
checking result is true => the real result is true
checking result is false =/=> the real result is false
while if it is complete
checking result is true => the real result is true
checking result is false => the real result is false

Partition
(A set {A1,A2,...,An} partitions another set A)
A collection of non-empty set {A1,A2,...,An} is a partition of a set A, iff
1. A=$A1 \cup A2 \cup ... \cup An$
2. A1, A2,..., An is mutually disjoint.