scientific article; zbMATH DE number 177249

MaRDI QIDQ4037101zbMATH OpenFDO

Authors Hiromi Hiraishi, Shintaro Meki, Kiyoharu Hamaguchi

Publication date 18 May 1993

zbMATH Keywords

computation tree logicCTLmodel checking algorithmvector processors

Mathematics Subject Classification ID

Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04) Modal logic (including the logic of norms) (03B45) Reliability, testing and fault tolerance of networks and computer systems (68M15) Semantics in the theory of computing (68Q55)

Review text

[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.

Recommendations

• Vectorized model checking for computation tree logic
• Model Checking CTL is Almost Always Inherently Sequential
• Efficient model checking algorithms for computation tree logic and their application to the verification of parallel programs
• Distributed Computing - IWDC 2004
• CTL^* model checking on a shared-memory architecture

Cited in

(3)

• Vectorized model checking for computation tree logic
• Model Checking Quantified Computation Tree Logic
• Efficient model checking algorithms for computation tree logic and their application to the verification of parallel programs

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4037101)