Fix a typo.
This commit is contained in:
parent
38e778d4e5
commit
56d4dbd224
Notes:
svn2git
2021-03-31 03:12:20 +00:00
svn path=/head/; revision=95717
@ -4,7 +4,7 @@ in the temporal logic CTL (Computational Tree Logic).
|
|||||||
|
|
||||||
One specifies the finite state system (finite automaton,
|
One specifies the finite state system (finite automaton,
|
||||||
Mealy machine, full adder circuit, ..) as a Kripke
|
Mealy machine, full adder circuit, ..) as a Kripke
|
||||||
structure in the SMV language and provides specificaations
|
structure in the SMV language and provides specifications
|
||||||
in CTL. The model checking algorithm allows to determine
|
in CTL. The model checking algorithm allows to determine
|
||||||
if the Kripke structure fulfills the specifications.
|
if the Kripke structure fulfills the specifications.
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user