# On Distributive Fixed-Point Expressions

RAIRO - Theoretical Informatics and Applications (2010)

- Volume: 33, Issue: 4-5, page 427-446
- ISSN: 0988-3754

## Access Full Article

top## Abstract

top## How to cite

topSeidl, Helmut, and Niwiński, Damian. "On Distributive Fixed-Point Expressions." RAIRO - Theoretical Informatics and Applications 33.4-5 (2010): 427-446. <http://eudml.org/doc/222054>.

@article{Seidl2010,

abstract = {
For every fixed-point expression e of alternation-depth r,
we construct a new fixed-point expression e' of alternation-depth 2
and size $\{\cal O\}(r\cdot|e|)$. Expression e' is equivalent to e
whenever operators are distributive and the underlying
complete lattice has a co-continuous least upper bound. We
alternation-depth but also w.r.t. the increase in size of the
resulting expression.
},

author = {Seidl, Helmut, Niwiński, Damian},

journal = {RAIRO - Theoretical Informatics and Applications},

keywords = {Fixed-point expressions; distributivity; alternation-depth;
lower bounds.; lower bounds; fixed-point expression},

language = {eng},

month = {3},

number = {4-5},

pages = {427-446},

publisher = {EDP Sciences},

title = {On Distributive Fixed-Point Expressions},

url = {http://eudml.org/doc/222054},

volume = {33},

year = {2010},

}

TY - JOUR

AU - Seidl, Helmut

AU - Niwiński, Damian

TI - On Distributive Fixed-Point Expressions

JO - RAIRO - Theoretical Informatics and Applications

DA - 2010/3//

PB - EDP Sciences

VL - 33

IS - 4-5

SP - 427

EP - 446

AB -
For every fixed-point expression e of alternation-depth r,
we construct a new fixed-point expression e' of alternation-depth 2
and size ${\cal O}(r\cdot|e|)$. Expression e' is equivalent to e
whenever operators are distributive and the underlying
complete lattice has a co-continuous least upper bound. We
alternation-depth but also w.r.t. the increase in size of the
resulting expression.

LA - eng

KW - Fixed-point expressions; distributivity; alternation-depth;
lower bounds.; lower bounds; fixed-point expression

UR - http://eudml.org/doc/222054

ER -

## References

top- H.R. Andersen and B. Vergauwen, Efficient Checking of Behavioral Relations and Modal Assertions Using Fixed-Point Inversion. In 7th International Conference on Computer-Aided Verification (CAV). Springer, Lecture Notes in Comput. Sci.939 (1995) 142-154.
- A. Arnold, The µ-Calculus Alternation-Depth Hierarchy is Strict on Binary Trees. Theoret. Informatics. Appl., Special issue on FICS'98, to appear. Zbl0945.68118
- A. Arnold and D. Niwinski, Fixed Point Characterization of Weak Monadic Logic Definable Sets of Trees, M. Nivat and A. Podelski, Eds. Elsevier, Amsterdam, Tree Automata and Languages (1992) 159-188. Zbl0794.03054
- G. Bhat and R. Cleaveland, Efficient Local Model Checking for Fragments of the Modal µ-Calculus. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, Lecture Notes in Comput. Sci.1055 (1996) 107-126.
- J.C. Bradfield, The Modal Mu-Calculus Alternation Hierarchy is Strict. In 7th International Conference on Concurrency Theory (CONCUR). Springer, Lecture Notes in Comput. Sci.1119 (1986) 233-246.
- H. Doornbos, R. Backhouse and J. van der Woude, A Calculational Approach to Mathematical Induction. Theoret. Comput. Sci.179 (1997) 103-135. Zbl0901.68124
- E.A. Emerson, C.S. Jutla and A.P. Sistla, On Model-Checking for Fragments of µ-Calculus. In 5th International Conference on Computer-Aided Verification (CAV). Springer, Lecture Notes in Comput. Sci.697 (1993) 385-396.
- E.A. Emerson and E.M. Clarke, Characterizing Correctness Properties of Parallel Programs Using Fixpoints. In 7th International Colloquium on Automata, Languages and Programming (ICALP). Springer, Lecture Notes in Comput. Sci.85 (1980) 169-181. Zbl0456.68016
- L. Flon and N. Suzuki, Consistent and Complete Proof Rules for the Total Correctness of Parallel Programs. In 19th IEEE Symp. on Foundations of Computer Science (FOCS) (1978). Zbl0373.68029
- M. Jurdzinski, Deciding the Winnner in Parity Games is in UP ⋂ co-UP. Inform. Process. Lett.68 (1998) 119-124.
- G. Lenzi, A Hierarchy Theorem for the µ-Calculus. In 23rd International Colloquium on Automata, Languages and Programming (ICALP). Springer, Lecture Notes in Comput. Sci.1099 (1996) 87-109. Zbl1045.03516
- D.E. Muller, A. Saoudi and P.E. Schupp, Alternating Automata, the Weak Monadic Theory of the Tree and its Complexity. In ICALP'86 (1986). Zbl0617.03020
- D. Niwinski, On Fixed Point Clones. In 13th International Colloquium on Automata, Languages and Programming (ICALP). Springer, Lecture Notes in Comput. Sci.226 (1986) 464-473. Zbl0596.68036
- D. Niwinski, Hierarchy of Objects Definable in the Fixed Point Calculus, in Polish. Ph.D. Thesis, University of Warsaw (1987).
- D. Niwinski, Fixed Points vs. Infinite Generation. In 3rd Annual IEEE Symposium on Logic in Computer Science (LICS), IEEE (1988) 402-409.
- D. Niwinski, Fixed Point Characterization of Infinite Behavior of Finite State Systems. Theoret. Comput. Sci.189 (1997) 1-69. Zbl0893.68102
- D.M.R. Park, On the Semantics of Fair Parallelism. In Abstract Software Specification. Springer, Lecture Notes in Comput. Sci.86 (1980) 504-526.
- D.M.R. Park, Concurrency and Automata on Infinite Sequences. In Theoret. Comput. Sci. Springer, Lecture Notes in Comput. Sci.104 (1981) 167-183.
- H. Rasiowa and R. Sikorski, Mathematics of Metamathematics. Panstowe Wydawnictwo Naukowe (1970). Zbl0122.24311
- W. Thomas, Automata on Infinite Objects, J. van Leeuwen, Ed., Handbook of Theoretical Computer Science. Elsevier, Amsterdam (1990).

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.