×

A selection property of the boolean \(\mu\)-calculus and some of its applications. (English) Zbl 0936.03030

Let \(\mathbb B\) be the Boolean algebra of two elements 0 and 1, \(I\) be a set of indices of arbitrary cardinality, \(\mathbb B^I\) is a complete lattice with minimum 0 and maximum 1, \(f(x_1,\dots,x_n): (\mathbb B^I)^n\to\mathbb B^I\) be a mapping monotonic in all its arguments, \(f_i(x_1,\dots,x_n): (\mathbb B^I)^n\to\mathbb B\) be the component of \(f\) of index \(i\). It is assumed that for each index \(i\in I\) there exists a set \(J_i\) of indices of arbitrary cardinality such that \[ f_i(x_1,\dots,x_n) = \sum_{j\in J_i}f_{i,j}(x_1,\dots,x_n). \] A selector is a mapping \(\sigma\) that associates with each \(i\) in \(I\) an element \(\sigma(i)\) of \(J_i\). Define \(f_\sigma(x_1,\dots,x_n): (\mathbb B^I)^n\to\mathbb B^I\) as the mapping whose \(i\)-th component is \(f_{i,\sigma(i)}(x_1,\dots,x_n): (\mathbb B^I)^n\to\mathbb B\). Let the quantities \(\mu\) and \(\nu\) be the least and the greatest correspondingly and every \(\theta_i\) be \(\mu\) or \(\nu\).
Theorem. Let \(f\) be defined as above and let \[ a = \theta_1 x_1\dots\theta_n x_n\cdot f(x_1,\dots,x_n)\in\mathbb B^I. \] Then there exists a selector \(\sigma\) such that \[ a = \theta_1 x_1\dots\theta_n x_n\cdot f_{\sigma}(x_1,\dots,x_n). \] Applications to the McNaughton’s games on graphs and to modal \(\mu\)-calculus are given.
Reviewer: A.Nabebin (Moskva)

MSC:

03B70 Logic in computer science
68Q60 Specification and verification (program logics, model checking, etc.)
03D05 Automata and formal grammars in connection with logical questions
06B23 Complete lattices, completions
06E30 Boolean functions
68Q45 Formal languages and automata
PDF BibTeX XML Cite
Full Text: DOI EuDML

References:

[1] 1. H. R. ANDERSEN, Model checking and boolean graphs. Theor. Comp. Sci., 1994, 126, pp. 3-30. Zbl0798.03017 MR1268020 · Zbl 0798.03017
[2] 2. A. ARNOLD, An initial semantics for the \mu -calculus on trees and Rabin’s complementation lemma. Theor. Comp. Sci., 1995, 148, pp. 121-132. Zbl0873.68157 MR1347671 · Zbl 0873.68157
[3] 3. A. ARNOLD and P. CRUBILLÉ, A linear algorithm to solve fixed-point equations on transition systems. Information Processing Letters, 1988, 29, pp. 57-66. Zbl0663.68075 MR974202 · Zbl 0663.68075
[4] 4. A. ARNOLD and D. NIWIŃSKI, Fixed point characterization of weak monadic logic definable sets of trees. In M. Nivat and A. Podelski, editors, Tree Automata and Languages, 1992, pp. 159-188, Elsevier. Zbl0794.03054 MR1196736 · Zbl 0794.03054
[5] 5. R. MCNAUGHTON, Infinite games played on finite graphs. Annals of Pure and Applied Logic, 1993, 65, pp. 149-184. Zbl0798.90151 MR1257468 · Zbl 0798.90151
[6] 6. R. S. STREETT and E. A. EMERSON, An automata theoretic decision procedure for the propositional mu-calculus. Information and Computation, 1989, 81, pp. 249-264. Zbl0671.03023 MR1000065 · Zbl 0671.03023
[7] 7. B. VERGAUWEN and J. LEWI, A linear algorithm for solving fixed-point equations on transition systems. In J.-C. Raoult, editor, CAAP’92, p. 321-341. Lect. Notes Comput. Sci., 1992, 581. MR1252008
[8] 8. I. WALUKIEWICZ, Monadic second order logic on tree-like structures. In STACS’96, p. 401-414. Lect. Notes Comput. Sci., 1996, 1046. MR1462113 · Zbl 1434.03105
[9] 9. W. ZIELONKA,, Infinite games on finitely coloured graphs with applications to automata on infinite trees. Technical Report 1091-95, LaBRI, Université Bordeaux I, 1995. · Zbl 0915.68120
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.