Proving partial order properties

DOI10.1016/0304-3975(94)90009-4zbMath0803.68070OpenAlexW2034410903MaRDI QIDQ1322161

Amir Pnueli, Doron A. Peled

Publication date: 8 January 1995

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(94)90009-4

zbMATH Keywords

safetycompletenesspartial order semanticsconcurrencytracessoundnessproof systemserializabilitysnapshot algorithmtemporal verification

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Semantics in the theory of computing (68Q55)

Related Items

Undecidability of partial order logics, Abstraction for model checking multi-agent systems, Adding partial orders to linear temporal logic, An algorithmic approach for checking closure properties of Ω-regular languages, Serializable histories in quantified propositional temporal logic, Combining partial-order reductions with on-the-fly model-checking., Deciding global partial-order properties, Difficult configurations -- on the complexity of LTrL, An expressively complete linear time temporal logic for Mazurkiewicz traces, Efficient model checking for LTL with partial order snapshots, An algorithmic approach for checking closure properties of temporal logic specifications and \(\omega\)-regular languages, The serializability problem for a temporal logic of transaction queries

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Adequate proof principles for invariance and liveness properties of concurrent programs
• Event fairness and non-interleaving concurrency
• Using branching time temporal logic to synthesize synchronization skeletons
• Decomposition of distributed programs into communication-closed layers
• Concurrent and maximally concurrent evolution of nonsequential systems
• Modeling concurrency with partial orders
• Concurrent systems and inevitability
• The \(\mu\)-calculus as an assertion-language for fairness arguments
• Recursive assertions and parallel programs
• Petri nets, event structures and domains. I
• Defining conditional independence using collapses
• Verification of distributed programs using representative interleaving sequences
• First-order dynamic logic
• Repeated snapshots in distributed systems with synchronous communications and their implementation in CSP
• Synthesis of Communicating Processes from Temporal Logic Specifications
• A proof rule for fair termination of guarded commands
• “Sometimes” and “not never” revisited
• Guarded commands, nondeterminacy and formal derivation of programs
• Soundness and Completeness of an Axiom System for Program Verification
• Communicating sequential processes