Abstract
We prove a general finite convergence theorem for “upward-guarded” fixpoint expressions over a well-quasi-ordered set. This has immediate applications in regular model checking of well-structured systems, where a main issue is the eventual convergence of fixpoint computations. In particular, we are able to directly obtain several new decidability results on lossy channel systems.
The first author is supported by the DFG-NWO project VOSS II and the DFG-project PROBPOR. The last two authors were supported by the ACI Sécurité & Informatique project Persée.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abdulla, P.A., Bertrand, N., Rabinovich, A., Schnoebelen, P.: Verification of probabilistic systems with faulty communication. Information and Computation 202(2), 141–165 (2005)
Abdulla, P.A., Bouajjani, A., d’Orso, J.: Deciding Monotonic Games. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol. 2803, pp. 1–14. Springer, Heidelberg (2003)
Abdulla, P.A., Čerāns, K., Jonsson, B., Tsay, Y.-K.: Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation 160(1/2), 109–127 (2000)
Abdulla, P.A., Jonsson, B.: Undecidable verification problems for programs with unreliable channels. Information and Computation 130(1), 71–90 (1996)
Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Information and Computation 127(2), 91–101 (1996)
Abdulla, P.A., Jonsson, B.: Channel representations in protocol verification. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 1–15. Springer, Heidelberg (2001)
Arnold, A., Niwiński, D.: Rudiments of μ-Calculus. Studies in Logic and the Foundations of Mathematics, vol. 146. Elsevier Science, Amsterdam (2001)
Baier, C., Bertrand, N., Schnoebelen, P.: A note on the attractor-property of infinite-state Markov chains. Information Processing Letters 97(2), 58–63 (2006)
Baier, C., Bertrand, N., Schnoebelen, Ph.: Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties. ACM Transactions on Computational Logic (to appear, 2006), http://arxiv.org/abs/cs.LO/0511023
Bardin, S., Finkel, A., Leroux, J., Schnoebelen, P.: Flat acceleration in symbolic model checking. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 474–488. Springer, Heidelberg (2005)
Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 403–418. Springer, Heidelberg (2000)
Cécé, G., Finkel, A., Purushothaman Iyer, S.: Unreliable channels are easier to verify than perfect channels. Information and Computation 124(1), 20–31 (1996)
Chatterjee, K., de Alfaro, L., Henzinger, T.A.: The Complexity of Stochastic Rabin and Streett Games,. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 878–890. Springer, Heidelberg (2005)
de Alfaro, L., Henzinger, T.A., Majumdar, R.: Symbolic algorithms for infinite-state games. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 536–550. Springer, Heidelberg (2001)
Finkel, A.: Decidability of the termination problem for completely specificied protocols. Distributed Computing 7(3), 129–135 (1994)
Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theoretical Computer Science 256(1–2), 63–92 (2001)
Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games: A Guide to Current Research. LNCS, vol. 2500. Springer, Heidelberg (2002)
Henzinger, T.A., Majumdar, R., Raskin, J.-F.: A classification of symbolic transition systems. ACM Trans. Computational Logic 6(1), 1–32 (2005)
Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. Theoretical Computer Science 256(1–2), 93–112 (2001)
Kruskal, J.B.: The theory of well-quasi-ordering: A frequently discovered concept. Journal of Combinatorial Theory, Series A 13(3), 297–305 (1972)
Kučera, A., Schnoebelen, P.: A general approach to comparing infinite-state systems with their finite-state specifications. Theoretical Computer Science 358(2-3), 315–333 (2006)
Martin, D.A.: The determinacy of Blackwell games. The Journal of Symbolic Logic 63(4), 1565–1581 (1998)
Mayr, R.: Undecidable problems in unreliable computations. Theoretical Computer Science 297(1–3), 337–354 (2003)
Milner, E.C.: Basic WQO- and BQO-theory. In: Rival, I. (ed.) Graphs and Order. The Role of Graphs in the Theory of Ordered Sets and Its Applications, pp. 487–502. D.Reidel Publishing (1985)
Ouaknine, J., Worrell, J.B.: On Metric Temporal Logic and Faulty Turing Machines. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006. LNCS, vol. 3921, pp. 217–230. Springer, Heidelberg (2006)
Perrin, D.: Finite automata. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, ch. 1, vol. B, pp. 1–57. Elsevier, Amsterdam (1990)
Raskin, J.-F., Samuelides, M., Van Begin, L.: Petri games are monotonic but difficult to decide. Tech. Report, 2003.21, Centre Fédéré en Vérification (2003), Available at: http://www.ulb.ac.be/di/ssd/cfv/TechReps
Raskin, J.-F., Samuelides, M., Van Begin, L.: Games for counting abstractions. In: Proc. 4th Int. Workshop on Automated Verification of Critical Systems (AVoCS 2004), London, UK, September. Electronic Notes in Theor. Comp. Sci, vol. 128(6), pp. 69–85. Elsevier Science, Amsterdam (2005)
Schnoebelen, P.: The verification of probabilistic lossy channel systems. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 445–465. Springer, Heidelberg (2004)
Sifakis, J.: A unified approach for studying the properties of transitions systems. Theoretical Computer Science 18, 227–258 (1982)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baier, C., Bertrand, N., Schnoebelen, P. (2006). On Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel Systems. In: Hermann, M., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2006. Lecture Notes in Computer Science(), vol 4246. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11916277_24
Download citation
DOI: https://doi.org/10.1007/11916277_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-48281-9
Online ISBN: 978-3-540-48282-6
eBook Packages: Computer ScienceComputer Science (R0)