Content deleted Content added
No edit summary |
→Gerth et al. algorithm: then then → then; person |
||
Line 116:
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
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,
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
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.
Line 213:
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
Otherwise, we add a new node q using the parameters at lines
In the case ''new'' is not empty, then we have more formulas to expand and control jumps from line 1 to 12.▼
Depending on structure of f, the rest of the function executes.▼
▲In the case ''new'' is not empty then we have more formulas to expand and
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.▼
▲At lines 12--14, a formula f from ''new'' is selected and moved to ''old''.
If f = f<sub>1</sub> ∧ f<sub>2</sub>, then
▲Depending on structure of f, rest of the function executes.
If f = '''X''' f<sub>1</sub>, then f<sub>1</sub> is added to ''next'' for the successor
▲If f is a literal then expansion continues at line 20, but if ''old'' already contains
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. ▼
▲''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.
▲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.
| |||