×

zbMATH — the first resource for mathematics

Computable fixpoints in well-structured symbolic model checking. (English) Zbl 1291.68247
Summary: We prove a general finite-time convergence theorem for fixpoint expressions over a well-quasi-ordered set. This has immediate applications for the verification of well-structured systems, where a main issue is the computability of fixpoint expressions, and in particular for game-theoretical properties and probabilistic systems where nesting and alternation of least and greatest fixpoints are common.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
Software:
TaPAS
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abdulla, PA; Baier, C; Purushothaman Iyer, S; Jonsson, B, Simulating perfect channels with probabilistic lossy channels, Inf Comput, 197, 22-40, (2005) · Zbl 1073.68058
[2] Abdulla, PA; Ben Henda, N; Alfaro, L; Mayr, R; Sandberg, S, Stochastic games with lossy channels, No. 4962, 35-49, (2008), Berlin · Zbl 1138.91336
[3] Abdulla, PA; Bertrand, N; Rabinovich, A; Schnoebelen, P, Verification of probabilistic systems with faulty communication, Inf Comput, 202, 141-165, (2005) · Zbl 1105.68003
[4] Abdulla, PA; Bouajjani, A; Jonsson, B; Nilsson, M, Handling global conditions in parameterized system verification, No. 1633, 134-145, (1999), Berlin · Zbl 1046.68573
[5] Abdulla, PA; Bouajjani, A; d’Orso, J, Deciding monotonic games, No. 2803, 1-14, (2003), Berlin · Zbl 1116.68491
[6] Abdulla, PA; Čerāns, K; Jonsson, B; Tsay, YK, Algorithmic analysis of programs with well quasi-ordered domains, Inf Comput, 160, 109-127, (2000) · Zbl 1046.68567
[7] Abdulla, PA; Collomb-Annichini, A; Bouajjani, A; Jonsson, B, Using forward reachability analysis for verification of lossy channel systems, Form Methods Syst Des, 25, 39-65, (2004) · Zbl 1073.68675
[8] Abdulla, PA; Jonsson, B, Undecidable verification problems for programs with unreliable channels, Inf Comput, 130, 71-90, (1996) · Zbl 0872.68112
[9] Abdulla, PA; Jonsson, B, Verifying programs with unreliable channels, Inf Comput, 127, 91-101, (1996) · Zbl 0856.68096
[10] Abdulla, PA; Jonsson, B; Nilsson, M; Saksena, M, A survey of regular model checking, No. 3170, 35-48, (2004), Berlin · Zbl 1099.68055
[11] Alur, R; Henzinger, T; Kupferman, O, Alternating-time temporal logic, J ACM, 49, 672-713, (2002) · Zbl 1326.68181
[12] Arnold A, Niwiński D (2001) Rudiments of \(μ\)-calculus, studies in logic and the foundations of mathematics, vol 146. Elsevier, Amsterdam · Zbl 0968.03002
[13] Baier, C; Bertrand, N; Schnoebelen, P, A note on the attractor-property of infinite-state Markov chains, Inf Process Lett, 97, 58-63, (2006) · Zbl 1191.68330
[14] Baier, C; Bertrand, N; Schnoebelen, P, On computing fixpoints in well-structured regular model checking, with applications to lossy channel systems, No. 4246, 347-361, (2006), Berlin · Zbl 1165.68397
[15] Baier, C; Bertrand, N; Schnoebelen, P, Verifying nondeterministic probabilistic channel systems against \(ω\)-regular linear-time properties, ACM Transactions on Computational Logic, 9, (2007) · Zbl 1367.68181
[16] Baier, C; Engelen, B, Establishing qualitative properties for probabilistic lossy channel systems: an algorithmic approach, No. 1601, 34-52, (1999), Berlin
[17] Baier C, Katoen JP (2008) Principles of model checking. MIT Press, Cambridge
[18] Bardin, S; Finkel, A; Leroux, J; Schnoebelen, P, Flat acceleration in symbolic model checking, No. 3707, 474-488, (2005), Berlin · Zbl 1170.68507
[19] Bertrand N, Schnoebelen P (2012) Revisiting stochastic games on lossy channel systems. Submitted for publication
[20] Boigelot, B, On iterating linear transformations over recognizable sets of integers, Theor Comput Sci, 309, 413-468, (2003) · Zbl 1070.68062
[21] Boigelot, B; Godefroid, P, Symbolic verification of communication protocols with infinite state spaces using qdds, Form Methods Syst Des, 14, 237-255, (1999)
[22] Boigelot, B; Legay, A; Wolper, P, Iterating transducers in the large, No. 2725, 223-235, (2003), Berlin · Zbl 1278.68157
[23] Boigelot, B; Legay, A; Wolper, P, Omega-regular model checking, No. 2988, 561-575, (2004), Berlin · Zbl 1126.68469
[24] Bouajjani, A; Habermehl, P; Moro, P; Vojnar, T, Verifying programs with dynamic 1-selector-linked structures in regular model checking, No. 3440, 13-39, (2005), Berlin · Zbl 1087.68585
[25] Bouajjani, A; Habermehl, P; Vojnar, T, Abstract regular model checking, No. 3114, 372-386, (2004), Berlin · Zbl 1103.68071
[26] Bouajjani, A; Jonsson, B; Nilsson, M; Touili, T, Regular model checking, No. 1855, 403-418, (2000), Berlin · Zbl 0974.68118
[27] Bouyer, P; Markey, N; Ouaknine, J; Schnoebelen, P; Worrell, J, On termination and invariance for faulty channel machines, Form Asp Comput, 24, 595-607, (2012) · Zbl 1259.68142
[28] Bouyer, P; Markey, N; Reynier, PA, Robust analysis of timed automata via channel machines, No. 4962, 157-171, (2008), Berlin · Zbl 1138.68431
[29] Bozzelli, L; Pinchinat, S, Verification of gap-order constraint abstractions of counter systems, No. 7148, 88-103, (2012), Berlin · Zbl 1325.68141
[30] Bradfield, JC; Stirling, C; Bergstra, JA (ed.); Ponse, A (ed.); Smolka, SA (ed.), Modal logics and mu-calculi: an introduction, 293-330, (2001), Amsterdam · Zbl 1002.03021
[31] Cécé, G; Finkel, A; Purushothaman Iyer, S, Unreliable channels are easier to verify than perfect channels, Inf Comput, 124, 20-31, (1996) · Zbl 0844.68035
[32] Čerāns, K, Deciding properties of integral relational automata, No. 820, 35-46, (1994), Berlin
[33] Chambart, P; Schnoebelen, P, The ordinal recursive complexity of lossy channel systems, 205-216, (2008), Los Alamitos · Zbl 1160.68460
[34] Cousot, P, Verification by abstract interpretation, No. 2772, 243-268, (2003), Berlin · Zbl 1274.68180
[35] Alfaro, L; Henzinger, TA; Majumdar, R, Symbolic algorithms for infinite-state games, No. 2154, 536-550, (2001), Berlin · Zbl 1006.68095
[36] Delzanno, G; Raskin, JF; Begin, L, Covering sharing trees: a compact data structure for parameterized verification, Int J Softw Tools Technol Transf, 5, 268-297, (2004)
[37] Demri, S; Lazić, R, LTL with the freeze quantifier and register automata, ACM Trans Computational Logic, 10, (2009) · Zbl 1351.68158
[38] Dufourd, C; Finkel, A; Schnoebelen, P, Reset nets between decidability and undecidability, No. 1443, 103-115, (1998), Berlin · Zbl 0909.68124
[39] Emerson, EA; Leeuwen, J (ed.), Temporal and modal logic, No. B, 995-1072, (1990), Berlin · Zbl 0900.03030
[40] Emerson, EA; Namjoshi, KS, On model checking for non-deterministic infinite-state systems, 70-80, (1998), Los Alamitos · Zbl 0945.68523
[41] Esparza, J, Decidability and complexity of Petri net problems—an introduction, No. 1491, 374-428, (1998), Berlin · Zbl 0926.68087
[42] Fenner, S; Gasarch, W; Postow, B, The complexity of finding SUBSEQ(A), Theory Comput Syst, 45, 577-612, (2009) · Zbl 1187.68295
[43] Figueira, D; Figueira, S; Schmitz, S; Schnoebelen, P, Ackermannian and primitive-recursive bounds with dickson’s lemma, 269-278, (2011), Los Alamitos
[44] Figueira, D; Segoufin, L, Future-looking logics on data words and trees, No. 5734, 331-343, (2009), Berlin · Zbl 1250.03050
[45] Finkel, A, Decidability of the termination problem for completely specified protocols, Distrib Comput, 7, 129-135, (1994)
[46] Finkel, A; Goubault-Larrecq, J, Forward analysis for WSTS, part I: completions, No. 3, 433-444, (2009), Dagstuhl · Zbl 1236.68183
[47] Finkel, A; McKenzie, P; Picaronny, C, A well-structured framework for analysing Petri nets extensions, Inf Comput, 195, 1-29, (2004) · Zbl 1101.68696
[48] Finkel, A; Schnoebelen, P, Well-structured transition systems everywhere!, Theor Comput Sci, 256, 63-92, (2001) · Zbl 0973.68170
[49] Glabbeek, RJv, The linear time—branching time spectrum II: the semantics of sequential systems with silent moves, No. 715, 66-81, (1993), Berlin
[50] Glabbeek, RJv; Bergstra, JA (ed.); Ponse, A (ed.); Smolka, SA (ed.), The linear time—branching time spectrum I, 3-99, (2001), Amsterdam
[51] Grädel E, Thomas W, Wilke T (eds) (2002) Automata, logics, and infinite games: a guide to current research. Lecture notes in computer science, vol 2500. Springer, Berlin · Zbl 1011.00037
[52] Gruber, H; Holzer, M; Kutrib, M, More on the size of higman-haines sets: effective constructions, Fundam Inform, 91, 105-121, (2009) · Zbl 1192.68410
[53] Habermehl, P; Vojnar, T, Regular model checking using inference of regular languages, No. 138, 21-36, (2005), Amsterdam · Zbl 1272.68256
[54] Haddad, S; Schmitz, S; Schnoebelen, P, The ordinal-recursive complexity of timed-arc Petri nets, data nets, and other enriched nets, 355-364, (2012), Los Alamitos · Zbl 1362.68214
[55] Henzinger, TA; Majumdar, R; Raskin, JF, A classification of symbolic transition systems, ACM Trans Comput Log, 6, 1-32, (2005) · Zbl 1367.68193
[56] Jančar, P, Undecidability of bisimilarity for Petri nets and some related problems, Theor Comput Sci, 148, 281-301, (1995) · Zbl 0873.68147
[57] Jančar, P; Esparza, J; Moller, F, Petri nets and regular processes, J Comput Syst Sci, 59, 476-503, (1999) · Zbl 0958.68121
[58] Jančar, P; Kučera, A; Mayr, R, Deciding bisimulation-like equivalences with finite-state processes, Theor Comput Sci, 258, 409-433, (2001) · Zbl 0974.68131
[59] Jeż, A; Okhotin, A, Representing hyper-arithmetical sets by equations over sets of integers, Theory Comput Syst, 51, 196-228, (2012) · Zbl 1279.68158
[60] Jongh, DHJ; Parikh, R, Well-partial orderings and hierarchies, Indag Math, 39, 195-207, (1977) · Zbl 0435.06004
[61] Kesten, Y; Maler, O; Marcus, M; Pnueli, A; Shahar, E, Symbolic model checking with rich assertional languages, Theor Comput Sci, 256, 93-112, (2001) · Zbl 0973.68119
[62] Khoussainov, B; Nerode, A, Automatic presentations of structures, No. 960, 367-392, (1995), Berlin
[63] Kouzmin, EV; Shilov, NV; Sokolov, VA, Model checking mu-calculus in well-structured transition systems, 152-155, (2004), Los Alamitos
[64] Kruskal, JB, The theory of well-quasi-ordering: a frequently discovered concept, J Comb Theory, Ser A, 13, 297-305, (1972) · Zbl 0244.06002
[65] Kučera, A; Schnoebelen, P, A general approach to comparing infinite-state systems with their finite-state specifications, Theor Comput Sci, 358, 315-333, (2006) · Zbl 1097.68075
[66] Kunc, M, What do we know about language equations?, No. 4588, 23-27, (2007), Berlin
[67] Leroux, J; Point, G, Tapas: the talence Presburger arithmetic suite, No. 5505, 182-185, (2009), Berlin · Zbl 1234.03002
[68] Mayr, R, Undecidable problems in unreliable computations, Theor Comput Sci, 297, 337-354, (2003) · Zbl 1044.68119
[69] Milner, EC; Rival, I (ed.), Basic WQO- and BQO-theory, 487-502, (1985), Dordrecht
[70] Perrin, D; Leeuwen, J (ed.), Finite automata, No. B, 1-57, (1990), Amsterdam · Zbl 0900.68312
[71] Rabinovich, A, Quantitative analysis of probabilistic lossy channel systems, Inf Comput, 204, 713-740, (2006) · Zbl 1103.68078
[72] Raskin JF, Samuelides M, Van Begin L (2003) Petri games are monotonic but difficult to decide. Tech. report 2003.21, Centre Fédéré en Vérification. Available at http://www.ulb.ac.be/di/ssd/cfv/TechReps · Zbl 1073.68675
[73] Raskin, JF; Samuelides, M; Begin, L, Games for counting abstractions, No. 128, 69-85, (2005), Amsterdam · Zbl 1272.91014
[74] Schmitz, S; Schnoebelen, P, Multiply-recursive upper bounds with higman’s lemma, No. 6756, 441-452, (2011), Berlin · Zbl 1333.68179
[75] Schnoebelen, P, Bisimulation and other undecidable equivalences for lossy channel systems, No. 2215, 385-399, (2001), Berlin · Zbl 1087.68609
[76] Schnoebelen, P, The verification of probabilistic lossy channel systems, No. 2925, 445-465, (2004), Berlin · Zbl 1203.68101
[77] Schnoebelen, P, Lossy counter machines decidability cheat sheet, No. 6227, 51-75, (2010), Berlin · Zbl 1287.68101
[78] Schnoebelen, P, Revisiting ackermann-hardness for lossy counter machines and reset Petri nets, No. 6281, 616-628, (2010), Berlin · Zbl 1287.68059
[79] Valk, R, Self-modifying nets, a natural extension of Petri nets, No. 62, 464-476, (1978), Berlin · Zbl 0415.68025
[80] Leeuwen, J, Effective constructions in well-partially-ordered free monoids, Discrete Math, 21, 237-252, (1978) · Zbl 0384.68073
[81] Wolper, P; Boigelot, B, Verifying systems with infinite but regular state spaces, No. 1427, 88-97, (1998), Berlin
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.