Structural analysis of Boolean equation systems

DOI10.1145/2071368.2071376MaRDI QIDQ2946656zbMATH OpenOpenAlexFDO

Authors Jeroen J. A. Keiren, Michel A. Reniers, T. A. C. Willemse

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1002.3222

zbMATH Keywords

bisimilarityBoolean equation systemsstructure graphs

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: We analyse the problem of solving Boolean equation systems through the use of structure graphs. The latter are obtained through an elegant set of Plotkin-style deduction rules. Our main contribution is that we show that equation systems with bisimilar structure graphs have the same solution. We show that our work conservatively extends earlier work, conducted by Keiren and Willemse, in which dependency graphs were used to analyse a subclass of Boolean equation systems, viz., equation systems in standard recursive form. We illustrate our approach by a small example, demonstrating the effect of simplifying an equation system through minimisation of its structure graph.

Recommendations

• Analysis of Boolean equation systems through structure graphs
• Parameterised Boolean equation systems
• CONCUR 2004 - Concurrency Theory
• Proof graphs for parameterised Boolean equation systems
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(7)

• Parameterised Boolean equation systems
• Consistent consequence for Boolean equation systems
• UN-KLEENE BOOLEAN EQUATION SOLVING
• scientific article; zbMATH DE number 1538042 (Why is no real title available?)
• Analysis of Boolean equation systems through structure graphs
• Analysis of Boolean Programs
• Theoretical Aspects of Computing – ICTAC 2005

Describes a project that uses

Uses Software

• CADP
• CAESAR_SOLVE

This page was built for publication: Structural analysis of Boolean equation systems

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