Abstract
We study the problem of checking weighted CTL properties for weighted Kripke structures in presence of imprecise weights. We consider two extensions of the notion of weighted Kripke structures, namely (i) parametric weighted Kripke structures, having transitions weights modelled as affine maps over a set of parameters and, (ii) weight-uncertain Kripke structures, having transition labelled by real-valued random variables as opposed to precise real valued weights.
We address this problem by using extended parametric dependency graphs, a symbolic extension of dependency graphs by Liu and Smolka. Experiments performed with a prototype tool implementation show that our approach outperforms by orders of magnitude an adaptation of a state-of-the-art tool for WKSs.
Work supported by the Advanced ERC Grant nr. 867096 (LASSO).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
Our is a special case of the so called affine transformation matrix (or projective transformation matrix) representation for generic affine tranformations.
- 2.
As usual, \(\bigsqcap \emptyset = A_\top \) and \(\bigsqcup \emptyset = A_\top \).
- 3.
To simplify the exposition, here unevaluated expressions are assumed to be modulo commutativity and associativity of \(+\).
- 4.
In fact, the vector \(\mathbf {X}\) is a multivariate random variable \(\mathbf {X} :\Omega \rightarrow \mathbb {R}^n\) with marginals \(X_i :\Omega \rightarrow \mathbb {R}_{\ge 0}\) (\(i= 1..n\)).
- 5.
The PVTool2 is available at https://github.com/AcId9381/PVTool.
- 6.
The UVTool is implemented using Mathematica [16] and is available at http://people.cs.aau.dk/~giovbacci/tools.html.
- 7.
The WKTool is available at https://github.com/jonasfj/WKTool.
References
Avni, G., Kupferman, O.: Stochastization of weighted automata. In: Italiano, G.F., Pighizzini, G., Sannella, D.T. (eds.) MFCS 2015. LNCS, vol. 9234, pp. 89–102. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-48057-1_7
Bacci, G., Hansen, M., Larsen, K.G.: On the verification of weighted Kripke structures under uncertainty. Full version, Aalborg University (2018). http://people.cs.aau.dk/~giovbacci/papers/uncertwks-full.pdf
Baier, C., Katoen, J.-P.: Principles of model checking. MIT Press, Cambridge (2008)
Chatterjee, K., Doyen, L., Henzinger, T.A.: Probabilistic weighted automata. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 244–258. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04081-8_17
Christoffersen, P., Hansen, M., Mariegaard, A., Ringsmose, J.T., Larsen, K.G., Mardare, R.: Parametric verification of weighted systems. In: 2nd International Workshop on Synthesis of Complex Parameters, SynCoP 2015, April 11, 2015, London, United Kingdom, pp. 77–90 (2015)
Dalsgaard, A.E., et al.: Extended dependency graphs and efficient distributed fixed-point computation. In: van der Aalst, W., Best, E. (eds.) PETRI NETS 2017. LNCS, vol. 10258, pp. 139–158. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57861-3_10
Droste, M., Kuich, W., Vogler, H. (eds.): Handbook of Weighted Automata, 1st edn. Springer Publishing Company, Incorporated, Heidelberg (2009). https://doi.org/10.1007/978-3-642-01492-5
Fahrenberg, U., Larsen, K.G., Thrane, C.: A quantitative characterization of weighted Kripke structures in temporal logic. Comput. Inf. 29, 1311–1324 (2010)
Jensen, J.F., Larsen, K.G., Srba, J., Oestergaard, L.K.: Efficient model-checking of weighted CTL with upper-bound constraints. STTT 18(4), 409–426 (2016)
Singh Kambo, N., Kotz, S.: On exponential bounds for binomial probabilities. Ann. Inst. Stat. Math. 18(1), 277 (1966)
Liu, X., Smolka, S.A.: Simple linear-time algorithms for minimal fixed points (extended abstract). In: Proceedings of the Automata, Languages and Programming, 25th International Colloquium, ICALP 1998, Aalborg, Denmark, July 13-17, 1998, pp. 53–66 (1998)
Monniaux, D.: Quantifier elimination by Lazy model enumeration. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 585–599. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14295-6_51
Okamoto, M.: Some inequalities relating to the partial sum of binomial probabilities. Ann. Inst. Stat. Math. 10(1), 29–35 (1959)
Srkk, S.: Bayesian Filtering and Smoothing. Cambridge University Press, New York (2013)
Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: 26th Annual Symposium on Foundations of Computer Science, Portland, Oregon, USA, 21–23 October 1985, pp. 327–338. IEEE Computer Society (1985)
Wolfram Research, Inc., Mathematica, Version 11.2. Champaign, IL (2017)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Bacci, G., Hansen, M., Larsen, K.G. (2018). On the Verification of Weighted Kripke Structures Under Uncertainty. In: McIver, A., Horvath, A. (eds) Quantitative Evaluation of Systems. QEST 2018. Lecture Notes in Computer Science(), vol 11024. Springer, Cham. https://doi.org/10.1007/978-3-319-99154-2_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-99154-2_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-99153-5
Online ISBN: 978-3-319-99154-2
eBook Packages: Computer ScienceComputer Science (R0)