No label defined (Q4037101)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
scientific article; zbMATH DE number 177249
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | No label defined |
scientific article; zbMATH DE number 177249 |
Statements
18 May 1993
0 references
model checking algorithm
0 references
computation tree logic
0 references
vector processors
0 references
CTL
0 references
0.9479940533638
0 references
0.9479940533638
0 references
0.8156635165214539
0 references
0.8156633973121643
0 references
0.779215931892395
0 references
[For the entire collection see Zbl 0753.00020.] A global model checking algorithm for computation tree logic (CTL) which is suitable for running on vector processors is presented. The basic idea is directly extracted from the definitions of CTL operators. However, the vectorized algorithm uses repeated uniform operations on array type data. The algorithm runs in bottom-up way by labelling each state with the truth value of each sub-formula contained in a given CTL formula. It runs in time liner in both the size of the transition system and the length of the CTL formula. An implementation on a vector processor FACOM VP 400 E and some experimental results are discussed as well.
0 references
