nach oben

Formal Methods in System Design

Erschienen in:

01.10.2013

Computable fixpoints in well-structured symbolic model checking

verfasst von: N. Bertrand, P. Schnoebelen

Erschienen in: Formal Methods in System Design | Ausgabe 2/2013

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

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.

Vorheriger Artikel A compositional modelling and analysis framework for stochastic hybrid systems

Nächster Artikel A survey of partial-observation stochastic parity games

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Note that the occurrence of X is not required to be under the immediate scope of a closure or interior operator. See the guarded term in Example 13.

Called “strong compatibility” in [48]. There exist alternative definitions of well-structured transition systems based on weaker notions of compatibility.

Semilinear subsets of Conf _S=Q×ℕ^d are all sets of the form ⋃_q∈Q{q}×R _q where each R _q⊆ℕ^d is semilinear. Equivalently, they can be seen as semilinear subsets of ℕ^d+1, or more precisely of {0,1,2,…,|Q|−1}×ℕ^d, by identifying Q with its cardinal.

Regular simulation is known to be decidable for well-structured systems [6]. By contrast, outside of the regular equivalence framework, all sensible behavioral relations between configurations of monotonic counter systems are undecidable [56, 75].

However, it is decidable whether f⪯σ (given σ) when S is finitely branching [6].

The F _d’s are known as the “Fubini numbers”, or the “ordered Bell numbers”, see A000670 in the Encyclopedia of Integer Sequences.

In the case of IRA’s, the optimal complexity is obtained with algorithms that are not WSTS-based [29].

For “c?m” operations, op(w) is only defined if the contents of channel c starts with m.

Abdulla PA, Baier C, Purushothaman Iyer S, Jonsson B (2005) Simulating perfect channels with probabilistic lossy channels. Inf Comput 197(1–2):22–40. doi:10.1016/j.ic.2004.12.001 CrossRefMATH

Abdulla PA, Ben Henda N, de Alfaro L, Mayr R, Sandberg S (2008) Stochastic games with lossy channels. In: Proc 11th int conf foundations of software science and computational structures (FOSSACS 2008). Lecture notes in computer science, vol 4962. Springer, Berlin, pp 35–49. doi:10.1007/978-3-540-78499-9_4

Abdulla PA, Bertrand N, Rabinovich A, Schnoebelen P (2005) Verification of probabilistic systems with faulty communication. Inf Comput 202(2):141–165. doi:10.1016/j.ic.2005.05.008 MathSciNetCrossRefMATH

Abdulla PA, Bouajjani A, Jonsson B, Nilsson M (1999) Handling global conditions in parameterized system verification. In: Proc 11th int conf computer aided verification (CAV 1999). Lecture notes in computer science, vol 1633. Springer, Berlin, pp 134–145. doi:10.1007/3-540-48683-6_14 CrossRef

Abdulla PA, Bouajjani A, d’Orso J (2003) Deciding monotonic games. In: Proc 17th int workshop computer science logic (CSL 2003) and 8th Kurt Gödel coll (KGL 2003). Lecture notes in computer science, vol 2803. Springer, Berlin, pp 1–14. doi:10.1007/978-3-540-45220-1_1

Abdulla PA, Čerāns K, Jonsson B, Tsay YK (2000) Algorithmic analysis of programs with well quasi-ordered domains. Inf Comput 160(1/2):109–127. doi:10.1006/inco.1999.2843 CrossRefMATH

Abdulla PA, Collomb-Annichini A, Bouajjani A, Jonsson B (2004) Using forward reachability analysis for verification of lossy channel systems. Form Methods Syst Des 25(1):39–65. doi:10.1023/B:FORM.0000033962.51898.1a CrossRefMATH

Abdulla PA, Jonsson B (1996) Undecidable verification problems for programs with unreliable channels. Inf Comput 130(1):71–90. doi:10.1006/inco.1996.0083 MathSciNetCrossRefMATH

Abdulla PA, Jonsson B (1996) Verifying programs with unreliable channels. Inf Comput 127(2):91–101. doi:10.1006/inco.1996.0053 MathSciNetCrossRefMATH

10.

Abdulla PA, Jonsson B, Nilsson M, Saksena M (2004) A survey of regular model checking. In: Proc 15th int conf concurrency theory (CONCUR 2004). Lecture notes in computer science, vol 3170. Springer, Berlin, pp 35–48. doi:10.1007/978-3-540-28644-8_3 CrossRef

11.

Alur R, Henzinger T, Kupferman O (2002) Alternating-time temporal logic. J ACM 49(5):672–713 MathSciNetCrossRef

12.

Arnold A, Niwiński D (2001) Rudiments of μ-calculus, studies in logic and the foundations of mathematics, vol 146. Elsevier, Amsterdam

13.

Baier C, Bertrand N, Schnoebelen P (2006) A note on the attractor-property of infinite-state Markov chains. Inf Process Lett 97(2):58–63. doi:10.1016/j.ipl.2005.09.011 MathSciNetCrossRefMATH

14.

Baier C, Bertrand N, Schnoebelen P (2006) On computing fixpoints in well-structured regular model checking, with applications to lossy channel systems. In: Proc 13th int conf on logic for programming and artificial intelligence, and reasoning (LPAR 2006). Lecture notes in computer science, vol 4246. Springer, Berlin, pp 347–361. doi:10.1007/11916277_24 CrossRef

15.

Baier C, Bertrand N, Schnoebelen P (2007) Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties. ACM Transactions on Computational Logic 9(1):5. doi:10.1145/1297658.1297663 MathSciNetCrossRef

16.

Baier C, Engelen B (1999) Establishing qualitative properties for probabilistic lossy channel systems: an algorithmic approach. In: Proc 5th int AMAST workshop formal methods for real-time and probabilistic systems (ARTS 1999). Lecture notes in computer science, vol 1601. Springer, Berlin, pp 34–52. doi:10.1007/3-540-48778-6_3 CrossRef

17.

Baier C, Katoen JP (2008) Principles of model checking. MIT Press, Cambridge MATH

18.

Bardin S, Finkel A, Leroux J, Schnoebelen P (2005) Flat acceleration in symbolic model checking. In: Proc 3rd int symp automated technology for verification and analysis (ATVA 2005). Lecture notes in computer science, vol 3707. Springer, Berlin, pp 474–488. doi:10.1007/11562948_35 CrossRef

19.

Bertrand N, Schnoebelen P (2012) Revisiting stochastic games on lossy channel systems. Submitted for publication

20.

Boigelot B (2003) On iterating linear transformations over recognizable sets of integers. Theor Comput Sci 309(1–3):413–468. doi:10.1016/S0304-3975(03)00314-1 MathSciNetCrossRefMATH

21.

Boigelot B, Godefroid P (1999) Symbolic verification of communication protocols with infinite state spaces using QDDs. Form Methods Syst Des 14(3):237–255. doi:10.1023/A:1008719024240 CrossRef

22.

Boigelot B, Legay A, Wolper P (2003) Iterating transducers in the large. In: Proc 15th int conf computer aided verification (CAV 2003). Lecture notes in computer science, vol 2725. Springer, Berlin, pp 223–235. doi:10.1007/978-3-540-45069-6_24 CrossRef

23.

Boigelot B, Legay A, Wolper P (2004) Omega-regular model checking. In: Proc 10th int conf tools and algorithms for the construction and analysis of systems (TACAS 2004). Lecture notes in computer science, vol 2988. Springer, Berlin, pp 561–575. doi:10.1007/978-3-540-24730-2_41 CrossRef

24.

Bouajjani A, Habermehl P, Moro P, Vojnar T (2005) Verifying programs with dynamic 1-selector-linked structures in regular model checking. In: Proc 11th int conf tools and algorithms for the construction and analysis of systems (TACAS 2005). Lecture notes in computer science, vol 3440. Springer, Berlin, pp 13–39. doi:10.1007/978-3-540-31980-1_2 CrossRef

25.

Bouajjani A, Habermehl P, Vojnar T (2004) Abstract regular model checking. In: Proc 16th int conf computer aided verification (CAV 2004). Lecture notes in computer science, vol 3114. Springer, Berlin, pp 372–386. doi:10.1007/978-3-540-27813-9_29 CrossRef

26.

Bouajjani A, Jonsson B, Nilsson M, Touili T (2000) Regular model checking. In: Proc 12th int conf computer aided verification (CAV 2000). Lecture notes in computer science, vol 1855. Springer, Berlin, pp 403–418. doi:10.1007/10722167_31 CrossRef

27.

Bouyer P, Markey N, Ouaknine J, Schnoebelen P, Worrell J (2012) On termination and invariance for faulty channel machines. Form Asp Comput 24(4–6):595–607. doi:10.1007/s00165-012-0234-7 MathSciNetCrossRefMATH

28.

Bouyer P, Markey N, Reynier PA (2008) Robust analysis of timed automata via channel machines. In: Proc 11th int conf foundations of software science and computational structures (FOSSACS 2008). Lecture notes in computer science, vol 4962. Springer, Berlin, pp 157–171. doi:10.1007/978-3-540-78499-9_12

29.

Bozzelli L, Pinchinat S (2012) Verification of gap-order constraint abstractions of counter systems. In: Proc 13th int conf verification, model checking, and abstract interpretation (VMCAI 2012). Lecture notes in computer science, vol 7148. Springer, Berlin, pp 88–103. doi:10.1007/978-3-642-27940-9_7 CrossRef

30.

Bradfield JC, Stirling C (2001) Modal logics and mu-calculi: an introduction. In: Bergstra JA, Ponse A, Smolka SA (eds) Handbook of process algebra. Elsevier, Amsterdam, pp 293–330. Chap 4 CrossRef

31.

Cécé G, Finkel A, Purushothaman Iyer S (1996) Unreliable channels are easier to verify than perfect channels. Inf Comput 124(1):20–31. doi:10.1006/inco.1996.0003 CrossRefMATH

32.

Čerāns K (1994) Deciding properties of integral relational automata. In: Proc 21st int coll automata, languages, and programming (ICALP 1994). Lecture notes in computer science, vol 820. Springer, Berlin, pp 35–46. doi:10.1007/3-540-58201-0_56 CrossRef

33.

Chambart P, Schnoebelen P (2008) The ordinal recursive complexity of lossy channel systems. In: Proc 23rd IEEE symp logic in computer science (LICS 2008). IEEE Comput Soc, Los Alamitos, pp 205–216. doi:10.1109/LICS.2008.47

34.

Cousot P (2003) Verification by abstract interpretation. In: Verification: theory & practice. Lecture notes in computer science, vol 2772. Springer, Berlin, pp 243–268. doi:10.1007/978-3-540-39910-0_11 CrossRef

35.

de Alfaro L, Henzinger TA, Majumdar R (2001) Symbolic algorithms for infinite-state games. In: Proc 12th int conf concurrency theory (CONCUR 2001). Lecture notes in computer science, vol 2154. Springer, Berlin, pp 536–550. doi:10.1007/3-540-44685-0_36 CrossRef

36.

Delzanno G, Raskin JF, Van Begin L (2004) Covering sharing trees: a compact data structure for parameterized verification. Int J Softw Tools Technol Transf 5(2–3):268–297. doi:10.1007/s10009-003-0110-0 CrossRef

37.

Demri S, Lazić R (2009) LTL with the freeze quantifier and register automata. ACM Trans Computational Logic 10(3):16. doi:10.1145/1507244.1507246

38.

Dufourd C, Finkel A, Schnoebelen P (1998) Reset nets between decidability and undecidability. In: Proc 25th int coll automata, languages, and programming (ICALP 1998). Lecture notes in computer science, vol 1443. Springer, Berlin, pp 103–115. doi:10.1007/BFb0055044 CrossRef

39.

Emerson EA (1990) Temporal and modal logic. In: van Leeuwen J (ed) Handbook of theoretical computer science, vol B. Elsevier, Berlin, pp 995–1072. Chap 16

40.

Emerson EA, Namjoshi KS (1998) On model checking for non-deterministic infinite-state systems. In: Proc 13th IEEE symp logic in computer science (LICS 1998). IEEE Comput Soc, Los Alamitos, pp 70–80. doi:10.1109/LICS.1998.705644

41.

Esparza J (1998) Decidability and complexity of petri net problems—an introduction. In: Lectures on Petri nets I: basic models. Lecture notes in computer science, vol 1491. Springer, Berlin, pp 374–428. doi:10.1007/3-540-65306-6_20 CrossRef

42.

Fenner S, Gasarch W, Postow B (2009) The complexity of finding SUBSEQ(A). Theory Comput Syst 45(3):577–612. doi:10.1007/s00224-008-9111-4 MathSciNetCrossRefMATH

43.

Figueira D, Figueira S, Schmitz S, Schnoebelen P (2011) Ackermannian and primitive-recursive bounds with Dickson’s lemma. In: Proc 26th IEEE symp logic in computer science (LICS 2011). IEEE Comput Soc, Los Alamitos, pp 269–278. doi:10.1109/LICS.2011.39 CrossRef

44.

Figueira D, Segoufin L (2009) Future-looking logics on data words and trees. In: Proc 34th int symp math found comp sci (MFCS 2009). Lecture notes in computer science, vol 5734. Springer, Berlin, pp 331–343. doi:10.1007/978-3-642-03816-7_29 CrossRef

45.

Finkel A (1994) Decidability of the termination problem for completely specified protocols. Distrib Comput 7(3):129–135. doi:10.1007/BF02277857 CrossRef

46.

Finkel A, Goubault-Larrecq J (2009) Forward analysis for WSTS, part I: completions. In: Proc 26th ann symp theoretical aspects of computer science (STACS 2009). Leibniz international proceedings in informatics, vol 3. Leibniz-Zentrum für Informatik, Dagstuhl, pp 433–444. doi:10.4230/LIPIcs.STACS.2009.1844

47.

Finkel A, McKenzie P, Picaronny C (2004) A well-structured framework for analysing Petri nets extensions. Inf Comput 195(1–2):1–29. doi:10.1016/j.ic.2004.01.005 MathSciNetCrossRefMATH

48.

Finkel A, Schnoebelen P (2001) Well-structured transition systems everywhere! Theor Comput Sci 256(1–2):63–92. doi:10.1016/S0304-3975(00)00102-X MathSciNetCrossRefMATH

49.

Glabbeek RJv (1993) The linear time—branching time spectrum II: the semantics of sequential systems with silent moves. In: Proc 4th int conf concurrency theory (CONCUR 1993). Lecture notes in computer science, vol 715. Springer, Berlin, pp 66–81. doi:10.1007/3-540-57208-2_6

50.

Glabbeek RJv (2001) The linear time—branching time spectrum I. In: Bergstra JA, Ponse A, Smolka SA (eds) Handbook of process algebra. Elsevier, Amsterdam, pp 3–99. Chap 1 CrossRef

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

52.

Gruber H, Holzer M, Kutrib M (2009) More on the size of Higman-Haines sets: effective constructions. Fundam Inform 91(1):105–121. doi:10.3233/FI-2009-0035 MathSciNetMATH

53.

Habermehl P, Vojnar T (2005) Regular model checking using inference of regular languages. In: Proc 6th int workshop on verification of infinite state systems (INFINITY 2004). Electronic notes in theor comp sci, vol 138. Elsevier, Amsterdam, pp 21–36. doi:10.1016/j.entcs.2005.01.044

54.

Haddad S, Schmitz S, Schnoebelen P (2012) The ordinal-recursive complexity of timed-arc Petri nets, data nets, and other enriched nets. In: Proc 27th IEEE symp logic in computer science (LICS 2012). IEEE Comput Soc, Los Alamitos, pp 355–364. doi:10.1109/LICS.2012.46

55.

Henzinger TA, Majumdar R, Raskin JF (2005) A classification of symbolic transition systems. ACM Trans Comput Log 6(1):1–32. doi:10.1145/1042038.1042039 MathSciNetCrossRef

56.

Jančar P (1995) Undecidability of bisimilarity for petri nets and some related problems. Theor Comput Sci 148(2):281–301. doi:10.1016/0304-3975(95)00037-W CrossRefMATH

57.

Jančar P, Esparza J, Moller F (1999) Petri nets and regular processes. J Comput Syst Sci 59(3):476–503. doi:10.1006/jcss.1999.1643 CrossRefMATH

58.

Jančar P, Kučera A, Mayr R (2001) Deciding bisimulation-like equivalences with finite-state processes. Theor Comput Sci 258(1–2):409–433. doi:10.1016/S0304-3975(00)00027-X MATH

59.

Jeż A, Okhotin A (2012) Representing hyper-arithmetical sets by equations over sets of integers. Theory Comput Syst 51(2):196–228. doi:10.1007/s00224-011-9352-5 MathSciNetCrossRefMATH

60.

de Jongh DHJ, Parikh R (1977) Well-partial orderings and hierarchies. Indag Math 39(3):195–207. doi:10.1016/1385-7258(77)90067-1 MathSciNetCrossRef

61.

Kesten Y, Maler O, Marcus M, Pnueli A, Shahar E (2001) Symbolic model checking with rich assertional languages. Theor Comput Sci 256(1–2):93–112. doi:10.1016/S0304-3975(00)00103-1 MathSciNetCrossRefMATH

62.

Khoussainov B, Nerode A (1995) Automatic presentations of structures. In: Proc int workshop logical and computational complexity (LCC 1994). Lecture notes in computer science, vol 960. Springer, Berlin, pp 367–392. doi:10.1007/3-540-60178-3_93 CrossRef

63.

Kouzmin EV, Shilov NV, Sokolov VA (2004) Model checking mu-calculus in well-structured transition systems. In: Proc 11th int symp temporal representation and reasoning (TIME 2004). IEEE Comput Soc, Los Alamitos, pp 152–155. doi:10.1109/TIME.2004.1314433

64.

Kruskal JB (1972) The theory of well-quasi-ordering: a frequently discovered concept. J Comb Theory, Ser A 13(3):297–305. doi:10.1016/0097-3165(72)90063-5 MathSciNetCrossRefMATH

65.

Kučera A, Schnoebelen P (2006) A general approach to comparing infinite-state systems with their finite-state specifications. Theor Comput Sci 358(2–3):315–333. doi:10.1016/j.tcs.2006.01.021 MATH

66.

Kunc M (2007) What do we know about language equations? In: Proc 11th int conf developments in language theory (DLT 2007). Lecture notes in computer science, vol 4588. Springer, Berlin, pp 23–27. doi:10.1007/978-3-540-73208-2_3 CrossRef

67.

Leroux J, Point G (2009) TaPAS: the Talence Presburger arithmetic suite. In: Proc 15th int conf tools and algorithms for the construction and analysis of systems (TACAS 2009). Lecture notes in computer science, vol 5505. Springer, Berlin, pp 182–185. doi:10.1007/978-3-642-00768-2_18 CrossRef

68.

Mayr R (2003) Undecidable problems in unreliable computations. Theor Comput Sci 297(1–3):337–354. doi:10.1016/S0304-3975(02)00646-1 MathSciNetCrossRefMATH

69.

Milner EC (1985) 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. Reidel, Dordrecht, pp 487–502

70.

Perrin D (1990) Finite automata. In: van Leeuwen J (ed) Handbook of theoretical computer science, vol. B. Elsevier, Amsterdam, pp 1–57. Chap 1

71.

Rabinovich A (2006) Quantitative analysis of probabilistic lossy channel systems. Inf Comput 204(5):713–740. doi:10.1016/j.ic.2005.11.004 MathSciNetCrossRefMATH

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

73.

Raskin JF, Samuelides M, Van Begin L (2005) Games for counting abstractions. In: Proc 4th int workshop on automated verification of critical systems (AVoCS 2004). Electronic notes in theor comp sci, vol 128. Elsevier, Amsterdam, pp 69–85. doi:10.1016/j.entcs.2005.04.005

74.

Schmitz S, Schnoebelen P (2011) Multiply-recursive upper bounds with Higman’s lemma. In: Proc 38th int coll automata, languages, and programming (ICALP 2011). Lecture notes in computer science, vol 6756. Springer, Berlin, pp 441–452. doi:10.1007/978-3-642-22012-8_35 CrossRef

75.

Schnoebelen P (2001) Bisimulation and other undecidable equivalences for lossy channel systems. In: Proc 4th int symp theoretical aspects of computer software (TACS 2001). Lecture notes in computer science, vol 2215. Springer, Berlin, pp 385–399. doi:10.1007/3-540-45500-0_19 CrossRef

76.

Schnoebelen P (2004) The verification of probabilistic lossy channel systems. In: Validation of stochastic systems—a guide to current research. Lecture notes in computer science, vol 2925. Springer, Berlin, pp 445–465. doi:10.1007/978-3-540-24611-4_13 CrossRef

77.

Schnoebelen P (2010) Lossy counter machines decidability cheat sheet. In: Proc 4th int workshop reachability problems (RP 2010). Lecture notes in computer science, vol 6227. Springer, Berlin, pp 51–75. doi:10.1007/978-3-642-15349-5_4 CrossRef

78.

Schnoebelen P (2010) Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets. In: Proc 35th int symp mathematical foundations of computer science (MFCS 2010). Lecture notes in computer science, vol 6281. Springer, Berlin, pp 616–628. doi:10.1007/978-3-642-15155-2_54 CrossRef

79.

Valk R (1978) Self-modifying nets, a natural extension of Petri nets. In: Proc 5th coll automata, languages, and programming (ICALP 1978). Lecture notes in computer science, vol 62. Springer, Berlin, pp 464–476. doi:10.1007/3-540-08860-1_35 CrossRef

80.

van Leeuwen J (1978) Effective constructions in well-partially-ordered free monoids. Discrete Math 21(3):237–252. doi:10.1016/0012-365X(78)90156-5 MathSciNetCrossRef

81.

Wolper P, Boigelot B (1998) Verifying systems with infinite but regular state spaces. In: Proc 10th int conf computer aided verification (CAV 1998). Lecture notes in computer science, vol 1427. Springer, Berlin, pp 88–97. doi:10.1007/BFb0028736 CrossRef

Titel: Computable fixpoints in well-structured symbolic model checking
verfasst von: N. Bertrand
P. Schnoebelen
Publikationsdatum: 01.10.2013
Verlag: Springer US
Erschienen in: Formal Methods in System Design / Ausgabe 2/2013
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI: https://doi.org/10.1007/s10703-012-0168-y

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 2/2013

Preface to the special issue on Probabilistic Model Checking

On-the-fly verification and optimization of DTA-properties for large Markov chains

A compositional modelling and analysis framework for stochastic hybrid systems

Algorithmic probabilistic game semantics

Bayesian statistical model checking with application to Stateflow/Simulink verification

A survey of partial-observation stochastic parity games