2012 | OriginalPaper | Chapter
Consistent Consequence for Boolean Equation Systems
Authors : Maciej W. Gazda, Tim A. C. Willemse
Published in: SOFSEM 2012: Theory and Practice of Computer Science
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Inspired by the concept of a consistent correlation for Boolean equation systems, we introduce and study a novel relation, called
consistent consequence
. We show that it can be used as an approximation of the solution to an equation system. For the closed, simple and recursive fragment of equation systems we prove that it coincides with
direct simulation
for parity games. In addition, we show that deciding both consistent consequence and consistent correlations are coNP-complete problems, and we provide a sound and complete proof system for consistent consequence. As an application, we define a novel abstraction mechanism for parameterised Boolean equation systems and we establish its correctness using our theory.