Abstract
Of special interest in formal verification are safety specifications, which assert that the system stays within some allowed region, in which nothing “bad” happens. Equivalently, a computation violates a safety specification if it has a “bad prefix” – a prefix all whose extensions violate the specification. The theoretical properties of safety specifications as well as their practical advantages with respect to general specifications have been widely studied. Safety is binary: a specification is either safety or not safety. We introduce a quantitative measure for safety. Intuitively, the safety level of a language L measures the fraction of words not in L that have a bad prefix. In particular, a safety language has safety level 1 and a liveness language has safety level 0. Thus, our study spans the spectrum between traditional safety and liveness. The formal definition of safety level is based on probability and measures the probability of a random word not in L to have a bad prefix. We study the problem of finding the safety level of languages given by means of deterministic and nondeterministic automata as well as LTL formulas, and the problem of deciding their membership in specific classes along the spectrum (safety, almost-safety, fraction-safety, etc.). We also study properties of the different classes and the structure of deterministic automata for them.
The research leading to these results has received funding from the European Research Council under the European Union’s Seventh Framework Programme (FP7/2007-2013) / ERC grant agreement no 278410, and from The Israel Science Foundation (grant no 1229/10).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
- 2.
Note that \(\varSigma =2^{AP}\) and our probability distribution is such that for each atomic proposition a and for each position in a computation, the probability that a holds in the position is \(\frac{1}{2}\).
- 3.
An anomaly of this definition is the language \(L=\varSigma ^\omega \). While \(Pr(L)=1\), making its safety level 0, we also have that L is a safety language. Thus, L is the only language that is both safety and has safety level 0.
- 4.
We did not find in the literature an NLOGSPACE-complete result for deciding liveness of a DPW. The proof, however, follows standard considerations, and we give it in the full version.
References
Alpern, B., Schneider, F.B.: Defining liveness. IPL 21, 181–185 (1985)
Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2, 117–126 (1987)
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 193. Springer, Heidelberg (1999)
Bloem, R., Gabow, H.N., Somenzi, F.: An algorithm for strongly connected component analysis in n log n symbolic steps. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 37–54. Springer, Heidelberg (2000)
Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42, 857–907 (1995)
Ben-David, S., Kupferman, O.: A framework for ranking vacuity results. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 148–162. Springer, Heidelberg (2013)
Emerson, E.A.: Alternative semantics for temporal logics. TCS 26, 121–130 (1983)
Filiot, E., Jin, N., Raskin, J.-F.: An antichain algorithm for LTL realizability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 263–277. Springer, Heidelberg (2009)
Harel, D., Katz, G., Marron, A., Weiss, G.: Non-intrusive repair of reactive programs. In: ICECCS, pp. 3–12 (2012)
Havelund, K., Roşu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342–356. Springer, Heidelberg (2002)
Jones, N.D.: Space-bounded reducibility among combinatorial problems. J. Comput. Syst. Sci. 11, 68–75 (1975)
Kemeny, J.G., Snell, J.L., Knapp, A.W.: Denumerable Markov Chains. Springer, New York (1976)
Kupferman, O., Vardi, G.: On relative and probabilistic finite counterabilty. In: Proceediongs of the 24th CSL. Springer (2015)
Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291–314 (2001)
Kupferman, O., Vardi, M.Y.: On bounded specifications. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 24–38. Springer, Heidelberg (2001)
Lamport, L.: Logical foundation. In: Paul, M., Siegert, H.J. (eds.) Distributed Systems - Methods and Tools for Specification. LNCS, 190th edn. Springer, Heidelberg (1985)
Landweber, L.H.: Decision problems for \(\omega \)-automata. Math. Syst. Theory 3, 376–384 (1969)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York (1992)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Safety. Springer, New York (1995)
Meyer, A.R., Stockmeyer, L.J.: The equivalence problem for regular expressions with squaring requires exponential time. In: Proceedings of the 13th SWAT, pp. 125–129 (1972)
Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. In: Proceedings of the 21st LICS, pp. 255–264 (2006)
Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th FOCS, pp. 46–57 (1977)
Pnueli, A., Shahar, E.: Liveness and acceleration in parameterized verification. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 328–343. Springer, Heidelberg (2000)
Safra, S.: On the complexity of \(\omega \)-automata. In: Proceedings of the 29th FOCS, pp. 319–327 (1988)
Sistla, A.P.: Safety, liveness and fairness in temporal logic. FAC 6, 495–511 (1994)
Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logic. J. ACM 32, 733–749 (1985)
Tarjan, R.E.: Depth first search and linear graph algorithms. SIAM J. Comput. 1(2), 146–160 (1972)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. I & C 115(1), 1–37 (1994)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Faran, R., Kupferman, O. (2015). Spanning the Spectrum from Safety to Liveness. In: Finkbeiner, B., Pu, G., Zhang, L. (eds) Automated Technology for Verification and Analysis. ATVA 2015. Lecture Notes in Computer Science(), vol 9364. Springer, Cham. https://doi.org/10.1007/978-3-319-24953-7_13
Download citation
DOI: https://doi.org/10.1007/978-3-319-24953-7_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24952-0
Online ISBN: 978-3-319-24953-7
eBook Packages: Computer ScienceComputer Science (R0)