Abstract
We study and compare two notions of non-termination on idempotent semirings: infinite iteration and divergence. We determine them in various models and develop conditions for their coincidence. It turns out that divergence yields a simple and natural way of modelling infinite behaviour, whereas infinite iteration shows some anomalies.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Arden, D.: Delayed logic and finite state machines. In: Theory of Computing Machine Design, pp. 1–35. University of Michigan Press (1960)
Cohen, E.: Separation and reduction. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 45–59. Springer, Heidelberg (2000)
Desharnais, J., Möller, B., Struth, G.: Termination in modal Kleene algebra. In: Lévy, J.-J., Mayr, E.W., Mitchell, J.C. (eds.) IFIP TCS 2004, pp. 647–660. Kluwer, Dordrecht (2004): Revised version: Algebraic Notions of Termination. Technical Report 2006-23, Institut für Informatik, Universität Augsburg (2006)
Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. ACM Trans. Computational Logic 7(4), 798–833 (2006)
Ésik, Z., Kuich, W.: A semiring-semimodule generalization of ω-context-free languages. In: Karhumäki, J., Maurer, H., Păun, G., Rozenberg, G. (eds.) Theory Is Forever. LNCS, vol. 3113, pp. 68–80. Springer, Heidelberg (2004)
Goldblatt, R.: An algebraic study of well-foundedness. Studia Logica 44(4), 423–437 (1985)
Höfner, P., Struth, G.: January 14 (2008), http://www.dcs.shef.ac.uk/~georg/ka
Höfner, P., Struth, G.: Automated reasoning in Kleene algebra. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 279–294. Springer, Heidelberg (2007)
Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation 110(2), 366–390 (1994)
McCune, W.: Prover9 and Mace4, January 14 (2008), http://www.cs.unm.edu/~mccune/prover9
Möller, B.: Kleene getting lazy. Sci. Comput. Programming 65, 195–214 (2007)
Möller, B., Struth, G.: Algebras of modal operators and partial correctness. Theoretical Computer Science 351(2), 221–239 (2006)
Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)
Pratt, V.: Dynamic algebras: Examples, constructions, applications. Studia Logica 50, 571–605 (1991)
Struth, G.: Reasoning automatically about termination and refinement. In: Ranise, S. (ed.) International Workshop on First-Order Theorem Proving, Technical Report ULCS-07-018, Department of Computer Science, University of Liverpool, pp. 36–51 (2007)
von Wright, J.: Towards a refinement algebra. Science of Computer Programming 51(1-2), 23–45 (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Höfner, P., Struth, G. (2008). Non-termination in Idempotent Semirings. In: Berghammer, R., Möller, B., Struth, G. (eds) Relations and Kleene Algebra in Computer Science. RelMiCS 2008. Lecture Notes in Computer Science, vol 4988. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78913-0_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-78913-0_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78912-3
Online ISBN: 978-3-540-78913-0
eBook Packages: Computer ScienceComputer Science (R0)