Abstract
We show that for several classes of idempotent semirings the least fixed-point of a polynomial system of equations is equal to the least fixed-point of a linear system obtained by “linearizing” the polynomials of
in a certain way. Our proofs rely on derivation tree analysis, a proof principle that combines methods from algebra, calculus, and formal language theory, and was first used in [5] to show that Newton’s method over commutative and idempotent semirings converges in a linear number of steps. Our results lead to efficient generic algorithms for computing the least fixed-point. We use these algorithms to derive several consequences, including an O(N
3) algorithm for computing the throughput of a context-free grammar (obtained by speeding up the O(N
4) algorithm of [2]), and a generalization of Courcelle’s result stating that the downward-closed image of a context-free language is regular [3].
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abdulla, P.A., Bouajjani, A., Jonsson, B.: On-the-fly analysis of systems with unbounded, lossy FIFO channels. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 305–318. Springer, Heidelberg (1998)
Caucal, D., Czyzowicz, J., Fraczak, W., Rytter, W.: Efficient computation of throughput values of context-free languages. In: Holub, J., Žďárek, J. (eds.) CIAA 2007. LNCS, vol. 4783, pp. 203–213. Springer, Heidelberg (2007)
Courcelle, B.: On constructing obstruction sets of words. EATCS Bulletin 44, 178–185 (1991)
Esparza, J., Kiefer, S., Luttenberger, M.: An extension of Newton’s method to ω-continuous semirings. In: Harju, T., Karhumäki, J., Lepistö, A. (eds.) DLT 2007. LNCS, vol. 4588, pp. 157–168. Springer, Heidelberg (2007)
Esparza, J., Kiefer, S., Luttenberger, M.: On fixed point equations over commutative semirings. In: STACS 2007. LNCS, vol. 4397, pp. 296–307. Springer, Heidelberg (2007)
Esparza, J., Kiefer, S., Luttenberger, M.: Derivation tree analysis for accelerated fixed-point computation. Technical report, Technische Universität München (2008)
Esparza, J., Kučera, A., Mayr, R.: Model checking probabilistic pushdown automata. Logical Methods in Computer Science (2006)
Etessami, K., Yannakakis, M.: Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. In: Diekert, V., Durand, B. (eds.) STACS 2005. LNCS, vol. 3404, pp. 340–352. Springer, Heidelberg (2005)
Gawlitza, T., Seidl, H.: Precise fixpoint computation through strategy iteration. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 300–315. Springer, Heidelberg (2007)
Harris, T.E.: The Theory of Branching Processes. Springer, Heidelberg (1963)
Higman, G.: Ordering by divisibility in abstract algebras. Proc. London Math. Soc. 2 (1952)
Hopkins, M.W., Kozen, D.: Parikh’s theorem in commutative Kleene algebra. In: LICS 1999 (1999)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)
Reps, T., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. Science of Computer Programming 58(1–2), 206–263 (2005); Special Issue on the Static Analysis Symposium 2003
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Esparza, J., Kiefer, S., Luttenberger, M. (2008). Derivation Tree Analysis for Accelerated Fixed-Point Computation. In: Ito, M., Toyama, M. (eds) Developments in Language Theory. DLT 2008. Lecture Notes in Computer Science, vol 5257. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85780-8_24
Download citation
DOI: https://doi.org/10.1007/978-3-540-85780-8_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85779-2
Online ISBN: 978-3-540-85780-8
eBook Packages: Computer ScienceComputer Science (R0)