Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
International Journal on Software Tools for Technology Transfer
Erschienen in: International Journal on Software Tools for Technology Transfer 5/2018

10.08.2018 | SPIN 2016

On-the-fly model checking for extended action-based probabilistic operators

verfasst von: Radu Mateescu, José Ignacio Requeno

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 5/2018

Einloggen

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

search-config
loading …

Abstract

The quantitative analysis of concurrent systems requires expressive and user-friendly property languages combining temporal, data handling, and quantitative aspects. In this paper, we aim at facilitating the quantitative analysis of systems modeled as PTSs (Probabilistic Transition Systems) labeled by actions containing data values and probabilities. We propose a new regular probabilistic operator that specifies the probability measure of a path described by a generalized regular formula involving arbitrary computations on data values. This operator, which subsumes the Until operators of PCTL and their action-based counterparts, can provide useful quantitative information about paths having certain (e.g., peak) cost values. We integrated the regular probabilistic operator into MCL (Model Checking Language) and we devised an associated on-the-fly model checking method, based on a combined local resolution of linear and Boolean equation systems. We implemented the method in the EVALUATOR model checker of the CADP toolbox and experimented it on realistic PTSs modeling concurrent systems.
Vorheriger Artikel Modeling and analyzing real-time wireless sensor and actuator networks using actors and model checking
Nächster Artikel Fair testing and stubborn sets

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 "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

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
Fußnoten
Literatur
1.
Agha, G., Meseguer, J., Sen, K.: PMaude: rewrite-based specification language for probabilistic object systems. Electron. Notes Theor. Comput. Sci. 153(2), 213–239 (2006)CrossRef
2.
Amestoy, P., Duff, I.S., L’Excellent, J.-Y., Koster, J.: MUMPS: a general purpose distributed memory sparse solver. In: PARA’2000, LNCS, vol. 1947, pp. 121–130. Springer, Berlin (2000)
3.
4.
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying continuous time Markov chains. In: CAV’96, LNCS, vol. 1102, pp. 269–276. Springer, Berlin (1996)
5.
Baier, C., Cloth, L., Haverkort, B.R., Kuntz, M., Siegle, M.: Model checking Markov chains with actions and state labels. IEEE Trans. Softw. Eng. 33(4), 209–224 (2007)CrossRef
6.
Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29(7), 1–18 (2003)MATH
7.
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH
8.
Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: VMCAI’04, LNCS, vol. 2937,pp. 44–57. Springer, Berlin (2004)
9.
Bolze, R., Cappello, F., Caron, E., Daydé, M.J., Desprez, F., Jeannot, E., Jégou, Y., Lanteri, S., Leduc, J., Melab, N., Mornet, G., Namyst, R., Primet, P., Quétier, B., Richard, O., Talbi, E.-G., Touche, I.: Grid’5000: a large scale and highly reconfigurable experimental grid testbed. IJHPCA 20(4), 481–494 (2006)
10.
11.
Champelovier, D., Clerc, X., Garavel, H., Guerte, Y., McKinty, C., Powazny, V., Lang, F., Serwe, W., Smeding, G.: Reference manual of the LNT to LOTOS translator (Version 6.2). Inria/Vasy and Inria/Convecs (2015)
12.
Chua, L.O., Lin, P.M.: Computer Aided Analysis of Electronic Circuits. Prentice Hall, Englewood Cliffs (1975)MATH
13.
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244–263 (1986)CrossRefMATH
14.
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)
15.
Cleaveland, R., Iyer, S.P., Narasimha, M.: Probabilistic temporal logics via the modal mu-calculus. TCS 342(2–3), 316–350 (2005)MathSciNetCrossRefMATH
16.
Cleaveland, R., Steffen, B.: A linear-time model-checking algorithm for the alternation-free modal mu-calculus. FMSD 2(2), 121–147 (1993)MATH
17.
Coste, N., Hermanns, H., Lantreibecq, E., Serwe, W.: Towards performance prediction of compositional models in industrial gals designs. In: CAV’2009, LNCS, vol. 5643, pp. 204–218. Springer, Berlin (2009)
18.
D’Argenio, P., Jeannet, B., Jensen, H., Larsen, K.: Reachability analysis of probabilistic systems by successive refinements. In: PAPM/PROBMIV’01, LNCS, vol. 2165, pp. 39–56. Springer, Berlin (2001)
19.
20.
De Nicola, R., Vaandrager, F.W.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) Semantics of Concurrency, LNCS, vol. 469, pp. 407–419. Springer, Berlin (1990)CrossRef
21.
Dijkstra, E.W.: Solution of a problem in concurrent programming control. CACM 8(9), 569 (1965)CrossRef
22.
Duflot, M., Fribourg, L., Picaronny, C.: Randomized dining philosophers without fairness assumption. Distrib. Comput. 17(1), 65–76 (2004)CrossRef
23.
Emerson, E.A., Lei, C-L.: Efficient model checking in fragments of the propositional mu-calculus. In: LICS’86, pp. 267–278. IEEE Press, New York (1986)
24.
Feller, W.: An Introduction to Probability Theory and Its Applications. Wiley, New York (2001)MATH
25.
Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. JCSS 18(2), 194–211 (1979)MathSciNetMATH
26.
Garavel, H.: OPEN/CAESAR: an open software architecture for verification, simulation, and testing. In: TACAS’98, LNCS, vol. 1384, pp. 68–84. Springer, Berlin. Full version available as INRIA Research Report RR-3352 (1998)
27.
Garavel, H., Lang, F.: SVL: a scripting language for compositional verification. In: FORTE’01, pp. 377–392. Kluwer, Dordrecht (2001)
28.
Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. STTT 15(2), 89–107 (2013)CrossRefMATH
29.
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Form. Asp. Comput. 6(5), 512–535 (1994)CrossRefMATH
30.
Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32, 137–161 (1985)CrossRefMATH
31.
Hermanns, H., Katoen, J.-P., Meyer-Kayser, J., Siegle, M.: Towards model checking stochastic process algebra. In: IFM’00, LNCS, vol. 1945, pp. 420–439. Springer, Berlin (2000)
32.
Israeli, A., Jalfon, M.: Token management schemes and random walks yield self-stabilizating mutual exclusion. In: PODC’90, pp. 119–131. ACM Press, New York (1990)
33.
Knuth, D.E., Yao, A.C.: The complexity of nonuniform random number generation. In: Traub, J.F. (ed.) Algorithms and Complexity: New Directions and Recent Results, pp. 357–428. Academic Press, New York (1976)
34.
35.
36.
Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: CAV’2011, LNCS, vol. 6806, pp. 585–591. Springer, Berlin (2011)
37.
Lamport, L.: A fast mutual exclusion algorithm. ACM Trans. Comput. Syst. 5(1), 1–11 (1987)CrossRef
38.
Larsen, K.G.: Proof systems for Hennessy–Milner logic with recursion. In: CAAP’88, LNCS, vol. 299, pp. 215–230. Springer, Berlin (1988)
39.
40.
Latella, D., Loreti, M., Massink, M.: On-the-fly fast mean-field model-checking. In: Trustworthy Global Computing, pp. 297–314. Springer, Berlin (2014)
41.
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Specification, vol. I. Springer, New York (1992)CrossRefMATH
42.
Mateescu, R.: Formal description and analysis of a bounded retransmission protocol. In: COST’96, University of Maribor, Slovenia (1996). Also available as INRIA Research Report RR-2965
43.
Mateescu, R.: Caesar_solve: a generic library for on-the-fly resolution of alternation-free Boolean equation systems. STTT 8(1), 37–56 (2006)CrossRef
44.
Mateescu, R., Monteiro, P.T., Dumas, E., de Jong, H.: CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks. TCS 412(26), 2854–2883 (2011)MathSciNetCrossRefMATH
45.
Mateescu, R., Requeno, J.I.: On-the-fly model checking for extended action-based probabilistic operators. In: SPIN’2016, LNCS, vol. 9641, pp. 189–207. Springer, Berlin (2016)
46.
Mateescu, R., Serwe, W.: Model checking and performance evaluation with CADP illustrated on shared-memory mutual exclusion protocols. SCP 78(7), 843–861 (2013)
47.
Mateescu, R., Sighireanu, M.: Efficient on-the-fly model-checking for regular alternation-free mu-calculus. SCP 46(3), 255–281 (2003)MathSciNetMATH
48.
Mateescu, R., Thivolle, D.: A model checking language for concurrent value-passing systems. In: FM’08, LNCS, vol. 5014, pp. 148–164. Springer, Berlin (2008)
49.
Wolper, P.: Temporal logic can be more expressive. In: FOCS’81, pp. 340–348. IEEE Press, New York (1981)
50.
van Glabbeek, R.J., Smolka, S.A., Steffen, B.: Reactive, generative and stratified models of probabilistic processes. Inf. Comput. 121(1), 59–80 (1995)MathSciNetCrossRefMATH
Metadaten
Titel
On-the-fly model checking for extended action-based probabilistic operators
verfasst von
Radu Mateescu
José Ignacio Requeno
Publikationsdatum
10.08.2018
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 5/2018
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-018-0499-0

Weitere Artikel der Ausgabe 5/2018

International Journal on Software Tools for Technology Transfer 5/2018 Zur Ausgabe

SPIN 2016

Discrete and continuous strategies for timed-arc Petri net games

SPIN 2016

Fair testing and stubborn sets

SPIN 2016

A case study of planning for smart factories

Introduction

Model checking: recent improvements and applications

SPIN 2016

Integrating river basin DSSs with model checking

SPIN 2016

Modeling and analyzing real-time wireless sensor and actuator networks using actors and model checking