Assumption/guarantee specifications in linear-time temporal logic
From MaRDI portal
Publication:671674
DOI10.1016/0304-3975(96)00069-2zbMATH Open0874.68210OpenAlexW2001219520MaRDI QIDQ671674FDOQ671674
Authors: Bengt Jonsson, Yih-Kuen Tsay
Publication date: 27 February 1997
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(96)00069-2
Recommendations
Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)
Cites Work
- The existence of refinement mappings
- The temporal semantics of concurrent programs
- Tentative steps toward a development method for interfering programs
- Proofs of Networks of Processes
- Defining liveness
- A logical view of composition
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Application of the composition principle to unity-like specifications
Cited In (13)
- Proving linearizability with temporal logic
- LTL is closed under topological closure
- Automated compositional proofs for real-time systems
- Conditions of contracts for separating responsibilities in heterogeneous systems
- Using Locales to Define a Rely-Guarantee Temporal Logic
- Title not available (Why is that?)
- Safe Reasoning with Logic LTS
- Model checking, synthesis, and learning
- From linear temporal logics to Büchi automata: the early and simple principle
- Assumption/guarantee specifications in linear-time temporal logic (extended abstract)
- Computer Science Logic
- Assume-guarantee reasoning with local specifications
- Safe reasoning with logic LTS
This page was built for publication: Assumption/guarantee specifications in linear-time temporal logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q671674)