Recognizing safety and liveness

From MaRDI portal
Publication:1100884

DOI10.1007/BF01782772zbMath0641.68039OpenAlexW1984478483WikidataQ56569331 ScholiaQ56569331MaRDI QIDQ1100884

Fred B. Schneider, Bowen Alpern

Publication date: 1987

Published in: Distributed Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01782772



Related Items

Efficient Runtime Verification of First-Order Temporal Properties, Inference Systems with Corules for Combined Safety and Liveness Properties of Binary Session Types, Spanning the spectrum from safety to liveness, Safety, liveness and fairness in temporal logic, Temporal Logic and Fair Discrete Systems, Modeling for Verification, Functional Specification of Hardware via Temporal Logic, Prognosis of \(\omega\)-languages for the diagnosis of *-languages: a topological perspective, Compositional System Security with Interface-Confined Adversaries, Certifying DFA bounds for recognition and separation, On the complexity of verification of time-sensitive distributed systems, Interpreting message flow graphs, Theory and methodology of assumption/commitment based system interface specification and architectural contracts, Monitoring hyperproperties with circuits, Control design for nondeterministic input/output automata, Monitoring first-order interval logic, Specification and verification of concurrent systems by causality and realizability, On monitoring linear temporal properties, Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans, An interface theory for service-oriented design, Quantitative safety and liveness, Automated repair for timed systems, Liminf progress measures, Discriminative Model Checking, LTL is closed under topological closure, Linear temporal logic symbolic model checking, Which security policies are enforceable by runtime monitors? A survey, First-order temporal logic monitoring with BDDs, An abstract interpretation-based model for safety semantics, Verification of asynchronous systems with an unspecified component, Proving correctness with respect to nondeterministic safety specifications, Snap-stabilization in message-passing systems, Certifying inexpressibility, A Novel Learning Algorithm for Büchi Automata Based on Family of DFAs and Classification Trees, Interval logics and their decision procedures. I: An interval logic, A complete characterization of deterministic regular liveness properties, On relative and probabilistic finite counterability, A Temporal Logic for Mutual Mobile Membranes with Objects on Surface, Heterogeneous and asynchronous networks of timed systems, Problems of synthesis of \(\Sigma\)-automata specified in languages LP and LF of first order logic, Computer says no: verdict explainability for runtime monitors using a local proof system, Safety and Liveness, Weakness and Strength, and the Underlying Topological Relations, Proving linearizability with temporal logic, Model checking usage policies, Turing machines, transition systems, and interaction, Transforming semantics by abstract interpretation, Characterization of temporal property classes, Prime languages, Using partial orders for the efficient verification of deadlock freedom and safety properties, On satisficing in quantitative games, A novel learning algorithm for Büchi automata based on family of DFAs and classification trees, Unnamed Item, Proving possibility properties, On the refinement of liveness properties of distributed systems, A formal theory of simulations between infinite automata, Enforcing Non-safety Security Policies with Program Monitors, The existence of refinement mappings, Safety and liveness of \(\omega\)-context-free languages, Two-process synchronization



Cites Work