Abstract
Lossy counter machines are defined as Minsky n-counter machines where the values in the counters can spontaneously decrease at any time. While termination is decidable for lossy counter machines, structural termination (termination for every input) is undecidable. This undecidability result has far reaching consequences. Lossy counter machines can be used as a general tool to prove the undecidability of many problems, for example (1) The verification of systems that model communication through unreliable channels (e.g. model checking lossy fifo-channel systems and lossy vector addition systems). (2) Several problems for reset Petri nets, like structural termination, boundedness and structural boundedness. (3) Parameterized problems like fairness of broadcast communication protocols.
Work supportet by DAAD Post-Doc grant D/98/28804.
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., 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. Springer, Heidelberg (1998)
Abdulla, P., Jonsson, B.: Verifying Programs with Unreliable Channels. In: LICS 1993, IEEE, Los Alamitos (1993)
Abdulla, P., Jonsson, B.: Undecidable verification problems for programs with unreliable channels. Information and Computation 130(1), 71–90 (1996)
Bouajjani, A., Mayr, R.: Model checking lossy vector addition systems. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol. 1563, p. 323. Springer, Heidelberg (1999)
Cécé, G., Finkel, A., Iyer, S.P.: Unreliable Channels Are Easier to Verify Than Perfect Channels. Information and Computation 124(1), 20–31 (1996)
Christensen, S., Hirshfeld, Y., Moller, F.: Bisimulation equivalence is decidable for Basic Parallel Processes. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715. Springer, Heidelberg (1993)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. LNCS, vol. 131, pp. 52–71 (1981)
Dufourd, C., Finkel, A., Schnoebelen, P.: Reset nets between decidability and undecidability. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, p. 103. Springer, Heidelberg (1998)
Dufourd, C., Jančar, P., Schnoebelen, P.: Boundedness of Reset P/T Nets. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, p. 301. Springer, Heidelberg (1999)
Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science: FORMAL MODELS AND SEMANTICS, vol. B. Elsevier, Amsterdam (1994)
Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: Proc. of LICS 1999. IEEE, Los Alamitos (1999)
Esparza, J., Kiehn, A.: On the model checking problem for branching time logics and Basic Parallel Processes. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939. Springer, Heidelberg (1995)
Hennessy, M., Milner, R.: On observing nondeterminism and concurrency. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 295–309. Springer, Heidelberg (1980)
Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. Journal of Association of Computer Machinery 32, 137–162 (1985)
Hirshfeld, Y., Jerrum, M., Moller, F.: Apolynomial-time algorithm for deciding bisimulation equivalence of normed Basic Parallel Processes. Journal of Mathematical Structures in Computer Science 6, 251–259 (1996)
Kozen, D.: Results on the propositional μ-calculus. TCS 27, 333–354 (1983)
Mayr, E.: An algorithm for the general Petri net reachability problem. SIAM Journal of Computing 13, 441–460 (1984)
Mayr, R.: Weak bisimulation and model checking for Basic Parallel Processes. In: Chandru, V., Vinay, V. (eds.) FSTTCS 1996. LNCS, vol. 1180. Springer, Heidelberg (1996)
Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall, Englewood Cliffs (1967)
Moller, F.: Infinite results. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, Springer, Heidelberg (1996)
Peterson, J.L.: Petri net theory and the modeling of systems. Prentice-Hall, Englewood Cliffs (1981)
Pnueli, A.: The temporal logic of programs. In: FOCS 1977. IEEE, Los Alamitos (1977)
Ruohonen, K.: On some variants of Post’s correspondence problem. Acta Informatica 19, 357–367 (1983)
Yen, H.: A unified approach for deciding the existence of certain Petri net paths. Information and Computation 96(1), 119–137 (1992)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mayr, R. (2000). Undecidable Problems in Unreliable Computations. In: Gonnet, G.H., Viola, A. (eds) LATIN 2000: Theoretical Informatics. LATIN 2000. Lecture Notes in Computer Science, vol 1776. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10719839_37
Download citation
DOI: https://doi.org/10.1007/10719839_37
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67306-4
Online ISBN: 978-3-540-46415-0
eBook Packages: Springer Book Archive