A sub-quadratic algorithm for conjunctive and disjunctive boolean equation systems

J.F. Groote, M.K. Keinänen

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

5 Citaten (Scopus)

Samenvatting

We present a new algorithm for conjunctive and disjunctive boolean equation systems which arise frequently in the verification and analysis of finite state concurrent systems. In contrast to the previously known O(e 2) time algorithms, our algorithm computes the solution to such a fixpoint equation system with size e and alternation depth d in O(e log d) time (here d <e). We show the correctness and complexity of the algorithm. We discuss heuristics and describe how the algorithm can be efficiently implemented. The algorithm is compared to a previous solution via experiments on verification examples. Our measurements indicate that the new algorithm makes the verification of a large class of fixpoint expressions more tractable.
Originele taal-2Engels
TitelTheoretical aspects of computing : second International colloquium, ICTAC 2005, Hanoi, Vietnam, October 17-21, 2005 : proceedings
RedacteurenD.V. Hung, M. Wirsing
Plaats van productieBerlin
UitgeverijSpringer
Pagina's532-545
ISBN van geprinte versie3-540-29107-5
DOI's
StatusGepubliceerd - 2005

Publicatie series

NaamLecture Notes in Computer Science
Volume3722
ISSN van geprinte versie0302-9743

Vingerafdruk Duik in de onderzoeksthema's van 'A sub-quadratic algorithm for conjunctive and disjunctive boolean equation systems'. Samen vormen ze een unieke vingerafdruk.

Citeer dit