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
topHow 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.
- 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.
- 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.
- 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.
- 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).
- 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.
- 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).
- 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.
- 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.
- 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).
- W. Thomas, Automata on Infinite Objects, J. van Leeuwen, Ed., Handbook of Theoretical Computer Science. Elsevier, Amsterdam (1990).
NotesEmbed ?
topYou 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.