formal_method_overview

Formal method (Based on WPI RBE 595) §

tag:#formalmethod

1. Formal specification §

1.1. Propositional logic §

• Proposition: true or false

• Atomic proposition (AP): the true or false does not depend on any other proposition e.g.: 现在路口是绿灯

• Logic connectives:

  • ”: ‘AND’, : ‘OR’. : Negation

  • : Implication

    Example

    运算顺序为从左至右，即 A: If it is a bear. 它是熊 B: then it can swim. 它会游泳 1. If A is false (it is not a bear), it might be able to swim (a fish) or not (a bird). 如果不是熊的话（A为false），可能会游泳也可能不会（比如是鱼或者是鸟），所以不是熊可以推出两种情况皆有可能（B既可能是true也可能是false）。 It can swim -> B=T It cannot swim -> B=F A false statement implies anything 2. If A is true (which it is a bear), it can swim (B=T). 如果是熊，一定会游泳

  • A and B does not necessary to have causal relationship (example)

  • : Equivalence

  0	0	1	0	0	1	1
  0	1	1	0	1	1	0
  1	0	0	0	1	0	0
  1	1	0	1	1	1	1

• Quantification:

  • : Existential
  • : Universal

1.2. First-order logic一阶逻辑 §

• 通过运算符（，，，，）和量化（，）将AP连接起来

1.3. Temporal logic时序逻辑 §

• Temporal operator(check wiki):

  Symbol	Symbol	meaning
  	X	Next
  	U	Until
  	F	Eventually in the future
  	G	Always

• E.g.: 例如有一个AP set ，可以是

  1. 其中的任意一个AP （如、、，避免直接表示成）
  2. 通过公式中提供的逻辑操作符（，，，）运算后定义（如），
  3. 嵌套定义（如）

• Practical properties in LTL

  • Reachability:
    • : simple reachbility
    • : conditional reachability
  • Safety
    • : invariant
  • Liveness
    • and others
  • Fairness
    • and others

2. Automata §

2.1. A finite-state semi-automaton: §

• : A finite set of states
• : A finite set of symbols (words，相当于自动机的“程序”)
• : A nondeterministic transition function
• 没有指定开始状态，也没有指定终止状态

2.2. A finite-state automaton: §

• : An initial state
• : A set of final states
• Büchi: An infinite word is accepted if it results in a run to visit infinitely often. （无限长的word，时不时就会经过终态）
• Regular: A finite word is accepted if it results in a run to ONE of the final states （有限长的word，最终抵达终态）
• Deterministic finite automaton (DFA) is a singleton
• : Language The set of words accepted by the automaton.

2.2.1. Regular languages正则语言 §

• Kleene star 闭包

  • 对集合内的符号进行有限次的串接（包括不对任何符号进行串接，即空集） E.g.:
  • 两层用途：
    1. Given a set , get the set by concatenating words from finitely many times,. Includes the empty set. (所有能匹配的字符串，每个字符串中words为有限数个)
    2. Given a set of words (strings), the smallest superset of it (??没有出现在课件里??)(反之)

• A run is accepting if . E.g.: 001/110/etc.

• A word is accepting if it triggers an accepting run. E.g.: 0010 (?终止状态一定是从它出发的又会回到它么？)

2.2.2. -regular languages §

• Given a set , the set are obtained by concatenating words from infinitely many times. e.g.:

2.2.3. Deterministic vs. nondeterministic §

• What’s the difference?

  • Nondeterministic (NFA, nondetereministic finite automaton) 在某个state ，给定一个word ，可能到达，也可能到达 E.g.: 从状态0出发，执行word a，可能到状态1或状态3

  • Determinization

  • 任意NFA均可转化为DFA(?) For any nondeterministic automaton with regualr acceptance condition, there exists a deterministic automaton with regular acceptance condition accepting the exact set of words

  • Non-deterministic Buchi are more expressive than deterministic Buchi. non-DBA的Language不能全部被DBA接受

    • There exist nondeterministic Buchi automata whose languages cannot be accepted by a deterministic Buchi automation

  • powerset幂集: 所有属于给定集合的子集（从空集到这个集合本身）。集合的powerset共个子集。

    Example

    If S is the set , then the subsets of S are (also denoted {)

2.2.4. Fragment of LTL=DBA(?) §

• draw some graph

• 允许使用部分LTL以描述一个DBA

• E.g.: includes formulas that are constrcuted from:

• fragment of LTL paper

• some other paper

3. Transition systems and compositions §

reader_software_specification_ch_8 some related slides another related slides

3.1. Finite state transition system §

• A finite state transition system TS is a tuple
  • : a finite set of states.
  • : a finite set of actions.
  • : a finite set of transitions.
  • : a finite set of initial states.
  • : a finite set of atomic propositions.
  • : a labeling function.

3.2. Predecessors and successors §

• a-successor of s:
• a-predecessor of s:
• A state is terminal iff

3.3. Deterministic transition system (TS) §

• 两层含义

  • Action-determinisitic If and for all , it holds that . For all actions and states, it has at most one suceessor state (至多有一个初始状态（为什么要限制?），并且从任意一个state执行的任意一个action最多有一个后续状态)ch. 8
  • AP-determinisitic If for all the following conditions hold: and for all 每个AP（原子命题）至多有一个初始状态，并至多有一个后续(post)状态。需要确认?

• Notation: for determinisitic transition function,

3.4. Interleaving of transition systems §

• , Transition relation is defined by and

3.5. Handshaking §

• , Transition relation is defined by
  1. If , , and , then
  2. If , and , then
  3. If , and , then

3.6. Transition system and LTL specification §

???

4. LTL verification of transition systems §

4.1. Basic properties: §

• Invariant: 一些状态恒为true/false（一些条件应始终成立/不成立）？？

  Example

  十字路口交通灯，AP南北向为绿灯，AP东西向为绿灯，记绿灯为g，红灯为r。 即为一系列红绿灯状态的组合。如：从任意一个时刻开始，记录一段时间（任意长时间）路口红绿灯的变化： (rg) —> (rr) —> (gr) —> (rr) —> (rg) —> …(红绿灯交替，不存在同时同时绿灯，变灯时可能出现同时红灯)，因为-Regular中包含任意有限长度的组合。 当交通灯的规则为，即不会同时出现绿灯/始终只有一红一绿或两红时，将任意中的元素代入交通灯规则，都为true(?)，所以对此规则是满足invariant的

  - Reachable state

• Safety: 一些状态恒为false（确保一些情况不会发生），e.g.: 路口两个方向不会同时为绿灯。

• Liveness：一些状态在一定情况下会发生，e.g.：路口会变绿灯。

4.2. Product of TS and Automaton §

• Transition system , automaton

	Transition system	Automaton
State
	: Action
Transition
Initial
	: a set of AP
	: the labeling function	: Input symbols
	(the same )	:the set of accepting state

待进一步检查的StackExchange上的Example

Ref: StackExchange

1. 首先找出新的initial set： ，所以有，新的initial set为

2. 新的transition的定义为 也就是对于TS中的进行一次状态转移（状态转移的label 通常被忽略），到达新的状态，用于表示状态的label作为自动机的输入，驱动自动机从状态转移到其下一状态。 中的下一状态为，标签为。在接受作为输入后转移至，所以的后续状态为

3. 后续计算为：

   i					note
   0
   1
   2
   3
   4					???

google

ch 4 p166, figure 4.6

German trafic light system (Principles of model checking, chapter 4, p162, p166):

• Traffic light example (bad prefix: p112, traffic light example: p113)

  1. A safety property for a traffic light常见的交通灯的安全属性:

     1. 至少有一个灯是亮着的 The bad prefixes: finite words contain . A minimal bad prefix在执行完一个有限长度的word时灯都不亮
     2. 不会同时亮两盏灯 Bad prefixes: words containing sets such as {red, green}, {red, yellow}, and so on. A minimal bad prefixes ends with such sets. 在一个有限长度的word执行完后有两个或两个以上的灯亮

  2. 假设，/{ }为green，并且只保证以下的安全属性（上述两种情况中第一种由现在假设的AP的特性保证：红黄灯不亮时绿灯必亮；忽略第二种，即红黄灯可以同时亮，但是绿灯不会和其它灯同时亮） ，包括四个input symbols，，，

     • ◎表示终结态

     • 红绿灯应满足的条件：在变红灯之前应有一段黄灯 例如不正确的words：{ } {red}。绿灯后立刻红灯

     • 对应的finite automaton for the minimal bad prefixes of a regular safety property. （若设计一个NFA，接受minimal bad prefixes）(P113，P162) 原书p113图3.9有误，参见errata (2010 July)。 从q1到q1的yellow包括了words：和 从q1到q0的¬yellow包括words：和

       Here, ¬yellow should be read as either or {red}.

       从q0到q1的yellow∧¬red即 从q0到q0为¬red∧¬yellow，即 从q0到qF的red包括了words：和

  3. German traffic light (GermanTrLight) P166

     • TS: four states with the usual transitions

       1. red -> red+yellow, 2) red+yellow -> green, 3) green -> yellow, 4) yellow -> red (note relevant, omitted) Label: L(red)={red}, L(yellow)={yellow}, L(green)==L(red+yellow).

       	Transition system	Automaton
       State	: {red, red+yellow, green, yellow}	: q0: {{ }1,{red}} q1: — {{yellow},{yellow,red}}
       	: Action
       Transition
       Initial
       	: {red,yellow}
       	: {00, 01,10,11}	: Input symbols
       	(the same )	:the set of accepting state

     • 原书（“Principles of model checking”）在P113及P166页对safety的条件叙述不一致，GermanTrLight允许同时出现red+yellow，但是在第三章中不允许出现。解决方案： 1. 将TS中red->red/yellow改为red->yellow。将red+yellow视为不安全状态（ref: Another traffic light example，slides 12） 2. 修改NFA，将q0->q1的输入改为，将q0->qF的输入改为，这样不会进入终态（下图采用这种解决方案，注意NFA与上面的图的区别） 3. 修改NFA，将q0->q0的输入改为，相乘后

     ^1.Note: { } stands for green

     1. 首先找出新的initial set： ，所以有，新的initial set为

     2. 新的transition的定义为 也就是对于TS中的进行一次状态转移（状态转移的label 通常被忽略），到达新的状态，用于表示状态的label作为自动机的输入，驱动自动机从状态转移到其下一状态。 中的下一状态为，标签为。在接受作为输入后转移至，所以的后续状态为

     3. 后续计算为：

        i					note
        0
        1
        2
        3					back to

     ref: Transition System to Buchi Automaton Translation

CSDN

5. Probabilistic modeling checking with Markov Decision Processes §

value function, value iteration, Bellman optimality equation, Q-function, asychronous value iteration

• Linear programming formulation 转化成线性规划问题 . where is a probability distribution over ** the contraction is monotonic? What does it mean?**
• The dual problem对偶问题
  • wiki
  • CSDN
  • 对偶，KKT条件，SVM

6. Reactive synthesis §

one-shot或repeated博弈

7. Abstraction of continuous systems §

SOS: sum of squares