Abstract
Automata constructions for logical properties play an important role in the formal analysis of the system both statically and dynamically. In this paper, we present constructions of finite-state probabilistic monitors (FPM) for safety properties expressed in LTL. FPMs are probabilistic automata on infinite words that have a special, absorbing reject state, and given a cut-point λ ∈ [0,1], accept all words whose probability of reaching the reject state is at most 1 − λ. We consider Safe-LTL, the collection of LTL formulas built using conjunction, disjunction, next, and release operators, and show that (a) for any formula ϕ, there is an FPM with cut-point 1 of exponential size that recognizes the models of ϕ, and (b) there is a family of Safe-LTL formulas, such that the smallest FPM with cut-point 0 for this family is of doubly exponential size. Next, we consider the fragment LTL(G) of Safe-LTL wherein always operator is used instead of release operator and show that for any formula ϕ ∈ LTL(G) (c) there is an FPM with cut-point 0 of exponential size for ϕ, and (d) there is a robust FPM of exponential size for ϕ, where a robust FPM is one in which the acceptance probability of any word is bounded away from the cut-point. We also show that these constructions are optimal.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Chadha, R., Sistla, A.P., Viswanathan, M.: On the expressiveness and complexity of randomization in finite state monitors. J. ACM 56(5), 26:1–26:44 (2009)
Baier, C., Gröβer, M.: Recognizing ω-regular languages with probabilistic automata. In: Proceedings of the IEEE Symposium on Logic in Computer Science, pp. 137–146 (2005)
Rabin, M.: Probabilitic automata. Information and Control 6(3), 230–245 (1963)
Paz, A.: Introduction to Probabilistic Automata. Academic Press (1971)
Baier, C., Bertrand, N., Größer, M.: On decision problems for probabilistic büchi automata. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 287–301. Springer, Heidelberg (2008)
Sistla, A.P.: Safety, liveness and fairness in temporal logic. Formal Aspect of Computing, 495–511 (1999)
Kupferman, O., Vardi, M.Y.: Model checking of safety properties. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 172–183. Springer, Heidelberg (1999)
Manna, Z., Pnueli, A.: Temporal verification of reactive and concurrent systems: Specification. Springer (1992)
Alur, R., La Torre, S.: Deterministic generators and games for ltl fragments. ACM Trans. Comput. Logic 5(1), 1–25 (2004)
Yao, A.: Some complexity questions related to distributed computing. In: Proceedings of the ACM Symposium on Theory of Computation, pp. 209–213 (1979)
Kushilevtiz, E., Nisan, N.: Communication Complexity. Cambridge University Press (1996)
Kremer, I., Nisan, N., Ron, D.: On randomized one-round communication complexity. In: Symposium on Theory of Computing (June 1995)
Motwani, R., Raghavan, P.: Randomized algorithms. Cambridge University Press, New York (1995)
Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238–266. Springer, Heidelberg (1996)
Vapnik, V.N., Chervonenkis, A.Y.: On the uniform convergence of relative frequencies of events to their probabilities. Theory of Probability & Its Applications 16(2), 264–280 (1971)
Kupferman, O., Rosenberg, A.: The blow-up in translating LTL to deterministic automata. In: van der Meyden, R., Smaus, J.-G. (eds.) MoChArt 2010. LNCS, vol. 6572, pp. 85–94. Springer, Heidelberg (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kini, D., Viswanathan, M. (2014). Probabilistic Automata for Safety LTL Specifications. In: McMillan, K.L., Rival, X. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2014. Lecture Notes in Computer Science, vol 8318. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54013-4_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-54013-4_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54012-7
Online ISBN: 978-3-642-54013-4
eBook Packages: Computer ScienceComputer Science (R0)