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
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Defining liveness
- Safety without stuttering
- Verification of concurrent programs: The automata-theoretic framework
- Temporal logic can be more expressive
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Verifying temporal properties without temporal logic