arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 1002.3222

Structural Analysis of Boolean Equation Systems

Jeroen Keiren·Michel A. Reniers·Tim A. C. Willemse
View original source ↗Read source document ↗Export metadata ↓

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.

Explore related subjects

cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Jeroen Keiren, Michel A. Reniers, Tim A. C. Willemse. 2010-02-17. Structural Analysis of Boolean Equation Systems. https://doi.org/10.1145/2071368.2071376

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Overview and Roadmap of Team Automata

Team Automata is a formalism for interacting component-based systems proposed in 1997, whereby multiple sending and receiving actions from concurrent automata can synchronise. During the past 25+ years, team automata have been studied and applied in many different contexts, involving 25+ researchers and resulting in 25+ publications. In this paper, we first revisit the specific notion of synchronisation and composition of team automata, relating it to other relevant coordination models, such as Reo, BIP, Contract Automata, Choreography Automata, and Multi-Party Session Types. We then identify several aspects that have recently been investigated for team automata and related models. These include communication properties (which are the properties of interest?), realisability (how to decompose a global model into local components?), tool support (what has been automatised or implemented?), and variability (can a family of concrete product (automata) models be captured concisely?). Our presentation of these aspects provides a snapshot of the most recent trends in research on team automata, and delineates a roadmap for future research, both for team automata and for related formalisms.

cs.LO↗
arXiv2026

Derivatives for Containers in Univalent Foundations

Containers conveniently represent a wide class of inductive data types. Their derivatives compute representations of types of one-hole contexts, useful for implementing tree-traversal algorithms. Derivatives of discrete containers (whose positions have decidable equality) satisfy a universal property with respect to linear morphisms of containers. This induces a well-behaved notion of linear substitution for one-hole contexts. Working in Univalent Foundations, we extend the derivative operation to untruncated containers (whose shapes and positions are arbitrary types). We prove that this derivative, defined in terms of a set of isolated positions, satisfies an appropriate universal property in the wild category of untruncated containers and linear morphisms, as well as basic laws with respect to constants, sums and products. A chain rule exists, but is in general non-invertible. In fact, a globally invertible chain rule is inconsistent in the presence of non-set types, and equivalent to a classical principle when restricted to set-truncated containers. We derive a rule for derivatives of least fixpoints from the chain rule, and characterize its invertibility. All of our results are formalized in Cubical Agda.

cs.LO↗
arXiv2026

Model Checking HyperRecHML is Decidable

Temporal hyperlogics combine explicit quantification over traces with temporal requirements evaluated over the quantified traces. HyperRecHML is a temporal hyperlogic which allows for arbitrary mixing of trace quantification and the use of fixed points for expressing temporal requirements, which makes it very expressive in comparison to other first-order hyperlogics. HyperRecHML has already been successfully applied in runtime verification, but the decidability of its model checking problem remains open. We answer this question positively by providing two main contributions. Firstly, a normalization procedure that allows to reduce arbitrary HyperRecHML formulas to a normal form with restricted nesting of trace quantification and fixed points. Secondly, we provide an automata-based model checking algorithm for formulas of this normal form. The complexity of our algorithm is comparable to similar ones for other hyperlogics, despite the extra expressive power.

cs.LO↗