Defining liveness
From MaRDI portal
Publication:1064056
DOI10.1016/0020-0190(85)90056-0zbMath0575.68030OpenAlexW2914206182MaRDI QIDQ1064056
Fred B. Schneider, Bowen Alpern
Publication date: 1985
Published in: Information Processing Letters (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0020-0190(85)90056-0
Related Items
Abstraction and composition: a verification method for co-operating systems, A case study in the mechanical verification of fault tolerance, A fully abstract trace model for dataflow and asynchronous networks, Liveness in timed and untimed systems, Inference Systems with Corules for Combined Safety and Liveness Properties of Binary Session Types, A temporal logic for asynchronous hyperproperties, Spanning the spectrum from safety to liveness, Deadness and how to disprove liveness in hybrid dynamical systems, Safety, liveness and fairness in temporal logic, Unnamed Item, Introduction to Model Checking, Functional Specification of Hardware via Temporal Logic, Recognizing safety and liveness, On control of systems modelled as deterministic Rabin automata, Specification and refinement of networks of asynchronously communicating agents using the assumption/commitment paradigm, Quiescence, fairness, testing, and the notion of implementation, A methodology for designing proof rules for fair parallel programs, Concurrent systems and inevitability, Model-Checking Linear-Time Properties of Quantum Systems, The refinement calculus of reactive systems, Assumption/guarantee specifications in linear-time temporal logic (extended abstract), Compositional reasoning about active objects with shared futures, Deciding safety and liveness in TPTL, An interface theory for service-oriented design, Symbolic synthesis of masking fault-tolerant distributed programs, Pattern-based and composition-driven automatic generation of logical specifications for workflow-oriented software models, Efficient fault-tolerant collision-free data aggregation scheduling for wireless sensor networks, Relating computer systems to sequence diagrams: the impact of underspecification and inherent nondeterminism, On the limits of refinement-testing for model-checking CSP, Shield synthesis, Synthesizing bounded-time 2-phase fault recovery, Harmonization of interacting automata, Model-based construction and verification of critical systems using composition and partial refinement, Assurance of dynamic adaptation in distributed systems, A theorem on atomicity in distributed algorithms, Observable behavior of distributed systems: component reasoning for concurrent objects, Some subsets of monadic first-order logic (MFO) used for the specification and synthesis of \(\Sigma\)-automata, Safety and liveness from a methodological point of view, On hierarchically developing reactive systems, Inference of \(\omega\)-languages from prefixes., Understanding deadlock and livelock behaviors in hybrid control systems, LTL is closed under topological closure, A sound and complete reasoning system for asynchronous communication with shared futures, Linear temporal logic symbolic model checking, Which security policies are enforceable by runtime monitors? A survey, Fairness and hyperfairness, Runtime verification using the temporal description logic \(\mathcal{ALC}\)-LTL revisited, Safety assurance via on-line monitoring, Correctness of concurrent processes, An abstract interpretation-based model for safety semantics, Automation of fault-tolerant graceful degradation, Finite-word hyperlanguages, Approximation of sets of superwords by \(L\)-language formulas, A note on fairness in I/O automata, Interval logics and their decision procedures. I: An interval logic, Assumption/guarantee specifications in linear-time temporal logic, Probabilistic communicating processes, Multi-parameterised compositional verification of safety properties, MinMax algorithms for stabilizing consensus, Approximately satisfied properties of systems and simple language homomorphisms, A complete characterization of deterministic regular liveness properties, Metric temporal logic with durations, On relative and probabilistic finite counterability, Liveness-Preserving Atomicity Abstraction, Operational specification with joint actions: Serializable databases, Quantitative model-checking of controlled discrete-time Markov processes, Sooner is safer than later, Synthesizing robust systems, Verification of distributed programs using representative interleaving sequences, Another glance at the Alpern-Schneider characterization of safety and liveness in concurrent executions, A Branching Time Logical System for Open Distributed Systems Development, CPO semantics of timed interactive actor networks, Safety and Liveness, Weakness and Strength, and the Underlying Topological Relations, Succinct representations of languages by DFA with different levels of reliability, Runtime enforcement monitors: Composition, synthesis, and enforcement abilities, \(\omega\)-regular languages are testable with a constant number of queries, A system for deduction-based formal verification of workflow-oriented software models, The asynchronous bounded-cycle model, Unnamed Item, Automated Compositional Reasoning of Intuitionistically Closed Regular Properties, Model checking of linear-time properties in multi-valued systems, Monitoring Metric First-Order Temporal Properties, Characterization of temporal property classes, Time and logic: A calculus of binary events, On computing the supremal right-closed control invariant subset of a right-closed set of markings for an arbitrary Petri net, Liveness in timed and untimed systems, P-A logic - a compositional proof system for distributed programs, AUTOMATED COMPOSITIONAL REASONING OF INTUITIONISTICALLY CLOSED REGULAR PROPERTIES, Verification of compliance for multilevel models in individual trace semantics, Behaviour approximated on subgroups, A trace-based model for multiparty contracts, From liveness to promptness, Timed CSP = Closed Timed Automata1, A semantic model for interacting cyber-physical systems, Programming interfaces and basic topology, Observable Behavior of Dynamic Systems: Component Reasoning for Concurrent Objects, Model checking hyperproperties for Markov decision processes, The complexity of automated addition of fault-tolerance without explicit legitimate states, On probabilistic snap-stabilization, Non-interference and local correctness in transactional memory, Synchronous \(t\)-resilient consensus in arbitrary graphs, Quantitative safety and liveness, Just testing, HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties, Unnamed Item, Finite-word hyperlanguages, Verifying Parameterized taDOM+ Lock Managers, Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems, A topological perspective on distributed network algorithms, Power of Randomization in Automata on Infinite Strings, Unwinding Possibilistic Security Properties, Enforcing Non-safety Security Policies with Program Monitors
Cites Work
