Recognizing safety and liveness

By B. Alpern, Fred B. Schneider. Distributed computing, 2005

546 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Temporal Logics for Hyperproperties (2013, background): “Let zip denote the usual function that maps an n-tuple of sequences to a single sequence of n-tuples—for example, zip([1, 2, 3], [4, 5, 6]) = [(1, 4), (2, 5), (3, 6)]—and let unzip denote its inverse.”
Software model checking (2009, unknown): “This intuition was formalized by [Alpern and Schneider 1987] as follows.”
Introduction to Embedded Systems - A Cyber-Physical Systems Approach (2013, background): “See Lamport (1977) and Alpern and Schneider (1987) for a theoretical treatment of safety and liveness.”
Hyperproperties (2010, methodology): “We have not obtained complete verification methods for hypersafety or for hyperliveness, but we have been able to generalize prior work on using invariance arguments to verify information-flow policies [7, 42].”
Principles of model checking (2008, methodology): “Propositions for the Region Transition System Consider the TCTL formula: Φ = ∀ 3 ( ∃♦[2,6]a } {{ } =Ψ1 ∧ ∃ ]2,5[ ∀♦ 3 (b ∧ (x = 9)) } {{ } =Ψ2 } {{ } =Ψ3 } {{ } =Ψ4 } {{ } =Ψ5 ),”
Edit automata: enforcement mechanisms for run-time security policies (2005, unknown): “These automata are similar to Schneider’s original security monitors.”