On Distributive Fixed-Point Expressions

Helmut Seidl; Damian Niwiński

RAIRO - Theoretical Informatics and Applications (2010)

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

Abstract

top
For every fixed-point expression e of alternation-depth r, we construct a new fixed-point expression e' of alternation-depth 2 and size 𝒪 ( r · | 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.

How to cite

top

Seidl, 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
  1. 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.  
  2. A. Arnold, The µ-Calculus Alternation-Depth Hierarchy is Strict on Binary Trees. Theoret. Informatics. Appl., Special issue on FICS'98, to appear.  Zbl0945.68118
  3. 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
  4. 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.  
  5. 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.  
  6. H. Doornbos, R. Backhouse and J. van der Woude, A Calculational Approach to Mathematical Induction. Theoret. Comput. Sci.179 (1997) 103-135.  Zbl0901.68124
  7. 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.  
  8. 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
  9. 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
  10. M. Jurdzinski, Deciding the Winnner in Parity Games is in UP ⋂ co-UP. Inform. Process. Lett.68 (1998) 119-124.  
  11. 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
  12. 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
  13. 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
  14. D. Niwinski, Hierarchy of Objects Definable in the Fixed Point Calculus, in Polish. Ph.D. Thesis, University of Warsaw (1987).  
  15. D. Niwinski, Fixed Points vs. Infinite Generation. In 3rd Annual IEEE Symposium on Logic in Computer Science (LICS), IEEE (1988) 402-409.  
  16. D. Niwinski, Fixed Point Characterization of Infinite Behavior of Finite State Systems. Theoret. Comput. Sci.189 (1997) 1-69.  Zbl0893.68102
  17. D.M.R. Park, On the Semantics of Fair Parallelism. In Abstract Software Specification. Springer, Lecture Notes in Comput. Sci.86 (1980) 504-526.  
  18. D.M.R. Park, Concurrency and Automata on Infinite Sequences. In Theoret. Comput. Sci. Springer, Lecture Notes in Comput. Sci.104 (1981) 167-183.  
  19. H. Rasiowa and R. Sikorski, Mathematics of Metamathematics. Panstowe Wydawnictwo Naukowe (1970).  Zbl0122.24311
  20. W. Thomas, Automata on Infinite Objects, J. van Leeuwen, Ed., Handbook of Theoretical Computer Science. Elsevier, Amsterdam (1990).  

NotesEmbed ?

top

You must be logged in to post comments.

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

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.