Generality of algebra: Difference between revisions

From formulasearchengine
Jump to navigation Jump to search
en>Helpful Pixie Bot
m ISBNs (Build KC)
 
en>Tkuvho
No edit summary
Line 1: Line 1:
The great thing about a bad economy is that people find new ways to make extra money, and often times they find it is much easier than going to work everyday, where they are making someone else rich. There are simple and fast ways to make money in your spare time, and all it requires is your ability to take action.<br><br>That's understandable. The beginnings can be, and usually are, challenging. But it's easy to handle this if you simplify things. Simple things are not necessarily worse than complex ones, so before you decide to embark on using the top notch trading technology, I suggest that you explore some really simple options, some basic yet solid elements that has been around for a very long time and are here to stay.<br><br>Getting involved in the world of investing can be a significant challenge and a daunting task for many people. It seems to be getting much easier, though. In the past, investors had to have a broker and they had to jump through hoops every single time they wanted to make a trade. This isn't the case anymore, as online stock trading has become the preferred method for the majority of investors. There is no arguing the fact that the internet has made life easier in a number of different ways, and this is just one more thing to add to that list. But what are the distinct advantages to going with online stock trading over traditional broker service?<br><br>Success in stock and options trading requires knowledge, hard work, and discipline. It isn't easy  [http://news.goldgrey.org/gold-price/ bars shop] and it isn't quick. But success in stock and options trading is quite achievable; you don't have to be a rocket scientist. You don't have to know "the secret".<br><br>Here are some important advice for you to earn cash with day trading. If you can apply these properly you can make some significant money trading stocks online.<br><br>For this you should plan to start investing in stocks as early in your life as possible. Consult your stock broker which long term trading plan suits best according to your individual circumstances. Save a fixed amount of money every month from your earnings and direct your broker to draw and invest it in the stock investment plan you have worked out.<br><br>A falling unemployment trend would be a sure sign of companies seeing visible growth ahead as hiring is usually lagging indicator. (Companies have to see and believe in a measurable improvement before the commit to new workers. Until then things like productivity and overtime can be watched. At present the BLS hours worked are rising and private sector jobs are growing albeit slowly.<br><br>The [http://Easiest.org easiest] and probably the most robust way to learn trading is to learn trading systems. All good traders use systems which is really nothing but a set of rules for picking stocks, entering trades and exiting them again. Systems allow you to take your emotions out of the trading and it allows you to be more scientific with your trading. Its really important that you learn and master as many trading systems as possible because for every market condition there is a system that can help you succeed even when the sky is falling.
In [[formal verification]],
finite state [[model checking]] needs to compute an equivalent [[Büchi automaton]] (BA) to a [[Linear temporal logic]] (LTL) formula,
i.e., the LTL formula and the BA recognizes the same [[ω-language]].
There are algorithms that translate a LTL formula to an equivalent BA.<ref name=VW94>M.Y. Vardi and P. Wolper, Reasoning about infinite computations, Information and Computation, 115(1994), 1–37.</ref>
<ref name=KMMP93>Y.Kesten,Z.Manna,H.McGuire,A.Pnueli,A decision algorithm for full propositional temporal logic, CAV’93, Elounda, Greece, LNCS 697, Springer–Verlag, 97-109.</ref>
<ref name=GPVW93>R. Gerth, D. Peled, M.Y. Vardi and P. Wolper, "Simple On-The-Fly Automatic Verification of Linear Temporal Logic," Proc. IFIP/WG6.1 Symp. Protocol Specification, Testing, and Verification (PSTV95), pp. 3-18,Warsaw, Poland, Chapman & Hall, June 1995.
</ref>
<ref name=GOCAV01>
P. Gastin and D. Oddoux, Fast LTL to Büchi automata translation, Thirteenth Conference on Computer Aided Verification (CAV ′01), number 2102 in LNCS, Springer-Verlag (2001), pp. 53–65.
</ref>
This transformation is normally done in two steps.
The first step produces a [[generalized Büchi automaton]](GBA) from a LTL formula.
The second step translates this GBA into a BA, which involves relatively
[[Büchi_automaton#Transforming_from_other_models_of_description_to_non-deterministic_B.C3.BCchi_automata|easy construction]].
Since LTL is strictly less expressive than BA, the reverse construction is not possible.
 
The algorithms for transforming LTL to GBA
differ in their construction strategies but they
all have common underlying principle, i.e.,  
each state in the constructed automaton represents a set of LTL formulas
that are ''expected'' to be satisfied by the remaining input word after occurrence of the state during a run.
 
==Transformation from LTL to GBA==
Here two algorithms are presented for the construction. The first one provides a declarative and easy to understand construction. The second one provides an algorithmic and efficient construction. Both the algorithms assume that the input formula f is constructed using the set of propositional variables ''AP'' and f is in [[Linear temporal logic#Negation normal form|negation normal form]].
For each LTL formula f' without ¬ as top symbol, let ''neg''(f') = ¬f', ''neg''(¬f') = f'.
For a special case f'='''true''', let ''neg''('''true''') = '''false'''.
 
===Declarative construction===
 
Before describing the construction, we need to present a few auxiliary definitions.  
For a LTL formula ''f'', Let ''cl''( f ) be a smallest set of formulas that satisfies the following conditions:
{|
|
* '''true'''  ∈ ''cl''( f )
*  f ∈ ''cl''( f )
* if f<sub>1</sub> ∈ ''cl''( f ) then ''neg''(f<sub>1</sub>) ∈ ''cl''( f )
* if '''X''' f<sub>1</sub> ∈ ''cl''( f ) then f<sub>1</sub> ∈ ''cl''( f )
|
* if f<sub>1</sub> ∧ f<sub>2</sub> ∈ ''cl''( f ) then f<sub>1</sub>,f<sub>2</sub> ∈ ''cl''( f )
* if f<sub>1</sub> ∨ f<sub>2</sub> ∈ ''cl''( f ) then f<sub>1</sub>,f<sub>2</sub> ∈ ''cl''( f )
* if f<sub>1</sub> '''U''' f<sub>2</sub> ∈ ''cl''( f ) then f<sub>1</sub>,f<sub>2</sub> ∈ ''cl''( f )
* if f<sub>1</sub> '''R''' f<sub>2</sub> ∈ ''cl''( f ) then f<sub>1</sub>,f<sub>2</sub> ∈ ''cl''( f )
|}
 
''cl''( f ) is closure of sub-formulas of f under negation.
Note that ''cl''( f ) may contain formulas that are not in negation normal form.
The subsets of ''cl''( f ) are going to serve as states of the equivalent GBA.
We aim to construct the GBA such that if a state ''corresponds'' to a subset M ⊂ ''cl''( f ) then the GBA has an accepting run starting from the state for a word iff the word satisfies every formula in M and violates every formula in ''cl''( f )/M.
For this reason,  
we will not consider each formula set M that is clearly inconsistent
or subsumed by a strictly super set M' such that M and M' are equiv-satisfiable.  
A set M ⊂ ''cl''( f ) is ''maximally consistent'' if it satisfies the following conditions:
{|
|
* '''true'''  ∈ M
* f<sub>1</sub> ∈ M iff ¬f<sub>1</sub> ∉ M
|
* f<sub>1</sub> ∧ f<sub>2</sub> ∈ M iff f<sub>1</sub> ∈ M and f<sub>2</sub> ∈ M
* f<sub>1</sub> ∨ f<sub>2</sub> ∈ M iff f<sub>1</sub> ∈ M or f<sub>2</sub> ∈ M
|}
Let ''cs''( f ) be the set of maximally consistent subsets of ''cl''( f ).
We are going to use only ''cs''( f ) as the states of GBA.
;GBA construction
An equivalent [[Generalized Büchi automaton|GBA]] to f is ''A''= ({init}∪''cs''( f ), 2<sup>''AP''</sup>, Δ,{init},'''F'''), where
* Δ = Δ<sub>1</sub> ∪ Δ<sub>2</sub>
** (M, a, M') ∈ Δ<sub>1</sub> iff ( M' ∩''AP'' ) ⊆ a ⊆ {p ∈ ''AP'' | ¬p ∉ M' } and:
*** '''X''' f<sub>1</sub> ∈ M iff f<sub>1</sub> ∈ M';
*** f<sub>1</sub> '''U''' f<sub>2</sub> ∈ M iff f<sub>2</sub> ∈ M or ( f<sub>1</sub> ∈ M and f<sub>1</sub> '''U''' f<sub>2</sub> ∈ M' );
*** f<sub>1</sub> '''R''' f<sub>2</sub> ∈ M iff f<sub>1</sub> ∧ f<sub>2</sub> ∈ M or ( f<sub>2</sub> ∈ M and f<sub>1</sub> '''R''' f<sub>2</sub> ∈ M' )
** Δ<sub>2</sub> = { (init, a, M') | ( M' ∩''AP'' ) ⊆ a ⊆ {p ∈ ''AP'' | ¬p ∉ M' } and f ∈ M' }
* For each f<sub>1</sub> '''U''' f<sub>2</sub> ∈ ''cl''( f ),&nbsp; {M ∈ ''cs''( f ) | f<sub>2</sub> ∈ M or ¬(f<sub>1</sub> '''U''' f<sub>2</sub>) ∈ M } ∈ '''F'''
The three conditions in definition of Δ<sub>1</sub> ensure that any run of ''A'' does not violate semantics of the temporal operators.
Note that '''F''' is a set of sets of states.
The sets in '''F''' are defined to capture a property of operator '''U''' that can not be verified by comparing two consecutive states in a run, i.e.,
if f<sub>1</sub> '''U''' f<sub>2</sub> is true in some state then eventually f<sub>2</sub> is true at some state later.
 
{{hidden begin
|title = Proof of correctness of the above construction
|titlestyle = background:lightblue;
|bg2        = lightgrey
}}
Let ω-word ''w''= a<sub>1</sub>, a<sub>2</sub>,... over alphabet 2<sup>''AP''</sup>. Let ''w''<sup>i</sup> = a<sub>i</sub>, a<sub>i+1</sub>,... .
Let M<sub>''w''</sub> = { f' ∈ ''cl''(f) | ''w'' <math>\vDash</math>  f' }, which we call ''satisfying'' set.
Due to the definition of ''cs''(f),  M<sub>''w''</sub>&nbsp;∈&nbsp;''cs''(f).
We can define a sequence
ρ<sub>''w''</sub> = init, M<sub>''w''<sup>1</sup></sub>, M<sub>''w''<sup>2</sup></sub>,... .
Due to the definition of ''A'',
if w <math>\vDash</math> f then ρ<sub>''w''</sub> must be an accepting run of ''A'' over ''w''.
 
Conversely, lets assume ''A'' accepts ''w''.
Let ρ = init, M<sub>1</sub>, M<sub>2</sub>,... be a run of ''A'' over ''w''.
The following theorem completes the rest of the correctness proof.
 
'''Theorem 1:''' For all i > 0,  M<sub>''w''<sup>i</sup></sub> =  M<sub>i</sub>.
 
'''Proof:''' The proof is by induction on the structure of f' ∈ ''cl''(f).
* Base cases:
** f' = '''true'''. By definitions, f' ∈ M<sub>''w''<sup>i</sup></sub> and f' ∈ M<sub>i</sub>.
** f' = p. By definition of ''A'', p ∈ M<sub>i</sub> iff p ∈ a<sub>i</sub> iff p ∈ M<sub>''w''<sup>i</sup></sub>.
* Induction steps:
** f' = f<sub>1</sub> ∧ f<sub>2</sub>. Due to the definition of consistent sets, f<sub>1</sub> ∧ f<sub>2</sub> ∈ M<sub>i</sub> iff f<sub>1</sub> ∈ M<sub>i</sub> and f<sub>2</sub> ∈ M<sub>i</sub>. Due to induction hypothesis, f<sub>1</sub> ∈ M<sub>''w''<sup>i</sup></sub> and f<sub>2</sub> ∈ M<sub>''w''<sup>i</sup></sub>. Due to definition of satisfying set, f<sub>1</sub> ∧ f<sub>2</sub> ∈ M<sub>''w''<sup>i</sup></sub>.
** f' = ¬f<sub>1</sub>, f' = f<sub>1</sub> ∨ f<sub>2</sub>, f' = '''X''' f<sub>1</sub> or f' = f<sub>1</sub> '''R''' f<sub>2</sub>. The proofs are very similar to the last one.
** f' = f<sub>1</sub> '''U''' f<sub>2</sub>. The proof of equality is divided in two entailment proofs.
*** If f<sub>1</sub> '''U''' f<sub>2</sub> ∈ M<sub>i</sub>, then f<sub>1</sub> '''U''' f<sub>2</sub> ∈ M<sub>''w''<sup>i</sup></sub>. By the definition of the transitions of ''A'', we can have the following two cases.
**** f<sub>2</sub> ∈ M<sub>i</sub>. By induction hypothesis, f<sub>2</sub> ∈ M<sub>''w''<sup>i</sup></sub>. So, f<sub>1</sub> '''U''' f<sub>2</sub> ∈ M<sub>''w''<sup>i</sup></sub>.
**** f<sub>1</sub> ∈ M<sub>i</sub> and f<sub>1</sub> '''U''' f<sub>2</sub> ∈ M<sub>i+1</sub>. And due to the acceptance condition of ''A'', there is at least one index j ≥ i such that f<sub>2</sub> ∈ M<sub>j</sub>. Let j' be the smallest of these indices. We prove the result by induction on k = {j',j'-1,...,i+1,i}. If k = j', then f<sub>2</sub> ∈ M<sub>k</sub>, we apply same argument as in the case of f<sub>2</sub> ∈ M<sub>i</sub>. If  i ≤ k < j', then f<sub>2</sub> ∉ M<sub>k</sub>, and so f<sub>1</sub> ∈ M<sub>k</sub> and f<sub>1</sub> '''U''' f<sub>2</sub> ∈ M<sub>k+1</sub>. Due to induction hypothesis on f', we have f<sub>1</sub> ∈ M<sub>''w''<sup>k</sup></sub>. Due to induction hypothesis on indices, we also have f<sub>1</sub> '''U''' f<sub>2</sub> ∈ M<sub>''w''<sup>k+1</sup></sub>. Due to definition of the semantics of LTL, f<sub>1</sub> '''U''' f<sub>2</sub> ∈ M<sub>''w''<sup>k</sup></sub>.
*** If f<sub>1</sub> '''U''' f<sub>2</sub> ∈ M<sub>''w''<sup>i</sup></sub>, then f<sub>1</sub> '''U''' f<sub>2</sub> ∈ M<sub>i</sub>. Due to the LTL semantics, we can have the following two cases.
**** f<sub>2</sub> ∈ M<sub>''w''<sup>i</sup></sub>. By induction hypothesis, f<sub>2</sub> ∈ M<sub>i</sub>. So, f<sub>1</sub> '''U''' f<sub>2</sub> ∈ M<sub>i</sub>.
**** f<sub>1</sub> ∈ M<sub>''w''<sup>i</sup></sub> and f<sub>1</sub> '''U''' f<sub>2</sub> ∈ M<sub>''w''<sup>i+1</sup></sub>. Due to the LTL semantics, there is at least one index j ≥ i such that f<sub>2</sub> ∈ M<sub>j</sub>. Let j' be the smallest of these indices. Proceed now as in proof of the converse entailment.
 
Due to the above theorem, M<sub>''w''<sup>1</sup></sub> =  M<sub>1</sub>. Due to the definition of the transitions of ''A'',  f ∈ M<sub>1</sub>. Therefore, f ∈ M<sub>''w''<sup>1</sup></sub> and ''w'' <math>\vDash</math> f.
{{hidden end}}
 
===Gerth et al. algorithm===
The following algorithm is due to Gerth, Peled, [[Moshe Y. Vardi|Vardi]], and Wolper.<ref name=GPVW93/>
The above construction creates exponentially many states upfront and many of those states may be unreachable.
The following algorithm has two steps.
In step one, it incrementally constructs a directed graph stored in a tableaux. In step two, it builds an [[labeled generalized Büchi automaton]] (LGBA) by defining nodes of the graph as states and directed edges as transitions.
This algorithm takes reachability into account and may produce a smaller automaton but the worst-case complexity remains the same.
 
The nodes of the graph are labeled by sets of formulas and are obtained by decomposing formulas according to their Boolean structure, and by expanding the temporal operators in order to separate what has to be true immediately from what has to be true from the next state on. For example, assume that an LTL formula  f<sub>1</sub> '''U''' f<sub>2</sub>  appears in the label of a node.
f<sub>1</sub> '''U''' f<sub>2</sub> is equivalent to f<sub>2</sub> ∨ ( f<sub>1</sub> ∧ '''X'''(f<sub>1</sub> '''U''' f<sub>2</sub>) ).
The equivalent expansion suggests that f<sub>1</sub> '''U''' f<sub>2</sub> is true in one of the following two conditions.
# f<sub>1</sub> holds in the current time and (f<sub>1</sub> '''U''' f<sub>2</sub>) holds in the next time step, or
# f<sub>2</sub> holds in the current time step
This logic can be encoded by creating two states (nodes) of the automaton and the automaton may non-deterministically jump to either of them.
In the first case, we have offloaded a part of burden of proof in the next time step
therefore we also create another state(node) that will carry the obligation for next time step in its label.
 
We also need to consider temporal operator '''R''' that may cause such case split.
f<sub>1</sub> '''R''' f<sub>2</sub> is equivalent to ( f<sub>1</sub> ∧ f<sub>2</sub>) ∨ ( f<sub>2</sub> ∧ '''X'''(f<sub>1</sub> '''R''' f<sub>2</sub>) )
and this equivalent expansion suggests that f<sub>1</sub> '''R''' f<sub>2</sub> is true in one of the following two conditions.
# f<sub>2</sub> holds in the current time and (f<sub>1</sub> '''R''' f<sub>2</sub>) holds in the next time step, or
# ( f<sub>1</sub> ∧ f<sub>2</sub>) holds in the current time step.
To avoid many cases in the following algorithm, let us define functions ''new1'', ''next1'' and ''new2'' that encode the above equivalences in the following table.
 
{| class="wikitable"
|-
! f !! new1(f) !! next1(f) !! new2(f)
|-
| f<sub>1</sub> '''U''' f<sub>2</sub> || {f<sub>1</sub>}  || { f<sub>1</sub> '''U''' f<sub>2</sub> } || {f<sub>2</sub>}
|-
| f<sub>1</sub> '''R''' f<sub>2</sub> || {f<sub>2</sub>}  || { f<sub>1</sub> '''R''' f<sub>2</sub> } || {f<sub>1</sub>,f<sub>2</sub>}
|-
| f<sub>1</sub> ∨ f<sub>2</sub> || {f<sub>2</sub>} || ∅ || {f<sub>1</sub>}
|}
We have also added disjunction case in the above table since it also causes a case split in the automaton.
 
Following are the two steps of the algorithm.
 
;Step 1. create_graph
 
In the following box, we present the first part of the algorithm that builds a directed graph. ''create_graph'' is the entry function, which expects the input formula f in the [[Linear temporal logic#Negation normal form|negation normal form]]. It calls recursive function ''expand'' that builds the graph by populating global variables ''Nodes'', ''Incoming'', ''Now'', and ''Next''.
The set ''Nodes'' stores the set of nodes in the graph. The map ''Incoming'' maps each node of ''Nodes'' to a subset of ''Nodes'' ∪ {init}, which defines the set of incoming edges.
''Incoming'' of a node may also contain a special symbol init that is used in the final automaton construction to decide the set of initial states.
''Now'' and ''Next'' map each node of ''Nodes'' to a set of LTL formulas.
For a node q, ''Now''(q) denotes the set of formulas that must be satisfied by the rest of the input word if the automaton is currently at node(state) q.
''Next''(q) denotes the set  of formulas that must be satisfied by the rest of the input word if the automaton is currently at the next node(state) after q.
 
'''typedefs'''
    '''LTL''': LTL formulas
    '''LTLSet''': Sets of LTL formulas
    '''NodeSet''': Sets of graph nodes ∪ {init}
 
  '''globals'''
    ''Nodes'' : set of graph nodes  := ∅
    ''Incoming'': ''Nodes'' → '''NodeSet''' := ∅
    ''Now''    : ''Nodes'' → '''LTLSet''' := ∅
    ''Next''  : ''Nodes'' → '''LTLSet''' := ∅
 
  '''function''' ''create_graph''('''LTL''' f){
    expand({f}, ∅, ∅, {init} )
    '''return''' (''Nodes'', ''Now'', ''Incoming'')
  }
 
  '''function''' expand('''LTLSet''' new, '''LTLSet''' old, '''LTLSet''' next, '''NodeSet''' incoming){
  1: '''if''' new = ∅ '''then'''
  2:    '''if''' ∃q ∈ ''Nodes'': ''Next''(q)=next ∧ ''Now''(q)=old '''then'''
  3:      ''Incoming''(q)  := ''Incoming''(q) ∪ incoming
  4:    '''else'''
  5:      q  := ''new_node''()
  6:      ''Nodes'' := ''Nodes'' ∪ {q}
  7:      ''Incoming''(q)  := incoming
  8:      ''Now''(q)  := old
  9:      ''Next''(q)  := next
10:      expand(''Next''(q), ∅, ∅, {q})
11: '''else'''
12:    f ∈ new
13:    new  := new\{f}
14:    old  := old ∪ {f}
15:    '''match''' f '''with'''
16:    | '''true''', '''false''', p, or ¬p, where  p ∈ ''AP''  →
17:      '''if''' f = '''false''' ∨ ''neg''(f) ∈ old '''then'''
18:          '''skip'''
19:      '''else'''
20:          expand(new, old, next, incoming)
21:    | f<sub>1</sub> ∧ f<sub>2</sub> →
22:      expand(new ∪ {f<sub>1</sub>,f<sub>2</sub>}, old, next, incoming)
23:    | '''X''' g →
24:      expand(new, old, next ∪ {g}, incoming)     
25:    | f<sub>1</sub> ∨ f<sub>2</sub>, f<sub>1</sub> '''U''' f<sub>2</sub>, or f<sub>1</sub> '''R''' f<sub>2</sub> →
26:       expand(new ∪ (''new1''(f)/old), old, next ∪ ''next1''(f), incoming)
27:      expand(new ∪ (''new2''(f)/old), old, next, incoming)
28: '''return'''
  }
 
The code of ''expand'' is labelled with line numbers for easy reference.
Each call to ''expand'' aims to add a node and its successors nodes in the graph.
The parameters of the call describes a potential new node.
The first parameter ''new'' contains the set of formulas that are yet to be expanded. The second parameter ''old'' contains the set of formulas that are already expanded.
The third parameter ''next'' is the set of the formula using which successor node will be created.
The fourth parameter ''incoming'' defines set of incoming edges when the node is added to the graph.
At line 1, the '''if''' condition checks if ''new'' contains any formula to be expanded.
If the ''new'' is empty then at line 2 the '''if''' condition checks if there already exists a state q' with same set of expanded formulas.
If that is the case, then we do not add a redundant node, but we add parameter ''incoming'' in ''Incoming''(q') at line 3.
Otherwise, we add a new node q using the parameters at lines 5–9 and we start expanding a successor node of q using ''next''(q) as its unexpanded set of formulas at line 10.
In the case ''new'' is not empty, then we have more formulas to expand and control jumps from line 1 to 12.
At lines 12–14, a formula f from ''new'' is selected and moved to ''old''.
Depending on structure of f, the rest of the function executes.
If f is a literal, then expansion continues at line 20, but if ''old'' already contains
''neg''(f) or f='''false''', then ''old'' contains an inconsistent formula and we discard this node by not making any recursive all at line 18.
If f = f<sub>1</sub> ∧ f<sub>2</sub>, then f<sub>1</sub> and f<sub>2</sub> are added to ''new'' and a recursive call is made for further expansion at line 22.
If f = '''X''' f<sub>1</sub>, then f<sub>1</sub> is added to ''next'' for the successor of the current node under consideration at line 24.
If f = f<sub>1</sub> ∨ f<sub>2</sub>, f = f<sub>1</sub> '''U''' f<sub>2</sub>, or f = f<sub>1</sub> '''R''' f<sub>2</sub> then the current node is divided into two nodes and for each node a recursive call is made. For the recursive calls, ''new'' and ''next'' are modified using functions ''new1'', ''next1'', and ''new2'' that were defined in the above table.
<!--
There are following four possible results of the call.
* The description is modified and a recursive call is made. (lines 20, 22, and 24)
* The description is split and recursive calls are made for each split. (lines 26 and 27)
* The description is discarded and no nodes are added (lines 3 and 18)
* The node corresponding to the description is added to the graph and a recursive call for a successor node is made. ( lines 5--10) -->
 
; Step 2. LGBA construction
Let (''Nodes'', ''Now'', ''Incoming'') = create_graph(f).
An equivalent LGBA to f is ''A''=(''Nodes'', 2<sup>''AP''</sup>, ''L'', Δ, ''Q''<sub>0</sub>, '''F'''), where
* ''L'' = { (q,a) | q ∈ ''Nodes'' and (''Now''(q) ∩ ''AP'') ⊆ a ⊆ {p ∈ P | ¬p ∉ ''Now''(q) } }
* Δ = {(q,q')| q,q' ∈ Nodes and q ∈ Incoming(q') }
* ''Q''<sub>0</sub> = { q ∈ Nodes | init ∈ ''Now''(q) }
* '''F''' = { { q ∈ Nodes | f<sub>2</sub> ∈ ''Now''(q) or (f<sub>1</sub> '''U''' f<sub>2</sub>) ∉ ''Now''(q) } |  f<sub>1</sub> '''U''' f<sub>2</sub> ∈ ''cl''( f ) }
 
Note that node labels in the algorithmic construction does not not contain negation of sub-formulas of f. In the declarative construction a node has the set of formulas that are expected to be true. The algorithmic construction ensures the correctness without the need of all the true formulas to be present in a node label.
 
==Tools==
*[http://spot.lip6.fr SPOT LTL2TGBA] - LTL2TGBA translator included in Object-oriented model checking library SPOT. Online translator available.
*[http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/ LTL2BA] - Fast LTL to BA translator via alternating automata. Online translator available.
*[http://sourceforge.net/projects/ltl3ba/ LTL3BA] - An up-to-date improvement of LTL2BA.
 
==References==
 
{{Reflist}}
 
{{DEFAULTSORT:Linear temporal logic to Buchi automaton}}
[[Category:Automata theory]]
[[Category:Model checking]]
[[Category:Temporal logic]]

Revision as of 10:06, 18 October 2013

In formal verification, finite state model checking needs to compute an equivalent Büchi automaton (BA) to a Linear temporal logic (LTL) formula, i.e., the LTL formula and the BA recognizes the same ω-language. There are algorithms that translate a LTL formula to an equivalent BA.[1] [2] [3] [4] This transformation is normally done in two steps. The first step produces a generalized Büchi automaton(GBA) from a LTL formula. The second step translates this GBA into a BA, which involves relatively easy construction. Since LTL is strictly less expressive than BA, the reverse construction is not possible.

The algorithms for transforming LTL to GBA differ in their construction strategies but they all have common underlying principle, i.e., each state in the constructed automaton represents a set of LTL formulas that are expected to be satisfied by the remaining input word after occurrence of the state during a run.

Transformation from LTL to GBA

Here two algorithms are presented for the construction. The first one provides a declarative and easy to understand construction. The second one provides an algorithmic and efficient construction. Both the algorithms assume that the input formula f is constructed using the set of propositional variables AP and f is in negation normal form. For each LTL formula f' without ¬ as top symbol, let neg(f') = ¬f', neg(¬f') = f'. For a special case f'=true, let neg(true) = false.

Declarative construction

Before describing the construction, we need to present a few auxiliary definitions. For a LTL formula f, Let cl( f ) be a smallest set of formulas that satisfies the following conditions:

  • truecl( f )
  • f ∈ cl( f )
  • if f1cl( f ) then neg(f1) ∈ cl( f )
  • if X f1cl( f ) then f1cl( f )
  • if f1 ∧ f2cl( f ) then f1,f2cl( f )
  • if f1 ∨ f2cl( f ) then f1,f2cl( f )
  • if f1 U f2cl( f ) then f1,f2cl( f )
  • if f1 R f2cl( f ) then f1,f2cl( f )

cl( f ) is closure of sub-formulas of f under negation. Note that cl( f ) may contain formulas that are not in negation normal form. The subsets of cl( f ) are going to serve as states of the equivalent GBA. We aim to construct the GBA such that if a state corresponds to a subset M ⊂ cl( f ) then the GBA has an accepting run starting from the state for a word iff the word satisfies every formula in M and violates every formula in cl( f )/M. For this reason, we will not consider each formula set M that is clearly inconsistent or subsumed by a strictly super set M' such that M and M' are equiv-satisfiable. A set M ⊂ cl( f ) is maximally consistent if it satisfies the following conditions:

  • true ∈ M
  • f1 ∈ M iff ¬f1 ∉ M
  • f1 ∧ f2 ∈ M iff f1 ∈ M and f2 ∈ M
  • f1 ∨ f2 ∈ M iff f1 ∈ M or f2 ∈ M

Let cs( f ) be the set of maximally consistent subsets of cl( f ). We are going to use only cs( f ) as the states of GBA.

GBA construction

An equivalent GBA to f is A= ({init}∪cs( f ), 2AP, Δ,{init},F), where

  • Δ = Δ1 ∪ Δ2
    • (M, a, M') ∈ Δ1 iff ( M' ∩AP ) ⊆ a ⊆ {p ∈ AP | ¬p ∉ M' } and:
      • X f1 ∈ M iff f1 ∈ M';
      • f1 U f2 ∈ M iff f2 ∈ M or ( f1 ∈ M and f1 U f2 ∈ M' );
      • f1 R f2 ∈ M iff f1 ∧ f2 ∈ M or ( f2 ∈ M and f1 R f2 ∈ M' )
    • Δ2 = { (init, a, M') | ( M' ∩AP ) ⊆ a ⊆ {p ∈ AP | ¬p ∉ M' } and f ∈ M' }
  • For each f1 U f2cl( f ),  {M ∈ cs( f ) | f2 ∈ M or ¬(f1 U f2) ∈ M } ∈ F

The three conditions in definition of Δ1 ensure that any run of A does not violate semantics of the temporal operators. Note that F is a set of sets of states. The sets in F are defined to capture a property of operator U that can not be verified by comparing two consecutive states in a run, i.e., if f1 U f2 is true in some state then eventually f2 is true at some state later.

Template:Hidden begin Let ω-word w= a1, a2,... over alphabet 2AP. Let wi = ai, ai+1,... . Let Mw = { f' ∈ cl(f) | w f' }, which we call satisfying set. Due to the definition of cs(f), Mw ∈ cs(f). We can define a sequence ρw = init, Mw1, Mw2,... . Due to the definition of A, if w f then ρw must be an accepting run of A over w.

Conversely, lets assume A accepts w. Let ρ = init, M1, M2,... be a run of A over w. The following theorem completes the rest of the correctness proof.

Theorem 1: For all i > 0, Mwi = Mi.

Proof: The proof is by induction on the structure of f' ∈ cl(f).

  • Base cases:
    • f' = true. By definitions, f' ∈ Mwi and f' ∈ Mi.
    • f' = p. By definition of A, p ∈ Mi iff p ∈ ai iff p ∈ Mwi.
  • Induction steps:
    • f' = f1 ∧ f2. Due to the definition of consistent sets, f1 ∧ f2 ∈ Mi iff f1 ∈ Mi and f2 ∈ Mi. Due to induction hypothesis, f1 ∈ Mwi and f2 ∈ Mwi. Due to definition of satisfying set, f1 ∧ f2 ∈ Mwi.
    • f' = ¬f1, f' = f1 ∨ f2, f' = X f1 or f' = f1 R f2. The proofs are very similar to the last one.
    • f' = f1 U f2. The proof of equality is divided in two entailment proofs.
      • If f1 U f2 ∈ Mi, then f1 U f2 ∈ Mwi. By the definition of the transitions of A, we can have the following two cases.
        • f2 ∈ Mi. By induction hypothesis, f2 ∈ Mwi. So, f1 U f2 ∈ Mwi.
        • f1 ∈ Mi and f1 U f2 ∈ Mi+1. And due to the acceptance condition of A, there is at least one index j ≥ i such that f2 ∈ Mj. Let j' be the smallest of these indices. We prove the result by induction on k = {j',j'-1,...,i+1,i}. If k = j', then f2 ∈ Mk, we apply same argument as in the case of f2 ∈ Mi. If i ≤ k < j', then f2 ∉ Mk, and so f1 ∈ Mk and f1 U f2 ∈ Mk+1. Due to induction hypothesis on f', we have f1 ∈ Mwk. Due to induction hypothesis on indices, we also have f1 U f2 ∈ Mwk+1. Due to definition of the semantics of LTL, f1 U f2 ∈ Mwk.
      • If f1 U f2 ∈ Mwi, then f1 U f2 ∈ Mi. Due to the LTL semantics, we can have the following two cases.
        • f2 ∈ Mwi. By induction hypothesis, f2 ∈ Mi. So, f1 U f2 ∈ Mi.
        • f1 ∈ Mwi and f1 U f2 ∈ Mwi+1. Due to the LTL semantics, there is at least one index j ≥ i such that f2 ∈ Mj. Let j' be the smallest of these indices. Proceed now as in proof of the converse entailment.

Due to the above theorem, Mw1 = M1. Due to the definition of the transitions of A, f ∈ M1. Therefore, f ∈ Mw1 and w f. Template:Hidden end

Gerth et al. algorithm

The following algorithm is due to Gerth, Peled, Vardi, and Wolper.[3] The above construction creates exponentially many states upfront and many of those states may be unreachable. The following algorithm has two steps. In step one, it incrementally constructs a directed graph stored in a tableaux. In step two, it builds an labeled generalized Büchi automaton (LGBA) by defining nodes of the graph as states and directed edges as transitions. This algorithm takes reachability into account and may produce a smaller automaton but the worst-case complexity remains the same.

The nodes of the graph are labeled by sets of formulas and are obtained by decomposing formulas according to their Boolean structure, and by expanding the temporal operators in order to separate what has to be true immediately from what has to be true from the next state on. For example, assume that an LTL formula f1 U f2 appears in the label of a node. f1 U f2 is equivalent to f2 ∨ ( f1X(f1 U f2) ). The equivalent expansion suggests that f1 U f2 is true in one of the following two conditions.

  1. f1 holds in the current time and (f1 U f2) holds in the next time step, or
  2. f2 holds in the current time step

This logic can be encoded by creating two states (nodes) of the automaton and the automaton may non-deterministically jump to either of them. In the first case, we have offloaded a part of burden of proof in the next time step therefore we also create another state(node) that will carry the obligation for next time step in its label.

We also need to consider temporal operator R that may cause such case split. f1 R f2 is equivalent to ( f1 ∧ f2) ∨ ( f2X(f1 R f2) ) and this equivalent expansion suggests that f1 R f2 is true in one of the following two conditions.

  1. f2 holds in the current time and (f1 R f2) holds in the next time step, or
  2. ( f1 ∧ f2) holds in the current time step.

To avoid many cases in the following algorithm, let us define functions new1, next1 and new2 that encode the above equivalences in the following table.

f new1(f) next1(f) new2(f)
f1 U f2 {f1} { f1 U f2 } {f2}
f1 R f2 {f2} { f1 R f2 } {f1,f2}
f1 ∨ f2 {f2} {f1}

We have also added disjunction case in the above table since it also causes a case split in the automaton.

Following are the two steps of the algorithm.

Step 1. create_graph

In the following box, we present the first part of the algorithm that builds a directed graph. create_graph is the entry function, which expects the input formula f in the negation normal form. It calls recursive function expand that builds the graph by populating global variables Nodes, Incoming, Now, and Next. The set Nodes stores the set of nodes in the graph. The map Incoming maps each node of Nodes to a subset of Nodes ∪ {init}, which defines the set of incoming edges. Incoming of a node may also contain a special symbol init that is used in the final automaton construction to decide the set of initial states. Now and Next map each node of Nodes to a set of LTL formulas. For a node q, Now(q) denotes the set of formulas that must be satisfied by the rest of the input word if the automaton is currently at node(state) q. Next(q) denotes the set of formulas that must be satisfied by the rest of the input word if the automaton is currently at the next node(state) after q.

typedefs
    LTL: LTL formulas
   LTLSet: Sets of LTL formulas
   NodeSet: Sets of graph nodes ∪ {init}
 
 globals
    Nodes : set of graph nodes  := ∅
   Incoming: NodesNodeSet := ∅
   Now    : NodesLTLSet := ∅
   Next   : NodesLTLSet := ∅
 
 function create_graph(LTL f){
    expand({f}, ∅, ∅, {init} )
    return (Nodes, Now, Incoming)
 }
 
 function expand(LTLSet new, LTLSet old, LTLSet next, NodeSet incoming){
 1: if new = ∅ then
 2:    if ∃q ∈ Nodes: Next(q)=next ∧ Now(q)=old then
 3:       Incoming(q)  := Incoming(q) ∪ incoming
 4:    else
 5:       q  := new_node()
 6:       Nodes := Nodes ∪ {q}
 7:       Incoming(q)  := incoming
 8:       Now(q)  := old
 9:       Next(q)  := next
10:       expand(Next(q), ∅, ∅, {q})
11: else
12:    f ∈ new
13:    new  := new\{f}
14:    old  := old ∪ {f}
15:    match f with
16:     | true, false, p, or ¬p, where  p ∈ AP  →
17:       if f = falseneg(f) ∈ old then
18:          skip
19:       else
20:          expand(new, old, next, incoming)
21:     | f1 ∧ f2 →
22:       expand(new ∪ {f1,f2}, old, next, incoming)
23:     | X g →
24:       expand(new, old, next ∪ {g}, incoming)       
25:     | f1 ∨ f2, f1 U f2, or f1 R f2 →
26:       expand(new ∪ (new1(f)/old), old, next ∪ next1(f), incoming)
27:       expand(new ∪ (new2(f)/old), old, next, incoming)
28: return
 }

The code of expand is labelled with line numbers for easy reference. Each call to expand aims to add a node and its successors nodes in the graph. The parameters of the call describes a potential new node. The first parameter new contains the set of formulas that are yet to be expanded. The second parameter old contains the set of formulas that are already expanded. The third parameter next is the set of the formula using which successor node will be created. The fourth parameter incoming defines set of incoming edges when the node is added to the graph. At line 1, the if condition checks if new contains any formula to be expanded. If the new is empty then at line 2 the if condition checks if there already exists a state q' with same set of expanded formulas. If that is the case, then we do not add a redundant node, but we add parameter incoming in Incoming(q') at line 3. Otherwise, we add a new node q using the parameters at lines 5–9 and we start expanding a successor node of q using next(q) as its unexpanded set of formulas at line 10. In the case new is not empty, then we have more formulas to expand and control jumps from line 1 to 12. At lines 12–14, a formula f from new is selected and moved to old. Depending on structure of f, the rest of the function executes. If f is a literal, then expansion continues at line 20, but if old already contains neg(f) or f=false, then old contains an inconsistent formula and we discard this node by not making any recursive all at line 18. If f = f1 ∧ f2, then f1 and f2 are added to new and a recursive call is made for further expansion at line 22. If f = X f1, then f1 is added to next for the successor of the current node under consideration at line 24. If f = f1 ∨ f2, f = f1 U f2, or f = f1 R f2 then the current node is divided into two nodes and for each node a recursive call is made. For the recursive calls, new and next are modified using functions new1, next1, and new2 that were defined in the above table.

Step 2. LGBA construction

Let (Nodes, Now, Incoming) = create_graph(f). An equivalent LGBA to f is A=(Nodes, 2AP, L, Δ, Q0, F), where

  • L = { (q,a) | q ∈ Nodes and (Now(q) ∩ AP) ⊆ a ⊆ {p ∈ P | ¬p ∉ Now(q) } }
  • Δ = {(q,q')| q,q' ∈ Nodes and q ∈ Incoming(q') }
  • Q0 = { q ∈ Nodes | init ∈ Now(q) }
  • F = { { q ∈ Nodes | f2Now(q) or (f1 U f2) ∉ Now(q) } | f1 U f2cl( f ) }

Note that node labels in the algorithmic construction does not not contain negation of sub-formulas of f. In the declarative construction a node has the set of formulas that are expected to be true. The algorithmic construction ensures the correctness without the need of all the true formulas to be present in a node label.

Tools

  • SPOT LTL2TGBA - LTL2TGBA translator included in Object-oriented model checking library SPOT. Online translator available.
  • LTL2BA - Fast LTL to BA translator via alternating automata. Online translator available.
  • LTL3BA - An up-to-date improvement of LTL2BA.

References

43 year old Petroleum Engineer Harry from Deep River, usually spends time with hobbies and interests like renting movies, property developers in singapore new condominium and vehicle racing. Constantly enjoys going to destinations like Camino Real de Tierra Adentro.

  1. M.Y. Vardi and P. Wolper, Reasoning about infinite computations, Information and Computation, 115(1994), 1–37.
  2. Y.Kesten,Z.Manna,H.McGuire,A.Pnueli,A decision algorithm for full propositional temporal logic, CAV’93, Elounda, Greece, LNCS 697, Springer–Verlag, 97-109.
  3. 3.0 3.1 R. Gerth, D. Peled, M.Y. Vardi and P. Wolper, "Simple On-The-Fly Automatic Verification of Linear Temporal Logic," Proc. IFIP/WG6.1 Symp. Protocol Specification, Testing, and Verification (PSTV95), pp. 3-18,Warsaw, Poland, Chapman & Hall, June 1995.
  4. P. Gastin and D. Oddoux, Fast LTL to Büchi automata translation, Thirteenth Conference on Computer Aided Verification (CAV ′01), number 2102 in LNCS, Springer-Verlag (2001), pp. 53–65.