Solving disjunctive/conjunctive boolean equation systems with alternating fixed points

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

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

9 Citations (Scopus)
5 Downloads (Pure)

Abstract

This paper presents a technique for the resolution of alternating disjunctive/conjunctive boolean equation systems. The technique can be used to solve various verification problems on finite-state concurrent systems, by encoding the problems as boolean equation systems and determining their local solutions. The main contribution of this paper is that a recent resolution technique from [13] for disjunctive/conjunctive boolean equation systems is extended to the more general disjunctive/conjunctive forms with alternation. Our technique has the time complexity O(m+n 2), where m is the number of alternation free variables occurring in the equation system and n the number of alternating variables. We found that many µ-calculus formulas with alternating fixed points occurring in the literature can be encoded as boolean equation systems of disjunctive/conjunctive forms. Practical experiments show that we can verify alternating formulas on state spaces that are orders of magnitudes larger than reported up till now.
Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems (Proceedings TACAS 2004, Part of ETAPS 2004, Barcelona, Spain, March 29-April 2, 2004)
EditorsK. Jensen, A. Podelski
Place of PublicationBerlin
PublisherSpringer
Pages436-450
Number of pages15
ISBN (Print)3-540021299-X
DOIs
Publication statusPublished - 2004

Publication series

NameLecture Notes in Computer Science
Volume2988
ISSN (Print)0302-9743

Fingerprint

Dive into the research topics of 'Solving disjunctive/conjunctive boolean equation systems with alternating fixed points'. Together they form a unique fingerprint.

Cite this