Assumption/guarantee specifications in linear-time temporal logic

DOI10.1016/0304-3975(96)00069-2MaRDI QIDQ671674zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Recommendations

• Assumption/guarantee specifications in linear-time temporal logic (extended abstract)
• Publication:4508313
• Computer Science Logic
• An abstract account of composition
• Temporal logic and fair discrete systems

Cites work

• scientific article; zbMATH DE number 4213463 (Why is no real title available?)
• scientific article; zbMATH DE number 3902010 (Why is no real title available?)
• scientific article; zbMATH DE number 1318522 (Why is no real title available?)
• A logical view of composition
• Application of the composition principle to unity-like specifications
• Defining liveness
• Proofs of Networks of Processes
• Tentative steps toward a development method for interfering programs
• The existence of refinement mappings
• The temporal semantics of concurrent programs

Cited in

(13)

• Proving linearizability with temporal logic
• Automated compositional proofs for real-time systems
• LTL is closed under topological closure
• Conditions of contracts for separating responsibilities in heterogeneous systems
• Using Locales to Define a Rely-Guarantee Temporal Logic
• scientific article; zbMATH DE number 1512628 (Why is no real title available?)
• 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)