scientific article
From MaRDI portal
Publication:3922147
zbMath0468.68026MaRDI QIDQ3922147
Amir Pnueli, Jonathan Stavi, Daniel J. Lehmann
Publication date: 1981
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)
Related Items (70)
Marking fairness in Petri nets ⋮ Merging regular processes by means of fixed-point theory ⋮ Mutex needs fairness ⋮ A complete rule for equifair termination ⋮ Sémantique asynchrone et comportements infinis en CPS ⋮ On fairness and randomness ⋮ Balanced Paths in Colored Graphs ⋮ Interleaving set temporal logic ⋮ An introduction to the regular theory of fairness ⋮ Deadlock and fairness in morphisms of transition systems ⋮ On the complexity of deciding fair termination of probabilistic concurrent finite-state programs ⋮ Infinite trees, markings, and well-foundedness ⋮ Appraising fairness in languages for distributed programming ⋮ Interpretations of recursion under unbounded nondeterminacy ⋮ Problems concerning fairness and temporal logic for conflict-free Petri nets ⋮ A methodology for designing proof rules for fair parallel programs ⋮ Concurrent systems and inevitability ⋮ The \(\mu\)-calculus as an assertion-language for fairness arguments ⋮ Fairness and communication-based semantics for session-typed languages ⋮ Méthode axiomatique sur les propriétés de fatalité des programmes parallèles ⋮ Model checking with fairness assumptions using PAT ⋮ On the limits of refinement-testing for model-checking CSP ⋮ Liminf progress measures ⋮ Event fairness and non-interleaving concurrency ⋮ Termination of just/fair computations in term rewriting ⋮ A Higher-Order Logic for Concurrent Termination-Preserving Refinement ⋮ Starvation-free mutual exclusion with semaphores ⋮ Shared-memory mutual exclusion: major research trends since 1986 ⋮ Completing the temporal picture ⋮ A tableau calculus for first-order branching time logic ⋮ Deductive verification of alternating systems ⋮ A simple proof of a completeness result for \(leads\)-\(to\) in the UNITY logic ⋮ Trapping mutual exclusion in the box calculus ⋮ On the logic of UNITY ⋮ The \({\mathcal NU}\) system as a development system for concurrent programs: \(\delta{\mathcal NU}\) ⋮ \(B\)-fairness and structural \(B\)-fairness in Petri net models of concurrent systems ⋮ Strong fairness and ultra metrics ⋮ Verification of distributed programs using representative interleaving sequences ⋮ On the complexity of verifying concurrent transition systems ⋮ Communicating processes, scheduling, and the complexity of nontermination ⋮ Ensuring liveness properties of distributed systems: open problems ⋮ A compositional approach to CTL\(^*\) verification ⋮ Verification by augmented abstraction: The automata-theoretic view ⋮ Explicit Fair Scheduling for Dynamic Control ⋮ Unnamed Item ⋮ Encoding fairness in a synchronous concurrent program algebra ⋮ Modal logics for communicating systems ⋮ Verification of concurrent programs: The automata-theoretic framework ⋮ Automatic and hierarchical verification for concurrent systems ⋮ On conditions for the liveness of weakly persistent nets ⋮ Model checking with strong fairness ⋮ Fifty years of Hoare's logic ⋮ Weak and strong fairness in CCS ⋮ Quantitatively fair scheduling ⋮ Quantitative Analysis under Fairness Constraints ⋮ Storage requirements for fair scheduling ⋮ A fair calculus of communicating systems ⋮ Fair termination revisited - with delay ⋮ Ten years of Hoare's logic: A survey. II: Nondeterminism ⋮ CCS: it's not fair! Fair schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions ⋮ Hybrid diagrams ⋮ Verification by augmented finitary abstraction ⋮ On the complexity of verifying concurrent transition systems ⋮ An investigation of controls for concurrent systems based on abstract control languages ⋮ On the verification of qualitative properties of probabilistic processes under fairness constraints. ⋮ Fairness and conspiracies ⋮ Fair Π ⋮ Global and local views of state fairness ⋮ A taxonomy of fairness and temporal logic problems for Petri nets ⋮ Proving partial order properties
This page was built for publication:
