An example of sequentialization of a parallel algorithm

DOI10.1016/0167-6423(89)90017-8MaRDI QIDQ1262778zbMATH OpenOpenAlexFDO

Authors André Arnold

Publication date 1989

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0167-6423(89)90017-8

zbMATH Keywords

finite transition systemleast fixed pointparallel algorithm

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Algorithms in computer science (68W99)

Review text

The verification that a finite transition system, representing a process, satisfies a formula of some branching-time logic amounts to computing the least fixed point of a system of equations over this transition system. \textit{A. Arnold} and \textit{P. Crubille} [Inf. Process. Lett. 29, No.2, 57- 66 (1988; Zbl 0663.68075)] proposed a sequential algorithm to compute these least fixed points. It is shown how this algorithm could be derived from a parallel one.

Recommendations

• A linear algorithm to solve fixed-point equations on transition systems
• An improved algorithm for the evaluation of fixpoint expressions
• Efficient model checking algorithms for computation tree logic and their application to the verification of parallel programs
• Parallel and symbolic model checking for fixpoint logic with chop
• scientific article; zbMATH DE number 719843

Cited in

(2)

• A linear algorithm to solve fixed-point equations on transition systems
• Complex variables approach to the short-axis-mode rotation of a rigid body

This page was built for publication: An example of sequentialization of a parallel algorithm

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